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.