RE: pure Prolog

Michael Kifer has done a good job reflecting how the term 'Pure Prolog"
is in use and suggested that because it is ambiguous, and that one of
its definitions is snynnymous with Horn Clauses, that the latter term
always be used when referring to Horn Clauses.

This is entirely sensible.

It is also useful to tease apart the technical issues that underly the
different related notions.

Assuming there is no pressing need, per se, to define the term "Pure
Prolog" and given it is ambiguous, perhaps it makes sense to just not
use it in most technical discussions. The concepts are more important
than the terms.

Mike

-----Original Message-----
From: Igor Mozetic [mailto:igor.mozetic@ijs.si] 
Sent: Monday, April 10, 2006 4:19 AM
To: Uli Sattler
Cc: public-rif-wg@w3.org
Subject: 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 15:09:19 UTC