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",
}