4

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
false
  • 10,264
  • 13
  • 101
  • 209
Ignas Ausiejus
  • 175
  • 1
  • 1
  • 9

1 Answers1

5

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

false
  • 10,264
  • 13
  • 101
  • 209