This file provides an interpreter for untyped lambda calculus
expressions.
* Use:
To evaluate a lambda calculus expression, type in the following,
replacing with the desired expression.
M-x lc-eval-expression RET () RET
Note that the expression must be surrounded by a set of
parentheses. Omit the period in `lambda' constructs.
To define a metavariable, evaluate the following code, replacing
with the name of the metavariable, and with
the desired expression.
(lc-def ())
If you wish to evaluate lambda calculus expressions
programmatically, you can use the `lc-eval' macro, which takes
something of the form (). There is no need to quote
the expression.
To see each individual step of the evaluation process, do the
following. By default, the expressions are pretty-printed; to
change that, customize the `lc-enable-pp' option.
M-x lc-step-expression RET () RET
* Implementation details:
This interpreter works in several stages.
** Translation (Lambda Calculus -> Emacs Lisp):
The first step is translation from a lambda calculus expression to
an Emacs Lisp expression. This involves determining bound and free
variables, and replacing implicit function calls with explicit
calls to `lc-apply'.
** Evaluation:
The next step is to evaluate the translated expression, namely:
substituting previously-defined expressions for free variables and
repeatedly applying function calls until a lambda expression is
reached.
In order to prevent infinite evaluation, a limit has been placed on
the number of consecutive evaluations that are permitted. The
default is 50. To change this, customize the `lc-max-steps'
option.
** Untranslation (Emacs Lisp -> Lambda Calculus):
The final step is to take the result from evaluation and make it
look like a lambda calculus expression. This involves removing the
"bound" and "free" prefixes from variables, removing calls to
`lc-apply', and making the resulting expression as minimal as
possible.
* Credits:
Most of the environment comes from the Types and Programming
Languages textbook by Benjamin C. Pierce. As far as I can tell,
these sample definitions are considered common knowledge, so I
should be able to distribute them.
A couple of the functions of the environment are from
, but were modified to use a
single-argument lambda form.
Thanks go to Riastradh on #emacs for suggesting that I use
functions rather than the macro mess I previously had.
* Endorsements:
From an IRC chat on #hcoop:
i'm currently making a lambda calculus interpreter in
Emacs Lisp
* Smerdyakov gags. :D
From an IRC chat on #emacs:
* mwolson is tantalizingly close to having the final piece of his
lambda calculus interpreter (in Emacs Lisp) done
:-)
*shudder*