🚀 go-pugleaf

In article <10805@cs.tulane.edu> feldman@cs.tulane.edu (Damon Feldman) writes:
>What are the advantages to the formal semantics of (pure) Prolog?
>In particular what are the individual advantages of the fixpoint
>semantics and the least model semantics?
>
>My feeling is that the model-theoretic semantics (declaritive) is by
>far more important than the others, because it allows the programmer
>to think in the predicate calc. rather than mentally model the actions
>of the interpretor. 

Predicate calculus is totally inadequate as a tool to think
about Prolog programs (even pure Prolog) !

Facts:
	repeat , fail		is an endless loop
+	fail , repeat		stops immediatly
------	--------------  	------------------
conclusion			',' is not modelled by the predicate
				calculus operator 'and'

Same thing can be told about ';' and 'or' (';' is not commutative),
and what about idempotence, distributivity... ? Clearly, Pre. Calc.
doesn't work if you have to consider the possibility of infinite
computations, the order in which the solutions are produced
and such things relevant to programming.

On the other hand, it can be shown (in a recent paper by me, hurray :-)
that the behaviour of ';',',' true and fail in "Pure Prolog + I-O"
can be described by a pepsi-axiomatization (looks like Pred-calc,
but isn't !) :-)

>The fixpoint semantics is then little more than a
>link to the least model semantics. 

And thus is a inappropriate tool, for the same reason!

M Billaud

PS: "Axiomatizations of Backtracking" by M Billaud
	in Proceedings STACS'92, LNCS xxx-- 
Michel BILLAUD                 :  billaud@geocub.greco-prog.fr
Departement d'Informatique     :  phone W: 56.84.57.92  // 56.84.69.22
IUT "A", Universite Bordeaux I :  "Je n'y comprends rien,
33405 Talence  (FRANCE)        :   ca doit etre de l'informatique"