(define-syntax Q ; quote a lambda term
(syntax-rules (lambda)
((Q (lambda (x) M)) (lambda (a)
(lambda (b)
(lambda (c)
(a (lambda (x) (Q M)))))))
((Q (M N)) (lambda (a)
(lambda (b)
(lambda (c)
((b (Q M)) (Q N))))))
((Q x) (lambda (a)
(lambda (b)
(lambda (c)
(c x)))))))
(define E ; evaluate a quoted lambda term
((lambda (m)
((lambda (f) (m (lambda (a) ((f f) a))))
(lambda (f) (m (lambda (a) ((f f) a))))))
(lambda (E)
(lambda (t)
(((t (lambda (M) (lambda (x) (E (M x)))))
(lambda (M) (lambda (N) ((E M) (E N)))))
(lambda (x) x))))))
(define test-1
(E (Q (lambda (i) i))))
(define test-2
(E (Q (((lambda (m)
((lambda (f) (m (lambda (a) ((f f) a))))
(lambda (f) (m (lambda (a) ((f f) a))))))
(lambda (E)
(lambda (t)
(((t (lambda (M) (lambda (x) (E (M x)))))
(lambda (M) (lambda (N) ((E M) (E N)))))
(lambda (x) x)))))
(lambda (a) (lambda (b) (lambda (c) (a (lambda (i) (lambda (a) (lambda (b) (lambda (c) (c i)))))))))))))
; ((lambda (i) i) 'ok)
; ok
; > (test-1 'ok)
; ok
; > (test-2 'ok)
; ok
Wednesday 23 July 2008
HOAS based self interpreter for lambda calculus
Just copied this out of Self-applicable Partial Evaluation for Pure Lambda Calculus
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment