matchでラムダ簡約器

Gaucheで、ファイルユーティリティはfile.utilなのに、マッチングユーティリティはutil.matchなのは、何故なんだぜ？毎回間違える･･･ここらへんの再発明な

;gaucheで
(use util.match) 
(define (cbv.reduce e)
 (letrec
  ((subst ;代入[式e中のvarをvalに置換]
    (lambda (var val e)
      (cond
       ( (not (list? e)) (if (equal? var e) val e) )
       ( else (map (lambda (x) (subst var val x)) e) ))))
   (rename ;アルファ変換
    (lambda (e)
	(match e
	 ( ('lambda (?var) ?body)
	   (if (symbol? ?var)
	       (let ((name (gensym (symbol->string ?var))))
		 `(lambda (,name) ,(subst ?var name (rename ?body))))
	     (error "orz" '(lambda ?var ?body))) )
	 ( ?x (if (not (list? ?x)) ?x (map rename ?x) )))))
   (main
    (lambda (e prev)
      (if (equal? e prev) e
	(match e
	 ( (('lambda (?var) ?body) ?arg) (main (subst ?var (main ?arg (list)) ?body) e) )
	 ( (?e1 ?e2) (main `(,(main ?e1 (list)) ,(main ?e2 (list))) e) )
	 ( ('lambda (?var) ?body) (list 'lambda (list ?var) (main ?body (list))) )
	 ( ?e ?e ))))))
  (main (rename e) (list))))

テスト。いい加減、gauche.testの使い方を覚えるべき

gosh>(cbv.reduce '((lambda (x) x) 1))
1
gosh>(cbv.reduce '((lambda (x) (x x)) (lambda (y) (y z))))
(z z)
gosh>(cbv.reduce '(((lambda (a) ((lambda (x) (lambda (a) (x a))) a)) list) 1))
(list 1)
gosh>(cbv.reduce '(((lambda (a) (lambda (x) (a (x a)))) 1) 2))
(1 (2 1))

多少記述量は減る。あとは、上のような感じのコードを自動的に生成するようにすれば、PLT-Redexを作れるかな

proof checker

HOLとか、Coqとか、そのへんについて調べていた。

HOLとは？
・証明チェッカ
・Higher Order Logicの略らしい
・MLベースで、MLで証明を書く感じらしい


HOLの処理系には、いくつかバリエーションがあるらしい。FlySpeck Projectでは、HOL Lightというのを使ってるらしいけど、これはOcamlベースのよう。Isabelle/HOLというのは、SMLベースっぽい。個人的にSMLの方が好きなので、こっちを。と思ったら、IsabelleのHPでは、Windowsは相手にされてないorz一応、Cygwinで何とかなるっぽいが


CoqとHOLの違いは、Coqが構成的論理をベースにしているのに対して、HOLは古典論理をベースにしている点にある。と、ここに書いてあった。CoqもHOLも具体的な適用例は数学諸分野から、ソフトウェア・ハードウェアの検証まで山ほどあるらしい。数学のメインストリームは古典論理を使っている一方、構成的プログラミングの理論を使うという点からすれば、Coqがいい。というか、CのFormal SemanticsをなんでHOLで与えてるんだアホー

簡易証明器

他の証明支援系なんかでも、帰納法のヒントの与え方が重要みたいな記述を読んだのに勇気付けられて、ここに書いたことをシステマティックに実行できるようにしてみた。unifyだけ自前の関数

(define (union L1 L2) ;和集合
 (cond
  ((null? L1) L2)
  ((member (car L1) L2) (union (cdr L1) L2))
  (else (union (cdr L1) (cons (car L1) L2)))))

(define (make-prover)
 (letrec
  ((rule-db '())
   (variable? ;%で始まるsymbolを変数と見なす
    (lambda (x) (and (symbol? x) (char=? #\% (string-ref (symbol->string x) 0)))))
   (subst
    (lambda (var val e)
      (cond
       ((equal? var e) val)
       ((not (list? e)) e)
       (else (map (lambda (x) (subst var val x)) e)))))
   (get-vars
    (lambda (e)
      (let loop ((L e) (vlist '()))
	(cond
	 ((null? L) vlist)
	 ((list? (car L)) (loop (cdr L) (union vlist (get-vars (car L)))))
	 ((variable? (car L)) (loop (cdr L) (union (list (car L)) vlist)))
	 (else (loop (cdr L) vlist))))))
   (rename-vars
    (lambda (e)
      (let ((vars (get-vars e)))
	(let loop ((rest vars) (ret e))
	  (if (null? rest) ret
	    (loop (cdr rest) (subst (car vars) (gensym "%") ret)))))))
   (reduce
    (lambda (e prev)
      (if (or (equal? e prev) (not (list? e))) e
	(let loop ((rest rule-db) (expr (rename-vars e)))
	  (cond
	   ( (null? rest) (reduce (map (lambda (x) (reduce x '())) e) e) )
	   ( (unify (caar rest) expr)
	     => (lambda (p) (reduce (p (cdar rest)) e)) )
	   ( else (loop (cdr rest) expr) )))))))
  (lambda (e)
   (match e
    ( ('view) rule-db )
    ( ('clear) (set! rule-db '()) )
    ( ('learn term) (set! rule-db (union (list (cons term 'true)) rule-db)) ) ;ruleを一個だけ追加
    ( ('load rules) (set! rule-db (union rules rule-db)) )
    ( ('reduce expr) (reduce expr '()) )
    ( ('induce var expr) 
      (reduce
       (list 'and (subst var 0 expr)
	     `(implies ,expr ,(subst var `(s ,var) expr)))  '()) )))))

(define prover (make-prover))
(prover
 '(load
   (( (+ 0 %x) . %x )
    ( (+ (s %x) %y) . (s (+ %x %y)) )
    ( (- %x 0) . %x )
    ( (- (s %x) (s %y)) . (- %x  %y) )
    ( (* 0 %x) . 0 )
    ( (* (s %x) %y) . (+ %y (* %x %y)) )
    ( (= 0 0) . true )
    ( (= 0 (s %x)) . false )
    ( (= (s %x) (s %y)) . (= %x  %y) )
    ( (<= 0 %x) . true )
    ( (<= (s %x) (s %y)) . (<= %x %y) )
    ( (append nil %x) . %x )
    ( (append (cons %x %y) %z) . (cons %x (append %y %z)) )
    ( (length nil) . 0 )
    ( (length (cons %x %y)) . (s (length %y)) )
    ( (and true %x) . %x )
    ( (and false %x) . false )
    ( (and %x true) . %x )
    ( (and %x false) . false )
    ( (not false) . true )
    ( (and (not %x) %x) . false )
    ( (and %x (not %x)) . false )
    ( (or %x %y) . (not (and (not %x) (not %y))) )
    ( (implies %A %B) . (not (and %A (not %B))) ) ;ならば
    ( (not (not %x)) . %x ))))

長いorz書換え規則の追加時に、フォーマットチェックしてないとか、色々あれだけど。make-proverは簡易インタープリタ作るイメージで、view,clear,load,learn,reduce,induceという6つの関数をサポートしている。viewは全ルールを表示。clearはルールデータベースを消去、loadとlearnは書換え規則の追加。loadは書換え規則のリストを受け取って、全部読み込む。learnはある項termがtrueであることを学習する。reduceは単純に項書換えによる簡約を行う。induceは、(induce n (P n))という書式で、(and (P 0) (implies (P n) (P (s n))))という式を生成してreduceするだけ。つまり、数学的帰納法。足し算の結合律を証明して見る。

;Gaucheで
>(prover '(induce I (= (+ I (+ J K)) (+ (+ I J) K))))
(= (+ J K) (+ J K))
>(prover '(induce J (= (+ J K) (+ J K))))
(= K K)
>(prover '(induce K (= K K)))
true

証明できるまで、ひたすら、induceとreduceを色々な変数に総当り方式で試していけば、これくらいは、完全に自動証明できるようになると思う。自然数論しか扱えないけど。せめてリストくらいは。帰納法は難しい。この難しさは、帰納法が、ある意味で一階論理より高度な対象だからなんだろう。しかし、半分くらいが、名前の衝突を回避するための非本質的な処理だったりするのがもうね、めんどくさい。

やってることは、結局データベース探索して、ルールが適用可能なら、適用して･･･の繰り返し。最終的にtrueが得られれば証明完了。単純だけど、人間がやってるのも、実際にはこんな程度のことなのかもしれない。頭の中にある知識と照合していくだけ。線形リストを頭から試していくようなおバカなやり方ではないだろうけど。

やっぱり色々適当すぎる。ルールの追加時に、union使ってるけど、変数名が違うだけの同一のルールを同一だと認識しないとか。あと、型情報みたいなのもないとだめだな〜