summaryrefslogtreecommitdiffhomepage
path: root/lambda-calculus.html.markdown
blob: 6103c015cb2a17e59388ad958ae78c388f2d1546 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
---
category: Algorithms & Data Structures
name: Lambda Calculus
contributors:
    - ["Max Sun", "http://github.com/maxsun"]
---

# Lambda Calculus

Lambda calculus (λ-calculus), originally created by 
[Alonzo Church](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Lambda_calculus#Beta_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](https://en.wikipedia.org/wiki/Currying).

- `(λx.λy.λz.xyz)` is equivalent to `f(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](https://en.wikipedia.org/wiki/Church_encoding).

For any number n: <code>n = λf.f<sup>n</sup></code> 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)n`

**Challenge:** try defining your own multiplication function!

## For more advanced reading:

1. [A Tutorial Introduction to the Lambda Calculus](http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf)
2. [Cornell CS 312 Recitation 26: The Lambda Calculus](http://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html)
3. [Wikipedia - Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus)