Solution to the third homework assignment.

Exercise 4.2.3 We use the following version of the lambda calculus for this exercise:

          exp ::= [varref]
               |  number
               |  ([exp] [exp])
               |  (lambda ([var]) [exp])

We first define free? for the above lambda calculus.

(define free?
  (lambda (var exp)
    (form-case exp
       (variable v (eq? v var))
       (lambda (formals body)
	 (and (not (eq? var (car formals)))
	   (free? var body)))
       (call (rator rands)
	 (or (free? var rator)
	     (free? var rands))))))

Then we have the main procedure:

(define substitute
  (lambda (e m x)
    (form-case e
      (variable v (if (eq? v x) m e))
      (constant c e)
      (lambda (formal-ls body)
	(cond
	  ((eq? (car formal-ls) x)
	   (list 'lambda formal-ls body))
	  ((not (free? x body))
	   (list 'lambda formal-ls body))
	  ((not (free? (car formal-ls) m))
	   (list 'lambda formal-ls (substitute body m x)))
	  (else (let ((z (gensym)))
		  (list 'lambda (list z)
		    (substitute (substitute body z
				  (car formal-ls))
		      m x))))))
      (call (rator rand) (list (substitute rator m x)
			   (substitute rand  m x))))))

Vikram Subramaniam, 1995