Stack Overflow
Stack Overflow

Questions tagged [non-termination]

In Prolog programs there are two kinds of non-termination: Existential and universal non-termination.

Universal termination of a query Q means that the query

?- Q, false.

terminates. Many Prolog programs can not and must not terminate universally. For example, the predicate length/2 describes lists of arbitrary length, and universal termination of the most general query in this case would mean that the predicate is incomplete.

Existential termination, on the other hand, occurs for example when a solution is found and reported.

There are ways to reason declaratively about termination properties of Prolog programs. The goal of termination analyzers for Prolog programs is to deduce more information about their termination properties. Termination analysis for subsets of Prolog is a field of active research in the logic programming community.

Non-termination is the lack of termination.

See also .

34 questions
42
votes
2 answers

Prolog successor notation yields incomplete result and infinite loop

I start to learn Prolog and first learnt about the successor notation. And this is where I find out about writing Peano axioms in Prolog. See page 12 of the PDF: sum(0, M, M). sum(s(N), M, s(K)) :- sum(N,M,K). prod(0,M,0). prod(s(N), M, P) :- …
Felastine
  • 793
  • 2
  • 8
  • 18
14
votes
1 answer

Steadfastness: Definition and its relation to logical purity and termination

So far, I have always taken steadfastness in Prolog programs to mean: If, for a query Q, there is a subterm S, such that there is a term T that makes ?- S=T, Q. succeed although ?- Q, S=T. fails, then one of the predicates invoked by Q is not…
mat
  • 40,498
  • 3
  • 51
  • 78
9
votes
1 answer

Proving False with negative inductive types in Coq

The third chapter of CPDT briefly discusses why negative inductive types are forbidden in Coq. If we had Inductive term : Set := | App : term -> term -> term | Abs : (term -> term) -> term. then we could easily define a function Definition uhoh (t…
user287393
  • 1,221
  • 8
  • 13
5
votes
2 answers

Prolog predicate - infinite loop

I need to create a Prolog predicate for power of 2, with the natural numbers. Natural numbers are: 0, s(0), s(s(0)) ans so on.. For example: ?- pow2(s(0),P). P = s(s(0)); false. ?- pow2(P,s(s(0))). P = s(0); false. This is my code: times2(X,Y) :- …
WordToTheWise
  • 93
  • 2
  • 2
  • 7
5
votes
1 answer

Find path and its length between nodes in a graph

I'm trying to solve this problem and I've already read this answer, but my problem is with infinte looping even if I've used a visited node list. Let's see my two…
tuxErrante
  • 1,274
  • 12
  • 19
4
votes
1 answer

Is there a cut-less way to implement same_length/3?

Say I want to assert that three lists are of the same length. I could do something like this: same_length(First, Second, Third) :- same_length(First, Second), same_length(Second, Third). This does the right thing when either First or Second are…
num1
  • 4,825
  • 4
  • 31
  • 49
4
votes
0 answers

Agda: how to do non-terminating IO (getLine) without (the deprecated?) ∞-style coinduction?

In this question about how to do getLine in Agda the main answer suggests using the partiality monad to deal with the possible non-termination of working with the resulting Costring. On the other hand, in version 2.5.3 the manual page on Coinduction…
André Gustavo Rigon
  • 73
  • 4
4
votes
1 answer

Monkey and banana in Thinking as Computation

I am reading the book Thinking as Computation and wrote the code as chapter 9.4: plan(L) :- initial_state(I), goal_state(G), reachable(I, L, G). initial_state([]). legal_move(S, A, [A | S]) :- poss(A, S). goal_state(S) :- …
Cu2S
  • 667
  • 1
  • 5
  • 21
3
votes
1 answer

How to choose the design for a well-founded inductive type?

While studying well-foundedness, I wanted to see how different designs behave. For example, for a type: data _<_ (x : Nat) : Nat -> Set where <-b : x < (suc x) <-s : (y : Nat) -> x < y -> x < (suc y) well-foundedness is easy to demonstrate.…
Sassa NF
  • 5,306
  • 15
  • 22
3
votes
2 answers

Prolog parsing is running out of stack

I have this code s(W) :- append(W1,W2,W), np(W1), vp(W2). vp(W) :- append(W1,W2,W), v(W1), np(W2). np(W) :- ( append(W1,W2,W), pn(W1), ph(W2) ; append(W1,W2,W), det(W1), n(W2) …
bngschmnd
  • 111
  • 1
  • 10
3
votes
2 answers

Prolog: check if two lists have the same elements

I am new to Prolog and I am having a problems checking if two lists have exactly the same elements. It is possible for the elements to be in different orders. I have this code: myremove(X, [X|T], T). myremove(X, [H|T], [H|R]) :- myremove(X, T,…
minus
  • 320
  • 1
  • 5
  • 14
3
votes
2 answers

Transforming a sentence creates an infinite loop - but how?

I can't figure out where this is going wrong. Please note that I am very new to Prolog and I'm sure I'm missing something - just no idea what that might be. Could anyone help me out please? Thanks, here is my code: printSentence([]). …
rtheunissen
  • 7,347
  • 5
  • 34
  • 65
2
votes
1 answer

Is Well-Founded recursion safe?

In the question about non-termination With clauses obscuring termination an answer suggests to recourse to <-wellFounded. I looked at the definition of <-wellFounded before, and it strikes me there is a --safe in OPTIONS. Is it meant to work without…
Sassa NF
  • 5,306
  • 15
  • 22
2
votes
2 answers

Prolog clause terminates individually, but not together

So ?- canCall(mary, Person). works and terminates and ?- canFind(mary, Person). also works and terminates. But somehow ?- canCall(mary, Person), canFind(mary, Person). does not terminate. What may be a possible reason?
absolutelydevastated
  • 1,657
  • 1
  • 11
  • 28
2
votes
1 answer

Prolog - some basic arithmetic operations implementation

I am new to Prolog, and need to implement some basic arithmetic operations on natural numbers, without using the built-in predicates. I represent natural number Term in unary notaion, meaning I have the constant 0, and the recursive successor…
Mike
  • 575
  • 1
  • 5
  • 15
1
2 3