🚀 go-pugleaf

> In article <1021@watdragon.UUCP> rggoebel@watdragon.UUCP writes:
> >I don't believe that cut, var, and
> >nonvar cannot be described logically, just because they aren't in Prolog
> >implementations.
> 
> The reason why cut, var and nonvar cannot be "described logically" is that
> they are non-logical (or meta-logical, if you wish) primitives, that is
> primitives used to control the search for proofs.

Perhaps you mean "... cannot be described logically using first order
predicate calculus".  

> The meaning of these primitives are dependent of the particular way an
> implementation looks for proofs. With a different implementation you
> could be forced to give a different meaning to cut, var and nonvar, or
> even find that they couldn't be given any meaning at all.

If the constructs are in any way "understandable", you ought to be able to
find mathematical models for them.  In the case of "cut", "var" etc. there's
a good chance these won't look like the Herbrand models we Prolog hackers are
accustomed to, of course, but that's rather different from saying that they
couldn't be given any meaning at all.

There has, in fact, been some work on giving the semantics of Prolog
(i.e. textual order on literals and clauses + Cut) using classical
denotational semantics, in terms of continuous functions over CPOs.
References are:

- Jones & Mycroft, "Stepwise Development of Denotational and Operational
		    Semantics for Prolog", Proc. 1st ISLP, Atlantic City,
		    Feb 1984.

- Debray & Mishra, "Denotational and Operational Semantics for Prolog",
		    Proc. Conf. on Formal Description of Programming
		    Concepts, Lyngby, Denmark, Aug 1986 (to appear).
-- 
Saumya Debray
SUNY at Stony Brook

	uucp: {allegra, philabs, ogcvax} !sbcs!debray
	arpa: debray%suny-sb.csnet@csnet-relay.arpa
	CSNet: debray@sbcs.csnet