SICP Exercise 1.41: Double Trouble

Define a procedure double that takes a procedure of one argument as argument and returns a procedure that applies the original procedure twice. For example, if inc is a procedure that adds 1 to its argument, then (double inc) should be a procedure that adds 2. What value is returned by

(((double (double double)) inc) 5)

The definition of double is quite simple - we just need to return a procedure that applies a passed procedure to the result of applying the same to procedure to a given variable. I.e.

(define (double f) (lambda (x) (f (f x))))

However, we need to be careful when answering "what value is returned by (((double (double double)) inc) 5)". Given a cursory glance you might thing "well double applies a procedure twice, and we've got double of double of double, so that will apply the procedure 2 × 2 × 2 = 8 times, and the procedure's inc, so that'll apply inc 8 times - i.e. add 8 to 5, giving 13."

Unfortunately not.

Here's what happens when you ask an interpreter:

> (((double (double double)) inc) 5)
21

What goes on here is a bit more subtle...

Looking closely at the parentheses we can see that the expression (double double) (where double is used as both the operator and the operand) produces the operand for the expression (double (double double)). This in turn becomes the operator in an expression with inc as the operand. Finally, that expression, ((double (double double)) inc) becomes the operator in an expression with 5 as the operand.

Now remembering that double takes a procedure as its parameter and produces a single-parameter lambda expression from that, we can see that:

• (double double) will produce a produce a single-parameter lambda expression that applies double twice in sequence to its parameter. The parameter to this lambda expression needs to be a procedure.
• (double (double double)) takes the lambda expression produced by (double double) as the operand and produces a further lambda expression. This lambda expression applies the preceding lambda expression twice in sequence to its parameter. Again, the parameter needs to be a procedure.
• ((double (double double)) inc) is where it perhaps gets a bit complicated. The procedure inc gets passed as the operand the lambda expression outlined in the preceding bullet. The evaluation of this is somewhat difficult to explain succinctly in text, but I'll try... It produces a lambda expression that applies inc twice to its single parameter. The result of this becomes the operand to a second lambda expression which applies inc twice to its operand. This is all wrapped in a third lambda expression, which becomes the operand to a further lambda expression, which uses this lambda expression as the operand to a lambda expression which produces another lambda expression which applies the operand twice, and then this becomes the operand to yet another lambda expression which produces a final lambda expression which applies its operand twice.

The effect of all this is that ((double (double double)) inc) is equivalent to applying inc 16 times, not 8 times. To try to clarify all that, let's run through an evaluation by substitution:

  (((double (double double)) inc) 5)
= (((double (lambda (x) (double (double x)))) inc) 5)

Here we've expanded (double double). The operator, double, takes the operand, also double, and produces a lambda expression with one parameter, x, that applies the operand to the results of applying the operand to x. Until x is bound that's about as far as we can take the expansion of that portion of the expression, so let's expand the next level out (and I hope you'll excuse me while I substitute λ for lambda to compress things a little):

  (((double (lambda (x) (double (double x)))) inc) 5)
= (((double (λ (x) (double (double x)))) inc) 5)
= (((λ (x)
       ((λ (x) (double (double x)))
           ((λ (x) (double (double x))) x)))
      inc)
     5)

Ouch! We've got an explosion of λs and xs going on here. I'm going to introduce x' and x'' to distinguish the xs and to hopefully make the next steps clearer:

= (((λ (x)
       ((λ (x'') (double (double x'')))
           ((λ (x') (double (double x'))) x)))
      inc)
     5)

Before we go any further though, let's look at what we have. We have an expression that is of the form ((<ComplicatedLambdaExpression> inc) 5). I.e. we have a rather complicated and nested lambda expression that is the operator in an expression which is going to be evaluated with the operand inc. Once this has been evaluated the resulting value will be used as the operand in an evaluating an expression with the operand 5.

So let's now evaluate the <ComplicatedLambdaExpression>:

  (((λ (x)
       ((λ (x'') (double (double x'')))
           ((λ (x') (double (double x'))) x)))
      inc)
     5)
= (((λ (x'') (double (double x''))) ((λ (x') (double (double x'))) inc)) 5)
= (((λ (x'') (double (double x''))) (double (double inc))) 5)
= (((λ (x'') (double (double x''))) (double (λ (x) (inc (inc x))))) 5)
= (((λ (x'') (double (double x'')))
       (λ (x) ((λ (x) (inc (inc x)))
                  ((λ (x) (inc (inc x))) x))))
     5)

Let's rename the xs again to clarify what's what:

= (((λ (x''') (double (double x''')))
       (λ (x) ((λ (x'') (inc (inc x'')))
                  ((λ (x') (inc (inc x'))) x))))
     5)

In order to simplify things a bit I'm going to make an assertion at this point: the following two expressions have equivalent functionality:

  (λ (x) ((λ (x'') (inc (inc x''))) ((λ (x') (inc (inc x'))) x)))
≡ (λ (x) (inc (inc (inc (inc x)))))

In other words, a lambda expression that takes a single parameter, x, and uses as the operand in an expression where the operator is a lambda expression that applies inc to the result of applying inc to its sole parameter and then using the result of evaluating that expression as the operand in a further expression where the operand is again a lambda expression that that applies inc to the result of applying inc to its sole parameter is equivalent to a lambda expression that takes a single parameter, x, and applies inc to the result of applying inc to the result of applying inc to the result of applying inc to its sole parameter.

Note that the interpreter will probably not make this substitution during its evaluation of the expression (given that it's not possible to determine the equivalence of two lambda expressions algorithmically). There will be a couple more equivalences asserted through the remainder of this evaluation - look out for them!

Okay, so now we can proceed as follows:

  (((λ (x''') (double (double x''')))
       (λ (x) ((λ (x'') (inc (inc x'')))
                  ((λ (x') (inc (inc x'))) x))))
     5)
≡ (((λ (x''') (double (double x'''))) (λ (x) (inc (inc (inc (inc x)))))) 5)
= ((double (double (λ (x) (inc (inc (inc (inc x))))))) 5)
= ((double (λ (x)
              ((λ (x) (inc (inc (inc (inc x)))))
                ((λ (x) (inc (inc (inc (inc x))))) x)))
     5)
≡ ((double (λ (x) (inc (inc (inc (inc (inc (inc (inc (inc x)))))))))) 5)
= ((λ (x)
      ((λ (x) (inc (inc (inc (inc (inc (inc (inc (inc x)))))))))
          ((λ (x) (inc (inc (inc (inc (inc (inc (inc (inc x))))))))) x)))
     5)
≡ ((λ (x)
      (inc
        (inc
          (inc
            (inc
              (inc
                (inc
                  (inc
                    (inc
                      (inc
                        (inc
                          (inc
                            (inc
                              (inc
                                (inc
                                  (inc
                                    (inc x)))))))))))))))))
     5)
= (inc
    (inc
      (inc
        (inc
          (inc
            (inc
              (inc
                (inc
                  (inc
                    (inc
                      (inc
                        (inc
                          (inc
                            (inc
                              (inc
                                (inc 5))))))))))))))))

Hopefully you'll also excuse me when I don't expand out fully the evaluations of inc for the rest of this...

  (inc
    (inc
      (inc
        (inc
          (inc
            (inc
              (inc
                (inc
                  (inc
                    (inc
                      (inc
                        (inc
                          (inc
                            (inc
                              (inc
                                (inc 5))))))))))))))))
= (inc
    (inc
      (inc
        (inc
          (inc
            (inc
              (inc
                (inc
                  (inc
                    (inc
                      (inc
                        (inc
                          (inc
                            (inc
                              (inc 6)))))))))))))))
= (inc
    (inc
      (inc
        (inc
          (inc
            (inc
              (inc
                (inc
                  (inc
                    (inc
                      (inc
                        (inc
                          (inc
                            (inc 7))))))))))))))
= (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc 8)))))))))))))
= (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc 9))))))))))))
= (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc 10)))))))))))
= (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc 11))))))))))
= (inc (inc (inc (inc (inc (inc (inc (inc (inc 12)))))))))
= (inc (inc (inc (inc (inc (inc (inc (inc 13))))))))
= (inc (inc (inc (inc (inc (inc (inc 14)))))))
= (inc (inc (inc (inc (inc (inc 15))))))
= (inc (inc (inc (inc (inc 16)))))
= (inc (inc (inc (inc 17))))
= (inc (inc (inc 18)))
= (inc (inc 19))
= (inc 20)
= 21

As a final aside, if you really wanted 13 as the result (i.e. you wanted the expression to be equivalent to applying inc 8 times to 5) then you need to move a few parentheses around:

> ((double (double (double inc))) 5)
13

Here:

• Evaluating (double inc) produces a lambda expression, λ_a, that applies inc twice.
• Evaluating (double (double inc)) takes λ_a as its operand and produces a second lambda expression, λ_b, that is equivalent to applying inc four times. I say equivalent to as of course it's actually producing a lambda expression that takes a single parameter and applies λ_a to that parameter, applying inc twice, and then evaluates λ_a again, but with this intermediate result as its operand, applying inc a further two times.
• Evaluating (double (double (double inc))) takes λ_b as its operand and produces a third lambda expression, λ_c, that is equivalent to applying inc eight times. Of course what it's actually doing is applying λ_b twice in sequence, which is equivalent to applying λ_a four times in sequence.