If there is no recursion in the definitions of the Prolog predicates,
then your Prolog "program" is decidable as a special case of the
decision procedure for Horn clauses in logic.
Recursion can enter Prolog in two (closely related) forms. One is
some circularity of references in the definitions of the predicates
themselves. You are probably familiar with the repeat/0 predicate,
provided as a built-in for many Prolog implementations but which has
the logical equivalent:
repeat.
repeat :- repeat.
Consider the following goal:
main :- repeat, fail.
This Prolog program will never terminate, because repeat will always
succeed on backtracking.
The second way that recursion can enter a Prolog program is through
recursively-defined data structures. Lists, to give a simple example,
are "defined" recursively, and unified Prolog data structures may
"consist" of partially-bound/partially-unbound portions, such as a
list entry "to be named later" or a tail that remains "free" after the
head is bound. Despite this, the unification algorithm (which taken
together with backtracking forms the basic corpus of a Prolog
implementation) is a decidable one (for first-order unification,
albeit one with exponential complexity in most Prolog interpreters).
So I would say that one way to guarantee decidability is to avoid
recursion in predicates (first kind above), but of course this is a
Draconian approach.
More practically one guarantees that a Prolog predicate is decidable,
despite using recursion, by a "proper" definition, sort of a
well-founded induction with certain "base case" clauses together with
some rules that are "reducing" the goal to one or more subgoals that
are provably closer to the base cases with each application.
regards, mathtalk-ga |
