Help
This app has only been tested for Google Chrome. It may or may not work on other browsers.
Lambda Toy verifies whether or not your expression is a well-formed formula in the lambda-calculus according to the definition of (Church, 1936). If it is a wff, it allows you to carry out the operations of alpha-conversion and beta-reduction.
To input your expression, type it into the text area and click submit. The symbol lambda may be substituted by a backslash \. This app recognizes well-formed formulas according to the following definition:
(Church, 1936)
We select a particular list of symbols, consisting of the symbols {, }, (, ), λ, [, ], and an enumerably infinite set of symbols a, b, c,... to be called variables. And we define the word formula to mean any finite sequence of symbols out of this list. The terms well-formed formula, free variable, and bound variable are then defined by induction as follows.
- A variable x standing alone is a well-formed formula and the occurrence of x in it is an occurrence of x as a free variable in it.
- If the formulas F and X are well-formed, {F}(X) is well-formed and an occurrence of x as a free (bound) variable in F or X is an occurrence of x as a free (bound) variable in {F}(X).
- If the formula M is well-formed and contains an occurrence of x as a free variable in M, then λx[M] is well-formed, and an occurrence of x in λx[M] is an occurrence of x as a bound variable in λx[M], and an occurrence of a variable y, other than x, as a free (bound) variable in M is an occurrence of y as a free (bound) variable in λx[M].
In the future, I plan to include support for abbreviations like λfx.f(x).
If your expression is recognized as a wff, you can carry out the following operations:
(Church, 1936)
I. To replace any part λx[M] of a formula by λy[S(x, y, M)] where y is a variable which does not occur in M.
II. To replace any part {λx[M]}(N) of a formula by S(x, N, M), provided that the bound variables in M are distinct both from x and from the free variables in N.
S(x, N, M) refers to the formula obtained by replacing all instances of x in the formula M by the formula N. Operation I is called alpha-conversion, or renaming. Operation II is called beta-reduction, or reducing. These operations are carried out by clicking on links. A bound variable will appear as a link at the site where it is bound. By clicking on this link, the variable will be renamed. For example, clicking on the link in λx[x] gives λy[y]. Whenever Operation II can be performed, the lambda symbol corresponding to it will appear as a link. Clicking on that link will reduce the formula. For example, clicking on the link in {λx[x]}(y) will give y.
Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics 58 (58): 345–363.