17 releases
0.2.2 | Sep 11, 2024 |
---|---|
0.2.1 | Feb 3, 2024 |
0.1.56 | Oct 19, 2023 |
0.1.54 | Mar 4, 2023 |
0.1.1 | Mar 25, 2022 |
#49 in Math
71KB
1.5K
SLoC
Lambdascript
Lambdascript executes beta-reduction steps on terms of the lambda calculus, with the option of inferring polymorphic types before reduction. It is not a high-performance implementation of lambda calculus. Rather, the tool serves three primary purposes, all of which are illustrational or educational in nature:
-
It demonstrates the usage of the rustlr parser generator. The LALR(1) grammar for lambdascript in rustlr format is given here.
-
For introductory level students in a programming languages class, the tools show every step of beta reduction, including alpha-conversions where necessary, in reducing a term to normal form. It includes both full beta-normalization using the normal order (call-by-name) strategy as well as weak normalization using call-by-value. Definitions can be given for terms such as S, K, I.
-
For more advanced students, the source code of the program demonstrates how lambda terms can be represented in abstract syntax and how reductions can be implemented. The typing module demonstrates how types can be inferred using the unification algorithm.
Usage
The program was written in Rust and should be installed as an executable: cargo install lambdascript
. You must have Rust installed (from https://rust-lang.org) to execute the cargo command.
The program can read from a script, or interactively from stdin.
By default, terms are evaluated in the untyped mode.
Given a file simple.ls
with the following contents:
define I = lambda x.x;
define K = lambda x.lambda y.x;
define S = lambda x.lambda y.lambda z.x z (y z);
define lazy INFINITY = (lambda x.x x) (lambda x.x x);
lambda y.K y INFINITY;
lambdascript untyped simple.ls
evaluates the input as a script.
The 'untyped' directive is optional since it's the default. It then enters
interactive mode with the definitions still loaded. Without the optional
file name, lambda script will just start in interactive mode.
Here is a sample session from executing simple.ls
:
λy.K y INFINITY
= λy.(λxλy.x) y INFINITY
< alpha conversion of y to y1 >
=> λy.(λy1.y) INFINITY
= λy.(λy1.y) ((λx.x x) (λx.x x))
=> λy.y
Entering interactive mode, enter 'exit' to quit...
<<< typed
TERMS DEFINED IN THE UNTYPED MODE WILL NOW BE TYPE-CHECKED BEFORE EVALUATION
<<< K I INFINITY
TYPE INFERENCE FOR <K I INFINITY> FAILED : UNTYPABLE
EVALUATION CANCELED
<<< I I
THE INFERRED TYPE OF <I I> IS e -> e
I I
= (λx.x) I
=> I
= λx.x
The reduction terminated in the untyped mode because normal-order
(call-by-name) evaluation is applied by default. If the the last line
of the file was replaced with weak (K I INFINITY x)
, then weak
reduction using call-by-value will take place, resulting in an
infinite loop. There will likewise be an infinite loop if lazy
was
missing from the definition of INFINITY
. Full, normal-order
evaluation and weak call-by-value are the only reduction strategies
implemented in lambdascript.
One can switch from typed to untyped mode with the typed
directive.
There is no syntax for types in terms. Most general types are always
inferred. Undefined free variables are not considered typable. Notice
that I I
is well-typed because the type scheme inferred for I
can
be instantiated twice. One can also execute the script directly in the
typed mode. lambdascript typed simple.ls
will show the types
inferred for all definitions:
THE INFERRED TYPE OF I IS: Π(a -> a)
THE INFERRED TYPE OF K IS: Π(a -> b -> a)
THE INFERRED TYPE OF S IS: Π((h -> f -> g) -> (h -> f) -> h -> g)
TYPE INFERENCE FOR <(λx.x x) (λx.x x)> FAILED : UNTYPABLE
DEFINITION OF INFINITY NOT ACCEPTED
In the typed mode, the undefined free variable INFINITY cannot be typed
TYPE INFERENCE FOR <λy.K y INFINITY> FAILED : e -> UNTYPABLE
EVALUATION CANCELED
Here, Π
quantifies all type variables in its scope.
Types are always inferred before beta-reduction, so it can be called static typing.
Lambdascript uses standard syntax for lambda terms: application
associates to the left and application binds tighter than abstraction,
meaning that the scope of a λ extends to the right as far as possible
unless bounded by parentheses. However, lambda expressions inside
applications must always by bound by parentheses: so x lambda y.y
should be replaced with x (lambda y.y)
. Defintions and terms to be
evaluated in a script must be separated by ; (semicolon). All
variables and identifiers are limited to a length of 15 characters.
The file pure.ls contains a full list of definitions of well-known (untyped) lambda-calculus combinators.
Interactive Interpreter Directives
At the <<<
prompt the following special directives can be given:
exit
orquit
: exits the programtyped
: switch to typed mode: types will be inferred and untypable terms will not be reduced.untyped
: switch to untyped modeuse lambda
oruse lam
oruse Lam
oruse \
: On some systems, the Greek character λ (unicode 0x03BB) may fail to display properly. To change the symbol displayed for lambda, you can choose between one of four alternatives (the choices are limited to these four because the symbol must be a statically allocated string).use greek
oruse unicode
: reverts to displaying λ, which is the defaulttrace off
: turns off the displaying of intermediate reduction steps: only the initial term and the final normal form are showntrace medium
: Beta-reduction steps are shown, but not the expansion of defintions nor alpha-conversiontrace on
ortrace max
: restore displaying of all steps: this is the default
Recent Updates:
Version 0.2.2 rigged the type of the FIX operator to (a -> a) -> a in typed mode.
Version 0.2.0 introduced the typed option.
Dependencies
~4.5MB
~74K SLoC