Basic evaluator and command line REPL for lambda calculus
Supports standard lambda notation:
- x - variables
- λx.M - abstractions
- (M N) - applications
Variable name can be either one lowercase 'a'..'z' or a sequence of uppercase 'A'..'Z' characters.
x
, y
, z
, ID
, TRUE
and FALSE
are all valid identifiers.
x1
, yD
or FalSE
are not. In fact FalSE
will be parsed as sequence of applications (F)(a)(l)(SE)
λ can be replaced with \
, for example λxy.x
can be written as \xy.x
. Abstractions of form λxy.(...)
will be automatically normalized to λx.λy.(...)
.
It is highly recommended to enclose abstractions in parenthesis to avoid confusing parser.
Any two terms appearing one after another are parsed as application.
Note that parenthesis are recommended to avoid confusion.
λx.xy
will be parsed as
- Abstraction:
- parameter: x
- body:
- Application:
- x
- y
To parse it as Application use parenthesis.
(λx.x)y
will be parsed as
- Application:
- Abstraction:
- parameter: x
- body:
- x
- y
Evaluator will perform beta-reduction on expression until it is no longer reducible. Evaluator also keeps track of all the reductions, so it is possible to trace back all the steps.
Assignments
One can use :=
to bind abstractions to names. Only lambda functions without free variables can be bound to a name*
ID := λx.x
Bound abstractions can be used in other expressions, i.e.
ID(a)
will be evaluated to a
.
Evaluator will automatically perform alpha-conversion and rename conflicting parameters**.
* To be implemented
** To be implemented as well
- lambda-core - lexer, parser and evaluator of lambda expressions
- cli-repl - CLI-based REPL for lambda expressions*
- web-repl - Web-based REPL for lambda expressions**
* Work in progress
** To be implemented later