LAMBDA CALCULUS (also written as λ-calculus) is a system in mathematical logic for expressing computation using function abstraction and application. The system captures the notion of computation; it is computationally equivalent to the Turing Machine and can therefore model any Turing machine program.
The system was defined in the 1930s by Alonzo Church in his paper "An Unsolvable Problem of Elementary Number Theory" as part of his research in the foundations of mathematics.
Here are a few input examples for the interpreter:
(\x.x)(\y.y)(\z.z)(\x.(\y.xy))y(\x.(\x.x))(\x.xy)yThe Wikipedia article for the lambda calculus system can be found here.
TURING MACHINES are a system that represent computation as states on an abstract tape machine. Compared to the lambda calculus, Turing machines are a much more abstract, semi-physical model of computation. Despite the system's simplicity, Turing machines can simulate the entire class of computations and are therefore equivalent in power to the lambda calculus.
The system was defined by Alan Turing in the 1930s in his paper “On Computable Numbers with an Application to the Entscheidungsproblem”.
Use the dropdown menu on the top-right of the machine to select an exemplar Turing machine.
The Wikipedia article for Turing machines can be found here.
MULTI-TAPE TURING MACHINES are a variant of the original Turing machine. As the name suggests, a multi-tape Turing machine hosts multiple tapes.
In the paper "The Weak Lambda Calculus as a Reasonable Machine", Dal Lago and Martini make it clear that the usual notation for the lambda calculus does "not take into account the complexity of handling variables, and substitutions". They therefore introduce a notation where binary integers are used to describe the number of binders.
In this new notation, the term (\x.x) converts to λ > 0, where 0 denotes the number of binders between the variable in its parameter and the argument. The term (λx.x)(λx.x) converts to @ λ > 0 λ > 0, where @ denotes an application and where > denotes the beginning of a free or bound variable.
The interpreter here is necessary to simulate the lambda calculus in a Turing machine as described in "The Weak Lambda Calculus as a Reasonable Machine".
To simulate the correct lambda term, enter a term in the lambda calculus interpreter on the first page. The term entered will then be updated into its appropriate notation in the multi-tape interpreter's form. After that, click run to simulate the lambda calculus term in the multi-tape Turing machine interpreter.