Re: pure Prolog

Hi Uli (and the RIF list),

> Am I right in assuming that SLD-resolution doesn't necessarily  
> terminate (otherwise, Horn logic would be decidable, which it isn't?!)

Yes, though I would attribute this to the language (Horn Clause, ie,
definite programs), not to any specific procedure (it is true for all of them).

> so, what kind is the "non-determinism" then? I am afraid "don't  know"? 
> Ie, depending on the order, it might or might not terminate  (yet, 
> regardless of the order, it always gives the same answer, it it  gives 
> one):

SLD is nondeterministic in the sense that it does not have to specify
two choices:
- goal selection or computation rule [LLoyd] - any fixed computation
rule will do.
- clause selection or search rule - it only has to be fair,
so that each success branch is eventually found.

"Standard/pure" Prolog does specify the choices: it implements depth-first
search rule (which is not fair) and can fall into an infinite branch.
Then, there is a question of "occurs-check" in unification which
might give rise (the lack of it) to unsoundness.

> SLD-resolution is a sound and complete inference procedure which
> does not necessarily terminate. However, the resolution algorithm or  
> SLD-refutation procedure
> is "don't know" non-deterministic and leaves open the order in which  atoms
> in the body are selected and the order in which clauses are tried.

I would separate the issue of decidability (and halting problem) from
the issues of Horn Clauses vs. pure Prolog.
The first has to do with the choice of the language (Turing complete)
while the second is the question of operational semantics and its
actual execution model.

Regards,
Igor

Received on Monday, 10 April 2006 11:21:20 UTC