-
Notifications
You must be signed in to change notification settings - Fork 22
/
Copy pathlambda-calculus.html
482 lines (458 loc) · 19.5 KB
/
lambda-calculus.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
<html>
<meta content="width=device-width, initial-scale=1.0" name="viewport">
<head>
<title>
leontrolski - Lambda calculus succinctly
</title>
<style>
body {margin: 5% auto; background: #fff7f7; color: #444444; font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, Helvetica, Arial, sans-serif; font-size: 16px; line-height: 1.8; max-width: 63%;}
@media screen and (max-width: 800px) {body {font-size: 14px; line-height: 1.4; max-width: 90%;}}
pre {width: 100%; border-top: 3px solid gray; border-bottom: 3px solid gray;}
a {border-bottom: 1px solid #444444; color: #444444; text-decoration: none; text-shadow: 0 1px 0 #ffffff; }
a:hover {border-bottom: 0;}
.inline {background: #b3b2b226; padding-left: 0.3em; padding-right: 0.3em; white-space: nowrap;}
blockquote {font-style: italic;color:black;background-color:#f2f2f2;padding:2em;}
details {border-bottom:solid 5px gray;}
</style>
<link href="https://unpkg.com/[email protected]/themes/prism-vs.css" rel="stylesheet">
<script src="https://cdnjs.cloudflare.com/ajax/libs/prism/1.20.0/components/prism-core.min.js">
</script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/prism/1.20.0/plugins/autoloader/prism-autoloader.min.js">
</script>
</head>
<body>
<a href="index.html">
<img src="pic.png" style="height:2em">
⇦
</a>
<p><i>2022-03-09</i></p>
<h1>
Lambda calculus succinctly in modern JavaScript
</h1>
<script>
const toInt = a => a(n => n + 1)(0)
const toBool = a => a(true)(false)
const True = a => b => a
const False = a => b => b
const not = a => a(False)(True)
const and = a => b => a(b)(a)
const or = a => b => a(a)(b)
// Note someBool ? a : b
// is equivalent to someBool(_ => a)(_ => b)(_)
const _0 = f => a => a
const _1 = f => a => f(a)
const _2 = f => a => f(f(a))
const _3 = f => a => f(f(f(a)))
const inc = n => f => a => f(n(f)(a))
const plus = n => m => n(inc)(m)
const mult = n => m => a => n(m(a))
const isEven = n => n(not)(True)
const isZero = n => n(True(False))(True)
const pair = a => b => f => f(a)(b)
const first = p => p(True)
const second = p => p(False)
const incSecond = p => pair(second(p))(inc(second(p)))
const dec = n => first(n(incSecond)(pair(_0)(_0)))
const minus = n => m => m(dec)(n)
const gte = n => m => isZero(n(dec)(m))
const lt = n => m => not(gte(n)(m))
const eq = n => m => and(gte(n)(m))(gte(m)(n))
const incAndCall = f => p => pair(
inc(first(p))
)(
f(first(p))(second(p))
)
const loop = n => m => f => a => second(
(minus(m)(n))(incAndCall(f))(pair(n)(a))
)
const _ = True
const sum = n => isZero(n)(_ => _0)(_ => plus(n)(sum(dec(n))))(_)
// Y-combinator
const Y = f => (x => f(_ => x(x)))(x => f(_ => x(x)))
// reduces to Y = f => f(_ => Y(f))
const sum2 = Y(g => n => isZero(n)
(_ => _0)
(_ => plus(n)(g(_)(dec(n))))
(_))
// Z-combinator
const Z = f => (x => f(v => x(x)(v)))(x => f(v => x(x)(v)))
// reduces to Z = f => v => f(Z(f))(v)
const sum3 = Z(g => n => isZero(n)
(_ => _0)
(_ => plus(n)(g(dec(n))))
(_))
</script>
<p>
The aim of this blog post is to give a flavour of how one might build a useful programming language (or for that matter mathematical system) from a really really small foundation. In our JavaScript notation, the building blocks are just:
</p>
<pre class="language-javascript"><code>f = x => M // function definition
f(y) // function application</code>
</pre>
<p>
That's it - no numbers, no lists, no loops, no boolean switches, no strings, no objects.
</p>
<p>
Instead, we'll give a flavour of how you might conjure up these things seemingly out of the ether.
</p>
<br>
<hr>
<br>
<h2>
Doing Lambda calculus with JavaScript notation
</h2>
<p>
You can Google 'Lambda calculus' for a deeper description, but in a nutshell it's a very small, Turing-complete, formal system for expressing computation as symbol manipulation. We're going to rewrite some of the fundamental ideas in familiar JavaScript notation which allows us to easily evaluate them. You can try this out in your browser's console - all the assignments below are in global scope.
</p>
<p>
In Lambda calculus notation, you might write something kinda like:
</p>
<pre class="language-javascript"><code>(λf.f 4) (λx.x²)</code>
</pre>
<p>
Let's cut straight to the Javascript version:
</p>
<pre class="language-javascript"><code>(f => f(4))(x => Math.pow(x, 2))</code>
</pre>
<p>
Each anonymous function λ takes one argument. When you call a function, you simply replace the argument each time it occurs in the function's body with the value the function was called with.
</p>
<p>
It's worth noting that this process (known as β-reduction) is just a dumb mechanical one of symbol replacement - nothing else weird is happening. This is important - <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Natural_deduction_and_lambda_calculus">
programs are proofs
</a>
and by repeatedly applying β-reduction, we can verify them.
</p>
<p>
In the case of the example above:
</p>
<pre class="language-javascript"><code>(λf.f 4) (λx.x²)</code>
</pre>
<p>
We can β-reduce the <code class="inline">f</code>
away to make:
</p>
<pre class="language-javascript"><code>((λx.x²) 4)</code>
</pre>
<p>
Then β-reduce the <code class="inline">x</code>
away to make:
</p>
<pre class="language-javascript"><code>(4²)</code>
</pre>
<p>
Which we know is 16.
</p>
<p>
Handily, with JavaScript notation, the interpreter will do the reduction automatically! So:
</p>
<pre class="language-javascript"><code>(f => f(4))(x => Math.pow(x, 2))</code>
</pre>
<p>
Does the two reductions above and also evaluates to 16.
</p>
<p>
Because of this handy time saving property of JavaScript, we'll continue to use that as our Lambda calculus notation.
</p>
<hr>
<h2>
Integers
</h2>
<p>
In the example above, we had such high level concepts as '4' and 'x²' - these are a bit cheaty, instead, we're going start from nothing except the rules of the calculus.
</p>
<p>
For integers, we're going to use a system called 'Church numerals'. These aren't nouns like 'one' and 'two', but adverbs like 'call <code class="inline">f</code>
with <code class="inline">a</code>
one time' or 'call <code class="inline">f</code>
on <code class="inline">a</code>
two times'. If that's a bit abstract, let's define 4 integers:
</p>
<pre class="language-javascript"><code>const _0 = f => a => a
const _1 = f => a => f(a)
const _2 = f => a => f(f(a))
const _3 = f => a => f(f(f(a)))</code>
</pre>
<details>
<summary>
Here's a helper function so we can print these as good ol' fashioned JavaScript numbers. <br>
<em>
This section is folded as it isn't written in formal Lambda calculus.
</em>
</summary>
<pre class="language-javascript"><code>const toInt = a => a(n => n + 1)(0)</code>
</pre>
</details>
<p>
Now let's add in some functions that operate on integers:
</p>
<pre class="language-javascript"><code>const inc = n => f => a => f(n(f)(a)) // n + 1
const plus = n => m => n(inc)(m) // n + m
const mult = n => m => a => n(m(a)) // n * m</code>
</pre>
<p>
We can test these in our browser's console using the helper from above, try running:
</p>
<pre class="language-javascript"><code>toInt(plus(_1)(_2))</code>
</pre>
<p>
Neat?
</p>
<p>
Let's see how that happened by filling in the variables, then repeatedly applying β-reduction:
</p>
<pre class="language-javascript"><code>plus(_1)(_2) // replace plus, _1, _2
(n => m => n(inc)(m))(f => a => f(a))(f => a => f(f(a))) // β n
(m => (f => a => f(a))(inc)(m))(f => a => f(f(a))) // β m
(f => a => f(a))(inc)(f => a => f(f(a))) // replace inc
(f => a => f(a))(n => f => a => f(n(f)(a)))(f => a => f(f(a))) // β first f
(a => (n => f => a => f(n(f)(a)))(a))(f => a => f(f(a))) // β first a
(n => f => a => f(n(f)(a)))(f => a => f(f(a))) // β n
f => a => f((f => a => f(f(a)))(f)(a)) // β second f
f => a => f((a => f(f(a)))(a)) // β second a
f => a => f(f(f(a)))</code>
</pre>
<p>
Phewph, that was long, but we did end up with <code class="inline">f => a => f(f(f(a)))</code>
, which is the Church numeral for '3', so we've shown definitively 1 + 2 = 3, yay!
</p>
<p>
We can see intuitively how we came up with some of the definitions. Remember earlier, we said the Church numeral 2 is the adverb 'call <code class="inline">f</code>
on <code class="inline">a</code>
two times', the definition for <code class="inline">plus</code>
should make sense with that in mind:
</p>
<pre class="language-javascript"><code>const plus = n => m => n(inc)(m)</code>
</pre>
<p>
Just says 'call <code class="inline">inc</code>
on <code class="inline">m</code>
<code class="inline">n</code>
times'
</p>
<h2>
Booleans
</h2>
<p>
Now we have a representation of integers based just on the calculus, let's define True and False:
</p>
<pre class="language-javascript"><code>const True = a => b => a
const False = a => b => b</code>
</pre>
<p>
These are, like our integers, very abstract. It's important to consider that the choice is somewhat arbitrary - we're just going to do β-reduction on expressions involving these, and if an expression reduces to <code class="inline">a => b => a</code>
then we consider it True.
</p>
<details>
<summary>
Here's a helper function so we can print these as good ol' fashioned JavaScript booleans.
</summary>
<pre class="language-javascript"><code>const toBool = a => a(true)(false)</code>
</pre>
</details>
<p>
Now let's add some functions that operate on boolean values:
</p>
<pre class="language-javascript"><code>const not = a => a(False)(True)
const and = a => b => a(b)(a)
const or = a => b => a(a)(b)</code>
</pre>
<p>
Again, try them in your browser's console like:
</p>
<pre class="language-javascript"><code>toBool(or(False)(True))</code>
</pre>
<br>
<details id="ternary">
<summary>
Aside on the ternary operator.
</summary>
<p>
The ternary operator in JavaScript looks like
</p>
<pre class="language-javascript"><code>someBool ? a : b</code>
</pre>
<p>
Note that neither <code class="inline">a</code>
nor <code class="inline">b</code>
are actually evaluated until the truthiness of <code class="inline">someBool</code>
has been evaluated. For example, when running:
</p>
<pre class="language-javascript"><code>false ? console.log(1) : console.log(2)</code>
</pre>
<p>
Only <code class="inline">2</code>
gets logged.
</p>
<p>
This means for the equivalent in our Lambda calculus, we need to do:
</p>
<pre class="language-javascript"><code>const _ = True // stands in for 'any value'
someBool(_ => a)(_ => b)(_)</code>
</pre>
<p>
In a language like Haskell, we don't need to do this as every expression is 'lazy' like the ternary expression is in JavaScript.
</p>
</details>
<br>
<p>
We're also going to define some functions that take an integer and return a boolean:
</p>
<pre class="language-javascript"><code>const isEven = n => n(not)(True)
const isZero = n => n(True(False))(True)</code>
</pre>
<h2>
Composite data
</h2>
<p>
Let's create a function to bundle two pieces of data into one, similar to what we might do with an Array in JavaScript.
</p>
<pre class="language-javascript"><code>const pair = a => b => f => f(a)(b)</code>
</pre>
<p>
That's great, but how do we get anything out of it?
</p>
<pre class="language-javascript"><code>const first = p => p(True)
const second = p => p(False)</code>
</pre>
<p>
Try this in your browser's console:
</p>
<pre class="language-javascript"><code>const myPair = pair(_2)(_0)
toInt(second(myPair))</code>
</pre>
<p>
We're in effect using the <code class="inline">pair</code>
function's closure to store information.
</p>
<br>
<p>
What can we do that's useful with this? We already have <code class="inline">inc</code>
that returns the next integer, let's write a <code class="inline">dec</code>
that returns the previous integer.
</p>
<pre class="language-javascript"><code>const incSecond = p => pair(second(p))(inc(second(p)))
const dec = n => first(n(incSecond)(pair(_0)(_0)))</code>
</pre>
<p>
Huh? Let's consider just <code class="inline">n(incSecond)(pair(_0)(_0))</code>
</p>
<p>
This says 'call <code class="inline">incSecond</code>
on <code class="inline">pair(_0)(_0)</code>
<code class="inline">n</code>
times'
</p>
<p>
So if <code class="inline">n</code>
were 3, then <code class="inline">incSecond(incSecond(incSecond(pair(_0)(_0))))</code>
</p>
<p>
Let's run through that (you might want to write your own helper function to <code class="inline">console.log</code>
<code class="inline">pair</code>
s):
</p>
<pre class="language-javascript"><code>incSecond(pair(_0)(_0)) // pair(_0)(_1)
incSecond(incSecond(pair(_0)(_1))) // pair(_1)(_2)
incSecond(incSecond(incSecond(pair(_1)(_2)))) // pair(_2)(_3)</code>
</pre>
<p>
Then we take the <code class="inline">first</code>
of <code class="inline">pair(_2)(_3)</code>
which is <code class="inline">_2</code>
- groovy!
</p>
<br>
<p>
Now we've got all the pieces to add a few other useful functions:
</p>
<pre class="language-javascript"><code>const minus = n => m => m(dec)(n)
const gte = n => m => isZero(n(dec)(m))
const lt = n => m => not(gte(n)(m))
const eq = n => m => and(gte(n)(m))(gte(m)(n))</code>
</pre>
<br>
<hr>
<h2>
Loops
</h2>
<p>
We've got a load of handy bits and bobs, now we can start making something that looks like a useful bit of code. In this case, we're going to recreate this JavaScript looping construct using just Lambda calculus:
</p>
<pre class="language-javascript"><code>const loop = (n, m, f, a) => {
let k = a
for (let i = n; i < m; i++){
k = f(i, k)
}
return k
}</code>
</pre>
<p>
I'll leave it to the reader to work out the meaning of it:
</p>
<pre class="language-javascript"><code>const incAndCall = f => p => pair(
inc(first(p))
)(
f(first(p))(second(p))
)
const loop = n => m => f => a => second(
(minus(m)(n))(incAndCall(f))(pair(n)(a))
)</code>
</pre>
<br>
<hr>
<h2>
Combinators
</h2>
<p>
Now for a sum function, in conventional JavaScript:
</p>
<pre class="language-javascript"><code>const sum = (n) => {
if (n == 0) return 0
else return sum(n - 1) + n
}</code>
</pre>
<p>
And in (nearly) pure Lambda calculus:
</p>
<pre class="language-javascript"><code>const sum = n => isZero(n)(_ => _0)(_ => plus(n)(sum(dec(n))))(_)</code>
</pre>
<em>
<code class="inline">_ = True</code>
and stands for 'any variable', we use it because of the reasons outlined <a href="#ternary">
above
</a>
.
</em>
<p>
This works, but is only 'nearly' pure Lambda calculus because <code class="inline">sum</code>
is referred to within the <code class="inline">sum</code>
function itself. It only works because that's how our JavaScript interpreter works, and is not built in syntax of the Lambda calculus.
</p>
<p>
To make it work without refering to itself, we define the 'Y-combinator':
</p>
<pre class="language-javascript"><code>const Y = f => (x => f(_ => x(x)))(x => f(_ => x(x)))</code>
</pre>
<em>
Note again the <code class="inline">_ =></code>
<a href="#ternary">
faff
</a>
to avoid infinite recursion.
</em>
<p>
If you work through the β-reduction, this is equivalent to:
</p>
<pre class="language-javascript"><code>Y = f => f(_ => Y(f))</code>
</pre>
<p>
Now we're able to redefine <code class="inline">sum</code>
without self-reference as:
</p>
<pre class="language-javascript"><code>const sum = Y(g => n => isZero(n)
(_ => _0)
(_ => plus(n)(g(_)(dec(n))))
(_))</code>
</pre>
</body>
</html>