在β还原器中显示中间项

Question

考虑以下β-reducor：

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

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

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

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

是否可以显示由该还原器计算的中间项？

Answer 1

不，这是一个大步的 NBE 算法(意思是"一次全部"(。 它的工作原理是将您的术语语言反映到主机语言中，以搭载主机执行引擎。