序言——生成整数 "unwindably"

Question

我正在尝试使用 De Bruijn 指数定义 lambda 演算项。我在 OS X 上使用 swi prolog。

如果我使用自然数的 zero|successor 表示，我可以交互式地完成部分指定的项。

nat(zero).
nat(s(X)) :- nat(X).

debruijn2(N)         :- nat(N).
debruijn2(ap(M, N))  :- debruijn2(M), debruijn2(N).
debruijn2(lambda(M)) :- debruijn2(M).

例如，Z 和 X 在 ap(Z, X) 中统一为 zero。

?- debruijn2(ap(X, Z)).
X = Z, Z = zero .

但是，使用length 来检查数字like this除非 debruijn 的参数只是一个整数，否则会产生类型错误。

debruijn(N)          :- length(_, N).
debruijn(ap(M, N))   :- debruijn(M), debruijn(N).
debruijn(lambda(M))  :- debruijn(M).

查询 debruijn(X). 成功并且 X 与 0 统一。

?- debruijn(X).
X = 0 .

但是，查询 debruijn(ap(Z, X)). 失败了，就好像 length(_, ·) 不可撤销地将其第二个参数限制为整数.

?- debruijn(ap(Z, X)).
ERROR: Type error: `integer' expected, found `ap(_2944,_2946)' (a compound)
ERROR: In:
ERROR:   [10] throw(error(type_error(integer,...),context(...,_3008)))
ERROR:    [8] debruijn(ap(_3036,_3038)) at <...>:2
ERROR:    [7] <user>
ERROR:
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
   Exception: (8) debruijn(ap(_2362, _2364)) ? creep

为什么 length/2 会产生类型错误，而不仅仅是无法应用于参数？

Answer 1

在 SWI-Prolog 上运行的替代方案，无需使用对 length/2 和 catch/3 的昂贵调用:

debruijn(N)         :- simple(N), nat(N).
debruijn(ap(M, N))  :- debruijn(M), debruijn(N).
debruijn(lambda(M)) :- debruijn(M).

nat(0).
nat(I) :-
    nat(1, I).

nat(I, I).
nat(I, J) :-
    I2 is I + 1,
    nat(I2, J).

simple/1 谓词如果其参数未实例化为复合项，则谓词成功。这是一个从未标准化但仍然存在于某些 Prolog 系统中的遗留谓词(例如，它是 SWI-Prolog 中的库谓词和 SICStus Prolog 中的内置谓词)。

与基于 length/2 的解决方案的不同之处在于，当 debruijn/1 以负数调用时的行为可能与您的用例相关或不相关.在这种情况下，此解决方案将进入循环并最终出现错误，但 length/2 将抛出异常，catch/3 包装器将转换为失败。