-
Notifications
You must be signed in to change notification settings - Fork 3
/
lambda.html
765 lines (675 loc) · 27.3 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
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
<html>
<head>
<title>Lambda tutorial</title>
<script language=JavaScript src="lambda.js"></script>
</head>
<body style="font-family:verdana">
<b>2021</b>: these are some casual notes I wrote two decades ago. I'm offering them here in case the simple exercises have some residual value. -- Chris Barker
<br>
<br>
<h1>Lambda tutorial</h1>
<p>These web pages provide a practical introduction to lambda
reduction, with a few pointers to more esoteric issues. I'm a
linguist, and I have linguists in mind for my audience, so linguistic
issues will be emphasized (e.g., a discussion of the interaction of
lambda with other binding operators such as ∃ "exists" and
∀ "forall").<p>
<p><b>Browser issues</b>: If your browser can handle JavaScript
1.2, and if you have JavaScript turned on, you will be able to
evaluate examples by clicking on a button, and to make up your own
examples to try; otherwise, the examples will just sit there. For
instance, try clicking on the "Reduce" button: <center><form> <input
type=text name=input size=50 value= "((lambda x (it x)) works)">
<input type=button value="Reduce" onClick="mytry(this.form)"> <input
type=Label name=result size=50> </form> </center> You should see the
string "(it works)" appear in the second window. This is a live
program written in JavaScript---you can type any expression into the
input box and try reducing it (you need to spell out "lambda" in the
input, the program will convert it to "λ" in the
output).
<p><b>Goal</b>: Church's λ-calculus provides a convenient way
of representing meanings, whether meanings of programs or of
expressions in English or some other natural language. As a result,
it is ubiquitous in computer science, logic, and formal approaches to
the semantics of natural language. The λ-calculus consists of
two things: a formal language and an associated notion of REDUCTION
(roughly equivalent to "computation"). In the context of the lambda
calculus, reduction is specifically called λ-reduction. What
these pages will attempt to do is teach you how to perform
λ-reduction accurately and confidently.</p>
<p><b>Other sources</b>:
I recommend
Hankin's
<i>Lambda Calculi : A Guide for Computer Scientists</i> (Oxford)
for a readable survey, and
Barendregt's <i>The Lambda Calculus</i> (Elsevier)
for a more complete reference work.
Barendregt and Barendsen's
shorter
introduction to the lambda calculus is also excellent.
Selinger has an excellent set of lecture notes covering many logical
and computational aspects of the lambda calculus.
For a more linguistic perspective, chapter 2 of Carpenter's
<i>Type-Logical Semantics</i> (MIT Press) presents a λ-calculus
within a framework for describing natural language.
</p>
<p><b>Acknowledgements</b>: Saber Ben Salem
made a number of helpful suggestions.</p>
<h2>Contents of this document:</h2>
<ul><a href="#binding">Binding: free versus bound</a></ul>
<ul><a href="#lambdareduction">λ-reduction</a></ul>
<ul><a href="#betareduction">β-reduction (the heavy lifting)</a></ul>
<ul><a href="#alphareduction">α-reduction (alphabetic variants)</a></ul>
<ul><a href="#etareduction">η-reduction</a></ul>
<ul><a href="#examples">Examples and practice</a></ul>
<ul><a href="#order">Order of combination versus order of reduction; convergence</a></ul>
<ul><a href="#conventions">Various alternative notational conventions</a></ul>
</pre>
<a name="binding">
<h2>Binding: free versus bound</h2>
<p>λ is a binding operator, just like backwards E ("∃")
or upside down A ("∀"). Consequently, it always binds
something (a variable), taking scope over some expression that
(usually) contains occurrences of the bound variable. More
practically, λ always occurs in the following configuration:
<center> (λ var body) </center> <br> Here, "var" is the
variable bound by the lambda operator, and "body" is the constituent
that the lambda operator has scope over. </p>
<p>For instance:
<center> (λ x (* (+ 3 x) (- x 4))) </center> <br> Here "x" is
the variable (the one immediately after the binding operator), and the
body is "(* (+ 3 x) (- x 4))". The body contains two occurrences of
"x", and both are <b>bound</b> by the λ operator; any variable
token that is not bound is <b>free</b>.
<center>
(λ x (* (+ y x) (- x z)))
</center>
<br>
In this form, the tokens of "y" and of "z" are both free.</p>
<p>Freedom is always relative to a particular expression. If the
preceding expression is embedded within a larger one, the free
variables can come to be bound:
<center>
(∃ y (λ x (* (+ y x) (- x z))))
</center>
<br>
In this case, the "y" has been bound, and only the "z" remains free.
</p>
<hr>
<a name=lambdareduction>
<h2>λ-reduction</h2>
<p>
The key notion of the λ-calculus is that it is possible to
arrive at a logically equivalent expression by means of a process
called λ-reduction. In the usual case, λ-reduction is
actually a combination of three distinct reduction operations, each of
which is discussed below. The key operation, the one that does the
heavy lifting, is called β-reduction, and that is operation we
will discuss first.
</p>
<p>By the way, some people say "λ-conversion" instead of
λ-reduction; others reserve "λ-conversion" to refer
specifically to a single step in a series of reductions. This
tutorial is trying not to be overly pedantic, so for present purposes
I don't care.</p>
<hr>
<a name=betareduction>
<h2>β-reduction (the heavy lifting)</h2>
<p> Nothing happens until a λ-binding form occurs in
construction with an argument, thus: <center> ((λ var body)
argument) </center> <br> Once a λ-based binding form occurs
with an argument like this, it is possible to reduce the expression to
a simpler form by means of β-reduction (sometimes with the help
of α-reduction and η-reduction).</p>
<p>The main idea of β-reduction is to replace every
free occurrence of the variable "var" in "body" with
"argument".
For instance, in the form below, both occurrences of "var" in the body
are free.
<center>
<form>
<input type=text name=input size=50 value=
"((lambda var ((fn1 var) & (fn2 var))) argument)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
</center>
<br>
Consequently, after β-reduction, both occurrences get replaced
with "argument", and the result is significantly simpler than the
original expression. </p>
<hr>
<a name=alphareduction>
<h2>α-reduction (alphabetic variants)</h2>
<p>
Unfortunately, applying β-reduction indiscriminately
can cause trouble when the body contains binding operators.
Consider:
<center>
<form>
<input type=text name=input size=30 value="((lambda x (lambda y1 (x y1))) z)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=30 value=" ">
</form>
</center>
<br>
Following the rules of β-reduction, we replace
"x" with "z" for a result of "(λ y1 (z y1))", and this result is
correct.
Note that
in the result the λ-operator binds exactly one
variable in the body, and the other variable remains free.</p>
<p>But consider what happens in this closely parallel but slightly
different situation:
<center>
<table noborder>
<tr>
<td>((λ x (λ y (x y))) y)</td>
<td>
β-reduction: substitute "y" in for "x" in the body "(λ y
(x y))" ==>
</td>
</tr>
<tr>
<td>(λ y (y y))</td>
</tr>
<tr><td><b>Wrong result!</b></td>
</tr>
</table>
</center>
<br>
The only difference here from the first example is that the argument
is "y" and not "z". But now, blindly following the rules of
β-reduction would produce the result "(λ y (y y))", in
which the λ-operator binds two variables, not just one, which
is not correct. The argument variable "y" is said to have been
`captured' by the inner λ-operator; another commonly-used
expression for this kind of situation is `variable collision'. </p>
<p>The solution is to make use of alphabetic variants. Roughly, two
expressions are "alphabetic variants" if they are identical except
perhaps for the choice of variable symbols.
For instance, the following expressions
are alphabetic variants of one another:
<center>
(λ x (λ y (x (+ y x))))
<br>
(λ z (λ y (z (+ y z))))
</center>
<br>
To create an alphabetic variant for an expression of the form
"(λ var body)", simply replace each free occurrence of "var" in
the expression with "new", where "new" is a variable symbol not
occurring anywhere in "body". (Since expressions have finite length,
as long as there is an infinite supply of variable symbols, it will
always be possible to find a suitable variable to serve the role of
"new".) This transformation is called α-reduction.
The crucial property of the reduced form is that each λ
operator binds the same number of variables in the same positions
within its body.</p>
<p>Some examples of alphabetic variants:
<center>
<table noborder>
<tr>
<td>1.</td>
<td>((λ x x) x)</td>
<td>α-reduction on "(λ x x)", substituting "y1" for "x" ==></td>
</tr>
<tr>
<td></td>
<td>((λ y1 y1) x)</td>
</tr>
<td>2.</td>
<td>((λ x x)(λ x (x x)))</td>
<td>α-reduction on "(λ x x)", substituting "y1" for "x" ==></td>
</tr>
<tr>
<td></td>
<td>((λ y1 y1)(λ x (x x)))</td>
</tr>
<tr>
<td>3.</td>
<td>(λ x (λ x (x x)))</td>
<td>α-reduction on "(λ x (λ x (x x)))",
substituting "y1" for "x" ==></td>
</tr>
<tr>
<td></td>
<td>(λ y1 (λ x (x x)))</td>
</tr>
</table>
</center>
<p>The third example may look surprising; the key fact is that
α-reduction specifically targets only <i>free</i> occurrences of
the variable in question (free relative to the λ body). Since
the second λ binds the last two occurrences of "x", performing
α-reduction on the larger form won't touch them.</p>
<p> <b>Now, back to the original problem.</b> The way to deal with
"((λ x (λ y (x y))) y)", then, is to first take an
alphabetic variant. Because alphabetic variants are guaranteed to be
logically equivalent, we can substitute variants in place of the
original sub expressions. If we do this cleverly, the "y"
and the "z"'s don't interact in the pernicious manner shown above.
<center>
<table noborder>
<tr>
<td>1.</td>
<td>((λ x (λ y (x y))) y)</td>
<td>α-reduction on "(λ y (x y))", substituting "y1" for "y" ==></td>
</tr>
<tr>
<td>2.</td>
<td>((λ x (λ y1 (x y1))) y)</td>
<td>β-reduction, substituting "y" for "x" ==></td>
</tr>
<tr>
<td>3.</td>
<td>(λ y1 (y y1))</td>
</tr>
</table>
</center>
The result contains exactly one free variable, which is correct.
(Note that "y" and "y1" count as entirely distinct variables, as
different as "y" is from "x".) </p>
<p>
Equivalent steps are taken automatically by the λ-reduction program:
<center>
<form>
<input type=text name=input size=30 value="((lambda x (lambda y (x y))) y)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=30 value=" ">
</form>
</center>
<br>
</p>
<p>It usually takes some practice to know when it is necessary to use
an alphabetic variant. The safest strategy is to automatically apply
α-reduction to every binding operator before each application of
β-reduction. See if you can work out the right result for this
form before clicking on the "Reduce" button; you will need three
applications of β-reduction and at least one application of
α-reduction:
<center>
<form>
<input type=text name=input size=40 value="((lambda x (x x))(lambda x (lambda y (x y))))">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=30 value=" ">
</form>
</center>
<br>
The program uses the safe strategy, blindly performing α-reduction
whenever a binding operator occurs inside a body. Experienced human
λ-reducers, however, typically apply α-reduction only
when it is absolutely necessary to avoid variable collision (it was
necessary at least once in the example immediately above). For
beginners, though, the best rule is: when in doubt, perform
α-reduction!</p>
<p><b>(Warning:)</b> I have modified the characterization of
β-reduction and of α-reduction somewhat in the interests of
simplicity. The simplified versions are perfectly sound, and provide
the full expressive power of the λ-calculus. If you're
interested in the traditional elaboration, consult either the Hankin
book or Berendregt book mentioned above.</p>
<hr>
<a name=etareduction>
<h2>η-reduction)</h2>
<p>η-reduction says that an expression of the form "(λ x (P
x))" is guaranteed to be equivalent to "P" alone, where "P" is any
expression (in which x does not occur free).
This equivalence is obvious enough, but α-reduction
and β-reduction alone do not guarantee it. However, few
practical applications of λ-reduction bother to implement
η-reduction. In particular, the programs given on this page do not:
<center>
<form>
<input type=text name=input size=30 value="(lambda x (P x))">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=30 value=" ">
</form>
</center>
<br>
Clicking on "Reduce" results in no change.</p>
<hr>
<a name="examples">
<h2>Examples and practice</h2>
<p>
Some examples (try to guess the result before clicking):
<br>
<form>
<input type=text name=input size=30 value="((lambda x x) 2)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=30 value=" ">
</form>
<br>
<form>
<input type=text name=input size=30 value="((lambda x (x x)) 2)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=30 value=" ">
</form>
<br>
<form>
<input type=text name=input size=30 value="((lambda x (x y z)) z)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=30 value=" ">
</form>
<br>
<form>
<input type=text name=input size=30 value="((lambda x (w y)) z)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=text name=result size=30 value=" ">
</form>
<br>
<br>
Looking at these reductions, it is easy to see how λ-reduction
gets computational work done, since it is capable of copying,
inserting, or discarding the information contained in the argument.
</p>
<p>Some more linguistically-related practice. Once again, try writing
down the anticipated result before clicking "Reduce":
<br>
<form>
<input type=text name=input size=40 value="((lambda x (P x)) j)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="((lambda x (P y)) j)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(((lambda x (lambda y (P y))) j) m)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(((lambda x (lambda y (P x))) j) m)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="((lambda P (P j)) (lambda x (Q x)))">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(((lambda x (lambda y (K x y))) j) m)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(((lambda y (lambda x (K x y))) j) m)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(P j)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="((lambda x (P x)) j)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="((lambda Q (Q j)) P)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(((lambda Q (lambda x (Q x))) P) j)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(((lambda x (lambda Q (Q x))) j) P)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="(((lambda Q (lambda x (Q x))) (lambda y (P y))) j)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=65 value="((((lambda GQ (lambda L (lambda x ((GQ L) x)))) (lambda Q (lambda x (Q x)))) P) j)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="((lambda x (A x (K x j))) m)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<form>
<input type=text name=input size=40 value="((lambda x ((lambda x (K x x)) j)) m)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
</p>
<p>
Now for something a little more difficult. Find an expression that
you can use to replace "X" so that the result is "(John sleeps)" (you
will have to type it into the input window in place of "X" to try it):
<form>
<input type=text name=input size=40 value="(X sleeps)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
<br>
<br>
Obviously, one solution is "John". But another is
"(λ P (John P))"--try it! (That is, delete "X"
and type in "(lambda P (John P))", then click "Reduce".)</p>
<p>Here's a harder problem: If the input is "((D man) sleep)", and the
result is "(∃ x ((man x) & (sleep x)))", what is "D"? (Hint:
the answer is an approximation of the meaning of the determiner
"some", as in "Some man sleeps". The symbol "∃" is supposed to
show up as a backwards E, and is usually read "there exists"; in any
case, the program expects you to type it in to the window as the
symbol "exists".)
<form>
<input type=text name=input size=40 value="((D man) sleeps)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
</p>
<br>
<a name=order>
<h2>Order of combination versus order of reduction; convergence</h2>
<p>It takes some practice to match up λ's with the correct argument.
Does the following form evaluate to "(2 3)" or "(3 2)"?
<center>
<form>
<input type=text name=input size=40 value="(((lambda x (lambda y (x y))) 2) 3)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
</center>
<br>
The rule of thumb is that the outermost λ goes with the
innermost argument. However, it is necessary to keep careful track of
the nesting of parentheses. The following form looks very much like
the last one, but the order of arguments is reversed:
<center>
<form>
<input type=text name=input size=40 value="((lambda x ((lambda y (x y)) 2)) 3)">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
</center>
<br>
Note that order of arguments depends entirely on the structure of the
parentheses, and not on the order in which the β-reductions are
carried out.</p>
<p>In fact, when a form contains more than one λ that can be
reduced, it does not matter which one is reduced first, the result
will be the same. (This is known as the Church-Rosser property, or,
informally, as the diamond property---see Hankin or Berendregt for
lengthy discussion.) For instance, for the last example, we could
either apply β-reduction to the innermost λ first, thus:
<center>
<table noborder>
<tr>
<td>((λ x ((λ y (x y)) 2)) 3)</td>
<td>β-reduction on "((λ y (x y)) 2)", substituting "2" for "y" in the body "(x y)" ==></td>
</tr>
<tr>
<td>((λ x (x 2)) 3)</td>
<td>β-reduction, substituting "3" for "x" in the body "(x 2)" ==></td>
</tr>
<tr>
<td>(3 2)</td>
</tr>
</table>
</center>
Or we could begin with the outermost λ:
<center>
<table noborder>
<tr>
<td>((λ x ((λ y (x y)) 2)) 3)</td>
<td>β-reduction on "((λ x ((λ y (x y)) 2)) 3)", substituting "3" for "x" in the body "((λ y (x y)) 2)" ==></td>
</tr>
<tr>
<td>((λ y (3 y)) 2)</td>
<td>β-reduction, substituting "2" for "y" in the body "(3 y)" ==></td>
</tr>
<tr>
<td>(3 2)</td>
</tr>
</table>
</center>
In other words, no matter what order the λ's are reduced, we
always converge on the same simplified result.</p>
<p>
That is, when the
reduction converges at all---some expressions can't be simplified
(e.g., "((λ x (x x))(λ x (x x)))", which reduces to
itself, or more pathological examples, such as this (DON'T CLICK ON
"REDUCE"!):
<center>
<form>
<input type=text name=input size=50 value="((lambda x (x x))(lambda x (lambda y (x x))))">
<input type=button value="Reduce" onClick="mytry(this.form)">
<input type=Label name=result size=40 value=" ">
</form>
</center>
<br>
For this expression, each so-called reducution makes the expression
longer, ad infinitum (try it, on paper!). If you try to evaluate that
expression in the browser program, you may crash your browser;
My browser enters an infinite loop, and I have to kill the browser.
<hr>
<a name=conventions>
<h2>Various alternative notational conventions</h2>
<p>I have been writing predicates and their arguments inside
parentheses, thus: "(pred arg)". Often in logic and linguistics, such
an expression would be written "pred(arg)", for instance, "f(x)" (as
in "f(x) = y"). I have chosen the first, more LISP-like notation
because it significantly simplifies the design of the program for
automating λ-reduction.</p>
<p>Often, instead of "(λ x (λ y (x y)))", people write
"λ x y . x y". For some reason, these people hate to draw
parentheses, and they hate to draw λ's. The dot shows where
the list of bound variables stops and the (innermost) body begins.
Because the scope of the λ operator(s) is not explicitly
marked, sloppy use of this abbreviatory convention often leads to
expressions that are ambiguous; this in turn often causes beginners
tremendous frustration.</p>
<hr>
<!--
<a name=semantics>
<h2>The semantics of the λ-operator</h2>
<p>The complexities of λ-reduction arise from trying to provide
a set of syntactic transformations that are guaranteed to preserve
meaning. That is, two expressions that are related by some
combination of α, β, and η reduction are guaranteed to
mean the same thing. In fact, although λ-reduction is sound,
it does not capture the full meaning of the λ-operator.</p>
<p> A simpler, more direct, and more complete way to understand
λ is to consider its meaning.</p>
<p>The following rule completely characterizes the meaning of the
λ-operator. First, let "[*]^g" mean "the denotation of `*'
with respect to the assignment function g", where an assignment
function is a function mapping variable symbols onto values, and
g[u/v] is that assignment function exactly like g except that it maps
the variable v onto the value u.
<center>
<img src="lambda.jpg" alt="The semantics of lambda.">
</center>
<br>
The paraphrase, then, is as follows: the meaning of a λ-form
that binds the variable <i>v</i> when applied to an argument <i>a</i>
is the meaning of the body <i>b</i> evaluated with respect to an
assignment function that sets the value of <i>v</i> equal to the
denotation of <i>a</i>.
<hr>
<a name=scheme>
<h2>Scheme reference code</h2>
<p>You're welcome to view the JavaScript program that runs on this
page (you can find it <a href="lambda.js">here</a>), which constitutes
a kind of definition of λ-reduction. It may be helpful,
however, to have a more compact <a href="lambda.scm">reference
implementation</a>, written in <a
href="http://www.swiss.ai.mit.edu/~jaffer/r5rs_toc.html">R5RS
Scheme</a>:
<center>
<pre>
(define (reduce f) ; 1
((lambda (value) (if (equal? value f) f (reduce value))) ; 2
(let r ((f f) (g ())) ; 3
(cond ((not (pair? f)) ; 4
(if (null? g) f (if (eq? f (car g)) (cadr g) (r f (caddr g))))) ; 5
((and (pair? (car f)) (= 2 (length f)) (eq? 'lambda (caar f))) ; 6
(r (caddar f) (list (cadar f) (r (cadr f) g) g))) ; 7
((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f))) ; 8
(cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g)))) ; 9
(else (map (lambda (x) (r x g)) f)))))) ;10
</pre>
</center>
If you have a Scheme interpreter, you can call the function like this:
<pre>
(reduce '(((lambda x (lambda y (x y))) 2) 3))
;Value: (2 3)
(reduce '((lambda x (lambda y (x y))) 2))
;Value: (lambda #[promise 2] (2 #[promise 2]))
</pre>
Comments: f is the form to be evaluated, and g is the local assignment
function; g has the structure (variable value g2), where g2 contains
the rest of the assignments. The named let function r executes one
pass through a form. The arguments to r are a form f, and an
assignment function g. Line 2: continue to process the form until
there are no more conversions left. Line 4 (substitution): If f is
atomic [or if it is a promise], check to see if matches any variable
in g and if so replace it with the new value. Line 6 (beta
reduction): if f has the form ((lambda variable body) argument), it is
a lambda form being applied to an argument, so perform lambda
conversion. Remember to evaluate the argument too! Line 8 (alpha
reduction): if f has the form (lambda variable body), replace the
variable and its free occurences in the body with a unique object to
prevent accidental variable collision. [In this implementation a
unique object is constructed by building a promise. Note that the
identity of the original variable can be recovered if you ever care by
forcing the promise.] Line 10: recurse down the subparts of f.
<p>
<a href="ski.html">Combinatory Logic</a></ul>
</p>
</body>
</html>
-->