-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathlc.html
More file actions
357 lines (357 loc) · 13.9 KB
/
lc.html
File metadata and controls
357 lines (357 loc) · 13.9 KB
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
<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "file:///home/bediger/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Lambda Calculator</title>
<!-- $Id: lc.html,v 1.11 2011/11/17 13:47:11 bediger Exp $ -->
<meta name="description" content="Article about Lambda Calculus Interpreter" />
<meta name="keywords" content="lambda calculus, intepreter" />
</head>
<body>
<h1>Lambda Calculator</h1>
<h2>Version 1.0</h2>
<p><em>last revision: 2011-11-12</em></p>
<p><a href="mailto:bediger@stratigery.com">Bruce Ediger</a><br/></p>
<p><a href="/index.html">Bruce Ediger's web pages</a></p>
<hr/>
<script language="JavaScript" type="text/javascript" src="partyon.js">
</script>
<hr />
<h1>Table of contents</h1>
<ol>
<li><a href="#INTRO">Introduction</a></li>
<li><a href="#STARTING">Starting</a></li>
<li><a href="#RUNNING">Using</a></li>
<li><a href="#DOWNLOADS">Downloads</a></li>
<li><a href="#INSTALL">Building and Installing</a></li>
</ol>
<h1><a name="INTRO">Introduction</a></h1>
<p>
This document describes how to download or build, then use <kbd>lc</kbd> v1.0,
yet another lambda calculator.
</p>
<p>
<kbd>lc</kbd> interprets a
programming language with similarities to various untyped lambda calculus
formal systems. It doesn't exactly interpret any "untyped lambda calculus"
in that it runs on computers with finite CPU speed and a finite memory.
Most or all formal systems fail to take limits into account.
</p>
<p>
<kbd>lc</kbd> performs normal-order (leftmost-outermoust) Beta and Eta reductions.
The user can turn off Eta reductions, but Beta reductions always remain in effect.
</p>
<p>
<kbd>lc</kbd> allows the user to create
<a href="#ABBREVIATION">abbreviations</a>, and simple
<a href="#PARAMETERIZED">parameterized abbreviations</a>.
Abbreviations allow the user to reference possibly very complex terms
with a single identifier. Parameterized abbreviations can be used
to facilitate use of terms with repetitive structure, like Church Numerals.
</p>
<h1><a name="STARTING">Starting</a></h1>
<p>
<kbd>lc</kbd> is a command line program. You invoke it by typing in
its name ("lc") and possibly some flags and options.
</p>
<h2>Command Line Options</h2>
<table border="0">
<tr><td><kbd>-L <em>filename</em></kbd></td><td></td><td>Read and intrepret <em>filename</em> before accepting interactive input.</td></tr>
<tr><td><kbd>-p</kbd></td><td></td><td>Do not print a prompt before accepting input.</td></tr>
</table>
<p>
<kbd>lc</kbd> uses "<kbd>LC></kbd>" as its command prompt.
when the user hits return, <kbd>lc</kbd> does Beta reduction,
and possibly Eta reduction, until it reaches a normal form.
It prints the normal form, then waits for more input.
</p>
<p>
<kbd>lc</kbd> reads from stdin and writes output to stdout, so you might
use it as part of a pipeline, or with input or output redirection.
</p>
<p>
The <kbd>-L</kbd> option with associated filenames can appear more than
once on the command line. <kbd>lc</kbd> will read and evaluate the files
in the order they appear on the command line.
</p>
<h1><a name="RUNNING">Using the interpreter</a></h1>
<p>
At the <kbd>LC></kbd> prompt, the user can type a
<a href="#TERMS">lambda calculus term</a>,
or an <a href="#COMMANDS">interpreter command</a>.
</p>
<p>
To quit, the user must cause an end-of-file condition (usually control-D
from the keyboard) or send an interrupt signal (usually control-C from
the keyboard).
</p>
<p>
The user can interrupt a long-running reduction with a keyboard interrupt
(usually control-C), which will return to the <kbd>LC></kbd> prompt.
Such an interrupt probably causes a memory leak. At exit <kbd>lc</kbd>
notifies the user if it detected any memory leaks.
</p>
<h2>Examples</h2>
<ul>
<li><a href="lc/bluff.combinator">Bluff Combinator</a></li>
<li><a href="lc/scott.numerals">Scott Numerals</a></li>
<li><a href="lc/lambdaI.church.numerals">Church Numerals in λI</a></li>
<li><a href="lc/church.numerals">Church Numerals</a></li>
</ul>
<h2><a name="TERMS">Lambda Calculus Terms</a></h2>
<p>
A <em>term</em> (to <kbd>lc</kbd>) consists of a variable, an abstraction,
or an application of one sub-term to another.
</p>
<h3>Identifiers</h3>
<p>
Any C- or Java-format identifier can serve as an <kbd>lc</kbd> <em>identifier</em>.
That means that identifiers take
the form of a string beginning with an upper or lowercase letter,
followed by zero or more letters, digits or underscores.
</p>
<h3>Variables</h3>
<p>
Variables, free or bound, have identifiers as names.
<kbd>lc</kbd> will rename bound variables to prevent "variable capture".
For instance, evaluating <kbd>(%x.%y.y x) y</kbd> results in <kbd>%a.a y</kbd>,
not <kbd>%y.y y</kbd>. The bound variable "y" in the original term
gets renamed to "a" in the final normal form.
</p>
<h3>Abstractions</h3>
<p>
An <em>abstraction</em> follows the traditional lambda calculus pattern:
<kbd>λx.<em>body</em></kbd>. The "<kbd>λx</kbd>" part
denotes the beginning of the abstraction, and the name of the dummy
variable that might appear in the body of the abstraction.
The body must constitute a term. Any legal-format variable can occur
as the bound variable in an abstraction.
</p>
<p>
Any of the ASCII characters <kbd>$</kbd>, <kbd>%</kbd>, <kbd>\</kbd> or
<kbd>^</kbd> (dollar sign, percent, backslash, caret)
can be used as the "λ" character in an abstraction.
You can't use a UTF-8 λ, as this program only understands ASCII.
</p>
<p>
Either the ASCII character <kbd>.</kbd> (period or full stop), or the string
<kbd>-></kbd> can denote where
the binding site stops, and where the body begins.
</p>
<p>
<kbd>lc</kbd> supports multi-variable abstraction notation.
In lambda calculus literature,
multi-variable abstractions often get written like this: <em>λxyz.x z y</em>
<kbd>lc</kbd> interprets the <em>xyz</em> part as a single bound variable named <kbd>xyz</kbd>,
so the user separates multiple variables with whitespace: <kbd>\x y z.x z y</kbd>.
The user can also write nested abstractions: <kbd>\x.\y\.z.x z y</kbd>.
</p>
<h5>Example Abstractions</h5>
<pre>
^x.x (x x)
%p q r.p r (q r)
\x.\y->x (x (x (x y)))
$x y z.x (y z)
</pre>
<h3>Applications</h3>
<p>
<em>Application</em> occurs by creating input with two terms side by side:
<kbd>X Y</kbd>. Terms associate to the left, so <kbd>X Y Z</kbd>
gets evaluated as <kbd>((X Y) Z)</kbd>. You have to explicitly parenthesize
terms to get association-to-the-right: <kbd>X (Y Z)</kbd>.
</p>
<p>
The body of an abstraction extends as far as possible. To apply an
abstraction to a second term, the user must parenthesize:
</p>
<pre>
(\x y z. x (y z)) A B C
</pre>
<p>
Without parenthesizing the abstraction, <kbd>\x y z. x (y z) A B C</kbd>
constitutes a single abstraction with a six-term sized body.
</p>
<h2><a name="COMMANDS">Interpreter Commands</a></h2>
<h3>Reduction Control and Display</h3>
<ul>
<li><kbd>timer on|off</kbd> - when on, prints elapsed time taken by reductions.</li>
<li><kbd>step on|off</kbd> - single step reductions. Requires user to hit return after each reduction.</li>
<li><kbd>trace on|off</kbd> - prints out what happens for each reduction.</li>
<li><kbd>eta on|off</kbd> - turn on or off Eta (η) reductions.</li>
<li><kbd>load <em>filename</em></kbd> - read and evaluation contents of <em>filename</em>.</li>
</ul>
<p>
You must double-quote file names containing any characters that
an <kbd>lc</kbd>
identifier can't contain. That means full or partially qualifed path names
(they contain slash characters) or any file names with whitespace in them.
</p>
<p>
You can check the state of any of these commands by typing them in without
"on" or "off" at the <kbd>LC></kbd> prompt.
</p>
<h3><a name="ABBREVIATION">Abbreviations</a></h3>
<ul>
<li><kbd>define <em>identifier</em> <em>term</em></kbd></li>
<li><kbd>def <em>identifier</em> <em>term</em></kbd></li>
<li><kbd>$$</kbd> - result of last expression evaluation.</li>
</ul>
<p>
<kbd>define</kbd> or <kbd>def</kbd> stores a copy of the <em>term</em> without
performing any reductions. Each time an <em>identifier</em> used in a previous
abbreviation appears, <kbd>lc</kbd> inserts a copy of the term so
abbreviated.
</p>
<p>
The special token <kbd>$$</kbd> represents the results of the last
successful reduction.
<kbd>$$</kbd> changes whenever <kbd>lc</kbd> calculates
a normal form. <kbd>$$</kbd> takes on the value of that new normal form.
The user can insert the last normal form calculated by inserting <kbd>$$</kbd>
one or more times in the next expression typed in.
</p>
<p>
The identifier of an abbreviation gets its term substituted
in its place, as if surrounded by parentheses. For example:
</p>
<pre>
LC> def abbrev1 (\x.\y.\z.x (y z))
LC> A abbrev1 C
A ((\x.\y.\z.x (y z)) C
</pre>
<p>
Abstractions can "capture" identifiers in the abbreviation that lexically
match the bound variable:
</p>
<pre>
LC> def X3 x x x
LC> (\x.X3) A
A A A
LC>
</pre>
<h3><a name="PARAMETERIZED">Parameterized Abbreviations</a></h3>
<ul>
<li><kbd>define <em>identifier</em> *<em>term</em></kbd></li>
<li><kbd>define <em>identifier</em> <em>term</em><sub>1</sub> *<em>term</em><sub>2</sub></kbd></li>
<li><kbd>define <em>identifier</em> *<em>term</em><sub>1</sub> *<em>term</em><sub>2</sub></kbd></li>
<li><kbd>define <em>identifier</em> *<em>term</em><sub>1</sub> <em>term</em><sub>2</sub></kbd></li>
</ul>
<p>
Marked parts of term abbreviated by <kbd>identifier</kbd>
get expanded. When the interpreter sees a use of an abbreviation like
<kbd><em>identifier</em>{N}</kbd>, it expands the marked terms N times.
The number <em>N</em></kbd> has to be greater than zero.
This feature can be used to make Church numerals more convenient.
</p>
<pre>
LC> def C0 \f n.n
LC> def C \f n.*f n
LC> print C{2}
%f.%n.f (f n)
LC>
</pre>
<p>
Note that the Church Numeral for zero is special: you can't define it
using parameterized abbreviations. This seems consistent with the inductive
definition of numbers in systems like Peano Arithmetic.
</p>
<p>
You can create simple or complex parameterized abbreviations:
</p>
<pre>
LC> def X \x.*x
LC> X{4}
%x.x x x x
LC> def XY \x y.*x (x *y)
LC> XY{3}
%x.%y.x (x (x (x (y y y))))
</pre>
<h3>Examining Terms</h3>
<ul>
<li><kbd>print <em>term</em></kbd> - print a term or abbreviation without any reductions.</li>
<li><kbd>free <em>term</em></kbd> - print the free variables appearing in a term.</li>
<li><kbd>bound <em>term</em></kbd> - print the bound variables appearing in a term.</li>
</ul>
<p>
None of these commands produce terms, just output on stdout.
</p>
<h3>Operations on Terms</h3>
<ul>
<li><kbd>godelize <em>term</em></kbd></li>
<li><kbd><a name="NORMALIZE">normalize</a> <em>term</em></kbd></li>
</ul>
<p>
<kbd>godelize</kbd> makes a godelization of a term by Torben Mogensen's
"higher order syntax" method. The godelization is in Beta normal form,
even if the original term is not.
</p>
<p>
<kbd>normalize</kbd> causes an out-of-normal-order reductions on
the term it applies to. Judicious use
of <kbd>normalize</kbd> can cause non-normal order evaluation,
or it can be used to store an abbreviation of a normal form.
</p>
<p>
Both of these operations produce terms, and so can appear in the definition of an
abbreviation, or in the midst of a more complicated term.
</p>
<h3>Comparing Terms</h3>
<ul>
<li><kbd><em>term<sub>1</sub></em> == <em>term<sub>2</sub></em></kbd> - lexical equality</li>
<li><kbd><em>term<sub>1</sub></em> = <em>term<sub>2</sub></em></kbd> - alpha equality</li>
</ul>
<p>
Lexical equivalence ("==") requires exact string-matching between all
variables, bound or free. Alpha equivalence ("=") requires string-matches
for all free variables, and identical appearances of bound variables and
their binding sites.
</p>
<p>
<kbd>lc</kbd> does not perform any reductions on either side of "=" or "==".
The user can use <a href="#NORMALIZE"><kbd>normalize</kbd></a> on either or both sides of a
comparison to compare beta normal forms.
</p>
<p>
Neither comparison produces a term, just output on stdout indicating
equivalence or non-equivalence.
</p>
<h1><a name="DOWNLOADS">Downloads</a></h1>
<ul>
<li><a href="lc/lc-1.0-1.i386.rpm">RPM package</a> for x86 linux</li>
<li><a href="lc/lc-1.0-1-i686.pkg.tar.xz">Arch package</a> for i686 linux</li>
<li><a href="lc/lc-1.0-i386-1.tgz">Slackware package</a> for x86 linux</li>
<li><a href="lc/lc">Plain old x86 Linux executable</a></li>
<li><a href="lc/lc-1.0.tar.gz">Source code</a></li>
</ul>
<h1><a name="INSTALL">Building and Installing</a></h1>
<p>
<kbd>lc</kbd> compiles and runs under Linux, and probably
Solaris and most BSD operating systems. I wrote it in the
strictest ANSI-C I could,
with the exception of some signals it handles.
</p>
<p>
I did not use GNU "autoconf" tools for this project, as I wanted to
use alternative C compilers, and lexer and compiler-compiler
(lex, flex, yacc, bison, byacc) alternatives.
</p>
<p>
Use one of these commands:
</p>
<table border="0">
<tr><td><kbd>make gnu</kbd></td><td> </td><td>GNU-named tools. Works for most or all linux distros.</td></tr>
<tr><td><kbd>make cc</kbd></td><td> </td><td>Traditional unix names for tools. Use for Solaris and *BSD</td></tr>
<tr><td><kbd>make pcc</kbd></td><td> </td><td>Compile with the re-invigorated <a href="http://pcc.ludd.ltu.se/">PCC</a> C compiler</td></tr>
<tr><td><kbd>make lcc</kbd></td><td> </td><td>Compile using the <a href="http://www.cs.princeton.edu/software/lcc/">lcc</a> C compiler.</td></tr>
<tr><td><kbd>make tcc</kbd></td><td> </td><td>Compile using the <a href="http://bellard.org/tcc/">tcc</a> C compiler.</td></tr>
<tr><td><kbd>make clang</kbd></td><td> </td><td>Compile with the LLVM C-language front end, <a href="http://clang.llvm.org/">Clang</a></td></tr>
</table>
<p>
This should result in an executable file named "lc".
You can use <kbd>mv</kbd> or <kbd>cp</kbd> to put the file named "lc" in your PATH,
or you can execute it in place. <kbd>lc</kbd> does not automatically
read startup or "rc" files, nor does it assume it runs while residing in a
specific directory.
</p>
</body>
</html>