Exercise 2.4 gives us the following alternative procedual implementation for creating pairs.
(define (cons x y)
(lambda (m) (m x y)))
(define (car z)
(z (lambda (p q) p)))
Using this implementation, we are told to verify that
(car (cons x y))yields x for any objects x and y using the substitution model from section 1.1.5.
Once we've done that, we need to write the corresponding definition of
Our first step to verifying that this implementation for
carwork should be to put the code in a Scheme interpreter and see them work.
> (car (cons 2 3))
> (car (cons 15 "Hello"))
> (car (cons "Hi!" 42))
Now let's use the substitution model to show that the following always yields x
(car (cons x y))
First we retrieve the body of
(lambda (m) (m x y))
We could replace the formal parameters x and y with the arguments 2 and 3 (or any others that we choose) at this point, but I'm going to keep working with x and y. Let's substitute the body of
(car (lambda (m) (m x y)))
Now we can retrieve the body of
carand substitute it.
((z (lambda (p q) p)) (lambda (m) (m x y)))
carprocedure takes a procedure z as an argument and applies it to
(lambda (p q) p), so there's one more substitution we need to do here before this step is really done. We need to take the second lambda in the expression above and replace z with it.
((lambda (m) (m x y)) (lambda (p q) p))
That might look scary, but it's just a procedure applied to another procedure. Since the procedure on the left takes one formal parameter, we can substitute the procedure on the right for that parameter.
((lambda (p q) p) x y)
Now it should be clear that this expression is a procedure that takes two parameters p and q, and passes two parameters to it. The procedure returns the first of the two parameters passed to it, so this expression simplifies to x.
The definition for
cdrthat corresponds to the above implementation of
(define (cdr z)
(z (lambda (p q) q)))
We can test it out the same way we originally tested the code provided in the text,
by running it in the interpreter.
> (cdr (cons 2 3))
> (cdr (cons 15 "Hello"))
> (cdr (cons "Hi!" 42))
For links to all of the SICP lecture notes and exercises that I've done so far, see The SICP Challenge.