EoPL reading (81) 2.2 An Abstraction for Inductive Data Type
検討再開。とりあえず fresh-id と all-ids がポイント高い、という事で例示されている手続きを吸わせてみる事に。
gosh> (all-ids '(lambda-exp p (app-exp (var-exp +) (app-exp (var-exp p) (var-exp x))))) (p + x) gosh>
ええと、
(lambda (p) (+ p x))
で、x を (* p 3) で置き換えるので、subst-id が x で subst-exp が (* p 3) になる。てーことは、subst-exp と上記のリストで重複してるシンボルが fresh-id する対象になる、という事で良いの??
なんとなく悩ましいんですが
- all-ids は lit-exp と priapp-exp を追加した形にしたい
- そしたら上記リストは (p x) になりますな
- ついでに subst-id と同値のものはナニしたい
- all-ids で一覧作って fresh-id するのは微妙
- all-ids 何度も呼ぶのは (ry
- 置き換えなナニは alist で (ry
ってコトでとりあえず all-ids を以下に
(add-load-path ".")
(load "define-datatype")
(define all-ids
(lambda (exp)
(let f ((rslt '()) (exp exp))
(cases expression exp
(var-exp (id) (if (memv id rslt)
rslt
(append rslt (list id))))
(lit-exp (datum) rslt)
(primapp-exp (prim rand1 rand2)
(f (f rslt rand1) rand2))
(lambda-exp (id body)
(f (append rslt (list id)) body))
(app-exp (rator rand)
(f (f rslt rator) rand))))))試験もコピーして以下を追加。
(test* "all-ids (5)"
'(x)
(all-ids '(lambda-exp x (primapp-exp + (var-exp x) (lit-exp 3)))))パス。最初 (app-exp (primapp-exp +) (app-exp (var-exp x) (lit-exp 3))) とか書いてて微妙にハマってたり。
で、色々ごにょごにょしつつ以下がでっち上がった。
(add-load-path ".")
(load "expression")
(load "fresh-id")
(define make-subst-alist
(lambda (ids l)
(let f ((rslt '()) (ids ids))
(if (null? ids)
rslt
(f (append rslt
(list (list (car ids)
(fresh-id l (symbol->string (car ids))))))
(cdr ids))))))
(define rename-or-not
(lambda (id alist)
(let ((s (assv id alist)))
(if s
(cadr s)
id))))
(define lambda-calculus-subst
(lambda (exp subst-exp subst-id)
(let ((rename-ids (all-ids exp)))
(let ((subst-alist (make-subst-alist rename-ids exp)))
(letrec
((subst
(lambda (exp)
(cases expression exp
(var-exp (id)
(if (eqv? id subst-id)
subst-exp
(var-exp (rename-or-not id subst-alist))))
(lambda-exp (id body)
(lambda-exp (rename-or-not id subst-alist)
(subst body)))
(app-exp (rator rand)
(app-exp (subst rator) (subst rand)))
(lit-exp (datum)
(lit-exp datum))
(primapp-exp (prim rand1 rand2)
(primapp-exp prim
(subst rand1)
(subst rand2)))))))
(subst exp))))))実は上記はダウト。以下な試験を作ってて
(use gauche.test)
(add-load-path ".")
(load "lambda-calculus-subst")
(test-start "make-subst-alist")
(test-section "make-subst-alist")
(test* "make-subst-alist (1)"
'()
(make-subst-alist '() '()))
(test* "make-subst-alist (2)"
'((x x0))
(make-subst-alist '(x) '(lambda-exp x (var-exp x))))
(test* "make-subst-alist (3)"
'()
(make-subst-alist '(x) '(lambda-exp p (var-exp p))))
(test-end)パスしません。
$ gosh test-lambda-calculus-subst.scm Testing lambda-calculus-subst ... <lambda-calculus-subst>-------------------------------------------------------- test lambda-calculus-subst (1), expects (lambda-exp p0 (primapp-exp + (var-exp p0) (primapp-exp * (var-exp p) (lit-exp 3)))) ==> ok test lambda-calculus-subst (2), expects (lambda-exp q (primapp-exp + (var-exp q) (primapp-exp * (var-exp p) (lit-exp 3)))) ==> ERROR: GOT (lambda-exp q0 (primapp-exp + (var-exp q0) (primapp-exp * (var-exp p) (lit-exp 3)))) failed. discrepancies found. Errors are: test lambda-calculus-subst (2): expects (lambda-exp q (primapp-exp + (var-exp q) (primapp-exp * (var-exp p) (lit-exp 3)))) => got (lambda-exp q0 (primapp-exp + (var-exp q0) (primapp-exp * (var-exp p) (lit-exp 3))))
なんか長いですが
(lambda (q) (+ q x))
が
(lambda (q0) (+ q0 (* p 3)))
になってます。むむむ、と言いつつ上記の下書きをニラんでて勘違いに気づきました。lambda-calculus-subst 手続きは正しくは以下。
(define lambda-calculus-subst
(lambda (exp subst-exp subst-id)
;; (let ((rename-ids (all-ids exp)))
(let ((rename-ids (all-ids subst-exp)))
(let ((subst-alist (make-subst-alist rename-ids exp)))
(letrec
((subst
(lambda (exp)
(cases expression exp
(var-exp (id)
(if (eqv? id subst-id)
subst-exp
(var-exp (rename-or-not id subst-alist))))
(lambda-exp (id body)
(lambda-exp (rename-or-not id subst-alist)
(subst body)))
(app-exp (rator rand)
(app-exp (subst rator) (subst rand)))
(lit-exp (datum)
(lit-exp datum))
(primapp-exp (prim rand1 rand2)
(primapp-exp prim
(subst rand1)
(subst rand2)))))))
(subst exp))))))これで試験にパスしたんですが、なんとなく腑にオチてません。あんまシンプルではないなぁ、と。
