Описание тега 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.