-
Notifications
You must be signed in to change notification settings - Fork 0
/
2023-07-23-revelation.html
351 lines (347 loc) · 16.6 KB
/
2023-07-23-revelation.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
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
<head>
<meta charset="utf-8" />
<meta name="generator" content="pandoc" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<meta name="author" content="Darius J Chuck" />
<meta name="dcterms.date" content="2023-07-23" />
<title>Revelation: Lambda Calculus Reduced To Four Primitive Operations</title>
<style>
html {
color: #1a1a1a;
background-color: #fdfdfd;
}
body {
margin: 0 auto;
max-width: 36em;
padding-left: 50px;
padding-right: 50px;
padding-top: 50px;
padding-bottom: 50px;
hyphens: auto;
overflow-wrap: break-word;
text-rendering: optimizeLegibility;
font-kerning: normal;
}
@media (max-width: 600px) {
body {
font-size: 0.9em;
padding: 12px;
}
h1 {
font-size: 1.8em;
}
}
@media print {
html {
background-color: white;
}
body {
background-color: transparent;
color: black;
font-size: 12pt;
}
p, h2, h3 {
orphans: 3;
widows: 3;
}
h2, h3, h4 {
page-break-after: avoid;
}
}
p {
margin: 1em 0;
}
a {
color: #1a1a1a;
}
a:visited {
color: #1a1a1a;
}
img {
max-width: 100%;
}
h1, h2, h3, h4, h5, h6 {
margin-top: 1.4em;
}
h5, h6 {
font-size: 1em;
font-style: italic;
}
h6 {
font-weight: normal;
}
ol, ul {
padding-left: 1.7em;
margin-top: 1em;
}
li > ol, li > ul {
margin-top: 0;
}
blockquote {
margin: 1em 0 1em 1.7em;
padding-left: 1em;
border-left: 2px solid #e6e6e6;
color: #606060;
}
code {
font-family: Menlo, Monaco, Consolas, 'Lucida Console', monospace;
font-size: 85%;
margin: 0;
hyphens: manual;
}
pre {
margin: 1em 0;
overflow: auto;
}
pre code {
padding: 0;
overflow: visible;
overflow-wrap: normal;
}
.sourceCode {
background-color: transparent;
overflow: visible;
}
hr {
background-color: #1a1a1a;
border: none;
height: 1px;
margin: 1em 0;
}
table {
margin: 1em 0;
border-collapse: collapse;
width: 100%;
overflow-x: auto;
display: block;
font-variant-numeric: lining-nums tabular-nums;
}
table caption {
margin-bottom: 0.75em;
}
tbody {
margin-top: 0.5em;
border-top: 1px solid #1a1a1a;
border-bottom: 1px solid #1a1a1a;
}
th {
border-top: 1px solid #1a1a1a;
padding: 0.25em 0.5em 0.25em 0.5em;
}
td {
padding: 0.125em 0.5em 0.25em 0.5em;
}
header {
margin-bottom: 4em;
text-align: center;
}
#TOC li {
list-style: none;
}
#TOC ul {
padding-left: 1.3em;
}
#TOC > ul {
padding-left: 0;
}
#TOC a:not(:hover) {
text-decoration: none;
}
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
div.columns{display: flex; gap: min(4vw, 1.5em);}
div.column{flex: auto; overflow-x: auto;}
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
ul.task-list{list-style: none;}
ul.task-list li input[type="checkbox"] {
width: 0.8em;
margin: 0 0.8em 0.2em -1.6em;
vertical-align: middle;
}
</style>
<!--[if lt IE 9]>
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
<![endif]-->
</head>
<body>
<a href="https://jevko.github.io/writing">jevko.github.io/writing</a>
<div style="text-align: center;">
<p>This is a part of the series:</p>
<p>"Exploring Simplified Lambda Calculus Notations"</p>
<p>Part I: <a href="https://jevko.github.io/writing/2023-07-20-lambda.html">"Summary"</a> (HTML).</p>
</p>Part II: <a href="https://jevko.github.io/writing/2023-07-23-revelation.html">"Revelation: Lambda Calculus Reduced To Four Primitive Operations"</a> (HTML).</p>
</div>
<header id="title-block-header">
<h1 class="title">Revelation: Lambda Calculus Reduced To Four Primitive
Operations</h1>
<p class="author">Darius J Chuck</p>
<p class="date">2023-07-23</p>
</header>
<style>
@media screen {
html {
/* todo: use for publishing a dark-mode draft: */
filter: invert(1);
font-size: 18pt;
}
}
</style>
<p><img src="img/2023-07-23-revelation.png" /></p>
<p><strong>Lambda calculus can be reduced down to 4 primitive
operations.</strong></p>
<p>First, let’s define a simplified grammar for a lambda calculus term
that captures these operations syntactically:</p>
<pre><code>term ::= abstraction
| application
| revelation
| reference</code></pre>
<p>A term is defined as either of the four basic operations.</p>
<p>We don’t want to worry about parentheses, associativity, and
precedence, so each operation shall use a distinct prefix operator with
fixed arity. Effectively we’ll be writing our terms in Polish notation –
the order of operations explicitly defined by the position of the
operators, which are always evaluated left-to-right.</p>
<p>The first two operations should be more or less familiar.</p>
<p>Abstraction is defined like so:</p>
<p><code>abstraction ::=</code>
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>𝛌</mi><annotation encoding="application/x-tex">\boldsymbol{\lambda}</annotation></semantics></math>
<code>term</code></p>
<p>The definition doesn’t mention variable names. We only have a lambda
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>λ</mi><annotation encoding="application/x-tex">\lambda</annotation></semantics></math>,
which we’ll call the <strong>abstraction operator</strong>, prefixed to
a term. This is the same as in N.G. de Bruijn’s namefree syntax.</p>
<p>Now application is defined as:</p>
<p><code>application ::=</code>
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>𝛂</mi><annotation encoding="application/x-tex">\boldsymbol{\alpha}</annotation></semantics></math>
<code>term term</code></p>
<p>Instead of using juxtaposition, we introduce a two-argument
<strong>application operator</strong>, alpha
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>α</mi><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>.
Predictably, it applies the second term to the first.</p>
<p>With that out of the way, let’s get to the interesting operations:
revelation and reference.</p>
<p>As can be guessed, these replace variable references.</p>
<p>We will leave revelation for the end. First let’s look at
reference:</p>
<p><code>reference ::=</code>
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>𝛕</mi><annotation encoding="application/x-tex">\boldsymbol{\tau}</annotation></semantics></math></p>
<p>It’s denoted simply by the letter tau
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>τ</mi><annotation encoding="application/x-tex">\tau</annotation></semantics></math>,
which is our zero-argument <strong>reference operator</strong>. What it
does is it refers to the topmost variable in current scope.</p>
<p>Normally the topmost variable is the one introduced by the lambda
closest to the current position. That is:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>τ</mi></mrow><annotation encoding="application/x-tex">
\lambda \tau
</annotation></semantics></math></p>
<p>means the same thing as
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>x</mi><mi>.</mi><mi>x</mi></mrow><annotation encoding="application/x-tex">\lambda x.x</annotation></semantics></math>.
in the conventional notation. Similarly:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>λ</mi><mi>τ</mi></mrow><annotation encoding="application/x-tex">
\lambda \lambda \tau
</annotation></semantics></math></p>
<p>means the same thing as
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>x</mi><mi>.</mi><mi>λ</mi><mi>y</mi><mi>.</mi><mi>y</mi></mrow><annotation encoding="application/x-tex">\lambda x.\lambda y.y</annotation></semantics></math>
in the conventional notation.</p>
<p>That’s all well and good, but how do we refer to a variable that is
not topmost in current scope?</p>
<p><strong>Here is where the revelation comes in</strong>:</p>
<p><code>revelation ::=</code>
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>𝛔</mi><annotation encoding="application/x-tex">\boldsymbol{\sigma}</annotation></semantics></math>
<code>term</code></p>
<p>Besides being a cool pun, the name is quite descriptive. The
<strong>revelation operator</strong>, denoted by sigma
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>,
<strong>creates a new scope for the term that follows it, with the
topmost variable discarded</strong>, thus <em>revealing</em> the next
variable to the term. The topmost variable in the new scope is the one
introduced by the lambda <em>one step back</em> from the current
position. So:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>λ</mi><mi>σ</mi><mi>τ</mi></mrow><annotation encoding="application/x-tex">
\lambda \lambda \sigma \tau
</annotation></semantics></math></p>
<p>means the same thing as
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>x</mi><mi>.</mi><mi>λ</mi><mi>y</mi><mi>.</mi><mi>x</mi></mrow><annotation encoding="application/x-tex">\lambda x.\lambda y.x</annotation></semantics></math>
in the conventional notation.</p>
<p>With these 4 operations, not only can we encode any and all lambda
terms that we can encode in the conventional notation without using
numerical de Bruijn indices or needing an infinite supply of names for
variables.</p>
<p>Being more “low-level”, this notation can actually represent most
lambda terms in more than one way.</p>
<p>For example, a conventionally-encoded lambda term like:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>x</mi><mi>.</mi><mi>λ</mi><mi>y</mi><mi>.</mi><mi>λ</mi><mi>z</mi><mi>.</mi><mi>x</mi></mrow><annotation encoding="application/x-tex">
\lambda x.\lambda y.\lambda z.x
</annotation></semantics></math></p>
<p>Can be represented as:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>λ</mi><mi>λ</mi><mi>σ</mi><mi>σ</mi><mi>τ</mi></mrow><annotation encoding="application/x-tex">
\lambda \lambda \lambda \sigma \sigma \tau
</annotation></semantics></math></p>
<p>or equivalently as:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>λ</mi><mi>σ</mi><mi>λ</mi><mi>σ</mi><mi>τ</mi></mrow><annotation encoding="application/x-tex">
\lambda \lambda \sigma \lambda \sigma \tau
</annotation></semantics></math></p>
<p>Having
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>
be an independent first-class operation, we can now choose the points at
which we reveal the interesting (or equivalently: discard the
uninteresting) variables.</p>
<p>This starts to matter when we add applications to the mix.</p>
<p>Consider a term like:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>x</mi><mi>.</mi><mi>λ</mi><mi>y</mi><mi>.</mi><mi>λ</mi><mi>z</mi><mi>.</mi><mi>x</mi><mspace width="0.167em"></mspace><mi>x</mi><mspace width="0.167em"></mspace><mi>x</mi><mspace width="0.167em"></mspace><mi>x</mi></mrow><annotation encoding="application/x-tex">
\lambda x.\lambda y.\lambda z.x\,x\,x\,x
</annotation></semantics></math></p>
<p>Naively we could represent it as:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>λ</mi><mi>λ</mi><mi>α</mi><mi>α</mi><mi>α</mi><mi>σ</mi><mi>σ</mi><mi>τ</mi><mi>σ</mi><mi>σ</mi><mi>τ</mi><mi>σ</mi><mi>σ</mi><mi>τ</mi><mi>σ</mi><mi>σ</mi><mi>τ</mi></mrow><annotation encoding="application/x-tex">
\lambda \lambda \lambda \alpha \alpha \alpha \sigma \sigma \tau \sigma \sigma \tau \sigma \sigma \tau \sigma \sigma \tau
</annotation></semantics></math></p>
<p>But actually, we don’t have to repeat the revelation operation twice
for every application. We can “factor it out”, like so:</p>
<p><math display="block" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mrow><mi>λ</mi><mi>λ</mi><mi>λ</mi><mi>σ</mi><mi>σ</mi><mi>α</mi><mi>α</mi><mi>α</mi><mi>τ</mi><mi>τ</mi><mi>τ</mi><mi>τ</mi></mrow><annotation encoding="application/x-tex">
\lambda \lambda \lambda \sigma \sigma \alpha \alpha \alpha \tau \tau \tau \tau
</annotation></semantics></math></p>
<p>Now the scopes which the
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>τ</mi><annotation encoding="application/x-tex">\tau</annotation></semantics></math>
operations “see” already have the unnecessary variables discarded.</p>
<p>This equivalent encoding of the lambda term is not only shorter but
more efficient in terms of the number of operations performed.</p>
<p><strong>With that, we are ready to introduce the notions of
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-equivalence
and
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-reduction
or
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-optimization,
along with its inverse,
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-deoptimization</strong>.</p>
<p>Those interested in how that may look like, I direct to the <a
href="https://xtao.org/blog/last-intro.html">Introduction to the LAST
programming language</a>, which describes the first incarnation of this
idea I implemented last year. The LAST language works exactly in the way
described here, except it uses the letters L, A, S, and T instead of
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>λ</mi><annotation encoding="application/x-tex">\lambda</annotation></semantics></math>,
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>α</mi><annotation encoding="application/x-tex">\alpha</annotation></semantics></math>,
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>,
and
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>τ</mi><annotation encoding="application/x-tex">\tau</annotation></semantics></math>.
The implementation also features
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-optimization,
there called S-optimization, which is an algorithm I developed that
transforms lambda terms into fully optimized
<math display="inline" xmlns="http://www.w3.org/1998/Math/MathML"><semantics><mi>σ</mi><annotation encoding="application/x-tex">\sigma</annotation></semantics></math>-equivalents.</p>
<p><strong>I haven’t mathematically proven that these are indeed fully
optimized. I’d appreciate if anybody could help with that.</strong></p>
<p>I think it’s pretty cool that it’s possible to simplify lambda
calculus like this and dig into its low-level details. It helps with
gaining a deeper understanding of foundations of mathematics. This in
turn is potentially useful in areas that draw from that, such as
computer science, theory of programming languages, category theory, as
well as philosophy or linguistics.</p>
<p>Recently I’ve been thinking about this a lot again and finding more
interesting insights, which I may get around to writting down at some
point. Meanwhile I hope this writing may help some puzzle pieces snap
together in somebody else’s head.</p>
<p><img src="img/2023-07-23-revelation.png" /></p>
</body>
</html>