## Attachment 'Talk.txt'

Download```
1 EVALUATION OF THE LAMBDA-CALCULUS - GENERIC EVALUATORS
2
3 by Alvaro Garcia Perez
4
5 October 23th 2009
6
7 We consider the evaluation of the pure untyped lambda-calculus (lCalc),
8 distinguishing "evaluators", which take a lCalc term and give another lCalc
9 term, from "interpreters", which take an lCalc term and give a value in a
10 domain different from lCalc terms. (The names "reducer" and "evaluator" could
11 have been used instead, but we do not use them because "evaluator" has the
12 same meaning than "reducer" in some contexts).
13
14 We are restricting ourselves to the case of the evaluators (take an lCalc term
15 and give another different y presumibly more reduced lCalc term). The abstract
16 syntax we are considering for the lCalc corresponds to the following fragment
17 of Haskell:
18
19 > data SLTTerm = Var String
20 > | Lam String SLTerm
21 > | App Term SLTerm
22
23 The different constructors represent variables, lambda-asbtractions (lAbs) and
24 applications repsectively. For this Haskell representation of the terms we can
25 give evaluators in Haskell, like the following one, which implements a
26 call-by-value evaluation order.
27
28 > evalCBV :: SLTerm -> SLTerm
29 > evalCBV v@(Var s) = v
30 > evalCBV l@(Lam v b) = l
31 > evalCBV (App m n) = let m' = evalCBV m
32 > n' = evalCBV n
33 > in case m' of
34 > (Lam v b) -> evalCBV $ subst v b n'
35 > _ -> App m' n'
36
37 This evaluator returns variables and lAbs without doing anything, for they not
38 need to be evaluated. It evaluates both the operand and the argument of
39 applications, distinguishing wether the evaluated operand is a lAbs and
40 returning the substitution of the argument for the bound variable in the body
41 of the lAbs in that case. Otherwise it returns the application of the
42 evaluated operand and the argument. We assume that |subst| is a function
43 implementing the capture avoiding subsitution of a variable for a term in
44 another term. This is enough for us and we will not be interested in
45 substitution and representations issues anymore in this minutes.
46
47 We can see this evaluator as a definitional evaluator if we consider (in a
48 rather abusive way) that Haskell is a sugared version of the lCalc. For this
49 kind of evaluators, [Rey72] noted that the semantics in the implementation
50 language (Haskell in our case) could interfere with the intended semantics for
51 the object language (the lCalc). If the implementation language have
52 non-strict semantics, then, the evaluator will impose non-strict semantics to
53 the object language, even if the intende ones (CBV) were strict. This cames
54 from the fact that is the implementation language who is really evaluating an
55 embeded representation of the object language. To get rid of this issue he
56 proposed the use of Continuation Passing Style (CPS), which amounts to
57 explicitly represent the computation which is next (the continuation) at a
58 particular point, applying it to the partial result at that point. This
59 increments the convolutedness of the evaluator, but resolves the semantics
60 preservation problem. [Plo75] gave simulations of CBV over call-by-name (CBN)
61 and vice versa using CPS.
62
63 Our previous CBV evaluator can be improved switching to a monadic style. This
64 lets the adoption of CPS as well as the use of some Haskell strict primitives
65 (through the selection of particular monads) to get rid of the semantics
66 preservation problem. The monadic CBV evaluator is as follows:
67
68 > evalCBV :: Monad m => SLTerm -> m SLTerm
69 > evalCBV v@(Var s) = return v
70 > evalCBV l@(Lam v b) = return l
71 > evalCBV (App m n) = do m' <- evalCBV m
72 > n' <- evalCBV n
73 > case m' of
74 > (Lam v b) -> evalCBV $ subst v b n'
75 > _ -> return $ App m' n'
76
77 The |let| clauses have been substituted by |<-| and |do| notation is used as
78 well. This monadic approach is semantics preserving only for some particular
79 selection of monads (or pseudo-monads), including |Cont|. We use this version
80 from this point on, assuming |Cont SLTerm SLTerm| will be used as the default
81 monad for the evaluators.
82
83 Considering other evaluation orders (as applicative-order) we realise that
84 evaluation is recursively invoked in some particular places in the
85 evaluators. It is possible to abstract those points as parameters of a generic
86 parametric evaluator. This evaluator will take some "smaller" evaluators
87 giving a particular evaluation strategy from them.
88
89 > type Ev m = SLTerm -> m SLTerm
90 > eval :: Monad m => Ev m -> Ev m -> Ev m ->
91 > Ev m -> Ev m -> Ev m
92 > eval la op1 ar1 op2 ar2 v@(Var s) = return v
93 > eval la op1 ar1 op2 ar2 (Lam v b) =
94 > do b' <- la b
95 > return $ Lam v b'
96 > eval la op1 ar1 op2 ar2 (App m n) =
97 > do m' <- op1 m
98 > case m' of
99 > (Lam v b) -> let su = eval la op1 ar1 op2 ar2
100 > in do n' <- ar1 n
101 > su $ subst v b n'
102 > _ -> do m'' <- op2 m
103 > n'' <- ar2 n
104 > return $ App m'' n''
105
106 This parametric evalautor can be instantiated into different evaluation orders
107 defining fix points where the evaluator is itself passed as parameter. Here we
108 present fix point definition for some well documented evaluation orders
109
110 > -- la op1 ar1 op2 ar2
111 > ---------------------------------------------
112 > aor = eval aor aor aor aor aor
113 > cbv = eval return cbv cbv cbv cbv
114 > cbn = eval return cbn return cbn return
115 > he = eval he he return he return
116
117 For every parameter, the |return| function (which is the identity function
118 lifted to the monadic world) or the fix point itself can occur. |aor| is
119 applicative-order, |cbv| is call-by-value, |cbn| is call-by-name and |he| is
120 head-spine [Ses02].
121
122 Note that the |op2| parameter is taking the unevaluated operator
123
124 > ...
125 > _ -> do m'' <- op2 m
126 > ...
127
128 instead of the result from the |op1| parameter. This is denotationally
129 accurate and make the parameters independent from each other, leading to a
130 generic evaluator with orthogonal parameters. A non-orthogonal version is
131 possible, where the result of |op1| is piped to the input of |op2|. This turns
132 the definition of the fix points slightly different, where |op1| and |op2| are
133 no longer independent and where some fix point definitions are equivalent. The
134 non-orthogonal version presents the adavantge of being operationally
135 accurate. This means that the evaluation of the operator is never done twice,
136 as would happen with the orthogonal version. Nevertheless, we will discuss the
137 orthogonal version, which is the most expressive of the two versions.
138
139 Def: We call uniform evaluation orders to those whose fix point definition
140 uses only single-step recursion. Some others can be defined, using
141 multiple-step recursion, and we call them hybrid evaluation orders.
142
143 > -- la op1 ar1 op2 ar2
144 > ----------------------------------------------------
145 > nor = eval nor cbn return (cbn >=> nor) nor
146 > ha = eval ha cbv ha (cbv >=> ha) ha
147 > hn = eval hn he return (he >=> hn) hn
148
149 With the hybrid evaluation orders, the two-staged nature of the evaluation in
150 the applications becomes clear, as they may use different evaluation orders in
151 the places of |op1| and |op2|. We are using composite paremters (through the
152 monadic composition operator |(>=>)|) for the |op2| operand, to denote that
153 the two evaluation stages take place (remember that for the orthogonal
154 version, the input of tue |op2| parameter is the unevaluated operator). This
155 is required for denotationally accuracy.
156
157 |nor| is normal-order, where |cbn| is used as subsidiary order. |ha| is
158 hybrid-applicative-order, which is an eager hybrid order taking |cbv| as
159 subsidiary order. |hn| is hybrid-normal-order, which is the analogous to
160 |nor|, but taking |he| as subsidiary order.
161
162 In order to reason about the hybrid evaluation orders we make the following
163 simplifiation. Let us consider only the parameter |la|, |ar1| and |ar2|, and
164 assume that |op1| = |op2| is the recursive occurrence of the fixpoint
165 definition.
166
167 Def: We say an evaluation order E is simplified if its definition is of the
168 form:
169
170 > la op1 ar1 op2 ar2
171 > -------------------------------------------------
172 > E = eval E_1 E E_2 E E_3
173
174 where E_n can be return or E.
175
176 The parameter space then contains eight different uniform
177 evaluation orders.
178
179 > -- la ar1 ar2
180 > -------------------------------
181 > cbn = eval return return return
182 > ncbn = eval return return ncbn
183 > hcbv = eval return hcbv return
184 > cbv = eval return cbv cbv
185 > he = eval he return return
186 > fnor = eval fnor return fnor
187 > haor = eval haor haor return
188 > aor = eval aor aor aor
189
190 Def: We say an evaluation order is weaker-than other evaluation order if the
191 parameters defining the former are weaker than the parameters defining
192 the latter. We consider |return| as weaker than a recursive call.
193
194 Then we can arrange the eight evaluation orders into a cube (a lattice) where
195 the weakest order is |cbn| and the strongest one is |aor|. We call this the
196 beta-cube, after the concept beta-reduction.
197
198 aor <--------- haor
199 ^ ^ ^ ^
200 | \ | \
201 | \ | \
202 | fnor <---------- he
203 | ^ | ^
204 | | | |
205 | | | |
206 cbv <-|------- hcbv |
207 ^ | ^ |
208 \ | \ |
209 \ | \ |
210 ncbn <--------- cbn
211
212 We consider the notions of normal forms each evaluation order is evaluating
213 to. We have normal form (NF), head normal form (HNF), weak normal form (WNF)
214 and weak head normal form (WHNF), defined as follows:
215
216 NF := \x.NF
217 | x NF_1 ... NF_n, (where x is a free variable, NF_n are normal forms
218 and n >= 0)
219
220 HNF := \x.HNF
221 | x T_1 ... T_n, (where x is a free variable, T_n are whatever
222 lambda-terms and n >= 0)
223
224 WNF := \x.T (where T is whatever lambda-term.)
225 | x WNF_1 ... WNF_n (where x is a free vairable, WNF_n are weak normal
226 forms and n >= 0)
227
228 WHNF := \x. T (where T is whatever lambda-term)
229 | x T_1 ... T_n (where T_n are whatever lambda-terms)
230
231 We consider also the strictness on the semantics of the evaluation orders. If
232 the result of a function applied to undefined leads always to unefined, then
233 we have strict semantics. Otherwise we have non-strict semnatics.
234
235 With this in mind we can rename the parameters the following way
236
237 |la| - non-weakness
238 |ar1| - strictness
239 |ar2| - non-headness
240
241 |la| and |ar2| indicating the normal form the evaluation order is evaluating
242 to, and |ar1| indicating if the evaluation order implements strict or
243 non-strict semantics.
244
245 |ncbn| is non-head-call-by-name. |hcbv| is head-call-by-value. |fnor| is
246 false-normal-order, which is like normal-order but prematurely evaluates inner
247 redexes in the operator of the applications. |haor| is head-applicative-order.
248
249 Def: We say an F is absorbent-to E (E and F evaluation oders) if E is a right
250 identity of F, this is, for any termt T, (F o E) T = F T.
251
252 (Note that the function composition operator (o) and monad composition
253 operator (>=>) have opposite variances. Thus, (F o E) correspond to
254 (E >=> F))
255
256 Def: We say H = hyb(E, F) is the hybridation of E and F (E and F uniform and
257 simplified evaluation orders) if E is weaker than F and
258
259 > la op1 ar1 op2 ar2
260 > -------------------------------------------------
261 > F = eval F_1 F F_2 F F_3
262 > H = eval H_1 F H_2 (F o E) H_3
263
264 where H_n = F_n, where the recursive occurrences of F in F_n range over H
265 in H_n.
266
267 Absorption Theorem: hyb(E, F) is absorbent to E.
268
269 Proof: Consider the natural deduction rules that define cbn and nor. (We write
270 -E-> for the binary relation induced by an evaluation order E between
271 its input an its result)
272
273 cbn | nor
274 -----------------------------------------------------------------------------
275 1) |
276 ---------- | ----------
277 x -cbn-> x | x -nor-> x
278 |
279 2) | B -nor-> B'
280 ---------------- | -----------------
281 \x.B -cbn-> \x.B | \x.B -nor-> \x.B'
282 |
283 3) |
284 M-cbn->(M'=\x.B),(subst B x N)-cbn->B' | M -cbn-> (M'=\x.B), N -nor-> N',
285 -------------------------------------- | (subst B x N) -nor-> B'
286 M N -cbn-> B' | --------------------------------
287 | M N -nor-> B'
288 |
289 4) M -cbn-> (M' =/= (\x.B)) | M-cbn->(M' =/= (\x.B)), M'-nor-> M'',
290 ----------------------- | N -nor-> N'
291 M N -cbn-> M'N | -------------------------------------
292 | M N -cbn-> M' N'
293
294 Then it follows inductively on the structure of the derivation that nor
295 is absorbent to cbn. For the rules 1) 2) and 4) this is direct. For the
296 rule 3) we use the induction hpothesis.
297
298 Every other possible pair of subsidiary and hybrid orders leads to the
299 same inductive proof. The substitution is what makes the proof hard,
300 but both the hybrid and the subsidiary evaluation orders use the same
301 evaluation order for |op1|. For the evaluation of the substitution the
302 hypothesis is enough.
303
304 This theorem induces us to think that the following definitions for nor are
305 equivalent:
306
307 > -- la op1 ar1 op2 ar2
308 > ----------------------------------------------------
309 > cbn = eval return cbn return cbn return
310 > nor = eval nor cbn return (cbn >=> nor) nor
311 > nor' = eval nor' cbn return nor' nor'
312
313 because we know that (cbn >=> nor) T = nor T. But this does not have to be
314 generally true, because in the definitions above nor =/= nor', as they are
315 different fix points. It is possible true but further poorf regarding fix
316 point issues must be done.
317
318 We expect that the hybridation operation and the absorption theorem can be
319 extended to the case where the evaluation orders being hybridated are not
320 uniform and simplified. This requires to extend the definition of the
321 weaker-than realtion to the infinite space induced by multiple-step recursion
322 definitions and extend the proof as well.
323
324 BIBLIOGRAPHY:
325
326 @InProceedings{Rey72,
327 author = "John Reynolds",
328 title = "Definitional Interpreters for Higher Order Programming
329 Languages",
330 booktitle = "ACM Conference Proceedings",
331 pages = "717--740",
332 publisher = "ACM",
333 year = "1972",
334 }
335 @Article{Plo75,
336 author = "G. D. Plotkin",
337 title = "Call-by-name, Call-by-value and the Lambda Calculus",
338 journal = "Theoretical Computer Science",
339 volume = "1",
340 year = "1975",
341 pages = "125--159",
342 }
343 @InProceedings{Ses02,
344 author = "Peter Sestoft",
345 title = "Demonstrating Lambda Calculus Reduction",
346 booktitle = "The Essence of Computation: Complexity, Analysis,
347 Transformation. Essays Dedicated to Neil D. Jones, number
348 2566 in Lecture Notes in Computer Science",
349 year = "2002",
350 pages = "420--435",
351 publisher = "Springer-Verlag",
352 }
```

## Attached Files

To refer to attachments on a page, use**, as shown below in the list of files. Do**

`attachment:filename`**NOT**use the URL of the

`[get]`link, since this is subject to change and can break easily.

You are not allowed to attach a file to this page.