Section 7: Recursive Definitions and Environments 



We want to devise a λexpression (a program in LC) that computes the leastfixed point of any function mapping some set of data values S to itself. In simple cases, we can let S be the natural numbers or the integers. One of the most surprising properties of the lambdacalculus (LC) is that there are a multitude (countably infinite) number of fundamentally different functions (with regard to equivalence under βconversion [a finite sequence of applications of the β rule combined with changing variable names whenever convenient]) in the lambdacalculus that compute the leastfixed point of a function. Consider the λexpression
Y = λf. [λx. f (x x)] [λx. f (x x)]
(where square brackets are used as alternate notation for parentheses for improved readability). It is easy to show that Y behaves like a fixedpoint operator, i.e., that
f (Y f) = Y f.
Y is typically called the least fixedpoint combinator. In the λcalculus, λ expressions with no free variables are called combinators. If we perform βreduction on the term
f (Y f),
we get:
f (Y f) > f ([λx. f (x x)] [λx. f (x x)])
Similarly, if we perform two βreduction steps on the term
Y f,
we get:
Y f > (λx. f (x x)) (λx. f (x x))) > f ([λx. f (x x)] [λx. f (x x)])
In callbyname functional languages, the λexpression Y defines the leastfixedpoint operator that we defined in the last section of our notes.
Now consider the λexpression
B = λf. λx. f (x f x).
If we perform two βreduction steps on the term
B f B,
we get:
B f B > (λx. f (x f x)) B > f (B f B)
Hence,
Y' = λf. B f B
is another fixedpoint operator. It is easy to confirm that:
Y' f = f (Y' f)
Both the Y and Y' combinators take a function f and find its fixed point in callbyname languages (where βreduction is always valid). Suppose we want to find the fixed point of the function FACT defined by:
λfact. λn. if n = 0 then 1 else n*(fact n1)
Now we can apply the Y combinator to this function to get its fixedpoint (assuming callbyname):
Y FACT > (λx. FACT (x x)) (λx. FACT (x x)) > FACT ((λx. FACT (x x)) (λx. FACT (x x))) = λn. if n = 0 then 1 else n*((Y FACT) n1)
where the final term uses the "collapsed" notation (Y FACT) instead of its expansion using βreduction.
If we use Y' instead of Y, we can avoid the use of collapsed notation:
Y' FACT > B FACT B > (λx. FACT (x FACT x)) B > FACT (B FACT B) > > λn. if n = 0 then 1 else n*((B FACT B) n1)
Note that we must are presuming callbyname semantics here. Under callbyvalue βreduction
Y f > (λx. f (x x)) (λx. f (x x))) > f ([λx. f (x x)] [λx. f (x x)]) > f (f ([λx. f (x x)] [λx. f (x x)])) > ...
and
Y' f > B f B > f(B f B) > f(f(B f B)) ...
which both diverge. In callbyvalue computations involving Y, the evaluation of
(λx. f (x x)) (λx. f (x x)))
must be suspended by wrapping it in a &lambdaabstraction:
λz. [(λx. f (x x)) (λx. f (x x)) z]
Alternatively, in callbyvalue computations involving Y', the evaluation of
B f
must be suspended by wrapping it in a &lambdaabstraction:
λx. f (λn.(x f x) n)
We can work around the pathologies of callbyvalue semantics by defining appropriate variant of the Y [or Y'] combinator that constructs the leastfixed point of an argument function of the specified type using callbyvalue semantics. The trick is to wrap the term f (x x) [or (x f x)] in an appropriate ηconversion (which is explained below). By appropriate we mean an ηconversion of the same type as the domain (and range) of f. In the pure λcalculus, every value is a unary function, but in functional programming languages, the domain of f may be functions of some other arity or even a nonfunctional lazy domain like lazy lists.
In the pure λcalculus, there are no atomic constants like natural numbers or booleans. The only constants are unary λexpressions (functions). Hence, it is natural to assert for any term M that:
M = λx. M x
or equivalently (in Scheme notation)
M = (lambda (x) (M x))
The rewrite rule
M > λx. Mx
is called ηconversion. Technically, this rule can be applied in either direction (in contrast to βreduction), but it is typically used in the direction shown above.
In the pure λcalculus, there are no atomic constants like natural numbers or booleans. The only constants are unary λexpressions (functions). Hence, it is natural to assert for any term M that:
M = λx. Mx
or equivalently (in Scheme notation)
M = (lambda (x) (M x))
In models of the pure λcalculus, this rule is typically required to hold. But it is not implied by the equational axiom of (safe) βconversion. It clearly does not hold for atomic (nonfunctional) constants, e.g.
7 != λx. 7
If the term M denotes a binary function (as is possible in Scheme or multiary generalizations of the λcalculus), then
M = (lambda (x y) (M x y))
which is not the same equation as standard ηconversion. Note that the implied type of M is different in "binary" ηconversion than it is in conventional ηconversion.
In realistic functional languages, conventional ηconversion does not hold. Rather, a restricted form of ηconversion holds for each type T. In other words, the appropriate η conversion for M depends on the type of M.
We can use conventional ηconversion to transform the callbyname Y operator to a callbyvalue least fixedpoint operator for unary functions:
λf. [λx. λy. f (x x) y] [λx. λy. f (x x) y]
(Recall that application associates to the left in the &lambdacalculus.) Similarly, we can transform the callbyname Y' operator to a callbyvalue least fixedpoint operator for unary functions:
λf. B' f B'
where
B' = λf. λx. f (λn.(x f x) n).
For binary functions (functionals f mapping D x D > D into itself), Y has the form:
λf. [λx. λy,z. f (x x) y] [λx. λy,z. f (x x) y]
or, equivalently, in Scheme notation
(lambda (f) ((lambda (x) (lambda (y z) (f (x x) y))) (lambda (x) (lambda (y z) (f (x x) y)))))
Slogan: Definitions build environments.
Let us add a recursive binding mechanism (akin to let) to our language where we restrict righthand sides to lambda expressions.
(definestruct reclet (lhs ; variable rhs ; required to be a lambdaexpression body))
where lhs is the new local variable, rhs is the lambdaexpression defining the value of the new variable, and body is an expression that can use the new local variable. The new variable lhs is visible in both rhs and body. The code for it in the interpreter might look like
((reclet? M) ... (MEval (recletbody M) (extend env (recletlhs M) (makeclosure (recletrhs M) E))))
To turn the rhs expression of M into a recursive closure, we desire that E be exactly like the environment that we are in the process of constructing. In other words, we would like a special kind of environment, env*, with the following property:
env* = (extend env (recletlhs M) (makeclosure (recletrhs M) env*))
Using the following callbyname procedure
(define FENV (lambda (env*) (extend env (recletlhs M) (makeclosure (recletrhs M) env*))))
the equation for env* can be rewritten as
env* = (FENV env*)
which shows that we want the environment to be the fixedpoint of the function FENV (from environments to environments).
If environments are implemented as functions (symbol > Value), the definition of fixenv, the function that finds the fixedpoint of FENV (and any other function mapping environments to enviroments), is simple:
(define fixenv (lambda (F) (local [(define renv (F (lambda (id) (lookup id renv))))] renv)))
If Scheme were a callbyname functional language, the code would be even simpler:
(define fixenv (lambda (F) (local [(define renv (F renv))] renv)))
In a callbyname language where local is a recursive binding form (as in Scheme),
(local [(define renv (F renv))] renv)))
binds renv to a suspension (closure of no arguments). When renv is evaluated in the body of the local, the suspension evaluates (F renv) in the environment constructed by local, which includes the new binding of renv. Hence,
(fixenv FENV) = (local [(define renv (FENV renv))] renv) = (local [(define renv (extend env (recletlhs M) (makeclosure (recletrhs M) renv)))] renv)
If
M = (makereclet x proc ast),
then
(local [(define renv (extend env (recletlhs M) (makeclosure (recletrhs M) renv)))] renv) = (local [(define renv (extend env x (makeclosure proc renv)))] renv) = (define renv' (extend env (makeclosure proc renv'))) renv'
which is exactly the recursively defined environment that we need. The (callbyvalue) Scheme solution requires the expression
(lambda (id) (lookup id renv))
instead of renv because callbyvalue evaluation requires a lambda form to suspend evaluation. On inputs of type environment (symbol > Value), the function
(lambda (env) (lambda (id) (lookup id env))
is the identity function except on improper values of env (undefined, divergence, or errors). On improper values for env,
(lambda (id) (lookup id env))
is still a legal environment (which will blow up only if it is applied to an Id).
In the absence of this suspension trick, the evaluation of the right hand side of the definition
(define renv (extend env (recletlhs M) (makeclosure (recletrhs M) renv)))
in Scheme, blows up because renv has no value (is undefined) until the evaluation of the definition is complete. The suspension trick wraps the argument renv inside a λexpresssion without changing its meaning for proper values of env.
We have used the recursive binding mechanism local in Scheme (and callbyname Scheme) to implement reclet. Note that we have placed a strong requirement on the rhs of reclet in LC. Therefore, this interpreter does not completely explain how local works in Scheme.
We could write an interpreter in Scheme that uses the Y operator instead of explicit recursion to define renv. Of course, the standard Y operator presumes callbyname but we could use a callbyvalue variant of Y (which wraps f (x x) in an appropriate ηconversion) to make our interpreter work for conventional Scheme callbyvalue semantics. But this reduction only provides mathematical insight into the meaning of reclet. It does not embody a translation that we can directly use in mapping reclet to machine code. We will investigate this issue later in the course.
If we represent environments as structures, how do we write fixenv? We need to construct an environment that contains references to copies of itself. In a "lazy" functional language like Haskell or Miranda, we could easily build the required structures using "lazy" constructors that defer the evaluation of their arguments. For example if we added lazycons to LC, the code would
(reclet x (lazycons 0 x) ...)
define x as a list consisting of 0 followed by x.
Instead of storing a value in each field of the constructed structure, a lazy constructor stores a suspension specifying how to evaluate the field when it is needed. This is exactly the same mechanism used to support callbyname argument passing to program defined functions. Note that this approach formulates self referential environments as infinite data structures rather data structures with cycles.
In functional Scheme, we cannot use ordinary data structures (nonfunctions) to solve the recursion equation
env* = (FENV env*)
because these structures cannot be infinite. However, in imperative Scheme, we can create the the necessary selfreferences using cycles created by bruteforce. We can overwrite the environment field inside the new closure to point to the extended environment. If we adhere to the list representation of environments introduced in Lecture 4, we must abandon the explicit definition the fixenv operation because finding the references to env* that we have to patch in (FENV env*) is either impossible (if F uses constructors that we have not anticipated) or inefficient (because we have to traverse all of the data structure (F env*)).
Fortunately, we don't need a a general function fixenv for our interpreter; all we need is a function (recextend M env) that builds the fixedpoint for FENV:
(FENV (recextend M env)) = (recextend M env)
We can define recextend as follows
(define recextend (lambda (M env) (local [(define var (recletlhs M)) (define rhs (recletrhs M)) (define clsr (makeclosure rhs null)) (define renv (extend env var clsr))] ; Is renv the appropriate environment yet? No. (setclosureenv! clsr renv))))
Given the environment env and the reclet expression M of a function, (recextend env M) extends the environment with the new function binding in M such that the environment embedded in the function binding is the extended environment. The reclet clause of our interpreter can now be written
((reclet? M) ... (MEval (recletbody M) (recextend env M)))
Exercise: Devise a minor change to the representation of environments as structures that makes it easy to write a general fixenv function. 
Hint: Scheme boxes. 
In LC we restricted the right hand sides of recursive bindings to lambdaexpressions. What happens if we allow arbitrary expressions as right hand sides. To evaluate such a right hand side rhs, we must call (MEval rhs env*) where env* is our selfreferential environment. If this evaluation actually tries to lookup the value of var, the computation should abort because the value of var is still being computed. (DrScheme follows this convention, but unfortunately, it is left unspecified in the Scheme standard.) For LC, we can rewrite recextend to support this generalization as follows:
(define recextend (lambda (M env) (local [(define var (recletlhs M)) (define rhs (recletrhs M)) (define renv (extend env var (void)))] ; (void) is a dummy value for var ; Is renv the appropriate environment yet? No. (setfirstpairval! renv (MEval rhs renv))))) (define setfirstpairval! (lambda (env val) (local [(define firstpair (first env))] (setpairval! firstpair val))))
To make MEval abort on the inspection of (void) we also need to add the clause
[(void? M) (error 'MEval "variable referenced before definition in reclet")]
to the definition of MEval.
Exercise: Generalize the code from the previous exercise to allow an arbitrary expression as the right hand side of a reclet. 
Hint: It is much simpler than the code above. 
At this point in the course, we have explained several language constructs, such as procedures and applications, in terms of their Scheme counterparts. A notable exception is environments, which we have represented explicitly. Indeed, since we explicitly manage variablevalue associations in our interpreters, we can analyze some of the lowerlevel behavior of the language such as its memory management.
Consider the evaluation of
(let (x 1) (let (y 2) (let (z 3) ...)))
We begin with the empty environment; as we encounter each let, we add a new level to our environment; as we leave the let body, we remove that level. At the end of the entire expression, our environment will be empty again. Hence, our environment will have behaved like a stack. Do environments always behave in this manner?
Consider this expression:
((lambda (x) (lambda (y) (y x))) 10)
This evaluates to an ``apply to 10'' function. This expression
((lambda (z) (lambda (w) (+ z w))) 20)
evaluates to a procedure that adds 20 to its argument. If we apply the former to the latter, what happens to the environment at each stage?
We begin with the empty environment; the first application is performed and the environment is extended with the binding [x = 10]. The closure is now created, and the environment is emptied. Then we evaluate the second expression, which adds the binding [z = 20]. The second closure (call it C2) is produced, and the environment is emptied again.
At this point, we are ready to perform the desired application. When we do, the environment has the bindings [x = 10] and [y = C2]. Now C2 is applied, which has the effect of replacing the current environment with its own, which contains the bindings [z = 20]. The application adds the binding [w = 10], at which point the addition is performed, 30 is returned, and the environment is emptied again.
The moral of this example is that environments for LC programs, no matter how we choose to represent them, branch out like trees, and a simple stack discipline is insufficient for maintaining them. In many programming languages (such as Fortran, Pascal, and C/C++), it is often the programmer's job to manage memory and the collection of environments in existence at any point in the program must be representable by a stack. Such languages prohibit language constructions that can create a collection of environments that cannot represented by a stack. In our interpreters for LC, we have left the task of managing the storage for LC environments to Scheme's runtime system. Otherwise, our interpreters would have been much more complex programs.
Exercise: Impose restrictions on LC so that it remains a procedural language yet does not require a treebased management of environments 
Hint: Follow the example of Pascal. 
The Y combinator is not necessarily the best way to actually implement recursion. Nearly all functional languages build in a fixedpoint operator and use a conventional call stack to implement it. Of course, implementations of the Y combinator rely on the same call stack, but there are no cyclic data structures in the stack.
The new expression type is:
type debruijn = Cn of int  Vr of int  Lm of debruijn  Ap of debruijn * debruijn  Fi of debruijn
With substitution semantics for variable bindings, the semantics of this new language are:
exception Error of string;; let rec plus e m = match e with Cn i > Cn i  Vr n > Vr (if n<m then n else n+1)  Ap (e1,e2) > Ap (plus e1 m, plus e2 m)  Lm (e) > Lm (plus e (m+1))  Fi (e) > Fi (plus e (m+1)) let rec subst i v e = match e with Cn i > Cn i  Vr n > (if n==i then v else if n>i then Vr (n1) else Vr n)  Ap (e1,e2) > Ap (subst i v e1, subst i v e2)  Lm (e) > Lm (subst (i+1) (plus v 0) e)  Fi (e) > Fi (subst (i+1) (plus v 0) e) (* Bigstep semantics *) let rec ev5 e = match e with Cn i > Cn i  Vr x > raise (Error "Unbound variable")  Lm e' > e  Ap (e1,e2) > (match (ev5 e1) with Lm e > let v = ev5 e2 in ev5 (subst 0 v e)  _ > raise (Error "Applying nonfunction"))  Fi e' > ev5 (subst 0 (Fi e') e')
The expression Fi e evaluates the contained expression e with e bound to a variable. The substitution replaces occurrences of the newly bound variable with the expression Fi e, delaying evaluation until it is needed.
With environment semantics, we define the fixed point operator as follows:
type debValue = V_Cn of int  V_Lm of (debValue list) * debruijn  V_Fi of (debValue list) * debruijn let rec ev6 env e = match e with Cn i > V_Cn i  Vr 0 > (match env with v::vs > (match v with V_Fi (env',e') > ev6 (v::env') e'  _ > v)  _ > raise (Error "Unbound variable"))  Vr n > (match env with v::vs > ev6 vs (Vr (n1))  _ > raise (Error "Unbound variable"))  Lm e' > V_Lm (env, e')  Ap (e1,e2) > (match (ev6 env e1) with (V_Lm (env',e)) > let v = ev6 env e2 in ev6 (v::env') e  _ > raise (Error "Applying nonfunction"))  Fi e' > ev6 ((V_Fi (env, e'))::env) e'
The fixed point expression Fi e evaluates to the evaluation of e with Fi e bound in the environment. Again, the expression e, and not the result of evaluating this expression, is stored in the environment; evaluation is delayed until it is needed.
In the rest of these notes, we consider in Scheme some additional ways to implement recursive definitions.