- The code below implements a normal-order interpreter for the untyped lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are not first class and do not alter the semantics of the lambda-calculus. Yet they make complex terms easier to define and apply.
-
- The code also includes a few convenience tools: tracing of all reduction, comparing two terms modulo alpha-renaming, etc.
-
- This calculator implements a normal-order evaluator for the untyped lambda-calculus with shortcuts. Shortcuts are distinguished constants that represent terms. An association between a shortcut symbol and a term must be declared before any term that contains the shortcut could be evaluated. The declaration of a shortcut does not cause the corresponding term to be evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet to be defined ones. Shortcuts make programming in lambda-calculus remarkably more convenient.
+ The code below implements a normal-order interpreter for the untyped
+ lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are
+ not first class and do not alter the semantics of the lambda-calculus. Yet they
+ make complex terms easier to define and apply.
+
+ The code also includes a few convenience tools: tracing of all reduction,
+ comparing two terms modulo alpha-renaming, etc.
+
+ This calculator implements a normal-order evaluator for the untyped
+ lambda-calculus with shortcuts. Shortcuts are distinguished constants that
+ represent terms. An association between a shortcut symbol and a term must be
+ declared before any term that contains the shortcut could be evaluated. The
+ declaration of a shortcut does not cause the corresponding term to be
+ evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet
+ to be defined ones. Shortcuts make programming in lambda-calculus remarkably
+ more convenient.
+
+ Besides terms to reduce, this lambda-calculator accepts a set of commands,
+ which add even more convenience. Commands define new shortcuts, activate
+ tracing of all reductions, compare terms modulo alpha-conversion, print all
+ defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are
+ entered at a read-eval-print-loop (REPL) "prompt" -- or "included" from a file
+ by a special command.