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:

1. It demonstrates the usage of the rustlr parser generator. The LALR(1) grammar for lambdascript in rustlr format is given here.

2. 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.

3. 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 demontrates the 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 read from stdin. Expressions and defintions are separated by ; (semicolon). Here's an example of reading and evaluating from stdin, which can be initiated by running the executable.

<<< (lambda x.x (lambda y.x y)) y;
(λx.x (λy.x y)) y
 =>  y (λy1.y y1)

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. Lambda expressions inside applications must always by bound by parentheses: so x lambda y.y should be replaced with x (lambda y.y). There is no notation for types in terms: types are inferred for terms.

Given a file simple.ls with the following contents:

define I = lambda x.x;
define K = lambda x.lambda y.x;
define lazy INFINITY = (lambda x.x x) (lambda x.x x);

K I INFINITY x;

lambdascript simple.ls produces the following output:

K I INFINITY x
= (λxλy.x) I INFINITY x
 =>  (λy.I) INFINITY x
= (λyλx.x) INFINITY x
 =>  (λx.x) x
 =>  x

The reduction terminated 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.

Given a file simpletyped.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 SKI = S K I;

lambdascript typed simpletyped.ls produces the following output:

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)
THE INFERRED TYPE OF SKI IS  Π(r -> r)

where Π represents quantification over type variables.

All variables and identifiers are limited to a length of 15 characters.

After a script is executed, the interpreter automatically enters interactive mode with the definitions from the script still available.

The file pure.ls contains a full list of definitions of well-known lambda-calculus combinators.

Interactive Interpreter Directives

At the <<< prompt the following special directives can be given:

• exit or quit : exits the program
• typed : switch to typed mode: types will be inferred and untypable terms will not be reduced.
• untyped : switch to untyped mode
• use lambda or use lam or use Lam or use \: 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 or use unicode: reverts to displaying λ, which is the default
• trace off: turns off the displaying of intermediate reduction steps: only the initial term and the final normal form are shown
• trace medium: Beta-reduction steps are shown, but not the expansion of defintions nor alpha-conversion
• trace on or trace max: restore displaying of all steps: this is the default

---