2006-09-02

Lisp on TRS

昨日の項書き換え系を使って、小さなLispを作る。おもちゃみたいなもんだけどこんな感じ



(define (variable? e) ;昨日と一緒

 (with-error-handler

   (lambda (x) #f)

  (lambda () (char=? #\% (string-ref (symbol->string e) 0)))))
(define lisp-rules

 (list

  '( (+ 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 )

  '( (and (not %x) %x) . false )

  '( (and %x (not %x)) . false )

  '( (or %x %y) . (not (and (not %x) (not %y))) )

  '( (-> %A %B) . (not (and %A (not %B))) ) ;ならば

  '( (not (not %x)) . %x )

  '( (not true) . false )

  '( (not false) . true )

  '( (if true %x %y) . %x )

  '( (if false %x %y) . %y )

  '( (even? 0) . true )

  '( (odd? 0) . false )

  '( (even? (s %x)) . (odd? %x) )

  '( (odd? (s %x)) . (even? %x) )

  '( (map %f nil) . nil )

  '( (map %f (cons %x %y)) . (cons (%f %x) (map %f %y)) )

  '( (fact 0) . (s 0) )

  '( (fact (s %x)) . (* (s %x) (fact %x)) )

  ))
(define lisp (make-TRS lisp-rules variable?))

ひたすら項書き換えルールをずらずら並べてるだけ。



(lisp '(+ (s (s 0)) (s (s (s 0)))))

みたいな感じでやると、ちゃんと計算してくれる。こいつは普通のLispより賢い(といってもSchemeで100行そこそこなんだけど)ので、ちょっとした推論とかやってのける



(lisp '(-> (= A B) (= (s A) (s B))))

とかやると、trueと返ってくるはず。「A=Bならば、s(A)=s(B)」という当たり前な命題だけど。もう少しルール追加してやると、より賢くなりそうな感じもする。けど、どんなに頑張ってもChurch算術の「証明能力」は超えないという気がする

2006-09-02

構成的プログラミング

構成的プログラミングとは、二引数述語Pがあって、

(forall (x) (exists (y) (P x y)))

みたいな命題の構成的証明を与えてやると、その証明から

(forall (x) (P x (f x)))

を満たす関数fを抽出できる、というようなものらしい。はっきり言って、何でそんなことができるのか、ちっとも分からないけど。そもそも、この構成的証明というのは手で与えるんだろうか。そうだとしたら、証明なんか書いてないで直接プログラム書いた方が速い。証明自体も自動的にやられるんだとしたら、多少面白い

(forall (y) (exists (x) (P x y)))

の証明を与えると、同様に、

(forall (x) (P (g x) x))

となる関数gが抽出できるので、制約プログラミングみたいな双方向性のプログラミングパラダイムが実現できる。制約プログラミングが具体的に何を指してるのかよく知らないけど。結局、実物見ないとよく分からない

ところで、「仕様からのプログラム合成」という謳い文句は聞こえがいいけど、仕様書くほうが普通にプログラム書くより大変だというケースというのはないのだろうか。構成的プログラミングの話は、主に述語論理で記述された論理式を対象にしているようなので、普通のアプリケーションの仕様を記述する言語として、述語論理というのは表現力不足というか、自然に書けるという気がしないのだけど。

2006-09-02

構成的と言えば

中学あたりで習う、背理法で証明できる初等的命題として、「sqrt(2)は無理数」ってのと、「素数は無限個ある」ってやつがあるけど、背理法使わずに初等的に証明するには、どうすればいいのだろう。論理式で書くと、以下のような感じか

(forall (p) (forall (q) (-> (= (* 2 (* p p)) (* q q)) (and (= p 0) (= q 0)))))

(forall (n) (exists (p) (and (< n p) (prime? p))))

素数の方は、丁度(forall (x) (exists (y) (P x y)))の形になってるけど、これの初等的な証明はちょっと思いつかない。

#述語prime?は、素数なら真、非素数なら偽を返す
#解析的なのでよければ、ゼータ関数がs=1で発散するというのでいいんだろうけど