16249
Comment:

← Revision 7 as of 20100513 18:21:59 ⇥
99

Deletions are marked like this.  Additions are marked like this. 
Line 1:  Line 1: 
EVALUATION OF THE LAMBDACALCULUS  GENERIC EVALUATORS by Alvaro Garcia Perez October 23th 2009 We consider the evaluation of the pure untyped lambdacalculus (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, lambdaasbtractions (lAbs) and applications repsectively. For this Haskell representation of the terms we can give evaluators in Haskell, like the following one, which implements a callbyvalue 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 nonstrict semantics, then, the evaluator will impose nonstrict 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 callbyname (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 pseudomonads), 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 applicativeorder) 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 applicativeorder, cbv is callbyvalue, cbn is callbyname and he is headspine [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 nonorthogonal 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 nonorthogonal 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 singlestep recursion. Some others can be defined, using multiplestep 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 twostaged 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 normalorder, where cbn is used as subsidiary order. ha is hybridapplicativeorder, which is an eager hybrid order taking cbv as subsidiary order. hn is hybridnormalorder, 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 definition. Def: We say an evaluation order E is simplified if its definition is of the form: > 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 weakerthan 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 betacube, after the concept betareduction. 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 lambdaterms and n >= 0) WNF := \x.T (where T is whatever lambdaterm.)  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 lambdaterm)  x T_1 ... T_n (where T_n are whatever lambdaterms) 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 nonstrict semnatics. With this in mind we can rename the parameters the following way la  nonweakness ar1  strictness ar2  nonheadness la and ar2 indicating the normal form the evaluation order is evaluating to, and ar1 indicating if the evaluation order implements strict or nonstrict semantics. ncbn is nonheadcallbyname. hcbv is headcallbyvalue. fnor is falsenormalorder, which is like normalorder but prematurely evaluates inner redexes in the operator of the applications. haor is headapplicativeorder. Def: We say an F is absorbentto 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)  Mcbn>(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))  Mcbn>(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 equivalent: >  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 weakerthan realtion to the infinite space induced by multiplestep recursion definitions and extend the proof as well. BIBLIOGRAPHY: @InProceedings{Rey72, author = "John Reynolds", title = "Definitional Interpreters for Higher Order Programming Languages", booktitle = "ACM Conference Proceedings", pages = "717740", publisher = "ACM", year = "1972", } @Article{Plo75, author = "G. D. Plotkin", title = "Callbyname, Callbyvalue and the Lambda Calculus", journal = "Theoretical Computer Science", volume = "1", year = "1975", pages = "125159", } @InProceedings{Ses02, 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 = "420435", publisher = "SpringerVerlag", } 
EVALUATION OF THE LAMBDACALCULUS  GENERIC EVALUATORS by Alvaro Garcia Perez October 23th 2009 
EVALUATION OF THE LAMBDACALCULUS  GENERIC EVALUATORS by Alvaro Garcia Perez October 23th 2009