-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMatthias-2015-07-27.html
217 lines (206 loc) · 12 KB
/
Matthias-2015-07-27.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
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<meta name="generator" content="pandoc" />
<title></title>
<style type="text/css">code{white-space: pre;}</style>
<link rel="stylesheet" href="pandoc.css" type="text/css" />
</head>
<body>
<p>Started in the 30s with Church.</p>
<p>Godel has a language that can prove anything.</p>
<p>Church says you can prove anything with functions.</p>
<p>Set notation was <code>^ x | x² < 0</code>, church annotated <code>'^ | x² < 0</code>, which was typeset as <code>λ | x² < 0</code>.</p>
<pre><code>e ⩴ x | λx.e | e e</code></pre>
<p>See things as trees:</p>
<pre><code>((λx.x)(λx.x)) = (λ.←) (λ.←)</code></pre>
<p>The names don't matter, the meaning of variable is its binding-site.</p>
<pre><code>λdavid. (david david) = λjeff. (jeff jeff)</code></pre>
<p>"<code>λ</code> is just 7th-grade algebra hyped up a little bit."</p>
<pre><code>f(x) ≔ x²
f(6) + 5 = 6² + 5 = 41
(λx.e)e' = e[x←e'] -- β
(λx.x) a = a
(λxy.xyy)ab = (λy.ayy)b = abb</code></pre>
<p>Lambdas are not functions! What about partial functions?</p>
<p><code>β</code> is a relation, and requires a <code>λ</code> on the outside.</p>
<pre><code>λx.λy.λz.⸤(λx.x)(zz)⸥y</code></pre>
<p>We can't reduce with <code>β</code>.</p>
<p><code>β</code> is a "notion of reduction".</p>
<p>We start defining <code>=⸤β⸣</code>:</p>
<pre><code>e β e'
---------
e =⸤β⸥ e'
e =⸤β⸥ e'
---------------
λx.e =⸤β⸥ λx.e'</code></pre>
<p>Template structure is called a "redex".</p>
<p>["redex" is not latin, it just means reducible expression. "contractum" is latin.]</p>
<p>Need another set of rules..</p>
<pre><code>e =⸤β⸥ e'
----------------
e₀ e =⸤β⸥ e₀ e'
e =⸤β⸥ e'
----------------
e e₀ =⸤β⸥ e' e₀</code></pre>
<p>We are creating a "syntactic compatibility closure".</p>
<p>We also need the reflexive, symmetric and transitive closure of <code>=⸤β⸥</code>.</p>
<p>This gives an equivalence relation.</p>
<p>We have "a system of calculating equivalences between terms".</p>
<p>Q: "does something have meaning?"</p>
<p>Two possible meanings:</p>
<ol style="list-style-type: decimal">
<li>"Can you prove 'true = false', or 'is everything related'" You need to prove (meta-proof), that you cannot prove (in the system), that some two terms are equal. This is called a consistency theorem, developed by Church+Rosser, "the Church+Rosser lemma". This shows that the system relates some terms, but not all terms.</li>
<li>Is there a topologically, algebraically generated space of functions generated by <code>λ</code> and satisfying <code>=⸤β⸥</code>. This was worked out by Dana Scott.</li>
</ol>
<p>"lambda-calculus and denotational semantics had a terrible influence on computer science" --MF</p>
<p>1958: Lisp and Algol 60 were created.</p>
<p>Lisp: - introduced <code>λ</code>-notation, got it wrong</p>
<p>Algol 60: - based on substitution model of <code>λ</code>-calculus - call-by-name parameter passing (<code>β</code>-rule) (was very slow) - then also introduced call-by-value - cvn vs cbv "one was correct, one was fast"</p>
<p>For the next 15 years, people struggled to relate call-by-name (correct) with call-by-value (fast).</p>
<p>Landin (1960s, '62, '63), invented the idea of abstract syntax. Bohm did the same thing. McCarthy tried something similar.</p>
<p>Abelson and Sussman make popular "applicative order application".</p>
<p>Dana Scott assigned a mathematical meaning to <code>λ</code>-calculus: 1. Created the function space 2. Assigning a mapping from <code>λ → ⟦⟧</code></p>
<p>MF opinion, denotational semantics took us off track.</p>
<p>Plotkin solved all of this (1972/1974) "Call-by-name, call-by-value and the lambda calculus". Launched enough research ideas to fill 15 people's entire research lives. Read this paper it's really good!!!</p>
<p>Gives an algorithm to understand what a calculus and a semantics is for a programming language (13 steps?).</p>
<p>Launched research into CPS.</p>
<ol style="list-style-type: decimal">
<li>Pick a term language, scoped</li>
<li>Pick a subset of terms, called programs, and another subset, called values (first appearance of words 'program' and 'value' in study of <code>λ</code> up to that point.)</li>
</ol>
<ul>
<li>Programs are things we don't really know what to do with immediately</li>
<li><p>Values are things "you see" at the end of computation. <code>λ</code> is a value.</p>
<pre><code> .- input
(λi.e) e' ~~~~~~> output
-----
^ program proper</code></pre></li>
</ul>
<ol start="3" style="list-style-type: decimal">
<li><p>Define a notion of reduction: <code>β</code> and <code>β-value</code></p>
<p>βᵥ: (λx.e)v ~> e[x←v]</p></li>
<li><p>Uniformly crate a calculus <code>=ₓ</code> from the notions of reduction.</p>
<p><code>=ₙ</code> from β and <code>=ᵥ</code> from β and βᵥ</p></li>
</ol>
<p>A way to equating arbitrary program fragments.</p>
<ol start="5" style="list-style-type: decimal">
<li><p>Define a semantics from <code>=ₓ</code></p>
<p>evalₓ ∈ 𝒫(Program × Value)</p>
<p>e evalₓ v 𝑖𝑓𝑓 e =ₓ x</p></li>
<li><p>Prove that <code>evalₓ</code> is a function.</p></li>
</ol>
<p>Via Church-Rosser Lemma, <code>evalˣ</code> is a (partial) function</p>
<pre><code> evalₓ(e) ≔ { n for "base" value
| 'closure for λ-expression }</code></pre>
<p>You can now prove things like:</p>
<pre><code> e (Y e) =ₙ Y e</code></pre>
<p>Computation should be directed, which for now is not specified, and problematic.</p>
<ol start="7" style="list-style-type: decimal">
<li><p>Prove that <code>=ₓ</code> satisfies a "standardization" property:</p>
<p>𝑖𝑓 e =ₓ e' 𝑡ℎ𝑒𝑛 then you can do so in an algorithmic fashion</p></li>
</ol>
<p>An algorithm means you know how to pick the next redex.</p>
<p>The algorithm is the same for CBN and CBV.</p>
<p>"left-most outer-most strategy", 𝑖.𝑒. standard reduction. <code>|-->ₓ</code>.</p>
<p>A strategy is a meta-function for picking a redex.</p>
<p>"If all you care about is the value at the end, you can use standard reduction".</p>
<pre><code> evalₓ(e) = v 𝑖𝑓𝑓 e |-->ₓ* v</code></pre>
<p>Proof in Curry and Fays, Curry Fays theorem.</p>
<p>(Aside: you must give readers a guide for how to pronounce math notation! A reader should be able to read your paper aloud.)</p>
<p>We have two semantics, <code>evalₓ</code> based on standard reduction, and <code>=ₓ</code> based on equality.</p>
<p>Must prove that <code>evalₓSR</code> is the same function as <code>evalₓ=</code>.</p>
<p>CBN calculus inconsistent with CBV interpreter, CBV calculus inconsistent with CBN interpreter.</p>
<p>What do calculations on program mean?</p>
<ol style="list-style-type: decimal">
<li>(Syntactic) because you prove Church/Rosser, you know that calculations are consistent with the "fast" interpreter</li>
<li>(Semantic) via snippet from Jim Morris (63) dissertation, created polymorphic lambda calculus (PAL): introduce a relation known as observational equivalence.</li>
</ol>
<p><code>e ≃ e'</code> means for all ways of placing a term into a complete program (a context) called C, evalₓ(C[e]) ~ evalₓ(C[e'])</p>
<p>Two versions: <code>≃ₙ</code> and <code>≃ᵥ</code>. These are the largest possible consistent equivalence relations that let you calculate programs. Therefore they are unique (because they are larges). They are the <em>truth</em>.</p>
<p>Every programming language has "the truth" (<code>≃ₙ</code>) by virtue of having an interpreter. The goal is to make the proof system (<code>=ₓ</code>) consistent with the truth.</p>
<p>MF: "On the expressive power of programming languages", previous draft attempted to prove <code>≃ᵥ ⊆ ≃ₙ</code>, was proved different two months earlier.</p>
<p>CBV and CBN functional programming are not related other than in the syntax of the terms. CBN is not "a different strategy".</p>
<p>Laziness and CBN are related, by subset.</p>
<p>Q: what use is studying functional programming if programs aren't purely functional?</p>
<pre><code>(f (call/cc g)) ~ g(f)</code></pre>
<p>A calculus equation for a very imperative idea.</p>
<p>Technical insights: "evaluation context semantics" <em>use contexts instead of inference rules</em>.</p>
<pre><code>e β e'
--------- <-- inference rule
e =⸤β⸥ e'</code></pre>
<p>"Syntactic compatibility"</p>
<p>"left-most-outer-most"</p>
<p>Contexts:</p>
<pre><code>e ⩴ x | λx.e | e e
C ⩴ □ | λx.C | C e | e C</code></pre>
<p>one-hole contexts.</p>
<p><code>C[e]</code> "textually" put <code>e</code> into hole.</p>
<pre><code>(λx.□)(λy.y)
/ \
λ λ←←
| | ↑
□ ⋅→→</code></pre>
<p>with contexts:</p>
<pre><code>=⸤β⸥ : e =⸤β⸥ e' 𝑖𝑓𝑓 ∃ C,
e = C[(λx.e₀)e₁]
e' = C[e₀[x ←e₁]]</code></pre>
<p>Evaluation context:</p>
<pre><code>E ⩴ □ | E e</code></pre>
<p>Thm: E[(λx.e)e'] is the LMOM redex.</p>
<p>For CBV you need:</p>
<pre><code>E ⩴ □ | v E | E e</code></pre>
<p>You could also use:</p>
<pre><code>E ⩴ □ | e E | E v</code></pre>
<p>also left-most-outer-most!</p>
<pre><code>E[(λx.e)e'] |-->ₙ E[e[x←e']]</code></pre>
<p>fully describes CBN standard reduction.</p>
<pre><code>E[(λx.e)v] |-->ᵥ E[e[x←v]]</code></pre>
<p>fully describes CBV standard reduction.</p>
<p>"evaluation context semantics" should be called "standard reduction semantics".</p>
<p>Technical Insight 2:</p>
<pre><code>E[ THING v ]</code></pre>
<p><code>THING</code> can manipulate <code>E</code>, the evaluation context.</p>
<p>From this you can do side-effects, continuations, etc.</p>
<p>𝑒.𝑔.</p>
<pre><code>E[raise e] ~> raise e</code></pre>
<p>full equational system for exceptions:</p>
<pre><code>x | λx.e | ee | raise e</code></pre>
<p>calculation system:</p>
<pre><code>C[(λx.e)v] =ₑₓ C[e[x←v]]
C[E[raise e]] =ₑₓ C[raise e]</code></pre>
<p>These two rules give you a consistent Church/Rosser system for exceptions. Same two equations work for CBN.</p>
<p>Standard reduction:</p>
<pre><code>E[(λx.e)v] |-->ₑₓ E[e[x←v]]
E[E'[raise e]] |-->ₑₓ E[raise e] [ |-->ₑₓ raise e , as a coincidence ]</code></pre>
<p>Standard reduction for assignment:</p>
<pre><code>e = x | λx.e | e e | set! x e | letrec ((x v) ..) e
v = λx.e
E = □ | E e | v E | set! x E
(βₛₑₜ): (λx.e) v R letrec ((x v)) e
(x): letrec (.. (x v) ..) E[x] R letrec (.. (x v) ..) E[v]
(set!): letrec (.. (x v) ..) E[set! x u] R letrec (.. (x u) ..) E[λx.x]
(scope extrusion:)
E[letrec (...) e] R letrec (...) E[e]
(merge:)
letrec (.. (x v) ..) (letrec (.. (y u) ..) e) R letrec (.. (x v) .. .. (y u) ..) e</code></pre>
<p>You can calculate in parallel, but standard reduction doesn't capture parallel execution.</p>
<p>Technical Insight 3:</p>
<pre><code>t: E[(λx.e)e'] = Pₜ
t+1: E[e[x←e']] = Pₜ₊₁</code></pre>
<p>Idea: separate <code>E</code> from the expression where the "machine" is looking for a redex.</p>
<p>Two register machine: control and stack registers:</p>
<pre><code>⟨e,E⟩</code></pre>
<p>Next idea: change data representation from context to stack:</p>
<pre><code>⟨e,[app₁]⟩
[app₂]
[app₃]
...</code></pre>
<p>Next idea: substitution is hard and inefficient. Make substitution lazy; reveals an explicit environment.</p>
<pre><code>control: e
environment: ρ mapping free-variables to values
stack: κ control stack</code></pre>
</body>
</html>