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算術の「証明能力」は超えないという気がする