Блог

Голландский математик Николас Говерт де Брейн изобрел эти индексы для представления терминов лямбда-исчисления без присвоения имен связанным переменным. Давайте возьмем это лямбда-выражение:

 K = λx.λy.x
 

При использовании индексов де Брейна, когда мы используем соглашение, как здесь, читается, что нулевой индекс де Брейна относится к первому охватывающему лямбда-связующему:

 K = λλ1
 

Индекс де Брейна 1 относится ко второму лямбда-связующему
, включающему индекс де Брейна. Как можно было бы написать код Prolog для подстановки,
чтобы мы могли вычислить бета-сокращение, например:

 Kab = a
 

Индексы Де Брейна — это инструмент для настройки, где подстановка сложнее, чем в Prolog. Логические переменные — превосходный инструмент. Я не думаю, что вам когда-нибудь захочется писать код Prolog для работы с индексами де Брейна. (Мета-вопросы к вам ниже.)

В любом случае, вторая страница 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) ).
 

Вы можете расшифровать правило бета-редукции таким же образом.

Затем мы можем это протестировать. На веселом языке, используемом в PDF, каждый базовый термин должен быть закодирован как числа, поэтому мы будем кодировать a как 123 и b как 456 произвольно. Сокращение термина (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).
 

Вы, конечно, это знаете.

Мета: Ваши вопросы о кодировании неясных тем из символьной логики не получают большого отклика. Отчасти это связано с тем, что большинство из них не очень интересны. Отчасти это связано с тем, что им не хватает всех деталей и демонстрации каких-либо усилий с вашей стороны. Но я думаю, что третья часть заключается в том, что сообщество не понимает, в чем весь смысл этих вопросов. Не секрет, что вы опытный программист и разработчик Prolog. Очевидно, что вы можете записать несколько простых уравнений в Prolog. Так зачем спрашивать об этом других? Предполагается ли, что это какой-то проект по созданию «вики сообщества» или базы данных реализаций стандартных символьных алгоритмов в Prolog? Это может быть даже интересно, но вы, вероятно, привлекли бы больше участников к проекту, если бы сообщили, что проект существует, и чего он должен достичь.

Я придумал другой подход, который ориентирован на линейную логику. Это означает, что он позволяет избежать вызова funny_arrow/4 внутри substitute/4 при каждом посещении связующего. Вот тестовый пример:

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

Исходный код выглядит следующим образом. Также исправляю опечатку в PDF, но с заглавной буквы, что funny_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).