Simple Kombinator Interpreter

Welcome to the combinatory logic interpreter.

Type an expression in the entry field and click ▶︎. A valid expression contains one or more terms and parenthesis around groups of terms. Unknown terms will be considered free variables and left as is.

New terms can be declared by prepending "name = " to the expression. They will appear in the box on the right and can be clicked to add them to the expression.

The interpreter supports lambda calculus and Church numerals. Lambda expressions are written as x->y->z-><expression>. Church numerals are written as non-negative integers.

The →SK button converts an expression into the SKI basis, term by term, and the →λ button attempts to find the shortest equivalent lambda term.

Enter ? to get detailed info on syntax.

The interpreter honors the following rules:

• Terms are accepted in the form of upper-case latin letters, or lower case identifiers. Uppercase letter terms are assumed to always be one letter and do not require spaces around them.
• A program consists of one or more statements, separated by semicolons (;). A statement may contain terms, parentheses (( and )), and whitespace. Parentheses may be omitted.
• Unknown terms are assumed to be free variables and will be left as is. Known terms and their reduction rules (or implementations) are listed in the right panel.
• If a statement is prepended with identifier = , it defines a new temporary term that can be used in further expressions.
• If that happens to the last statement in the group, it will be permanently added to list of available terms, overriding the existing term with the same name.
• An x->y->z-><some expression> is a lambda expression. Lambdas may be mixed with ordinary combinators. Please use Haskell instead.
• A non-negative integer is assumed to be a church number, i.e. a term with two arguments x and y returning x(...{n times}...(x(y)...).

Examples:

• SIIx evaluates to x(x) // where x is a free variable;
• T = S(K(SI))K declares the T combinator;
• M = SII; Mx evaluates to x(x), M will not be available afterwards;
• 5 x y evaluates to x(x(x(x(x(y)))));
• x->y->x is an equivalent of Kx.

Enter '?' to get this message again.