Prolog中基于De Bruijn索引的替换 [英] De Bruijn index based substitution in Prolog

问题描述

荷兰数学家 Nicolaas Govert de Bruijn 发明了这些指数用于在不命名绑定变量的情况下表示 lambda 演算的术语.让我们以这个 lambda 表达式为例:

The Dutch mathematician Nicolaas Govert de Bruijn invented these indexes for representing terms of lambda calculus without naming the bound variables. Lets take this lambda expression:

K = λx.λy.x

当我们使用约定时，de Bruijn 索引读取为 此处，零 de Bruijn 索引指的是第一个封闭的 lambda 绑定器:

With de Bruijn indexes it reads, when we use the convention, as here, that the zero de Bruijn index refers to the first enclosing lambda binder:

K = λλ1

de Bruijn 索引 1 指的是包含在德布鲁因指数.如何为替换编写 Prolog 代码，所以我们可以计算 beta 减少，例如:

The de Bruijn index 1 refers to the second lambda binder enclosing the de Bruijn index. How would one write Prolog code for a substitution, so that we can compute beta reduction such as:

Kab = a

推荐答案

De Bruijn 索引是一种用于替代比 Prolog 更困难的设置的工具.逻辑变量是一种高级工具.我认为您永远不会想要编写 Prolog 代码来处理 de Bruijn 索引.(元问题在下面回答你.)

De Bruijn indices are a tool for settings where substitution is more difficult than in Prolog. Logical variables are a superior tool. I don't think you would ever want to write Prolog code to deal with de Bruijn indices. (Meta questions back to you below.)

无论如何，PDF 的第二页链接自question 包含所有需要的 Prolog 实现.它只是使用非标准的、所谓的功能性"语法.

Anyway, the second page of the PDF linked from the question contains a Prolog implementation of everything that's needed. It just uses non-standard, so-called "functional", syntax.

这是正确语法中的移位关系:

Here is the shifting relation in proper syntax:

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 减少规则.

You can transcribe the beta reduction rule in the same way.

然后我们可以测试一下.在 PDF 中使用的搞笑语言中，每个基本术语都必须编码为数字，因此我们将选择将 a 编码为 123 和 b456 任意.(K a) b 项的约简将通过减少应用两个减少步骤来完成，首先将 K a 减少到 KA 然后应用KA 到 b.给你:

Then we can test this. In the hilarious language used in the PDF, every basic term must be encoded as numbers, so we will choose to encode a as 123 and b as 456 arbitrarily. Reduction of the term (K a) b will be done by reducing applying two reduction steps, to first reduce K a to KA and then applying KA to b. Here you go:

?- 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 相同.通过定义，您可以更简单、更高效地获得相同的结果:

The result KAB is the same as A. You can get the same more simply and more efficiently by defining:

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 实现数据库?这甚至可能很有趣，但如果您传达一个项目的存在以及它的目的是实现什么，您可能会获得更多的项目参与者.

Meta: Your questions about encoding obscure topics from symbolic logic are not getting a lot of traction. Part of this is because most of them are not very interesting. Part of it is because they lack all detail and demonstration of any effort on your part. But I think a third part is that the community doesn't understand what your whole point with these questions is. It is not a secret that you are an accomplished Prolog programmer and implementor. Obviously you can transcribe a few simple equations into Prolog. So why ask others about it? Is this meant to be some kind of project to set up a "community wiki" or database of Prolog implementations of standard symbolic algorithms? That might even be interesting, but you would probably get more participants in the project if you communicated that a project exists, and what it is meant to achieve.

这篇关于Prolog中基于De Bruijn索引的替换的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！