Tiny introduction to Lambda Calculus with an interactive interpreter.

The code used in this post can be found here: http://github.com/Fraguinha/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 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. e.g.: λ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. e.g.: (λx.x) y is an application that applies the function λx.x to the argument y.

Playground

Expression:

(\x.x) y
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

Statements are separated by semicolons