Tracing lambda expression evaluation

Question

I am having trouble with some tricky-looking lambda expressions in Scheme, and I would like to see how they are being evaluated by the interpreter.

I would like the Scheme interpreter to print all the evaluation steps, as seen in SICP Section 1.1.5, "The Substitution Model for Procedure Application".

I am looking for a solution using any Scheme interpreter. I have already tried Racket's tracing, but it only traces procedure calls, not every expression.

Motivating example

Given the definition of Church numerals from SICP Exercise 2.6:

(define zero (lambda (f) (lambda (x) x)))

(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

and the task:

Define one and two directly (not in terms of zero and add-1).

I wish to check my definitions of one and two against the results of evaluating (add-1 zero) and (add-1 (add-1 zero)).

This is what I would like the Scheme interpreter to print out:

> (add-1 zero)
(add-1 (lambda (f) (lambda (x) x)))
(lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) x)) f) x))))
(lambda (f) (lambda (x) (f ((lambda (x) x) x))))
(lambda (f) (lambda (x) (f x)))
>

Answer 1

Give Racket's built-in stepper a try, there's a little how-to in this answer.

Answer 2

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:
  1. Evaluate the subexpressions of the combination.
  2. 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.