时间戳

首页 > 解决方案 > prolog - 生成整数“unwindably”

prolog - prolog - 生成整数“unwindably”

问题描述

我正在尝试用 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并与inX统一。zeroap(Z, X)

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

但是，使用lengthto 检查这样的数字会产生类型错误，除非参数 todebruijn只是一个整数。

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产生类型错误而不是仅仅未能应用于参数？

标签： prolog

解决方案

在 SWI-Prolog 上运行的替代方案，无需对length/2and进行昂贵的调用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包装器将转换为失败。

推荐阅读