これ、意外にムズいな。ちょい整理。
- extend-subst で symbol を term に置換する subst なオブジェクトが戻される
- var-term が term な何かと置換 (constant-ter または app-term という理解)
- extend が戻す手続きは基本的に sym と i が eqv? なら t を戻せば良いの?
つうことで
procedural なソレは以下な理解で良いのだろうか。
(add-load-path ".")
(load "term")
(define empty-subst
(lambda ()
(lambda (sym)
(eopl:error 'apply-subst "No binding for ~s" sym))))
(define extend-subst
(lambda (i t s)
(lambda (sym)
(if (eqv? sym i)
t
(apply-env s sym)))))
(define apply-subst
(lambda (s i)
(s i)))
ちなみに term な定義が以下。
(add-load-path "../../define-datatype")
(load "define-datatype")
(define-datatype term term?
(var-term (id symbol?))
(constant-term (datum constant?))
(app-term (terms (list-of term?))))
で、subst-in-term が以下なカンジで良いのかどうか。
(define subst-in-term
(lambda (t s)
(cases term t
(var-term (id) (s id))
(constant-term (datum) datum)
(app-term (terms) (let f ((l terms))
(if (null? l)
'()
(cons (subst-in-term (car l) s)
(f (cdr l)))))))))
試験は別途、ということで一旦エントリ投入。