SICP exercise 2.04

From Drewiki

Problem

Here is an alternative procedural representation of pairs. For this representation, verify that (car (cons x y)) yields x for any objects x and y.

What is the corresponding definition of cdr? (Hint: To verify that this works, make use of the substitution model of section 1.1.5 of the text.)

Solution

As the problem statement suggests, we can verify this representation using the substitution model of evaluation. If z is an object created by the cons procedure given above, then:

Substituting the definition of cons for z:

Now substitute the second lambda expression for the value of m in the first lambda expression to get:

Applying the lambda expression to its arguments x and y, we get this:

Now we need the definition of cdr:

Verifying by substitution, where z is an object constructed by cons: