显示 β-reductor 中的中间项

Question

考虑以下 β-减速器：

(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))))

我想分析一下它的β-reduction order。但是，由于我对 Scheme 不太了解，所以我希望看到它作为纯 lambda 表达式计算的中间项（现在它只打印最终结果）。我知道如何显示一条线，但我无法在正确的位置挤压 (display term) (newline)。

下面是两个简单的术语，可用于验证解决方案 - Church one (λfx.f x) 和 succ (λnfx.f (n f x))（我希望我写了它们在方案中正确）：

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

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

(normalize (succ One))

是否可以显示这个reductor计算的中间项？

Answer 1

不，这是一个大步长的NBE算法（意思是"all at once"）。它的工作原理是将您的术语语言反映到宿主语言中，以搭载在宿主执行引擎上。

显示 β-reductor 中的中间项

Displaying intermediate terms in a β-reductor

io

scheme

lambda-calculus