Lambda Reducer Documentation


This software is written in JavaScript and allows for the reduction of lambda terms. This overall scheme is:



White space is ignored. All output is valid input.

C++ style comments (/*...*/ and //...\n) are honored


Two terms next to each other make an application. As usual, we associate application to the left, so "x y z" is parsed as x applied to y, and the resultant applied to z.


Variables can contain many characters (see formal grammar). They must not begin with an uppercase letter. They should not be only an underscore, as that is reserved for a dummy variable binding a K redex, and is printed in a special case. They may contain numbers, but numbers at the end of a variable are special. They are placed by the printing algorithm to make alpha distinct variable when necessary. So the input "x403" will output "x". The input "\x4.x4 y1" will output "\x1.x1 y". "\x.x\x x" will print "\x1.x1(\x2.x2)". Note: bound variables are always printed with a number at the end, free variables are never.

This creates some weird situations. For instance, "y1 y2" will output "y y" even though the variables are different. I agree, this is a problem, but the solution is that you should never use numbers at the end of a free variable. In fact, just don't use numbers at the end of any variables unless it comes from output from the program otherwise you wish losing semantic meaning when using output as input.

The numbers chosen for bound variables seem rather arbitrary, but the current implementation has them corresponding to the depth of the binding location. This is a good choice for alpha distinction. It is aesthetically a bad choice. Sorry.


The lambda symbol can either be typed using a backslash character (\) or a unicode lowercase lambda. The dot, which is usually thought of as a binder separator, is instead used for a precedence operator. The interpretation of the dot is that it is treated as if a left parenthesis is placed in the place of the dot, and is closed as far as possible to the right. That is to say, everything to the right of the dot is grouped. This matches with what we want when we say \x.x y.

Some things that may annoy you:


Metafunction are a useful construct. A metafunction is one which takes in arguments, like F(\x.x,\x\y x) is a metafunction which takes in I for its first argument and K for its second. In the event that a metafunction is not bound, a metafunction will be an atomic unit in the code, and reductions can occur internally. For instance, if you normalize "F(\x x a)" you get "F(a)". Similarly, you get the same if you normalize "\x F(x) a".

Metafunctions must be alphanumeric and must begin with an uppercase letter. The restriction against special characters is artificial.

Let bindings

A program can begin with sequence of let bindings of the form "let [[varname]] = [[program]] : [[program]]".

For recursive functions, you can use the familiar "letrec x = [[program possibly involving x]] : [[program]]". Of course you can do this with just let, but the x in both parts are separate. letrec is actually short hand for the application of a fixed point combinator; you can see exactly what by doing something with it

Function let bindings

Another kind of let binding is one which binds a metafunction. The syntax for this is "let [[FunctionName]](x,y,z) = [[program]]:[[program]]" that list of variables is actually arbitrarily long. Variables can, of course, be unused in the definition.

No arity checks are done in function instantiation. This means that partial argument may be given and then the term replaced is a lambda term expecting more arguments. If too many arguments are given, those are applied as well and a contraction is attempted for each term applied. This means you should be very careful of giving too many arguments. For example, "let F(x) = \y.y: F(a,\y.y y)" will reduce to "(\y.y y)".

If a variable is repeated in the variable list defining the function then the current implementation will only bind the rightmost variable. This may change in the future.

The empty list "()" can be given in either definition or instantiation.


There are string literals, using the quote symbol: ".

Strings have some semantics too; namely, if you apply two strings, then a reduction can be done where the strings are concatenated.

There are no escape sequence for strings, except quotes and backslashes, need to be escaped. So you can say for instance: "My favorite program is " "\"Hello World\"".

Natural numbers

There are natural numbers. They are not variables, and do not expand to anything by themselves (in particular, they are not Church numerals). You can do addition, (cut-off) subtraction, multiplication, division, and equality (which returns Church booleans) given by symbols +, -, *, /, ==. These are written in prefix, of course.

These operations are curried. In particular + 3 will contract to +3, which is the operation which adds 3 to something. I'm not convinced this is ideal, but I think it's pretty close. +3 can be written instead of +3, since you cannot write the latter. So be careful with your spacing with numerals and numeric operations.

Division by 0 is undefined behavior (currently, it's 0, but this will probably be changed someday).


There are a few predefined constants, all beginning with a dollar sign: $. They are some of the usual combinators, $I, $K, $S, $B, $Y $true, $false.

$true and $false are used for contracting ==. So, == 1 1 will reduce to $true, which itself is \x\y.x.

Formal Grammar

The following is the grammar that is used to generate the parser using JISON.

License and Source

This is written in JavaScript. Moreover, the source provided is not meant for humans to read. The parsing component is generated by JISON using the above grammar.

The DOM is manipulated using jQuery.

See the bitbucket for non-obfuscated source code. This software is licensed under the MIT license, which is a very permissive license which essentially just requires used segments of source code to be labeled.


There are no known bugs, although there is very little error checking and no semantic analysis to speak of. If you find a bug, or would like to suggest an improvement either in implementation or design or a suggest feature please email me at Hotspots current involve DOM manipulations more than anything else.