An interpreter for the lambda calculus
| basic-functions.lisp | Add the theta combinator | |
| lambda-calculus.asd | Version 1.1 | |
| lambda-calculus.lisp | Accept variable names not made only of characters and digits | |
| LICENSE | lambda-calculus | |
| README.org | lambda-calculus | |
| test.lisp | Add len and append functions. | |
lambda-calculus, an interpreter for the lambda calculus
Description
This program is an interpreter for the pure lambda calculus.
The lambda terms have the following format:
A, whereAis a symbol (alpha characters)(B C), whereBandCare lambda terms(lambda D E), whereDis a symbol andEis a lambda term
The beta-reduce function takes a lambda term and reduces it to its normal
form using the beta-reduction rule.
The are-alpha-equivalent function takes two lambda terms and indicates if
they are equivalent with regard to alpha-conversion.
Examples
The basic-functions.lisp file contains the Church encodings of a few basic functions (logic, arithmetic, pairs, Y combinator).
Load the interpreter and the basic functions:
(load "lambda-calculus")
(load "basic-functions")A few examples:
(lambda-calculus:beta-reduce '(lambda a (lambda b a)))
-> (LAMBDA A (LAMBDA B A))(lambda-calculus:beta-reduce '((lambda a (lambda b a)) x)
-> (LAMBDA B X)(lambda-calculus:beta-reduce true.)
-> (LAMBDA A (LAMBDA B A))(lambda-calculus:beta-reduce false.)
-> (LAMBDA A (LAMBDA B B))(lambda-calculus:beta-reduce one.)
-> (LAMBDA F (LAMBDA X (F X)))(lambda-calculus:beta-reduce `(,inc. ,one.))
-> (LAMBDA F (LAMBDA X (F (F X))))(lambda-calculus:beta-reduce `((,eq. (,inc. ,one.)) ,two.))
-> (LAMBDA A (LAMBDA B A))(lambda-calculus:are-alpha-equivalent '(lambda x x) '(lambda y y))
-> T(lambda-calculus:are-alpha-equivalent '(lambda x (x y)) '(lambda y x))
-> NIL(lambda-calculus:are-alpha-equivalent '(lambda x (lambda y (x y)))
'(lambda y (lambda x (y x))))
-> T(lambda-calculus:are-alpha-equivalent '(lambda x (lambda y (x y)))
'(lambda y (lambda x (x y))))
-> NIL