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.

New! Use @atomic T=a->b->b a to declare new atomic combinators that reduce in one step. Other terms may be used in the definition, but the right-hand side must always start with abstraction (->). Self-referencing definitions supported, too. This is a highly experimental feature, please share your feedback in this issue.

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 numeral, i.e. a term with two arguments x and y returning x(...{n times}...(x(y)...).
• New atomic combinators can be declared with @atomic name = x->y->...<expression>. The right-hand side must always start with an abstraction (->). Self-referencing definitions are supported. This feature is highly experimental.

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.