forked from scgruber/Lambda-Graph-Generator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
115 lines (114 loc) · 5.13 KB
/
index.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
<!DOCTYPE html>
<!--
index.html
Lambda Graph Generator
Sam Gruber <[email protected]>
-->
<html>
<head>
<title>Lambda Graph Generator</title>
<script src="jquery-1.9.1.min.js" type="text/javascript"></script>
<script src="util.js" type="text/javascript"></script>
<script src="nodes.js" type="text/javascript"></script>
<script src="interact.js" type="text/javascript"></script>
<script src="lgg.js" type="text/javascript"></script>
<link href="style.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<header>
<h1>The Lambda Calculus</h1>
<h2>An Illustrated Primer</h2>
</header>
<article>
<h2>Preface</h2>
<section>
<div class="content">
<p>This document is based upon the text of the <a href="http://en.wikipedia.org/wiki/Lambda_calculus">Lambda calculus</a> article on English Wikipedia. It is made available under the <a href="http://creativecommons.org/licenses/by-sa/3.0/">Creative Commons Attribution Share-Alike 3.0 License</a>.</p>
<p>In this document you will see diagrams, such as the one to the right, which show the structure of a Lambda Calculus expression visually. These diagrams can be changed by typing in the text field below them. These diagrams are constructed based on a few rules:</p>
<ol>
<li>Large circles surround Lambda Abstractions, which are similar to functions in a typical programming language.</li>
<li>Small circles which lie on the boundary of larger circles denote inputs to Lambda Abstractions. These may be unbound and simply labeled, or contain another expression which is bound to the variable.</li>
<li>Lines track the path of execution inside the expression. Where two lines meet, an application occurs, where the object on the continuous line accepts the terminated line's object as an argument.</li>
</ol>
</div>
<div class="drawing">
<canvas id="lgg-canvas-0" width="300" height="200"></canvas>
<br/>
<input id="lgg-text-0" type="text" value="(\xyz.xz(yz))(\a.a)"></input>
</div>
<div class="clear"></div>
</section>
<h2>Arithmetic in Lambda Calculus</h2>
<section>
<div class="content">
<p>There are several possible ways to define the natural numbers in lambda calculus, but by far the most common are the Church numerals, which can be defined as follows:</p>
<blockquote>
0 := (\fx.x)<br/>
1 := (\fx.f x)<br/>
2 := (\fx.f (f x))<br/>
3 := (\fx.f (f (f x)))<br/>
</blockquote>
<p>The Church numeral n is a function that takes a function f as argument and returns the n-th composition of f, i.e. the function f composed with itself n times. Such repeated compositions (of a single function f) obey the laws of exponents, which is why these numerals can be used for arithmetic.</p>
</div>
<div class="drawing">
<canvas id="lgg-canvas-1" width="300" height="200"></canvas>
<br/>
<input id="lgg-text-1" type="text" value="(\fx.f (f x))"></input>
</div>
<div class="clear"></div>
</section>
<section>
<div class="content">
<p>We can define a successor function, which takes a number n and returns n + 1 by adding an additional application of f:</p>
<blockquote>
SUCC := (\nfx.f (n f x))<br/>
</blockquote>
</div>
<div class="drawing">
<canvas id="lgg-canvas-2" width="300" height="200"></canvas>
<br/>
<input id="lgg-text-2" type="text" value="(\nfx.f (n f x))"></input>
</div>
<div class="clear"></div>
</section>
<section>
<div class="content">
<p>Since adding m to a number n can be accomplished by adding 1 m times, we can define addition:</p>
<blockquote>
PLUS := (\mn.m SUCC n)<br/>
PLUS := (\mn.m (\nfx.f (n f x)) n)<br/>
PLUS := (\mnfx.m f (n f x))<br/>
</blockquote>
</div>
<div class="drawing">
<canvas id="lgg-canvas-3" width="300" height="200"></canvas>
<br/>
<input id="lgg-text-3" type="text" value="(\mnfx.m f (n f x))"></input>
</div>
<div class="clear"></div>
</section>
<section>
<div class="content">
<p>And similarly we can define multiplication in terms of addition:</p>
<blockquote>
MULT := (\mn.m (PLUS n 0))<br/>
...STUFF...<br/>
MULT := (\mnf. m (nf))<br/>
</blockquote>
</div>
<div class="drawing">
<canvas id="lgg-canvas-4" width="300" height="200"></canvas>
<br/>
<input id="lgg-text-4" type="text" value="(\mn.m (\mnfx.m f (n f x)) n (\fx.x))"></input>
</div>
<br/>
<div class="drawing">
<canvas id="lgg-canvas-5" width="300" height="200"></canvas>
<br/>
<input id="lgg-text-5" type="text" value="(\mnf. m (nf))"></input>
</div>
<div class="clear"></div>
</section>
</article>
</body>
</html>