The code used in this post can be found here: Lambda.

Lambda Calculus

At it’s core, Lambda Calculus is composed of three elements: variables, abstractions, and applications.

• Variables are placeholders that represent an unknown value or a lambda term. They are typically represented by a single lowercase letter.

• Abstractions are expressions that define a function. They consist of a lambda, followed by a variable, followed by a dot, followed by a lambda term. i.e.: λx.x is an abstraction that defines a function that takes x and returns x.

• Applications are expressions that apply a function to an argument. They consist of two lambda terms separated by a space. The left term is the function to be applied, and the right term is the argument to which the function will be applied. i.e.: (λx.x) y is an application that applies the function λx.x to the argument y.

Playground

Expression:
Result:

Syntax

x or x'

λx.M or \x.M

M N

where M and N are lambda terms

This interpreter supports sintatic sugar like:

λxyz.M instead of λx.λy.λz.M

and

M N O instead of ((M N) O)

Terms can be defined in this way:

Y=λf.(λx.f(xx))(λx.f(xx))

or

S=λxyz.xz(yz);K=λxy.x;I=λx.x

or even

TRUE=λxy.x