I think it should be: `ADD = λab.(a S)b`
5.8 KiB
category | name | contributors | ||||||
---|---|---|---|---|---|---|---|---|
Algorithms & Data Structures | Lambda Calculus |
|
Lambda Calculus
Lambda calculus (λ-calculus), originally created by Alonzo Church, is the world's smallest programming language. Despite not having numbers, strings, booleans, or any non-function datatype, lambda calculus can be used to represent any Turing Machine!
Lambda calculus is composed of 3 elements: variables, functions, and applications.
Name | Syntax | Example | Explanation |
---|---|---|---|
Variable | <name> |
x |
a variable named "x" |
Function | λ<parameters>.<body> |
λx.x |
a function with parameter "x" and body "x" |
Application | <function><variable or function> |
(λx.x)a |
calling the function "λx.x" with argument "a" |
The most basic function is the identity function: λx.x
which is equivalent to
f(x) = x
. The first "x" is the function's argument, and the second is the
body of the function.
Free vs. Bound Variables:
- In the function
λx.x
, "x" is called a bound variable because it is both in the body of the function and a parameter. - In
λx.y
, "y" is called a free variable because it is never declared before hand.
Evaluation:
Evaluation is done via β-Reduction, which is essentially lexically-scoped substitution.
When evaluating the
expression (λx.x)a
, we replace all occurences of "x" in the function's body
with "a".
(λx.x)a
evaluates to:a
(λx.y)a
evaluates to:y
You can even create higher-order functions:
(λx.(λy.x))a
evaluates to:λy.a
Although lambda calculus traditionally supports only single parameter functions, we can create multi-parameter functions using a technique called currying.
(λx.λy.λz.xyz)
is equivalent tof(x, y, z) = ((x y) z)
Sometimes λxy.<body>
is used interchangeably with: λx.λy.<body>
It's important to recognize that traditional lambda calculus doesn't have numbers, characters, or any non-function datatype!
Boolean Logic:
There is no "True" or "False" in lambda calculus. There isn't even a 1 or 0.
Instead:
T
is represented by: λx.λy.x
F
is represented by: λx.λy.y
First, we can define an "if" function λbtf
that
returns t
if b
is True and f
if b
is False
IF
is equivalent to: λb.λt.λf.b t f
Using IF
, we can define the basic boolean logic operators:
a AND b
is equivalent to: λab.IF a b F
a OR b
is equivalent to: λab.IF a T b
a NOT b
is equivalent to: λa.IF a F T
Note: IF a b c
is essentially saying: IF((a b) c)
Numbers:
Although there are no numbers in lambda calculus, we can encode numbers using Church numerals.
For any number n: n = λf.fn
so:
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f(f x)
3 = λf.λx.f(f(f x))
To increment a Church numeral,
we use the successor function S(n) = n + 1
which is:
S = λn.λf.λx.f((n f) x)
Using successor, we can define add:
ADD = λab.(a S)b
Challenge: try defining your own multiplication function!
Get even smaller: SKI, SK and Iota
SKI Combinator Calculus
Let S, K, I be the following functions:
I x = x
K x y = x
S x y z = x z (y z)
We can convert an expression in the lambda calculus to an expression in the SKI combinator calculus:
λx.x = I
λx.c = Kc
λx.(y z) = S (λx.y) (λx.z)
Take the church number 2 for example:
2 = λf.λx.f(f x)
For the inner part λx.f(f x)
:
λx.f(f x)
= S (λx.f) (λx.(f x)) (case 3)
= S (K f) (S (λx.f) (λx.x)) (case 2, 3)
= S (K f) (S (K f) I) (case 2, 1)
So:
2
= λf.λx.f(f x)
= λf.(S (K f) (S (K f) I))
= λf.((S (K f)) (S (K f) I))
= S (λf.(S (K f))) (λf.(S (K f) I)) (case 3)
For the first argument λf.(S (K f))
:
λf.(S (K f))
= S (λf.S) (λf.(K f)) (case 3)
= S (K S) (S (λf.K) (λf.f)) (case 2, 3)
= S (K S) (S (K K) I) (case 2, 3)
For the second argument λf.(S (K f) I)
:
λf.(S (K f) I)
= λf.((S (K f)) I)
= S (λf.(S (K f))) (λf.I) (case 3)
= S (S (λf.S) (λf.(K f))) (K I) (case 2, 3)
= S (S (K S) (S (λf.K) (λf.f))) (K I) (case 1, 3)
= S (S (K S) (S (K K) I)) (K I) (case 1, 2)
Merging them up:
2
= S (λf.(S (K f))) (λf.(S (K f) I))
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))
Expanding this, we would end up with the same expression for the church number 2 again.
SK Combinator Calculus
The SKI combinator calculus can still be reduced further. We can
remove the I combinator by noting that I = SKK
. We can substitute
all I
's with SKK
.
Iota Combinator
The SK combinator calculus is still not minimal. Defining:
ι = λf.((f S) K)
We have:
I = ιι
K = ι(ιI) = ι(ι(ιι))
S = ι(K) = ι(ι(ι(ιι)))