Lecture 6: Recursive Definitions and Environments |
|
|
|
|
Slogan: Definitions build environments.
Let us add a recursive binding mechanism to our language where we restrict right-hand sides to lambda expressions. We extend our expression structure as follows:
type debruijnrec =
Cn of int
| Vr of int
| Lm of debruijnrec
| Ap of debruijnrec * debruijnrec
| RecLet of debruijnrec * debruijnrec
We then present a naive interpreter implementation for this expression:
type debValue =
V_Cn of int
| V_Lm of (debValue list) * debruijnrec
let rec ev5 env e =
match e with
Cn i -> V_Cn i
| Vr 0 ->
(match env with
v::vs -> v
| _ -> raise (Error "Unbound variable"))
| Vr n ->
(match env with
v::vs -> ev5 vs (Vr (n-1))
| _ -> raise (Error "Unbound variable"))
| Lm e' -> V_Lm (env, e')
| Ap (e1,e2) ->
(match (ev5 env e1) with
(V_Lm (env',e)) ->
let v = ev5 env e2 in
ev5 (v::env') e
| _ -> raise (Error "Applying non-function"))
| RecLet (e1,e2) ->
match e1 with
Lm e1' ->
ev5 ((ev5 env e1)::env) e2
(* We want env == (ev5 env e1)::env *)
| _ -> raise (Error "rec-let requires function in RHS")
Note that we want env == (ev5 env e1)::oldenv. That is, we want to find the fixed point of the environment. Using the following procedure
let fenv oldenv e env = (ext oldenv V_Lm (env,e))
the equation for env can be rewritten as
env = fenv oldenv e env
which shows that we want the environment to be the fixed-point of the function fenv (from environments to environments).
If environments are implemented as functions from numbers (Debruijn references) to values (fun int -> DebValue), we first need to make some changes to the core interpreter code. In particular, a closure value now has to take into account the new type of environment:
type debValueF =
V_Cn of int
| V_Lm of (int -> debValueF) * debruijnrec
We also define general functions for handling the environment:
let emptyenv i = raise (Error "Unbound variable") let ext env v = fun i -> if i = 0 then v else env (i-1) let lookup env i = env i
the definition of fix-env, the function that finds the fixed-point of fenv (and any other function mapping environments to enviroments), is simple:
let fix_env f env exp =
(let rec renv _ = f env exp (fun i -> (renv 0) i) in
renv 0)
This binds renv to a closure with a single parameter _. This parameter is never used, and is only here to delay evaluation of the right-hand side of the let rec. Similarly, on the right-hand side, the subexpression
(fun i -> lookup (renv 0) i)
serves to suspend evaluation of renv 0. Note that if OCaml was a call-by-name language, this could be replaced by (renv 0), since this subexpression would not yet be evaluated.
When renv is evaluated in the body of the let rec, the closure evaluates (f env exp (fun i -> (renv 0) i) in the environment constructed by let rec, which includes the new binding of renv. Hence,
fix-env fenv env exp
= let rec renv _ = fenv env exp (fun i -> lookup (renv 0) i) in
renv 0
= fenv env exp (fun i -> lookup (renv 0) i)
= ext env V_Lm ((fun i -> lookup (renv 0) i),e)
= fun i -> if i = 0 then V_Lm ((fun i -> lookup (renv 0) i),e) else env (i-1)
This is exactly the new recursively defined environment that we need.
the function
fun env i -> lookup env i
is an identity function except on improper values of env (undefined, divergence, or errors). On improper values for env,
fun i -> lookup env i
is still a legal environment (which will blow up only if it is applied. In the absence of this suspension trick, the evaluation of the right hand side of the definition eventually reaches
fenv env exp (renv 0)
in OCaml, this 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 closure without changing its meaning for proper values of env.
The evaluation function is now as follows:
let rec ev6 env e =
match e with
Cn i -> V_Cn i
| Vr n -> lookup env n
| 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 (ext env' v) e
| _ -> raise (Error "Applying non-function"))
| RecLet (e1,e2) ->
match e1 with
Lm e1' ->
ev6 (fix_env fenv env e1') e2
| _ -> raise (Error "rec-let requires function in RHS")
We have used the recursive binding mechanism let rec in OCaml to implement rec-let. Note that we have placed a strong requirement on the rhs of rec-let in LC. Therefore, this interpreter does not completely explain how let rec works in OCaml. We will give a more complete explanation later in the course.
| Challenge: Do we need OCaml's let rec to interpret rec-let from LC? |
| Hint: Take a look at the sample programs in1 and in2 for assignment 2. The book The Seasoned Schemer by Matthias Felleisen and Daniel Friedman contains an extensive discussion of the Y operator. |
If we represent environments as structures, how do we write fix-env? 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 lazy-cons to LC, the code would be
(rec-let x (lazy-cons 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 call-by-name 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 OCaml, we cannot use ordinary data structures (non-functions) to solve the recursion equation
env = fenv oldenv e env
because these structures cannot be infinite. However, in imperative OCaml, we can create the the necessary self-references using cycles created by brute-force. 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 fix-env operation because finding the references to env that we have to patch in fenv oldenv e env is either impossible (if fenv uses constructors that we have not anticipated) or inefficient (because we have to traverse all of the data structure fenv oldenv e env).
Fortunately, we don't need a general function fix-env for our interpreter; all we need is a code to build the fixed-point. We first redefine type debValue to include a void (undefined) value. We also must specify in the type declaration that a closure's (V_Lm's environment is a reference (and therefore mutable):
type debValueR =
V_Cn of int
| V_Lm of (debValueR list ref) * debruijnrec
| Void
Now, there are several changes required to the interpreter's evaluation function. First V_Lm takes an environment reference instead of an environment as a parameter; the environment must be boxed using the ref operator:
let rec ev7 env e =
match e with
Cn i -> V_Cn i
| Vr 0 ->
(match env with
v::vs -> v
| _ -> raise (Error "Unbound variable"))
| Vr n ->
(match env with
v::vs -> ev7 vs (Vr (n-1))
| _ -> raise (Error "Unbound variable"))
| Lm e' -> V_Lm (ref env, e')
Likewise, since V_Lm takes a reference to the closure environment, closure application must dereference this environment before evaluating the closure application. The dereference operator is !.
| Ap (e1,e2) ->
(match (ev7 env e1) with
(V_Lm (env',e)) ->
let v = ev7 env e2 in
ev7 (v::!env') e
| _ -> raise (Error "Applying non-function"))
Finally, on a RecLet, the correct recursive environment must be built:
| RecLet (e1,e2) ->
match e1 with
Lm e1' ->
let env' = ref (Void::env) in
First, a temporary environment is created.
let vlm = V_Lm(env',e1') in
The V_Lm is then created using this temporary environment
(env' := vlm::env;
The environment within the closure is now updated to contain the right-hand side.
ev7 !env' e2) | _ -> raise (Error "rec-let requires function in RHS")
This new environment is now also used to evaluate the let's internal expression. Note again that we use the ! operator to dereference this environment.
This code extends the environment with the new closure such that the environment embedded in the closure is the extended environment.
| Exercise: Devise a minor change to the representation of environments as structures that makes it easy to write a general fix-env function. |
| Hint: Change what gets boxed. |
In LC we restricted the right hand sides of recursive bindings to lambda-expressions. 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 self-referential 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 rec-extend to support this generalization as follows:
(define rec-extend
(lambda (M env)
(local
[(define var (rec-let-lhs M))
(define rhs (rec-let-rhs M))
(define renv (extend env var (void)))]
; (void) is a dummy value for var
; Is renv the appropriate environment yet? No.
(set-first-pair-val! renv (MEval rhs renv)))))
(define set-first-pair-val!
(lambda (env val)
(local
[(define first-pair (first env))]
(set-pair-val! first-pair 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 rec-let")]
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 rec-let. |
| Hint: It is much simpler than the code above. |
Say we have functions from R to R, where R denotes the set of real numbers. We might have a function like
f(x) = 2x + 1
The fixed-point of f is the value x such that x = f(x). Hence, x = 2 x + 1, implying that the fixed-point x = -1.
Does every function from R to R have a fixed-point? No: consider g(x) = x + 1. Substituting x and reducing, we get 0 = 1, which is a contradiction. On the other hand, h(x) = x has an infinite number of solutions. Hence, a function from R to R could have zero, one, several, or an infinite number of fixed-points. However, we will show that for every function from environments to environments, we can construct a fixed-point.
We can use fixed-points to assign a mathematical meaning to any recursive definition expressed in a computational framework. For example, we can assign a mathematical meaning to any recursive definition of a function in terms of already defined functions.
Consider the equation
fact(n) = if zero?(n) then 1 else n * fact(n - 1)
over the natural numbers N = {0, 1, 2, ...} where the primitive functions zero?, *, -, and if-then-else have their usual meaning. The defined function
fact
obviously must satisfy the equation
fact = map n to if zero?(n) then 1 else n * fact(n - 1)
which is mathematically equivalent to being a fixed-point of the functional FACT defined by the non-recursive equation
FACT(f) = map n to if zero?(n) then 1 else n * f(n - 1)
How do we find the fixed-point of such an equation? We interpret F as an inductive definition of the graph of the partial function fix(F).
A partial function mapping N to N is any a subset G of N x N such that (a,b) in G and (a,c) in G imply that b = c. A (total) function mapping N to N is a partial function F such that for every a in N, there exists b such that (a,b) in F. Computed functions correspond to partial functions rather than total functions because they may diverge on some inputs.
We use the term graph of a function to indicate that we are interpreting the function simply as a set of ordered pairs.
Let us restate the definition of the fixed-point fact of FACT as an inductive definition of the graph of a function.
Given a, b in N, the pair (a,b) belongs to the graph of fact iff either:
All of the inductive data definitions presented in Comp 210 can be interpreted in exactly the same way. Each data definition specifies a function D mapping sets to sets. The set specfied by the definition is the least set d such that D(d) = d.
How is the fixed-point of a function F mapping sets over N to sets over N constructed? By repeatedly applying the function F to the empty set. The fixed-point f of F is
Union {Fk(empty) | k = 0,1,...}
where Fk(empty) is k applications of F to empty: F(F(F( ... F(empty)...))) and F0(empty) = empty.
Consider the FACT example above.
FACT1(empty) = {(0,1)}
FACT2(empty) = {(0,1), (1,1)}
FACT3(empty) = {(0,1), (1,1), (2,2)}
...
FACTN+1(empty) = {(0,1), (1,1), (2,2), ..., (N,N!)}
...
Each additional application of FACT permits the recursive evaluation of our equation defining fact to go one level deeper. FACT1 is the function computed by the equation for fact if the first recursive call diverges. FACTN is the function computed by the equation if the Nth recursive call (in depth) diverges.
Any recursive definition of a function from N to N can be interpreted in this way. How do we apply this idea to solving our recursion equation over environments? If we represent envivronments as functions, then exactly the same technique works. The only difference is that the function FENV maps environments to environments instead of N to N.
If environments are represented some other way, then the representation must permit us to find a non-empty least fixed-point for FENV. Otherwise, the representation is incorrect.
Consider the function FADD on sets of N defined by
FADD(S) = {s+1 | s in S}
What is its least fixed-point? The emtpy set! In a computational setting every computable function mapping a data domain D (e.g., N, sets over N, functions over N) into D has a least fixed-point. But the fixed-point may be the trivial "empty" element of D. By definition, a computational data domain must be a partial order with a least element that contains the limits of infinite ascending chains of elements. Similarly, any computable function over such a domain must preserve limits of ascending chains (continuity). It is not difficult to prove that every continuous function f on a domain D has a least fixed point: it the limit (least upper bound) of the ascending chain empty, f(empty), f(f(empty)), ... Consider the recursive definition
x = x + 1
over N. What is the "least" element of N satisfying this equation? There is no conventional natural number that suffices. But the computational analog of the set N includes one additional element, called bottom, which is the meaning of a non-terminating computation. Does the equation
bottom = bottom + 1
hold? Yes! Both sides of the equation represent non-termination.
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 variable-value associations in our interpreters, we can analyze some of the lower-level 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 run-time 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 tree-based management of environments |
| Hint: Follow the example of Pascal. |