Differences between revisions 1 and 7 (spanning 6 versions)
Revision 1 as of 2010-05-13 18:18:36
Size: 16249
Editor: MengWang
Revision 7 as of 2010-05-13 18:21:59
Size: 99
Editor: MengWang
Deletions are marked like this. Additions are marked like this.
Line 1: Line 1:

                           by Alvaro Garcia Perez

                                                           October 23th 2009

We consider the evaluation of the pure untyped lambda-calculus (lCalc),
distinguishing "evaluators", which take a lCalc term and give another lCalc
term, from "interpreters", which take an lCalc term and give a value in a
domain different from lCalc terms. (The names "reducer" and "evaluator" could
have been used instead, but we do not use them because "evaluator" has the
same meaning than "reducer" in some contexts).

We are restricting ourselves to the case of the evaluators (take an lCalc term
and give another different y presumibly more reduced lCalc term). The abstract
syntax we are considering for the lCalc corresponds to the following fragment
of Haskell:

> data SLTTerm = Var String
> | Lam String SLTerm
> | App Term SLTerm

The different constructors represent variables, lambda-asbtractions (lAbs) and
applications repsectively. For this Haskell representation of the terms we can
give evaluators in Haskell, like the following one, which implements a
call-by-value evaluation order.

> evalCBV :: SLTerm -> SLTerm
> evalCBV v@(Var s) = v
> evalCBV l@(Lam v b) = l
> evalCBV (App m n) = let m' = evalCBV m
> n' = evalCBV n
> in case m' of
> (Lam v b) -> evalCBV $ subst v b n'
> _ -> App m' n'

This evaluator returns variables and lAbs without doing anything, for they not
need to be evaluated. It evaluates both the operand and the argument of
applications, distinguishing wether the evaluated operand is a lAbs and
returning the substitution of the argument for the bound variable in the body
of the lAbs in that case. Otherwise it returns the application of the
evaluated operand and the argument. We assume that |subst| is a function
implementing the capture avoiding subsitution of a variable for a term in
another term. This is enough for us and we will not be interested in
substitution and representations issues anymore in this minutes.

We can see this evaluator as a definitional evaluator if we consider (in a
rather abusive way) that Haskell is a sugared version of the lCalc. For this
kind of evaluators, [Rey72] noted that the semantics in the implementation
language (Haskell in our case) could interfere with the intended semantics for
the object language (the lCalc). If the implementation language have
non-strict semantics, then, the evaluator will impose non-strict semantics to
the object language, even if the intende ones (CBV) were strict. This cames
from the fact that is the implementation language who is really evaluating an
embeded representation of the object language. To get rid of this issue he
proposed the use of Continuation Passing Style (CPS), which amounts to
explicitly represent the computation which is next (the continuation) at a
particular point, applying it to the partial result at that point. This
increments the convolutedness of the evaluator, but resolves the semantics
preservation problem. [Plo75] gave simulations of CBV over call-by-name (CBN)
and vice versa using CPS.

Our previous CBV evaluator can be improved switching to a monadic style. This
lets the adoption of CPS as well as the use of some Haskell strict primitives
(through the selection of particular monads) to get rid of the semantics
preservation problem. The monadic CBV evaluator is as follows:

> evalCBV :: Monad m => SLTerm -> m SLTerm
> evalCBV v@(Var s) = return v
> evalCBV l@(Lam v b) = return l
> evalCBV (App m n) = do m' <- evalCBV m
> n' <- evalCBV n
> case m' of
> (Lam v b) -> evalCBV $ subst v b n'
> _ -> return $ App m' n'

The |let| clauses have been substituted by |<-| and |do| notation is used as
well. This monadic approach is semantics preserving only for some particular
selection of monads (or pseudo-monads), including |Cont|. We use this version
from this point on, assuming |Cont SLTerm SLTerm| will be used as the default
monad for the evaluators.

Considering other evaluation orders (as applicative-order) we realise that
evaluation is recursively invoked in some particular places in the
evaluators. It is possible to abstract those points as parameters of a generic
parametric evaluator. This evaluator will take some "smaller" evaluators
giving a particular evaluation strategy from them.

> type Ev m = SLTerm -> m SLTerm
> eval :: Monad m => Ev m -> Ev m -> Ev m ->
> Ev m -> Ev m -> Ev m
> eval la op1 ar1 op2 ar2 v@(Var s) = return v
> eval la op1 ar1 op2 ar2 (Lam v b) =
> do b' <- la b
> return $ Lam v b'
> eval la op1 ar1 op2 ar2 (App m n) =
> do m' <- op1 m
> case m' of
> (Lam v b) -> let su = eval la op1 ar1 op2 ar2
> in do n' <- ar1 n
> su $ subst v b n'
> _ -> do m'' <- op2 m
> n'' <- ar2 n
> return $ App m'' n''

This parametric evalautor can be instantiated into different evaluation orders
defining fix points where the evaluator is itself passed as parameter. Here we
present fix point definition for some well documented evaluation orders

> -- la op1 ar1 op2 ar2
> ---------------------------------------------
> aor = eval aor aor aor aor aor
> cbv = eval return cbv cbv cbv cbv
> cbn = eval return cbn return cbn return
> he = eval he he return he return

For every parameter, the |return| function (which is the identity function
lifted to the monadic world) or the fix point itself can occur. |aor| is
applicative-order, |cbv| is call-by-value, |cbn| is call-by-name and |he| is
head-spine [Ses02].

Note that the |op2| parameter is taking the unevaluated operator

> ...
> _ -> do m'' <- op2 m
> ...

instead of the result from the |op1| parameter. This is denotationally
accurate and make the parameters independent from each other, leading to a
generic evaluator with orthogonal parameters. A non-orthogonal version is
possible, where the result of |op1| is piped to the input of |op2|. This turns
the definition of the fix points slightly different, where |op1| and |op2| are
no longer independent and where some fix point definitions are equivalent. The
non-orthogonal version presents the adavantge of being operationally
accurate. This means that the evaluation of the operator is never done twice,
as would happen with the orthogonal version. Nevertheless, we will discuss the
orthogonal version, which is the most expressive of the two versions.

Def: We call uniform evaluation orders to those whose fix point definition
     uses only single-step recursion. Some others can be defined, using
     multiple-step recursion, and we call them hybrid evaluation orders.

> -- la op1 ar1 op2 ar2
> ----------------------------------------------------
> nor = eval nor cbn return (cbn >=> nor) nor
> ha = eval ha cbv ha (cbv >=> ha) ha
> hn = eval hn he return (he >=> hn) hn

With the hybrid evaluation orders, the two-staged nature of the evaluation in
the applications becomes clear, as they may use different evaluation orders in
the places of |op1| and |op2|. We are using composite paremters (through the
monadic composition operator |(>=>)|) for the |op2| operand, to denote that
the two evaluation stages take place (remember that for the orthogonal
version, the input of tue |op2| parameter is the unevaluated operator). This
is required for denotationally accuracy.

|nor| is normal-order, where |cbn| is used as subsidiary order. |ha| is
hybrid-applicative-order, which is an eager hybrid order taking |cbv| as
subsidiary order. |hn| is hybrid-normal-order, which is the analogous to
|nor|, but taking |he| as subsidiary order.

In order to reason about the hybrid evaluation orders we make the following
simplifiation. Let us consider only the parameter |la|, |ar1| and |ar2|, and
assume that |op1| = |op2| is the recursive occurrence of the fixpoint

Def: We say an evaluation order E is simplified if its definition is of the

     > la op1 ar1 op2 ar2
     > -------------------------------------------------
     > E = eval E_1 E E_2 E E_3

     where E_n can be return or E.

The parameter space then contains eight different uniform
evaluation orders.

> -- la ar1 ar2
> -------------------------------
> cbn = eval return return return
> ncbn = eval return return ncbn
> hcbv = eval return hcbv return
> cbv = eval return cbv cbv
> he = eval he return return
> fnor = eval fnor return fnor
> haor = eval haor haor return
> aor = eval aor aor aor

Def: We say an evaluation order is weaker-than other evaluation order if the
     parameters defining the former are weaker than the parameters defining
     the latter. We consider |return| as weaker than a recursive call.

Then we can arrange the eight evaluation orders into a cube (a lattice) where
the weakest order is |cbn| and the strongest one is |aor|. We call this the
beta-cube, after the concept beta-reduction.

aor <--------- haor
 ^ ^ ^ ^
 | \ | \
 | \ | \
 | fnor <---------- he
 | ^ | ^
 | | | |
 | | | |
cbv <-|------- hcbv |
  ^ | ^ |
   \ | \ |
    \ | \ |
    ncbn <--------- cbn

We consider the notions of normal forms each evaluation order is evaluating
to. We have normal form (NF), head normal form (HNF), weak normal form (WNF)
and weak head normal form (WHNF), defined as follows:

NF := \x.NF
      | x NF_1 ... NF_n, (where x is a free variable, NF_n are normal forms
                          and n >= 0)

HNF := \x.HNF
      | x T_1 ... T_n, (where x is a free variable, T_n are whatever
                        lambda-terms and n >= 0)

WNF := \x.T (where T is whatever lambda-term.)
      | x WNF_1 ... WNF_n (where x is a free vairable, WNF_n are weak normal
                           forms and n >= 0)

WHNF := \x. T (where T is whatever lambda-term)
      | x T_1 ... T_n (where T_n are whatever lambda-terms)

We consider also the strictness on the semantics of the evaluation orders. If
the result of a function applied to undefined leads always to unefined, then
we have strict semantics. Otherwise we have non-strict semnatics.

With this in mind we can rename the parameters the following way

|la| - non-weakness
|ar1| - strictness
|ar2| - non-headness

|la| and |ar2| indicating the normal form the evaluation order is evaluating
to, and |ar1| indicating if the evaluation order implements strict or
non-strict semantics.

|ncbn| is non-head-call-by-name. |hcbv| is head-call-by-value. |fnor| is
false-normal-order, which is like normal-order but prematurely evaluates inner
redexes in the operator of the applications. |haor| is head-applicative-order.

Def: We say an F is absorbent-to E (E and F evaluation oders) if E is a right
     identity of F, this is, for any termt T, (F o E) T = F T.

     (Note that the function composition operator (o) and monad composition
     operator (>=>) have opposite variances. Thus, (F o E) correspond to
     (E >=> F))

Def: We say H = hyb(E, F) is the hybridation of E and F (E and F uniform and
     simplified evaluation orders) if E is weaker than F and

     > la op1 ar1 op2 ar2
     > -------------------------------------------------
     > F = eval F_1 F F_2 F F_3
     > H = eval H_1 F H_2 (F o E) H_3

     where H_n = F_n, where the recursive occurrences of F in F_n range over H
     in H_n.

Absorption Theorem: hyb(E, F) is absorbent to E.

Proof: Consider the natural deduction rules that define cbn and nor. (We write
       -E-> for the binary relation induced by an evaluation order E between
       its input an its result)

               cbn | nor
1) |
           ---------- | ----------
           x -cbn-> x | x -nor-> x
2) | B -nor-> B'
        ---------------- | -----------------
        \x.B -cbn-> \x.B | \x.B -nor-> \x.B'
3) |
M-cbn->(M'=\x.B),(subst B x N)-cbn->B' | M -cbn-> (M'=\x.B), N -nor-> N',
-------------------------------------- | (subst B x N) -nor-> B'
           M N -cbn-> B' | --------------------------------
                                       | M N -nor-> B'
4) M -cbn-> (M' =/= (\x.B)) | M-cbn->(M' =/= (\x.B)), M'-nor-> M'',
     ----------------------- | N -nor-> N'
         M N -cbn-> M'N | -------------------------------------
                                       | M N -cbn-> M' N'

       Then it follows inductively on the structure of the derivation that nor
       is absorbent to cbn. For the rules 1) 2) and 4) this is direct. For the
       rule 3) we use the induction hpothesis.

       Every other possible pair of subsidiary and hybrid orders leads to the
       same inductive proof. The substitution is what makes the proof hard,
       but both the hybrid and the subsidiary evaluation orders use the same
       evaluation order for |op1|. For the evaluation of the substitution the
       hypothesis is enough.

This theorem induces us to think that the following definitions for nor are

> -- la op1 ar1 op2 ar2
> ----------------------------------------------------
> cbn = eval return cbn return cbn return
> nor = eval nor cbn return (cbn >=> nor) nor
> nor' = eval nor' cbn return nor' nor'

because we know that (cbn >=> nor) T = nor T. But this does not have to be
generally true, because in the definitions above nor =/= nor', as they are
different fix points. It is possible true but further poorf regarding fix
point issues must be done.

We expect that the hybridation operation and the absorption theorem can be
extended to the case where the evaluation orders being hybridated are not
uniform and simplified. This requires to extend the definition of the
weaker-than realtion to the infinite space induced by multiple-step recursion
definitions and extend the proof as well.


  author = "John Reynolds",
  title = "Definitional Interpreters for Higher Order Programming
  booktitle = "ACM Conference Proceedings",
  pages = "717--740",
  publisher = "ACM",
  year = "1972",
  author = "G. D. Plotkin",
  title = "Call-by-name, Call-by-value and the Lambda Calculus",
  journal = "Theoretical Computer Science",
  volume = "1",
  year = "1975",
  pages = "125--159",
  author = "Peter Sestoft",
  title = "Demonstrating Lambda Calculus Reduction",
  booktitle = "The Essence of Computation: Complexity, Analysis,
                  Transformation. Essays Dedicated to Neil D. Jones, number
                  2566 in Lecture Notes in Computer Science",
  year = "2002",
  pages = "420--435",
  publisher = "Springer-Verlag",
by Alvaro Garcia Perez
October 23th 2009


None: Minutes20091023 (last edited 2010-05-13 18:21:59 by MengWang)