Displaying intermediate terms in a β-reductor

Question

Consider the following β-reductor:

(define (normalize v)
  (set! count 0)
  (set! reflected '())
  (reify v))

(define (reify v)
  (if (memq v reflected)
      (v cancel)
      (let ((x (gensym)))
    (ABS x (reify (v (reflect x)))))))

(define (reflect e)
  (let ((f (lambda (v)
         (if (eq? v cancel)
         e
         (reflect (APP e (reify v)))))))
    (set! reflected (cons f reflected))
    f))

(define (APP e1 e2) `(,e1 ,e2))

(define (ABS x e) `(lambda (,x) ,e))

(define reflected '())

(define count 0)

(define cancel '(cancel))

(define (gensym)
  (set! count (+ 1 count))
  (string->symbol (string-append "x" (number->string count))))

I would like to analyze its β-reduction order. However, since I'm not too savvy with Scheme, I would like to see the intermediate terms (right now it only prints the end result) it calculates as pure lambda expressions. I know how to display a line, but I am unable to squeeze a (display term) (newline) in the right spot.

Below are two simple terms that can be used to verify a solution - Church one (λfx.f x) and succ (λnfx.f (n f x)) (I hope I wrote them correctly in Scheme):

(define One
  (lambda (f) (lambda (x) (f x))))

(define succ
  (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))

(normalize (succ One))

Is it possible to display the intermediate terms calculated by this reductor?

Answer 1

No, This is a big-step NBE algorithm (meaning "all at once"). it works by reflecting your term language into the host languages to piggy back on the hosts execution engine.