Lecture 6, Comp 311

Recursive Definitions and Environments

Slogan: Definitions build environments.

Let us add a recursive binding mechanism to our language. We can represent its abstract syntax with the following data definition:

(define-struc rec-let (lhs   ; variable
		       rhs   ; required to be a lambda-expression
		       body))

((rec-let? M) ... (Interp (rec-let-body M)
		    (extend env
		      (rec-let-lhs M)
		      (make-closure (rec-let-rhs M) E))))

env* = (extend env (rec-let-lhs M) (make-closure (rec-let-rhs M) env*))

Using the following procedure

(define FENV
  (lambda (env*)
    (extend env (rec-let-lhs M) (make-closure (rec-let-rhs M) env*))))

env* = (FENV env*)

Detour: Finding Fixed-Points

Say we have functions from R to R. We might have a function like

f(x) = 2x + 1

Does every function from R to R have a fixed-point? No: consider g(x) = x + 1. Substituting xf 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 or an infinite number of fixed-points. However, 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]

fact

fact = map n to if zero?[n] then 1 else n * fact[n - 1]

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 set fact iff either:

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

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!)}
...

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}

x = x + 1

bottom = bottom + 1

Environments via Functions

If environments are implemented as functions, the definition of fix-env, the function that finds the fixed-point of FENV (and any other function mapping environments to enviroments), is straightforward:

(define fix-env
  (lambda (F)
    (local
       [(define renv (F (lambda (id) (lookup id renv))))]
      renv)))

(define fix-env
  (lambda (F)
    (local
       [(define renv (F renv))]
      renv)))

(lambda (id) (lookup id renv))

(local
   [(define renv (F renv))]
  renv)))

So we have used the recursive binding mechanism local in Scheme 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 local works in Scheme.

Hint: Take a look at Y.

Environments via Structures

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. Instead of storing a value in each field of the constructed structure, a lazy constructor stores a suspsension 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.

In functional Scheme, we cannot use ordinary, non-functional data structures to solve the recursion equation

env* = (FENV env*)

(FENV (rec-extend M env)) = (rec-extend M env)

(define rec-extend
  (lambda (M env)
    (local 
       [(define var (rec-let-lhs M))
        (define rhs (rec-let-rhs M))
        (define clsr (make-closure var rhs null))
	(define renv (extend env (rec-let-lhs M) clsr))]
      ; Is renv the appropriate environment yet?  No.
      (set-closure-env! clsr renv))))

Given the environment env and the rec-let expression M of a function, (rec-extend 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 rec-let clause of our interpreter can now be written

((rec-let? M) ... (Interp (rec-let-body M) (rec-extend env M)))

Memory Management, Part 0

So far we have understood several things, such as procedures and applications, in terms of their Scheme counterparts. A notable exception is environments, which we have represented explicitly. Indeed, due to this explicit management of variable-value associations, we can analyze such lower-level aspects of the language as its memory management.

Consider the evaluation of

(let (x 1)
  (let (y 2)
    (let (z 3)
      ...)))

Consider this expression:

((lambda (x) (lambda (y) (y x))) 10)

((lambda (z) (lambda (w) (+ z w))) 20)

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 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. It is often the programmer's job to keep track of memory; in our presentation, we have left this task to Scheme's run-time system. Hence, this is another manner in which we have modeled LC by appealing to the underlying implementation in Scheme.