Confused with behavior of this procedure

Question

(CONTEXT)

I've defined a procedure that applies another one-argument procedure object to it's parameter twice. Take for example the procedure inc that adds 1 to it's argument, (double inc) will add two. hence ((double inc) 5) returns 7.

(THE PROBLEM)

I expected for (((double (double double)) inc) 5) to return 13. Since double double will apply a procedure 4 times and thus the most-left double will result in a the application of the one-parameter procedure 8 times. A lineair growth.

I'm wrong. Look below for what the procedure actually returns.

Clearly i'm missing something and there's a flaw in my understanding.

(define (double proc)
(lambda (y) (proc (proc y))))

(define (inc x) (+ x 1))

> ((double inc) 5)
7
> (((double double) inc) 5)
9
> (((double (double double)) inc) 5)
21
> (((double (double (double double))) inc) 5)
261    
> 

Answer 1

This should be fairly easy to deduct using both reason or substitution model.

Reason:

(double double)

This is like double but twice, quadrouple. When applied with a function it will apply that function 4 times.

(double (double double))

This is doubling quadrouple. The result of quadrouple will be quadroupled making it 4*4. When applied with a function it will apply that 16 times.

(double (double (double double)))

This is doubling the previous one. Then the same again. 16*16 makes it apply the result 256 times.

Thus (double double) is 2^2, (double (double double)) is (2^2)^2 and (double (double (double double))) is ((2^2)^2)^2 or 2^8 for short.

This relates to lambda calculus where power is defined as λb.λe.e b or (lambda (b) (lambda (e) (e b)). Now double is the church numeral for 2. Do you see that you are doing ((2^2)^2)^2?

Substitution

Here are the expressions reduced. I sometimes jump steps later since it's pretty much the same that happens several times.

((double inc) 5)               ; ==>
((lambda (y) (inc (inc y))) 5) ; ==>
(inc (inc 5))                  ; ==> 7


(((double double) inc) 5)                   ; ==>
(((lambda (y) (double (double y))) inc) 5)  ; ==>
(((lambda (y) (double (double y))) inc) 5)  ; ==>
((double (double inc)) 5)                   ; ==>
((double (lambda (y) (inc (inc y)))) 5)     ; ==>
((lambda (y) ((lambda (y) (inc (inc y))) ((lambda (y) (inc (inc y))) y))) 5) ; ==>
((lambda (y) (inc (inc (inc (inc y))))) 5) ; ==>
(inc (inc (inc (inc 5)))) ; ==> 9


(((double (double double)) inc) 5)                                                                ; ==>
(((double (lambda (y) (double (double y)))) inc) 5)                                               ; ==>
(((lambda (y) ((lambda (y) (double (double y))) ((lambda (y) (double (double y))) y))) inc) 5)    ; ==>
(((lambda (y) (double (double (double (double y))))) inc) 5)                                      ; ==>
((double (double (double (lambda (y) (inc (inc y)))))) 5)                                         ; ==>
((double (double (lambda (y) (inc (inc (inc (inc y))))))) 5)                                      ; ==>
(inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc (inc 5)))))))))))))))) ; ==> 21

I'll leave the last one as an exercise.

Answer 2

The problem is in your interpretation of what double expands to when nested.

Just apply substitution of y with inc, one level at a time, and you'll see what's happening:

(double inc) expansion using let to make things clearer:

(lambda (y)
        (let ([proc inc])
             ((proc (proc y))))

So far, so good.

((double double) inc) expansion:

     (lambda (y)
        (let ([proc (lambda (y_0) (double (double y_0)))])
             (proc (proc y))))

The first application works as intended, but the second doubles not the application of the inc function, but of the double function itself, as you apply double to the function double in (double double).

If you do it again, i.e. ((double (double double) inc), you can see it gets messy...

What you're probably looking for is to apply the result of a single application of double to the result of another single application...

As in:

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