Think Stitch
PRINCIPIA  最近の更新


Scheme 関数7個で作る証明チェッカー

かんたんな証明チェッカーを作ってみたいと思います. 関数はたったの7個です. まず1個目の関数が12,000行あります,なんてことはありません :P. 証明パズルとして楽しめると思います.

この証明チェッカーは,David Gries さんと Fred B. Schneider さんによる本 A Logical Approach to Discrete Math (邦訳:コンピュータのための数学)を見ながら作りました. 公理と定理の番号はすべて本に合わせてあります.

等式論理

対象とする論理体系は等式論理とします. かんたんにするために命題だけを扱うことにして,述語や量化記号は扱いません. つまり命題等式論理ということです.

もしかしたら等式論理というのはあまりなじみがないかもしれません. 正確なところは本などを見ていただくとして,しろうとなりに説明をすると,等号だけが述語で,それに関する推論規則だけを持つ体系です. 残りの論理記号,論理和とか含意とかはすべて関数記号になってます. これらの性質は公理によって導入されます.

等式論理は何がいいかというと,いわゆる代数における式変形と同じように,同値変形によって計算ができることです. これがプログラムの正当性を証明するときなどに便利なんです. その話を始めるときりがないので,今回はやめときます.

数学記号としての等号は,= の代わりに3本線の ≡ を使います. ふつう,2本線の等号を連ねて

\[ x = y = z \]

と書いたら

\[ x = y\ \land\ y = z \]

を意味することが多いと思います.これは不等号と同じ使い方です.例えば

\[ x \le y \le z \]

\[ x \le y\ \land\ y \le z \]

を意味するでしょう.

しかし等号を論理値から論理値への述語関数 bool × bool => bool だと考えると,ちょっと意外な性質があります.それは結合法則が成り立つということです.

\[ (x \equiv y) \equiv z \ \ =\ \ x \equiv (y \equiv z) \]

このことは真理表を書いてみればすぐにわかります.

x y z x ≡ y y ≡ z (x ≡ y) ≡ z x ≡ (y ≡ z)
0 0 0 1 1 0 0
1 0 0 0 1 1 1
0 1 0 0 0 1 1
1 1 0 1 0 0 0
0 0 1 1 0 1 1
1 0 1 0 0 0 0
0 1 1 0 1 0 0
1 1 1 1 1 1 1

したがって括弧を使わずに書くことができるわけです.

\[ x \equiv y \equiv z \]

結合法則を満たす等号を2本線と区別するために3本線の等号を使います. これは数式の場合の約束で,プログラムの方では = を使います.(ごめんなさい).

等式論理の推論規則

等式論理の推論規則は4つあります.Wikipedia から写しました. いずれも意味は明らかだと思います.

Substitution \[\vdash P \ \ \longrightarrow\ \ \vdash P[x := E] \]

Leibniz \[\vdash P=Q \ \ \longrightarrow\ \ \vdash E[x := P] = E[x := Q] \]

Transitivity \[\vdash P=Q,\ \vdash Q=R \ \ \longrightarrow\ \ \vdash P=R \]

Equanimity \[\vdash P,\ \vdash P=Q \ \ \longrightarrow\ \ \vdash Q \]

(ターンスタイルの使い方がこれでいいのかどうかわかりませんが...)

論理式の表現

論理式はS式で次のように表すことにします.

P ::= (= P P ...)
    | true
    | false
    | (not P)
    | (or P P)
    | (and P P)
    | (imp P P)

true と false は定数です.imp は含意(ならば)を表します.

等号は対称律,結合律,推移律を満たします. そこで最初から任意個数並べられるようにしてしまうことにします. 本来ならば公理を用意すべきですが,これらをすべて公理から導出しようとするとあまりにも証明が面倒になるので,公理を「ハードコーディング」してしまうことにします.:P

証明チェッカーのプログラム

ではさっそく証明チェッカーの関数を作っていきます.

1. (delete1 x xs)

1つ目の関数は (delete1 x xs) です. この関数はリスト xs を前から見たときに最初に現れる x を取り除いたリストを返す関数です. 比較は equal? で行うことにします. これくらい最初からあるとしてもいいんですけど,いちおう 1/7 です.

(define (delete1 x xs)
  (cond ((null? xs) 
         (error 'delete1 "not found" x))
        ((equal? x (car xs))
         (cdr xs))
        (else
         (cons (car xs)
               (delete1 x (cdr xs))))))

指定した値 x がリスト xs に含まれていない場合はエラーとします.

2. (consume bag1 bag2)

2番目の関数 consume は2つのリスト bag1, bag2 を引数にとります. それぞれを要素の重複を許す多重集合(マルチセット,バッグ)と考えたとき,bag1 から bag2 の要素をすべて取り除いた残りの多重集合をリストとして返します.

(define (consume bag1 bag2)
  (if (null? bag2)
      bag1
      (consume (delete1 (car bag2) bag1) (cdr bag2))))

bag2 に同じ要素が複数あったら,その同じ数だけ bag1 から取り除かれます. bag2 の要素は bag1 に必ずふくまれていなければいけません.

例は次のようになります.

(consume '(a b c p p d) '(p c d))
=> (a b p)

3. (equiv-expr? x)

与えられた式が等式 (= p q r ...) であるかどうかを判定する述語です. これで 3/7 です.

(define (equiv-expr? x)
  (and (pair? x) (eq? (car x) '=)))

4. (flatten-equiv x)

推論規則を使って字面的に式を変形すると,等式が入れ子になってしまうことがあります. これを平たくする関数を用意しておきます.

ついでに,結果が (= p) となったら = を取り去って p に変形するようにしておきます.

(define (flatten-equiv x)
  (if (equiv-expr? x)
      (let ((r
             (append-map
              (lambda (y)
                (let ((z (flatten-equiv y)))
                  (if (equiv-expr? z)
                      (cdr z)
                      (list z))))
              (cdr x))))
        (if (null? (cdr r))
            (car r)
            (cons '= r)))
      x))

append-map は使ってもいいですよね?.例は次のとおりです.

(flatten-equiv '(= (= a b) c))
=> (= a b c)

(flatten-equiv '(= p))
=> p

5. (substitution theorem var expr)

残りの3つは推論規則に対応する関数です. まず substitution です. Common Lisp の subst と引数の順序が異なるので,フルスペリングで substitution としました. 定理 theorem に現れる変数 var に,式 expr を字句代入した結果の式を返します.

(define (substitution theorem var expr)
  (flatten-equiv
   (cond ((eq? theorem var) expr)
         ((pair? theorem)
          (cons (substitution (car theorem) var expr)
                (substitution (cdr theorem) var expr)))
         (else theorem))))

flatten-equiv の使い方がぜいたくですけど,ま,いいでしょう.

(substitution '(= (not (= p q)) (not p) q) 'q 'p)
=> (= (not (= p p)) (not p) p)

6. (equanimity P theorem)

P と theorem はどちらも公理または定理です. theorem は P = Q という形でなければなりません. P, Q それぞれが等式であってもかまいません. 例えば,theorem が (= p q r s) で P が (= q r) ならば Q が (= p s) であると見なされます. この Q を求める結果ということになります.

(define (equanimity P theorem)
  (if (equiv-expr? theorem)
      (flatten-equiv
       (cons '= 
             (consume
              (cdr theorem)
              (if (and (pair? P) (eq? (car P) '=))
                  (cdr P)
                  (list P)))))
      (error 'equanimity "theorem must be an equation" theorem)))
(equanimity 'p '(= p true))
=> true

(equanimity '(= q r) '(= p q r s))
=> (= p s) 

7. (leibniz theorem expr var P)

最後は leibniz です.theorem は P = Q の形でなければなりません.

結果は expr[var := P] = expr[var := Q] という式になります.

(define (leibniz theorem expr var P)
  (let ((Q (equanimity P theorem)))
    (flatten-equiv
     (list '= 
           (substitution expr var P)
           (substitution expr var Q)))))
(leibniz '(= a b c d) '(or p (not p)) 'p 'b)
=> (= (or b (not b))
      (or (= a c d) (not (= a c d))))

(leibniz '(= a b c d) '(or p (not p)) 'p '(= c a))
=> (= (or (= c a) (not (= c a)))
      (or (= b d) (not (= b d))))

(leibniz '(= a b c d) '(or p (not p)) 'p '(= b d c))
=> (= (or (= b d c) (not (= b d c)))
      (or a (not a)))

証明の書き方

では証明を書いてみます.証明記述のルールは3つあります.

  1. 公理または定理からスタートします.
  2. 関数 substitution, leibniz, equanimity だけを使います.
  3. 関数 substitution と leibniz の第1引数,それから equanimity の2つの引数は公理または定理でなければなりません.

このルールを守っている限り,3つの関数の返す式は定理になります. そこで,いつものように(?)証明はゴールを目指すパズルになるわけです.

最初の公理:対称律と true の公理

最初の公理は等号の対称律です.これは = 式にはハードコードされていますけど,並びの順序を変えたいときに必要になります. \[ p \equiv q \equiv q \equiv p \]

次の公理は定数 true に関する公理です. \[ \textit{true} \equiv q \equiv q \]

いずれも次のように定義しておきます.

(define axiom-3.2 '(= p q q p))
(define axiom-3.3 '(= true q q))

最初の証明: true

はじめに true が定理であることを証明してみます. こういう基礎的なところは逆にわかりにくかったりしますので,そのまま先に進んでもらって,何をしているのかわかってから見直した方がよいかもしれません.

;;; true
(define theorem-3.4
  (equanimity
   (equanimity
    axiom-3.3
    (leibniz axiom-3.3 '(= true x) 'x 'true))
   (substitution axiom-3.3 'q 'true)))

まず公理(3.3)に leibniz を適用すると,次の定理が得られます.

(leibniz axiom-3.3 '(= true x) 'x 'true)
=> (= true true true q q)

これと,再び公理(3.3)とから

(equanimity
  axiom-3.3
  (leibniz axiom-3.3 '(= true x) 'x 'true))
=> (= true true)

となります.さらにもう1度公理(3.3)で q を true に置き換えたものを用意すると,true が導出できました. 公理からはじめて,ルールを守って true を導出できたので,true は定理です. これに theorem-3.4 と名前を付けました.これ以降,定理として使えます.

等号の反射律

この体系では,等号の反射律は定理として証明できます.

;;; (= q q)
(define theorem-3.5
  (equanimity theorem-3.4 axiom-3.3))

否定 not の公理と false の公理

続いて否定と定数 false の公理を導入しましょう.

否定の公理 \[ \neg (p \equiv q) \equiv \neg p \equiv q \] false の公理 \[ \textit{false} \equiv \neg \textit{true} \]

(define axiom-3.8 '(= false (not true)))
(define axiom-3.9 '(= (not (= p q)) (not p) q))

ちょっと込み入った証明をやってみましょう. \[ \neg p \equiv q \equiv p \equiv \neg q \]

;;; (= (not p) q p (not q))
(define theorem-3.11
  (equanimity
   (equanimity
    (equanimity
     (substitution theorem-3.5 'q '(not (= p q)))
     (leibniz axiom-3.2 '(= (not (= p q)) (not x)) 'x '(= p q)))
    (leibniz axiom-3.9 '(= x (not (= q p))) 'x '(not (= p q))))
   (leibniz
    (substitution
     (substitution
      (substitution axiom-3.9 'p 'x)
      'q 'p)
     'x 'q)
    '(= (not p) q x) 'x '(not (= q p)))))

もう1つ,2重否定をやりましょう. \[ \neg \neg p \equiv p \]

;;; (= (not (not p)) p)
(define theorem-3.12
  (equanimity
   (substitution theorem-3.11 'p '(not p))
   (leibniz theorem-3.11 '(= (not (not p)) x) 'x 'p)))

論理和 (or p q)

論理和 (or p q) は5つ公理があります. 最後は好き嫌いの分かれる(?)排中律です.

\[ p \lor q \equiv q \lor p \] \[ (p \lor q) \lor r\ \ \equiv\ \ p \lor (q \lor r) \] \[ p \lor p \ \ \equiv p \] \[ p \lor (q \equiv r) \equiv p \lor q \equiv p \lor r\] \[ p \lor \neg p\]

(define axiom-3.24 '(= (or p q) (or q p)))
(define axiom-3.25 '(= (or (or p q) r) (or p (or q r))))
(define axiom-3.26 '(= (or p p) p))
(define axiom-3.27 '(= (or p (= q r)) (or p q) (or p r)))
(define axiom-3.28 '(or p (not p)))

3つ定理を証明します.

\[ p \lor \textit{true} \equiv \textit{true}\]

;;; (= (or p true) true)
(define theorem-3.29
  (equanimity
   (equanimity
    (substitution
     (substitution axiom-3.27 'q 'p)
     'r 'p)
    (leibniz
     (substitution axiom-3.3 'q 'p)
     '(= (or p x) (or p p) (or p p)) 'x '(= p p)))
   (leibniz
    (substitution axiom-3.3 'q '(or p p))
    '(= (or p true) x) 'x '(= (or p p) (or p p)))))

\[ p \lor \textit{false} \equiv p\]

;;; (= (or p false) p)
(define theorem-3.30
  (equanimity
   (equanimity
    (equanimity
     (equanimity
      (equanimity
       axiom-3.28
       (substitution
        (substitution axiom-3.27 'q 'p)
        'r '(not p)))
      (leibniz axiom-3.26 '(= (or p (= p (not p))) x) 'x '(or p p)))
     (leibniz
      (substitution axiom-3.9 'q 'p)
      '(= (or p x) p) 'x '(= p (not p))))
    (leibniz
     (substitution axiom-3.3 'q 'p)
     '(= (or p (not x)) p) 'x '(= p p)))
   (leibniz axiom-3.8 '(= (or p x) p) 'x '(not true))))

\[ p \lor q \equiv p \lor \neg q \equiv p\]

;;; (= (or p q) (or p (not q)) p)
(define theorem-3.32
  (equanimity
   (equanimity
    (equanimity
     (equanimity
      theorem-3.30
      (leibniz axiom-3.8 '(= (or p x) p) 'x 'false))
     (leibniz axiom-3.3 '(= (or p (not x)) p) 'x 'true))
    (leibniz
     (substitution axiom-3.9 'p 'q)
     '(= (or p x) p) 'x '(not (= q q))))
   (leibniz 
    (substitution
     (substitution axiom-3.27 'q '(not q))
     'r 'q)
    '(= x p) 'x '(or p (= (not q) q)))))

論理積 (and p q)

論理積の公理は1つだけです.これは黄金律というのだそうです. 黄金率とまぎらわしいですけど. \[ p \land q \equiv p \equiv q \equiv p \lor q \]

;;; golden rule
(define axiom-3.35 '(= (and p q) p q (or p q)))

論理和と論理積がそろったので,ド・モルガンをやります. 等式論理でも面倒なド・モルガン.

;;; (= (not (and p q)) (or (not p) (not q)))
(define theorem-3.47
  (equanimity
   theorem-3.11
   (equanimity
    (equanimity
     (equanimity
      (leibniz axiom-3.35 '(not x) 'x '(and p q))
      (leibniz
       (substitution axiom-3.9 'q '(= q (or p q)))
       '(= (not (and p q)) x) 'x '(not (= p q (or p q)))))
     (leibniz theorem-3.32
              '(= (not (and p q)) (not p) q x) 'x '(or p q)))
    (leibniz
     (equanimity
      (substitution 
       (substitution 
        (substitution theorem-3.32 'p 'x)
        'q 'p)
       'x '(not q))
      (leibniz
       (substitution axiom-3.24 'q '(not q))
       '(= (or (not q) (not p)) x (not q)) 'x '(or (not q) p)))
     '(= (not (and p q)) (not p) q x p) 'x '(or p (not q))))))

含意 (imp p q)

最後は含意の公理です.ちょっと変わってます. \[ p \Rightarrow q \equiv p \lor q \equiv q \]

よくある含意の定義は定理になります.

;;; (= (imp p q) (or (not p) q))
(define theorem-3.59
  (equanimity
   axiom-3.57
   (leibniz
    (equanimity
     (equanimity
      (substitution
       (substitution
        (substitution theorem-3.32 'p 'x)
        'q 'p)
       'x 'q)
      (leibniz axiom-3.24 '(= (or q (not p)) x q) 'x '(or q p)))
     (leibniz 
      (substitution axiom-3.24 'p '(not p))
      '(= x (or p q) q) 'x '(or q (not p))))
    '(= (imp p q) x) 'x '(= (or p q) q))))

群の公理

ちょっとした応用として,群の公理を扱ってみます. いまは最初から左右の単位元と逆元を公理で与えちゃうそうですけど,ここでは右単位元と右逆元だけから,左単位元の存在を証明してみます.

まず群の公理です.

(define axiom-group-assoc '(= (* (* x y) z) (* x (* y z))))
(define axiom-group-right-identity '(= (* x e) x))
(define axiom-group-right-inverse '(= (* x (r x)) e))

e は単位元です.定数ですから subsutitution で置換はできません. r は逆元を表す関数記号です.

証明は次のとおりです.:P

(define theorem-left-identity
  (equanimity
   (equanimity
    (equanimity
     (equanimity
      (equanimity
       (equanimity
        (equanimity
         (equanimity
          (equanimity
           (equanimity
            (leibniz axiom-group-right-identity '(* e x) 'x '(* x e))
            (leibniz axiom-group-right-inverse '(= (* P (* x e)) (* e x)) 'P 'e))
           (leibniz
            (substitution axiom-group-right-inverse 'x '(r x))
            '(= (* (* x (r x)) (* x P)) (* e x)) 'P 'e))
          (leibniz
           (substitution
            (substitution axiom-group-assoc 'y '(r x))
            'z '(r (r x)))
           '(= (* (* x (r x)) P) (* e x)) 'P '(* x (* (r x) (r (r x))))))
         (leibniz
          axiom-group-right-inverse
          '(= (* (* x (r x)) (* P (r (r x)))) (* e x)) 'P '(* x (r x))))
        (leibniz
         (substitution
          (substitution
           (substitution
            axiom-group-assoc 'x '(* x (r x)))
           'y 'e)
          'z '(r (r x)))
         '(= P (* e x)) 'P '(* (* x (r x)) (* e (r (r x))))))
       (leibniz
        (substitution
         (substitution
          axiom-group-assoc 'y '(r x))
         'z 'e)
        '(= (* P (r (r x))) (* e x)) 'P '(* (* x (r x)) e)))
      (leibniz
       (substitution axiom-group-right-identity 'x '(r x))
       '(= (* (* x P) (r (r x))) (* e x)) 'P '(* (r x) e)))
     (leibniz
      (substitution
       (substitution
        axiom-group-assoc 'y '(r x))
       'z '(r (r x)))
      '(= P (* e x)) 'P '(* (* x (r x)) (r (r x)))))
    (leibniz
     (substitution axiom-group-right-inverse 'x '(r x))
     '(= (* x P) (* e x)) 'P '(* (r x) (r (r x)))))
   (leibniz axiom-group-right-identity '(= P (* e x)) 'P '(* x e))))

補足

人の書いた証明を読むのは骨が折れますけど,自分で証明を組み立てるのはかなり楽しいです. ただし,5分後には自分の証明も読めなくなりますw.

こんなものでもちょっと拡張したくなります.

2013/11/09
© 2013,2014,2015 PRINCIPIA Limited