Lambda calculus

Previous: Computer science

Lambda calculus is a Formal System in mathematics for expressing computation based on function abstraction using variable binding and substitution. Functional programming derives its core concepts from lambda calculus. The LISP family of languages is directly based on it. In 1937, Alan Turing proved that lambda calculus and Turing machine are equivalent models of computation.

Features of the language:

• Single-letter variable names (a-z)
• Application: ab means call function a with parameter b (left associative, so abc = (ab)c)
• Abstraction: define anonymous functions using λ
• Parentheses for grouping expressions

Grammar:

Lambda      ::= Variable | Grouping | Abstraction | Application Variable    ::=
<letter> Grouping    ::= "(" Lambda ")" Abstraction ::= λ variable "." Lambda
Application ::= Lambda Lambda

Three conversion rules:

• α-conversion (Alpha): rename bound variables
• β-reduction (Beta): substitute arguments for parameters
• η-conversion (Eta): eliminate unused parameters

A variable without a lambda binding is called free. A variable with a lambda binding is called bound. A lambda expression with no free variables is called a closure.

Logic encoding:

true  = λx.(λy.x) false = λx.(λy.y)