Is this lambda abstraction created as a generator of a recursive function?

Question

In lambda calculus, a recursive function $f$ is obtained by

$$ f = Y g $$

where $Y$ is the Y combinator and $g$ is the generator of $f$ i.e. $f$ is a fixed point of $g$ i.e. $f == g f$.

In The Scheme Programming Language, I saw an example implementing a recursive function $f$ that sums the integers in a list:

(let ([sum (lambda (f ls)
 (if (null? ls)
 0
 (+ (car ls) (f f (cdr ls)))))])
(sum sum '(1 2 3 4 5))) => 15

What is the mathematical derivation that drives to create the lambda abstraction

 lambda (f ls)
 (if (null? ls)
 0
 (+ (car ls) (f f (cdr ls))))

? It looks like a generator of $f$, but not entirely.

Thanks.

Answer 1

If you look at the $Z$ combinator (because we're in an eager context), you have $$Z=\lambda g.(\lambda f.g(\lambda v.ffv))(\lambda f.g(\lambda v.ffv))$$

If you look at the code, we don't apply a fixed point combinator to sum, we simply apply sum to itself, so there's no reason for sum to be "generator".

You can also readily show that sum is (modulo currying) equal to $\lambda f.g(\lambda v.ffv)$ for some $g$, basically by replacing (f f ...) with (h ...) where h is the argument to $g$ in the definition for sum (minus the outermost lambda).

• Tim: Thanks. I figured it out at the same time also by looking up the definition of the Y combinator (not sure whether it is called Y or Z). Before seeing the example in the book, I had never met a recursive function computed in such a "convoluted" yet "systematic" way. When is the technique in the example useful?