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 attachment:filename, as shown below in the list of files. Do NOT use the URL of the [get] link, since this is subject to change and can break easily.
  • [get | view] (2010-05-13 18:29:01, 15.5 KB) [[attachment:Talk.txt]]
  • [get | view] (2009-06-19 17:51:01, 340.8 KB) [[attachment:alvaro_garcia_20090529.pdf]]
  • [get | view] (2009-06-15 15:06:09, 231.6 KB) [[attachment:alvaro_garcia_20090612.pdf]]
  • [get | view] (2009-06-22 14:42:05, 1513.8 KB) [[attachment:tom_gadts.pdf]]
 All files | Selected Files: delete move to page copy to page

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