(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