Tracking the evaluation of a lambda expression
I am having problems with some complex lambda expressions in Scheme and would like to see how they are evaluated by the interpreter.
I would like the Schema interpreter to print all of the evaluation steps as shown in SICP Section 1.1.5, "Substitution Model for Procedure Application" .
I am looking for a solution using any Schema interpreter. I've already tried rocket tracing , but it only tracks the procedure calls, not every expression.
An example of motivation
Given the definition of church figures 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
andtwo
directly (not in terms ofzero
andadd-1
).
I want to check my definitions for one
both two
the evaluation results (add-1 zero)
and (add-1 (add-1 zero))
.
This is what I would like the Schema interpreter to print:
> (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)))
>
source to share
It's very easy with combinatorial-like equations (what was once called the applicative style, which 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 matters: a b c d
in fact (((a b) c) d)
, but is a b c = d
equivalent (define a (lambda (b) (lambda (c) d)))
.
It is now clear what the intended meaning is f
and x
: x
means a specific implementation of a "zero" item, and f
means a specific implementation of a "successor" operation, consistent with a specific specific implementation of a "zero". f
and x
should really be named mnemonically:
zero s z = z
add1 n s z = s (n s z)
Not that hard to look at, with a more convenient syntax, right? lambda
himself was a typographical accident. Now,
one s z = s z ; e.g. (1+ 0)
two s z = s (s z) ; e.g. (1+ (1+ 0))
Steps tracking according to SICP 1.1.3 procedure ,
- To evaluate a combination, follow these steps:
- Evaluate the combination subexpressions.
- Apply a procedure that is the value of the leftmost subexpression (operator) for arguments that are the values of other subexpression (operands).
and 1.1.5 model of justice for the application of procedures
- To apply a compound procedure to arguments, evaluate the body of the procedure with each formal parameter replaced with 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 replacement actually stops because the result is a simple lambda expression i.e. not a combination. Only when two more arguments are supplied is the entire evaluation performed:
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 continue according to the actual definitions of s
and z
. This is what is shown in the above equations (1) in shorter terms.
source to share