I am trying to make a program that divides two Peano numbers. Unfortunately, the cycle starts running after I look for other answers. Is there any way to avoid duplicates using my method?
s(0).
s(X):- X.
plus(0,Y,Y).
plus(s(X), Y, s(Z)):- plus(X,Y,Z).
minus(A, B, C) :- plus(C, B, A).
division(0, _ , 0).
division(X, s(0), X).
division(A, B, s(N)) :- minus(A, B, R), division(R, B, N).
Output
?- division(s(s(s(s(0)))), s(0),X).
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
X = s(s(s(s(0)))) ;
false.
Output#2
?- divide(s(s(s(s(0)))), Y,X).
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(s(s(s(0)))),
X = s(0) ;
Y = X, X = s(s(0)) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
Y = s(0),
X = s(s(s(s(0)))) ;
;ERROR: Out of local stack
Correctness. First, let's consider correctness issues. According to your definition, 0/0 = 0. That is, division(0, 0, 0). So you are stating that dividing 0 by 0 is 0. Another issue is the definition of s/1. See successor-arithmetics for more.
Redundant answers. To identify sources of redundancy, consider the clauses of each predicate. Is it possible that they both apply for the same ground query? Let's see: For plus/3 this cannot happen because the fact needs 0 in the first argument, but the rule needs s(_). This can never happen at the same time. Thus there is no source of redundancy. For division/3 however, both apply for division(0, s(0), 0). Further the second fact and the rule may apply both too.
Non-termination. Before going into the technical details discussed in another answer, let's first take a step back about what you are expecting that you get from 4/X = Y. Evidently, these solutions (X,Y): [(1,4),(2,2),(4,1)]. But what about a solution with 0?