Re: pure Prolog

On 10 Apr 2006, at 12:19, Igor Mozetic wrote:

> 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.
>

...but I guess it would still help to know whether this non- 
determinism might "only" affect the performance, or the answer  
behaviour as well: i.e., depending on the choice, you might either  
end with a (correct) answer or without any answer due to non- 
termination.

> "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.

I completely agree with you: I only tried to see more clearly what we  
mean by

- sound and complete inference procedure (namely a sound, complete,  
but not terminating one) and by
- non-deterministic (namely a non-determinism that not only  
influences the procedure's performance, but also its answer behaviour)

Cheers, Uli

>
> Regards,
> Igor

Received on Monday, 10 April 2006 11:27:34 UTC