These are formulas that can be used in your λ-expressions.
They are formatted
(λ*.*
expression)
λname.
where each name corresponds to an expression.
Each time one the above names is encountered in a λ-term, it is substituted for its corresponding expression.
You can create your own formulas using the "Add Formula" button below.
Note that due to the fact that λ-terms are anonymous functions, formulas can only refer to previous formulas – circular definitions are impossible and will yield unexpected results if attempted.
Result
≡SKI
≡β
≡η
≡α
Guide
Enter a λ-expression into the input field
To enter the character 'λ',
simply use the backslash key '\'
Hit enter or press Evaluate to evaluate the λ-expression
The evaluation will yield β- and η-reductions of the entered expression, as well as any α-equivalent terms present in the Formulæ list
Any λ-expressions that take longer than 100 ms to evaluate, or that result in a stack overflow will yield ⊥, which represents an irreducible term
Due to the way browsers run this script (most likely on a low-priority thread), λ-expressions may sometimes take longer than 100 ms to evaluate, and time out, yielding ⊥, regardless of whether they are theoretically reducible or not
This is especially the case when switching back to this tab after spending (CPU) time elsewhere – the tab would be backgrounded, and thus would take extremely long (> 100 ms) to compute λ-evaluations
The solution is simple – keep hitting Evaluate until the tab is foregrounded again and yields the correct evaluation
Formulas that can be used in λ-expressions are found in the Formulæ dropdown
A formula is an alias for an expression;
It's a variable that is substituted for its corresponding expression during evaluation
An assortment of combinators are already preloaded into the list
Custom formulas can be added using the Add Formula button
A λ-expression can be converted to an expression containing only the S, K & I combinators using the SKI button
Definitions for these combinators (the so-called SKI calculus) can be found in Formulæ section