Programming Languages -- Spring '98

Homework 4 (honors part): Reduction

Reduction

Having implemented a general substitution procedure subst*, (subst.ss) you are ready to start working on reduction. Why have we spent so much time on substitution? To answer this question, let's try to understand what a lambda calculus expression means.

Each programming language has two aspects. The syntax tells us what sequences of characters constitute valid programs or expressions in the language. BNF grammars give us a convinient way to represent the syntax of a language. The syntax defines the static structure of the language and by itself will never clarify what a particular program does. The semantics, on the other hand, defines the dynamic (run-time) behaviour of a program. It gives meaning to syntactically correct programs by associating them with values, describing a sequence of simplifying transformations that programs can go through, or by defining how the state of the underlying computer changes as the program is executing.

Let's forget for a moment that we have base values (numbers) in our lambda calculus. What can a lambda calculus expression mean? Since there are no base values floating around, we can't associate expressions with simple values. The approach that we will take specifies how a given program can be simplified or transformed to another equivalent program. A meaning of a program is then the sequence of transformations that lead us from the original program to some equivalent program that cannot be reduced any further. We say that these unreducible expressions are in normal form.

For example, here are some expressions in normal form:

 x
 (x x)
 (lambda (x) x)
 (lambda (x) (x x))

We will consider just one transformation called beta-conversion. It says that an application of a lambda expression to a sequence of arguments can be reduced to the body of the lambda expression with the formal parameters replaced by the arguments. This is where we will need subst* in its full power. An expression can contain multiple occurences of applictions of lambda expressions and can be reduced by collapsing any of those applications. A particular semantics specifies an order in which those applications are performed.

Example. The following expression is reduced to its normal form in two steps.

(lambda (x) ((lambda (x) (x x)) (lambda (x) x)))

=>

(lambda (x) ((lambda (x) x) (lambda (x) x)))

=>

(lambda (x) (lambda (x) x))

1. Write the procedure reduce that takes a lambda calculus expression in its record form and reduces it to its normal form by repeatedly substituting arguments for formal parameters in the body of a direct lambda application.

   Applications should be evaluated in normal order. That means that the outer most application is reduced first. In particular, when the operator of an application is a lambda expression, the arguments of the application should not be reduced prior the reduction of the application. Rather, they should be substituted as is inside the body of the lambda expression.

   > (listify (reduce (recordify '(lambda (x) x))))
   (lambda (x) x)
   
   > (listify (reduce (recordify '((lambda (x) x) y))))
   y
   
   > (listify (reduce (recordify '((lambda (f x) (f x)) (lambda (x) x) z))))
   z
   
   ;;; Think about why the following expression does not go into an
   ;;; infinite  loop.
   
   > (listify
       (reduce
         (recordify '((lambda (x) (lambda (x) x))
   		   ((lambda (x) (x x)) (lambda (x) (x x)))))))
   (lambda (x) x)
   
   > (listify
       (reduce
         (recordify '((lambda (n)
   		     (n (lambda (x) (lambda (t f) f)) (lambda (t f) t)))
   		   (lambda (s z) z)))))
   (lambda (t f) t)
   
   > (listify
       (reduce
         (recordify '((lambda (n) (lambda (s z) (s (n s z))))
   		   ((lambda (n) (lambda (s z) (s (n s z))))
   		    ((lambda (n) (lambda (s z) (s (n s z))))
   		     ((lambda (n) (lambda (s z) (s (n s z))))
   		      ((lambda (n) (lambda (s z) (s (n s z))))
   		       (lambda (s z) z)))))))))
   (lambda (s z) (s (s (s (s (s z))))))
   
   
   > (listify
       (reduce
         (recordify
   	'(((lambda (f)
   	     ((lambda (y) (f (y y))) (lambda (y) (f (y y)))))
   	   (lambda (f)
   	     (lambda (n)
   	       (((lambda (n)
   		   (n (lambda (x) (lambda (t f) f)) (lambda (t f) t)))
   		 n)
   		((lambda (n) (lambda (s z) (s (n s z)))) (lambda (s z) z))
   		((lambda (n m)
   		   (n (lambda (x)
   			((lambda (n m)
   			   (n (lambda (n) (lambda (s z) (s (n s z))))
   			     (m (lambda (n) (lambda (s z) (s (n s z))))
   			       (lambda (s z) z))))
   			 x
   			 m))
   		     (lambda (s z) z)))
   		 n
   		 (f ((lambda (n)
   		       ((lambda (pr) (pr (lambda (t f) t)))
   			(n (lambda (pr)
   			     ((lambda (x y) (lambda (f) (f x y)))
   			      ((lambda (pr) (pr (lambda (t f) f))) pr)
   			      ((lambda (n) (lambda (s z) (s (n s z))))
   			       ((lambda (pr) (pr (lambda (t f) f))) pr))))
   			  ((lambda (x y) (lambda (f) (f x y)))
   			   (lambda (s z) z)
   			   (lambda (s z) z)))))
   		     n)))))))
   	  ((lambda (n) (lambda (s z) (s (n s z))))
   	   ((lambda (n) (lambda (s z) (s (n s z))))
   	    ((lambda (n) (lambda (s z) (s (n s z))))
   	     (lambda (s z) z))))))))
   (lambda (s z) (s (s (s (s (s (s z)))))))
   

Submission