De Bruijn index based substitution in Prolog

Question

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

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

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

Answer 1

I came up with another take, which is tailored towards linear logic. That means it avoids calling funny_arrow/4 inside substitute/4 every time a binder is visited. Here is a test case:

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

The source code is as follows. Also correcting the typo in the PDF, but capitalizing that funny_arrow/4 can not only take -1 and 1, but also other values:

Warning the below code is not steadfast!

% 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).

Answer 2

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.)

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) ).

And here is substitution:

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) ).

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

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).

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).

and then:

?- 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).

You know this, of course.

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.