This is very easy with combinators-like equations (what was once called applicative style I believe )
zero f x = x
add1 n f x = f (n f x)
one f x = add1 zero f x = f (zero f x) = f x **(1)**
two f x = add1 one f x = f (one f x) = f (f x) **(2)**
With combinators, everything is curried: a b c d
is actually (((a b) c) d)
and a b c = d
is equivalent to (define a (lambda (b) (lambda (c) d)))
.
Now it is clear what is the intended meaning of f
and x
: x
stands for a concrete implementation of "zero" data element, and f
stands for a concrete implementation of "successor" operation, compatible with a given concrete implementation of "zero". f
and x
should have really be named mnemonically:
zero s z = z
add1 n s z = s (n s z)
Not so tricky-looking anymore, with more convenient syntax, right? lambda
itself was a typographical accident anyway. Now,
one s z = s z ; e.g. (1+ 0)
two s z = s (s z) ; e.g. (1+ (1+ 0))
Tracing the steps according to the SICP 1.1.3 combinations evaluation procedure,
- To evaluate a combination, do the following:
- Evaluate the subexpressions of the combination.
- Apply the procedure that is the value of the leftmost subexpression (the operator) to the arguments that are the values of the other subexpressions (the operands).
and the 1.1.5 sustitution model for procedure application
- To apply a compound procedure to arguments, evaluate the body of the procedure with each formal parameter replaced by the corresponding argument.
we get
add1 zero =
( n f x => f (n f x) ) ( f x => x ) =
( f x => f ( ( f x => x ) f x ) )
and here the substitution stops actually, because the result is a simple lambda expression, i.e. not a combination. Only when two more arguments are supplied, the evaluation is done in full:
add1 zero s z =
( n f x => f (n f x) ) ( f x => x ) s z =
( f x => f ( ( f x => x ) f x ) ) s z =
( x => {s} ( ( f x => x ) {s} x ) ) z = ; {s} is definition-of s
{s} ( ( f x => x ) {s} {z} ) = ; {z} is definition-of z
; must find the value of the operand in combination
{s} ( ( x => x ) {z} ) =
{s} {z}
and then the calculation will proceed according to the actual definitions of s
and z
. That is what the equations (1) shown above indicate, in shorter notation.