Created
September 18, 2018 12:21
-
-
Save bor0/16733c375699661adf6dbfe4f7145a70 to your computer and use it in GitHub Desktop.
Lambda Calculus Interpreter
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
; Constructors | |
(define (lambda-expr? e) | |
(and (pair? e) | |
(equal? (car e) 'λ) | |
(equal? (caddr e) '→))) | |
(define (make-lambda argn argv) (list 'λ argn '→ argv)) | |
(define (lambda-param e) (cadr e)) | |
(define (lambda-body e) (cadddr e)) | |
; Substitution procedures | |
(define (lambda-subst e src dst) | |
(cond ((equal? e src) dst) | |
((lambda-expr? e) (if (eq? (lambda-param e) src) | |
e ; If this lambda expression has a param name same as src, do not substitute | |
; Otherwise, construct a new lambda with this param and substitute src to dst in the lambda body | |
(make-lambda (lambda-param e) (lambda-subst (lambda-body e) src dst)))) | |
; If it's a list of expressions recursively substitute them | |
((pair? e) (cons (lambda-subst (car e) src dst) | |
(lambda-subst (cdr e) src dst))) | |
(else e))) | |
; Evaluation procedures | |
(define (can-beta-reduce? e) | |
(and (pair? e) | |
; If the first parameter in the list is a lambda expression, or the first parameter can also be reduced | |
;(or (lambda-expr? (car e)) (can-beta-reduce? (car e))) | |
(lambda-expr? (car e)) | |
; And there is a second value in the list (to apply to the lambda expr) | |
(pair? (cdr e)))) | |
(define (beta-reduce e . vs) | |
(if (and (pair? vs) (lambda-expr? e)) | |
; Substitute current value in lambda-body and recursively reduce the remaining values | |
(apply beta-reduce | |
(lambda-subst (lambda-body e) (lambda-param e) (car vs)) | |
(cdr vs)) | |
; No values, so just return the expression | |
e)) | |
(define (lambda-eval e) | |
(cond ((can-beta-reduce? e) (lambda-eval (apply beta-reduce e))) | |
((pair? e) (let ([new-e (cons (lambda-eval (car e)) | |
(lambda-eval (cdr e)))]) | |
(if (can-beta-reduce? new-e) | |
(lambda-eval new-e) | |
new-e))) | |
(else e))) |
Test for logic:
(define true (make-lambda 'x (make-lambda 'y 'x)))
(define false (make-lambda 'x (make-lambda 'y 'y)))
(define l-and (make-lambda 'p (make-lambda 'q '(p q p))))
(define l-or (make-lambda 'p (make-lambda 'q '(p p q))))
(define l-not (make-lambda 'p (list 'p false true)))
(and
(equal? (lambda-eval (list l-and false false)) false)
(equal? (lambda-eval (list l-and false true)) false)
(equal? (lambda-eval (list l-and true false)) false)
(equal? (lambda-eval (list l-and true true)) true)
(equal? (lambda-eval (list l-or false false)) false)
(equal? (lambda-eval (list l-or false true)) true)
(equal? (lambda-eval (list l-or true false)) true)
(equal? (lambda-eval (list l-or true true)) true)
(equal? (lambda-eval (list l-not true)) false)
(equal? (lambda-eval (list l-not false)) true))
Test for pairs:
(define one (make-lambda 'f (make-lambda 'x '(f x))))
(define two (make-lambda 'f (make-lambda 'x '(f (f x)))))
(define true (make-lambda 'x (make-lambda 'y 'x)))
(define false (make-lambda 'x (make-lambda 'y 'y)))
(define pair (make-lambda 'x (make-lambda 'y (make-lambda 'f '(f x y)))))
(define first (make-lambda 'p (list 'p true)))
(define second (make-lambda 'p (list 'p false)))
(define test-pair (lambda-eval (list pair 1 2)))
(and
(equal? (lambda-eval (list first test-pair)) 1)
(equal? (lambda-eval (list second test-pair)) 2))
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Test for numbers: