Wednesday 23 July 2008

HOAS based self interpreter for lambda calculus

Just copied this out of Self-applicable Partial Evaluation for Pure Lambda Calculus


(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

No comments: