1

荷兰数学家 Nicolaas Govert de Bruijn 发明了这些索引来表示 lambda 演算的项，而无需命名绑定变量。让我们来看看这个 lambda 表达式：

K = λx.λy.x

使用 de Bruijn 索引时，当我们使用约定时，如here，零 de Bruijn 索引指的是第一个封闭的 lambda binder：

K = λλ1

de Bruijn 指数 1 是指包含 de Bruijn 指数的第二个 lambda 粘合剂。如何为替换编写 Prolog 代码，以便我们可以计算 beta 减少，例如：

Kab = a
4

2 回答 2

2

De Bruijn 索引是用于替换比 Prolog 中更困难的设置的工具。逻辑变量是一种优越的工具。我认为您永远不会想编写 Prolog 代码来处理 de Bruijn 索引。（元问题在下面回复你。）

无论如何，从问题链接的 PDF的第二页包含所需的一切的 Prolog 实现。它只是使用非标准的、所谓的“函数式”语法。

这是正确语法中的转换关系：

funny_arrow(I, C, Term, Shifted) :-
    (   number(Term)
    ->  (   Term < C
        ->  Shifted = Term
        ;   Shifted is Term + I )
    ;   Term = lambda(E)
    ->  Shifted = lambda(Shifted1),
        C1 is C + 1,
        funny_arrow(I, C1, E, Shifted1)
    ;   Term = apply(E1, E2)
    ->  Shifted = apply(Shifted1, Shifted2),
        funny_arrow(I, C, E1, Shifted1),
        funny_arrow(I, C, E2, Shifted2) ).

这是替换：

substitute(Term, E, M, Substituted) :-
    (   number(Term)
    ->  (   Term = M
        ->  Substituted = E
        ;   Substituted = Term )
    ;   Term = lambda(E1)
    ->  Substituted = lambda(E1Subst),
        funny_arrow(1, 0, E, EShifted),
        M1 is M + 1,
        substitute(E1, EShifted, M1, E1Subst)
    ;   Term = apply(E1, E2)
    ->  Substituted = apply(E1Subst, E2Subst),  % typo in original?
        substitute(E1, E, M, E1Subst),
        substitute(E2, E, M, E2Subst) ).

您可以以相同的方式转录 beta 减少规则。

然后我们可以测试一下。在 PDF 中使用的搞笑语言中，每个基本术语都必须编码为数字，因此我们将选择aas123和bas456任意编码。减少术语(K a) b将通过减少应用两个减少步骤来完成，首先减少K a到KA，然后应用KA到b。干得好：

?- K = lambda(lambda(1)),
   A = 123,
   B = 456,
   reduce(apply(K, A), KA),
   reduce(apply(KA, B), KAB).
K = lambda(lambda(1)),
A = KAB, KAB = 123,
B = 456,
KA = lambda(124).

结果KAB与 相同A。您可以通过定义更简单、更有效地获得相同的结果：

apply(lambda(X, E), X, E).

接着：

?- K = lambda(X, lambda(Y, X)),
   apply(K, a, KA),
   apply(KA, b, KAB).
K = lambda(a, lambda(b, a)),
X = KAB, KAB = a,
Y = b,
KA = lambda(b, a).

你当然知道这一点。

Meta：您关于从符号逻辑中编码晦涩主题的问题并没有引起很大的关注。部分原因是它们中的大多数都不是很有趣。部分原因是他们缺乏所有细节和展示你所做的任何努力. 但我认为第三部分是社区不理解您对这些问题的全部意义。你是一个有成就的 Prolog 程序员和实现者并不是什么秘密。显然，您可以将一些简单的方程式转录到 Prolog 中。那么为什么要问别人呢？这是否意味着某种项目来建立“社区维基”或标准符号算法的 Prolog 实现数据库？这甚至可能很有趣，但如果您传达项目存在以及它的目的是什么，您可能会在该项目中获得更多参与者。

于 2020-12-18T21:27:20.083 回答
0

我想出了另一种方法，它是针对线性逻辑量身定制的。这意味着每次访问活页夹时，它都会避免在substitute/4 中调用funny_arrow/4。这是一个测试用例：

/* example from PDF */
?- apply(b(b(1*2)), 1, X).
X = b(2*1).

源代码如下。还更正了 PDF 中的错字，但大写 fun_arrow/4 不仅可以取 -1 和 1，还可以取其他值：

警告下面的代码不是坚定的！

% apply(+Expr, +Expr, -Expr)
apply(b(R), S, T) :-
   subst(R, 0, S, T).

% subst(+Expr, +Integer, +Expr, -Expr)
subst(P*Q, J, D, R*S) :- !,
   subst(P, J, D, R),
   subst(Q, J, D, S).
subst(b(P), J, D, b(R)) :- !,
   K is J+1,
   subst(P, K, D, R).
subst(J, K, _, J) :- integer(J), J < K, !.
subst(0, 0, D, D) :- !.
subst(J, J, D, R) :- integer(J), !,
   shift(D, 0, J, R).
subst(J, _, _, K) :- integer(J), !, K is J-1.
subst(I, _, _, I).

% shift(+Expr, +Integer, +Integer, -Expr)
shift(P*Q, J, D, R*S) :- !,
   shift(P, J, D, R),
   shift(Q, J, D, S).
shift(b(P), J, D, b(R)) :- !,
   K is J+1,
   shift(P, K, D, R).
shift(J, K, _, J) :- integer(J), J < K, !.
shift(J, _, D, K) :- integer(J), !, K is J+D.
shift(I, _, _, I).
于 2020-12-18T22:27:55.080 回答