Reputation: 280
I need to implement binary addition in prolog, where binary numbers are represented as follows:
0: bot
1 : o(bot)
2 -> 10: z(o(bot))
3 -> 11: o(o(bot))
10 -> 1010: z(o(z(o(bot))))
I've written this:
add(X,bot,X):-!.
add(bot,X,X):-!.
add(z(X),z(Y),Res):- add(X,Y,D), Res = z(D).
add(z(X),o(Y),Res):- add(X,Y,D), Res = o(D).
add(o(X),z(Y),Res):- add(X,Y,D), Res = o(D).
add(o(X),o(Y),Res):-addc(X,Y,D), Res = z(D).
addc(X,bot,Res):-add(X,o(bot),Res),!.
addc(bot,X,Res):-add(X,o(bot),Res),!.
addc(z(X),z(Y),Res):- add(X,Y,D),Res = o(D).
addc(z(X),o(Y),Res):-addc(X,Y,D),Res = z(D).
addc(o(X),z(Y),Res):-addc(X,Y,D),Res = z(D).
addc(o(X),o(Y),Res):-addc(X,Y,D),Res = o(D).
It works when the first 2 arguments are concrete:
?-add(o(o(bot)),z(o(o(bot))),D).
D = o(z(z(o(bot))))
When one of the first 2 arguments is a variable, it goes into an infinite recursion:
?-add(o(o(bot)),X,z(o(o(bot)))).
Stack limit (0.2Gb) exceeded
Stack sizes: local: 0.1Gb, global: 34.9Mb, trail: 11.6Mb
Stack depth: 1,524,958, last-call: 50%, Choice points: 762,476
Possible non-terminating recursion:
[1,524,958] add(bot, <compound s/1>, _1496)
[1,524,957] add(bot, <compound s/1>, <compound z/1>)
How can i make this work for any one non-concrete argument?
Upvotes: 2
Views: 188
Reputation: 10102
(Using bot
for what is otherwise considered zero
, null
or 0
is a bit odd. Lattices are not our major concern here.)
First, we try to understand why the program does not terminate. This can be quite tricky, in particular in presence of the !
which is one of Prolog's impure elements. They are needed to a certain degree, but here in this case, they are harmful only, as they are hindering our reasoning. So instead of the first two cutful clauses, write1
add(bot, X, X).
add(X, bot, X) :- dif(X, bot).
and similarly for the next two cuts. Note that those two clauses are now disjoint. After this we have a pure monotonic program and thus we can apply various reasoning techniques. In this case, a failure-slice is just what we need. To better understand the reason for non-termination, I will add goals false
into the program, for there is a nice property we can exploit: If the new program does not terminate, then also the old one will not terminate. In this manner we can narrow down the problem to a smaller part of the original program. After a couple of tries, I came up with the following failure-slice:
add(bot,X,X) :- false.add(X,bot,X) :- false, dif(X,bot).add(z(X),z(Y),Res) :- false, add(X,Y,D), Res = z(D).add(z(X),o(Y),Res) :- false, add(X,Y,D), Res = o(D).add(o(X),z(Y),Res) :- false, add(X,Y,D), Res = o(D).add(o(X),o(Y),Res) :- addc(X,Y,D), false,Res = z(D). addc(bot,X,Res) :- add(X,o(bot),Res), false. addc(X,bot,Res) :- dif(X, bot), add(X,o(bot),Res), false.addc(z(X),z(Y),Res) :- false, add(X,Y,D), Res = o(D).addc(z(X),o(Y),Res) :- false, addc(X,Y,D), Res = z(D).addc(o(X),z(Y),Res) :- false, addc(X,Y,D), Res = z(D).addc(o(X),o(Y),Res) :- addc(X,Y,D), false,Res = o(D).?- add(o(o(bot)),X,z(o(o(bot)))).
Out of the ~2^23 possible failure slices, this appears to be a minimal one. That is, any further false
makes the program terminate.
Let's look at it: Everywhere Res
is either ignored or just passed further on. Therefore the third argument has no influence on termination whatsoever. But you can put all those Res =
equations just after the :-
. That's the earliest possible place.
add(bot,X,X).
add(X,bot,X):- dif(X,bot).
add(z(X),z(Y), z(D)) :- add(X,Y,D).
add(z(X),o(Y), o(D)) :- add(X,Y,D).
add(o(X),z(Y), o(D)) :- add(X,Y,D).
add(o(X),o(Y), z(D)) :- addc(X,Y,D).
addc(bot,X,Res):- add(X,o(bot),Res).
addc(X,bot,Res):- dif(X, bot), add(X,o(bot),Res).
addc(z(X),z(Y),o(D)):- add(X,Y,D).
addc(z(X),o(Y),z(D)):- addc(X,Y,D).
addc(o(X),z(Y),z(D)):- addc(X,Y,D).
addc(o(X),o(Y),o(D)):- addc(X,Y,D).
Also cTI gives favorable termination conditions:
% NTI summary: Complete result is optimal.
add(A,B,C)terminates_if b(A),b(B);b(C).
% optimal. loops found: [add(z(_),z(_),z(_)),add(o(bot),o(o(_)),z(z(_))),add(o(o(_)),o(bot),z(z(_)))]. NTI took 8ms,72i,30i
addc(A,B,C)terminates_if b(A),b(B);b(C).
% optimal. loops found: [addc(z(z(_)),z(z(_)),o(z(_))),addc(bot,o(_),z(_)),addc(o(_),bot,z(_))]. NTI took 4ms,96i,96i
So add/3
terminates either if the first two, or the last argument are given. So you do not need the first argument. In stead, even the more general query terminates:
?- add(X,Y,z(o(o(bot)))).
X = bot, Y = z(o(o(bot)))
; X = z(o(o(bot))), Y = bot
; X = z(bot), Y = z(o(o(bot)))
; X = z(o(o(bot))), Y = z(bot)
; X = z(z(bot)), Y = z(o(o(bot)))
; X = z(z(o(bot))), Y = z(o(bot))
; X = z(z(z(bot))), Y = z(o(o(bot)))
; X = z(z(o(bot))), Y = z(o(z(bot)))
; X = z(o(bot)), Y = z(z(o(bot)))
; X = z(o(o(bot))), Y = z(z(bot))
; X = z(o(z(bot))), Y = z(z(o(bot)))
; X = z(o(o(bot))), Y = z(z(z(bot)))
; X = o(bot), Y = o(z(o(bot)))
; X = o(z(o(bot))), Y = o(bot)
; X = o(z(bot)), Y = o(z(o(bot)))
; X = o(z(o(bot))), Y = o(z(bot))
; X = o(z(z(bot))), Y = o(z(o(bot)))
; X = o(z(o(bot))), Y = o(z(z(bot)))
; X = Y, Y = o(o(bot))
; X = o(o(bot)), Y = o(o(z(bot)))
; X = o(o(z(bot))), Y = o(o(bot))
; X = Y, Y = o(o(z(bot)))
; false.
1 And even better, use if_/3
of library reif
for SICStus and
SWI to keep those clauses as determinate as possible.
add(A, B, C) :- if_(A = bot, B = C, ( B = bot, A = C ) ).
Upvotes: 2