Lambda Reducer Documentation

Overview

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

• Write a term in the text area box
• Click "Enter Term" when done.
• Either click on the binding site of the redex to contract that redex, or click "Normalize" to do a normalization strategy on the term

Syntax

General

White space is ignored. All output is valid input.

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

Application

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

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.

Binding

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:

• You cannot do shorthand for curried lambda terms. But, because the dot is a precedence operator, it can be omitted this case, although the lambda cannot. So, K can be written \x\y x. The function composition B can be written \f\g\x. f(g x), or \f\g\x. f.g x
• Variables must have a space between them. This is to allow variable names with length larger than 1.
• Variables must not begin with an uppercase character. This is to make the grammar disambiguous (see metafunctions; we need to distinguish between "a(x)" being metafunction instantiation or application).Many special characters are allowed in a variable name except for characters with special significance, such as ., \, (, ), :, =, the comma itself). The word "let" is not allowed to be variable name, and therefore nothing of the form "let\d+" should be a free variable name, lest you generate something whose output cannot be input.
• Although you can, you should not use an underscore by itself as a variable name. This will break the alpha renaming for printing. It is allowed, however, because all output for the program is also valid input. An underscore as a bound variable represents a K redex.

Metafunctions

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.

Strings

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 +₃, 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 +₃, 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).

Constants

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

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.

Bugs

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 wgunther@math.cmu.edu. Hotspots current involve DOM manipulations more than anything else.