-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlambda.html
322 lines (317 loc) · 13.9 KB
/
lambda.html
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
<!DOCTYPE html>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, user-scalable=no" />
<meta name="viewport" content="initial-scale=1, maximum-scale=1" />
<meta name="mobile-web-app-capable" content="yes">
<meta name="apple-mobile-web-app-capable" content="yes" />
<link rel="shortcut icon"
href="data:image/svg+xml,%3Csvg xmlns='http://www.w3.org/2000/svg'
width='80' height='80'%3E
%3Ctext x='10' y='64' font-family='Arial' font-size='64'
stroke-width='12' stroke='%23eee'%3E&%23955;%3C/text%3E
%3Ctext x='10' y='64' font-family='Arial' font-size='64'
stroke-width='8' stroke='%23222'%3E&%23955;%3C/text%3E
%3C/svg%3E" />
<title>Lambda Calculus</title>
<h1>Lambda Calculus</h1>
<div class="lambda" data-library="true" data-sk="true"></div>
<p>
Lambda Calculus is an abstract model of computation. Other models,
such as the Turing Machine, are equivalent (this is part of the
<a href="https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis"
>Church-Turing Thesis</a>). This program implements lambda
expressions, normal order reduction and a library of useful
functions. The lambda calculus itself contains only variables,
grouping, abstractions and applications. Notice that this does
not include boolean logic, data structures, recursion or numbers.
And yet the library included here contains all of these things
because lambda calculus provides a universal foundation on which
any computation can be built.
</p>
<h2>Contents</h2>
<ol><li>
<a href="#definition">Definition</a>
</li><li>
<a href="#computation">Computation</a>
</li><li>
<a href="#instructions">Instructions</a>
</li><li>
<a href="#arithmetic">Arithmetic</a>
</li><li>
<a href="#recusion">Recusion</a>
</li></ol>
<h2><a name="definition">Definition</a></h2>
<p>
A lambda calculus expression is composed from four patterns:
</p><ul><li>
Variable: any identifier other than <code>lambda</code> which
does not contain <code>λ</code>, <code>.</code>, <code>(</code>
or <code>)</code>
</li><li>
Grouping: <code>(</code> [expression] <code>)</code>
</li><li>
Abstraction: <code>lambda</code>
[variable]<code>.</code>[expression]
</li><li>
Application: [expression1] [expression2]
</li></ul><p>
Any combination of these components is a valid lambda calculus
expression. Note that while all lambda calculus abstractions
accept exactly one argument, in practice we allow more than one by
providing additional variables between the lambda and the dot.
For example, instead of writing
<code>λa.λb.a</code> we will usually write
<code>λa b.a</code> instead. These have the same meaning. Here
are some examples:
</p><ul><li><code>
λa.a
</code></li><li><code>
λn f a.n (λg h.h (g f)) (λu.a) (λu.u)
</code></li><li><code>FIX (λf n.(EQUAL? n ZERO) ONE
(MULTIPLY n (f (PREDECESSOR n))))
</code></li></li></ul><p>
Variables within a lambda calculus expression are either bound or
free. Any variable following a lambda is bound in the expression
following the next dot. A variable not bound in this way is free.
The first two examples above have no free variables. The third
has many free variables, including <code>FIX</code>,
<code>EQUAL?</code> and <code>MULTIPLY</code>.
</p><p>
Any lambda expression with no free variables is called a
combinator. Many combinators are useful enough that we give them
names. For example <code>λa.a</code> is called the identity
combinator. This is the simplest possible combinator. In 1985
Raymond Smullyan wrote a book entitled
<a href="https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird">To
Mock a Mockingbird</a> which is the source of many of these
names. Here are some examples:
</p><ul><li>
Identity: <code>λa.a</code>
</li><li>
Mockingbird: <code>λm.m m</code>
</li><li>
Kestrel: <code>λa b.a</code>
</li><li>
Kite: <code>λa b.b</code>
</li><li>
Cardinal: <code>λa b c.a c b</code>
</li><li>
Bluebird: <code>λa b c.a (b c)</code>
</li><li>
Thrush: <code>λa b.b a</code>
</li><li>
Virio: <code>λa b f.f a b</code>
</li><li>
Starling: <code>λa b c.a c (b c)</code>
</li></ul>
<h2><a name="computation">Computation</a></h2>
<p>
Computation in lambda calculus is performed by reductions. A
reduction applies an expression to an abstraction by replacing
all instances of a variable with that expression inside the body
of the abstraction. For example, let's reduce the following
lambda expression:
</p><ul><li>
<code>(λa.a) VALUE</code>
</li><li>
<code>a [a := VALUE]</code>
</li><li>
<code>VALUE</code>
</li></ul><p>
The first step above is our original expression. In the second
step we replace an abstraction with its body and note the need to
replace all instances of its variable with some value. In the
third step we perform that replacement and the reduction is
complete. That's simple in this case, but there may be no
instance to replace or there may be more than one. Here is
another example where the substition must be done twice:
</p><ul><li>
<code>(λf a.f (f a)) λb.b</code>
</li><li>
<code>λa.f (f a) [f := (λb.b)]</code>
</li><li>
<code>λa.(λb.b) ((λb.b) a)</code>
</li></ul><p>
Once a reduction is complete it may be possible to further reduce
the expression as it is in the example above. In the following
example, we reduce three times:
</p><ul><li>
<code>(λn.n ((λa b.a) (λa b.b)) (λa b.a)) (λa b.b)</code>
</li><li>
<code>n ((λa b.a) (λa b.b)) (λa b.a) [n := (λa b.b)]</code>
</li><li>
<code>(λa b.b) ((λa b.a) (λa b.b)) (λa b.a)</code>
</li><li>
<code>(λb.b) [a := ((λa b.a) (λa b.b))] (λa b.a)</code>
</li><li>
<code>(λb.b) (λa b.a)</code>
</li><li>
<code>b [b := (λa b.a)]</code>
</li><li>
<code>λa b.a</code>
</li></ul><p>
At the end of this process no further reductions are possible.
When this happens we say that the expression is in normal form.
If an expression has a normal form there is only one. This is the
<a href="https://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem"
>Church-Rosser Theorem</a>.
</p><p>
Not all expressions have a normal form. What would an expression
without a normal form look like? One example is the mockingbird
combinator applied to itself:
</p><ul><li>
<code>(λm.m m) (λm.m m)</code>
</li><li>
<code>m m [m := (λm.m m)]</code>
</li><li>
<code>(λm.m m) (λm.m m)</code>
</li></ul><p>
Our reduction is complete, but we're back where we started. This
expression can be further reduced but it will never make progress
toward any conclusion. As a consequence it will never reach a
normal form.
</p>
<h2><a name="instructions">Instructions</a></h2>
<p>
As we will see, lambda calculus is not an efficient way to perform
computations. However it's still impressive that such a simple
system is universal. Select a library function from the drop down
box to study it. Can you understand how it works? Or type your
own lambda expressions into the text area. It's okay to type the
word <code>lambda</code> rather than the <code>λ</code> symbol as
long as you put a space between it and the variable name.
</p><p>
Click the <q>Reduce</q> button to perform a single step of
computation. Most computations require a large number of steps,
so you can instead click the <q>Repeat</q> button to continuously
perform reductions. This will terminate when no more reductions
are possible, if that ever happens. You can see what happens to a
program that does not terminate by copying and pasting the
following:
</p><div class="lambda" data-delay="500"
data-expr="(λn.n n) λm.m m">
</div><p>
Click <q>Repeat</q> to watch this reduce indefinitely. Click
<q>Reset</q> to stop the process; it will never stop on its own.
</p>
<h2><a name="arithmetic">Arithmetic</a></h2>
<p>
Let's explore a computation that does terminate. We'll use the
built in library to add two numbers.
</p><div class="lambda" data-library="true" data-expr="+ 3 2">
</div><p>
This is a valid expression, but the symbols have no meaning in
lambda calculus. We'll solve this problem by replacing them with
expressions from a built in library. Click the <q>Library</q>
button to do this.
</p><p>
Our library replaces numbers with
<a href="https://en.wikipedia.org/wiki/Church_encoding">Church
Encoded</a> numerals. A number is represented by a function
that accepts two arguments and applies the first to the second
that number of times. This means <code>TWO</code> has been
replaced by <code>λf a.f (f a)</code> and <code>THREE</code>
has been replaced by <code>λf a.f (f (f a))</code>. Instead of
the addition operator, we have a function that applies the
successor repeatedly using one of the numbers.
</p><p>
Click the <q>Reduce</q> button to perform a single reduction. This
still leaves a complex expression that doesn't directly represent
any number. It will take five more clicks to get to an expression
in normal form. Instead of doing all that clicking, the
<q>Repeat</q> button can be used to complete the process
automatically. A small delay (which can be increased or decrased
using the slider) is introduced between each reduction.
Click the <q>Reset</q> button to restore the original expression
and try this a few different ways.
</p><p>
Even after the expression is reduced to normal form, it may not be
obvious just what we've computed. In this case, we can see that
the result is a function which takes two arguments and applies the
first to the second five times. That's the Church Numeral
representation of five, which is what we should expect from adding
three to two. Use the <q>Discover</q>
button to replace the result with a value from the library, if
possible. In this example you should get the number five.
</p><p>
There's one more shortcut to try. The <q>Go</q> button does
evertyhing we've described here in one step: first it replaces
symbols with values from the library, then it reduces until a
normal form is reached and finally it looks for a library value
to replace it with. Try clicking <q>Reset</q> followed by <q>Go</q>
above. You can also try replacing the numbers to see that you
still get a correct answer.
</p><p>
Consider this:
</p><div class="lambda" data-library="true"
data-expr="EQUAL? 5 λf a.f (f (f (f (f a))))">
</div><p>
Click the <q>Go</q> button. After 134 steps you should get
<code>TRUE</code>. That makes sense. We can check that this
result is meaningful by trying an incorrect equation:
</p><div class="lambda" data-library="true"
data-expr="EQUAL? 7 λf a.f (f (f (f (f a))))">
</div><p>
Now after 146 steps this reduces to <code>0</code>. What
happened? As it turns out, in lambda calculus we represent
zero and false using the same expression. This means the
program needs to pick one to recognize. Try putting
<code>FALSE</code> in the text area and clicking <q>Library</q>
to see that these are the same thing.
</p><p>
We can build more complicated expressions. For example:
</p><div class="lambda" data-library="true"
data-expr="EQUAL? 5 (+ 2 3)">
</div><p>
After 146 steps this reduces to <code>TRUE</code>. Replace five
with some other number to get <code>0</code> (which is the same
as <code>FALSE</code>. Try other numbers in expressions like this
to confirm that the correct results are reached.
</p><p>
<code>GREATER?</code>, <code>LESS?</code>, <code>SUBTRACT</code>,
<code>MULTIPLY</code>, <code>DIVIDE</code> and <code>POWER</code>
are also available. Try creating simple arithmetic expressions
like this one:
</p><div class="lambda" data-library="true"
data-expr="GREATER? (- 5 2) 2">
</div><p>
This should reduce to <code>TRUE</code> in 63 steps.
</p>
<h2><a name="recusion">Recursion</a></h2>
<p>
Sometimes computations are more convenient to express in terms
of recursion. This means a function calls itself on a reduced
form of its input in order to break down a problem. Of course,
lambda calculas has no support for recursion. Even so, our
library contains a recursive function called <code>FACTORIAL</code>.
Here is an example of this function you can try running yourself:
</p><div class="lambda" data-library="true"
data-expr="FACTORIAL 3">
</div><p>
After 646 steps this arrives at the Church Numeral representation
of <code>6</code> (because three factorial is three times two
times one).
</p><p>
Computing <code>FACTORIAL 4</code> takes 3,873 steps and
results in Church Numeral <code>24</code>. Computing
<code>FACTORIAL 5</code> takes 26,899 steps and a long time but it
reduces to a function of two variables that applies the first to
the second one hundred twenty times. 5! = 5 × 4 × 3
× 2 × 1 = 120. So how does this work? It makes use
of the <code>FIX</code> combinator -- also known as the
fixed point or
<a href="https://en.wikipedia.org/wiki/Fixed-point_combinator"
>Y combinator</a>. The Y combinator followed by a function
reduces to that function followed by an application of the Y
combinator to that function. This means it will call the function
with itself as an argument indefinitely. As long as the function
this is applied to has some terminating condition this won't
reduce forever. This makes it possible for the function to call
itself without any support for recursion in the programming
environment.
</p>
<script type="module">//<![CDATA[
import Lambda from "./ripple/lambda.mjs";
document.querySelectorAll(".lambda").forEach(
element => Lambda.createInterface(element));
//]]></script>