General information
Lambda Calculus is a formal system of logic, suitable for expressing computation, devised by Alonzo Church in the 1930s. This client-side JavaScript-based application is an evaluator thereof.
To evaluate some lambda calculus term, type it in the evaluator text box, and, if it is syntactically correct, submit it to the evaluator. When entering a term, be sure to have selected the right type system (untyped is the default), as the parser uses this information to correctly parse the term. Now you can select a particular redex and reduce it by a mouse-click. Redexes will be highlighted on mouse-hover, and with compliance with selected reduction strategy. You can check for total number of reducible expressions down on the bottom panel. After the mouse-click, new, reduced expression will appear below the original. After this point, you can continue in a similar fashion until the term has no remaining redexes. Alternatively, if you wish to evaluate the expression at once, you can click on the arrow with asterisk →* after reducible term. If the evaluation is short enough, each reduction step will appear below the clicked one. On the other hand, if the evaluation is long (precisely, more than 50 steps), only the final reduced expression will be shown.
Term syntax
Parser-accepted, syntactically valid term is a sequence of lower- and uppercase letters, numerals, dots, equality signs, lambda characters, whitespace characters, and parentheses, adhering to one of the following grammars according to the selected type system:
This grammar holds for the untyped lambda calculus terms, and also for Hindley-Milner type system:TERM ::= (TERM TERM) | VARIABLE | ALIAS_CONSTANT | (λVARIABLE.TERM) | Let VAR = TERM In TERM | LetRec VAR = TERM In TERM
VARIABLE ::= LOWERCASE_LETTER | LOWERCASE_LETTER NUMERAL_STRING
ALIAS_CONSTANT ::= NUMERAL_STRING | UPPERCASE_LETTER_STRING
TYPE ::= (TYPE → TYPE) | Int | Bool
TERM ::= (TERM TERM) | VARIABLE | ALIAS_CONSTANT | (λVARIABLE:TYPE.TERM) | Let VAR = TERM In TERM | LetRec VAR : TYPE = TERM In TERM
VARIABLE ::= LOWERCASE_LETTER | LOWERCASE_LETTER NUMERAL_STRING
ALIAS_CONSTANT ::= NUMERAL_STRING | UPPERCASE_LETTER_STRING
Reductions
Besides desugaring the Let expressions, there are three reductions possible: beta reduction, which replaces all the lambda-bound variables inside a function with a argument, delta reduction, that reduces application of constants, and eta reduction, removing the unneeded lambda abstractions.
Beta reductions are highlighted by blue outline for function, red outline for an argument. Delta reductions are indicated by a green outline, and Let expressions and eta reductions are indicated by yellow outline.
There are some available reduction strategies that you can select from the head navigation bar. When using a typed system, you can use only call by value strategy. To select a reducible expression, click on it. The result will be appended to the already existing derivation on the screen.
Aliases & Constants
Altough similar in appearance, aliases and constants are somewhat different. To input alias or constant, simply type its name into input box. You can change default setting to interpret aliases and constant with same name as constants, instead of aliases, or, if you want to use both constants and aliases from set of shared names, use exclamantion mark ! before some term to override default setting for this given term. For example, there is an alias "PLUS," that stands for pure lambda calculus church-encoded addition, and constant function "PLUS," that takes two constant numbers and outputs another numerical constant as result. Alias is a name for a given term, while Constant is pre-defined symbol that does not stand for any other term. Constants can be functions or primitive values, such as numbers and boolean values, all of which are defined outside of the lambda calculus.
To define your own alias, use the choose the Add an alias option from the Options menu, write the name of the term to the left-hand side of the equality sign, and the term to the right-hand side. You can also use the term on the last line right away.
| Alias | Constant | |||
|---|---|---|---|---|
| name | description and term | arity | description | |
| n | Church encoded natural numbers, input up to 3 digits only | 0 | integer primitives. JavaScript implementation-defined range | |
| λf.λx.f n x | ||||
| SUCC | successor function on Chuch numerals | 1 | successor function on constants | |
| λnfx.f (n f x) | ||||
| PRED | predecessor function, the least result is zero | 1 | predecessor function, negative results allowed |
|
| λnfx.n (λgh.h (g f)) (λ u.x) (λ u.u) | ||||
| PLUS | addition function on Church numerals | 2 | addition function on constants | |
| λmnfx.m f (n f x) | ||||
| MINUS | substraction on Church numerals, the least result is zero | 2 | substraction on constants, negative results allowed |
|
| λmn.n PRED m | ||||
| TIMES | multiplication on Church numerals | 2 | multiplication function on constants | |
| λmnf.m (n f) | ||||
| ISZERO | predicate testing if a Church numeral is zero, returning Church Boolean |
1 | predicate testing is a numeral constant is zero |
|
| λn.n (λx.FALSE TRUE) | ||||
| LEQ | predicate testing if a Church numeral is less than, or equal to another |
2 | predicate testing if a numeral constant is less than, or equal to another |
|
| λmn.ISZERO (MINUS m n) | ||||
| DIV | division on Church numerals | 2 | division function on integer constants | |
| recursive definition below | ||||
| EQ | predicate testing if two Church numerals are equal | 2 | equality function on numerical constants, returns Boolean constant |
|
| λmn.AND (LEQ m n) (LEQ n m) | ||||
| TRUE | Church Boolean true | 0 | Boolean true constant | |
| λxy.x | ||||
| FALSE | Church Boolean false | 0 | Boolean false constant | |
| λxy.y | ||||
| ITE | conditional, the first argument is Church Boolean | 3 | conditional, the first argument Boolean constant, type system dependent semantics |
|
| λxyz.x y z | ||||
| OR | logical conjunction on Church Booleans | 2 | logical conjunction on Boolean constants | |
| λyx.y y x | ||||
| AND | logical disjunction on Church Booleans | 2 | logical disjunction on Boolean constants | |
| λyx.y x y | ||||
| NOT | logical negation on Church Booleans | 1 | logical negation on Boolean constants | |
| λx.x FALSE TRUE | ||||
| FIX | undefined | 1 | fixed point of the abstraction input | |
| Y | fixed point combinator | undefined | ||
| λf.(λx.f (x x)) (λ x.f (x x)) | ||||
| THETA | fixed point combinator, displayed as Θ | undefined | ||
| (λxf.f (x x f)) (λxf.f (x x f)) | ||||
| OMEGA | Omega combinator, displayed as Ω | undefined | ||
| (λx.x x) (λ x.x x) | ||||
| S | pure λ-calculus S combinator | 3 | S combinator constant | |
| λxyz.x z (y z) | ||||
| K | pure λ-calculus K combinator | 2 | K combinator constant | |
| λij.i | ||||
| I | pure λ-calculus I combinator | 1 | I combinator constant | |
| λi.i | ||||
Type system
None – Untyped lambda calculus
The default "type system" is no type system at all. This enables reductions of any terms, potentially resulting in inconsistencies, but it gives you a freedom of self-application.
Simply typed lambda calculus
The simple simply typed lambda calculus is supplied with type annotations marking the expected input to a function. Because using the call by value, a type of a reducible function and its argument can be determined without an outside context, and it will stop evaluation of terms that do not match the expected argument and the supplied one.
Hindley-Milner type system
This type system does not need type annotations, and it can derive the types of types without help. It is able to derive the most general, polymorphic type.
Import & Export
Export
There are several output options: you can print the evaluation, generate Latex source, or save it as a file. These export options save the whole evaluation as shown on the screen, this means selected options, including Alias expansion and Shorthand form, are used. In case of exporting the evaluation into a file, user-defined Aliases are also saved to the file.
Import
You can import a previously saved file: either a full derivation, including the user-defined aliases, or just the aliases. The page URL is pointing to the last term, so you can copy and paste it.
Bottom panel
This panel is designated to present you with useful information: Whether the current term (the last in the evaluation) contains redexes, and if so, what kind of redexes, and especially, how many. If a typed system is selected, this panel will also show information about type correctness. Information about currently selected type system is shown in the right corner of this panel, but you cannot change it during the evaluation.
Examples
To evaluate particular expression, just click on it—a new window with evaluator set to a given expression will be open in your browser.
λx.f x
(λnfx.n (λgh.h (g f)) (λu.x) (λu.u)) (λfx.f (f (f (f x))))
Θ (this can be input only as "THETA")
PLUS 2 2
(λx1w2.x1) (λw.w w2)
Ω (this can be input only using "OMEGA")
(λx1x2x3x4.PLUS x2 x4) FALSE 2 TRUE 5
(λx:Int → Bool.x) (λw:Int.EQ w 12)
(λf.f 2 2) TIMES
Let f = 234 In PLUS f f
SUCC (SUCC 4)
About
Created in 2018 by JavaScript needed for mail rendition as a practical part of bachelor thesis at Masaryk University.
Computer Modern font is licensed under free and open-source SIL OPEN FONT LICENSE.
This work is licensed under CC0 - Public Domain to the extent permitted by law. The source code is available at gitLab.