Path: utzoo!yunexus!geac!syntron!jtsv16!uunet!munnari!munnari.oz!lee From: lee@munnari.oz (Lee Naish) Newsgroups: comp.lang.prolog Subject: Re: The meaning of "declarative" Message-ID: <2452@munnari.oz> Date: 10 Oct 88 08:17:44 GMT Article-I.D.: munnari.2452 References: Sender: news@munnari.oz Reply-To: lee@munmurra.UUCP (Lee Naish) Distribution: comp.lang.prolog Organization: University of Melbourne, Comp Sci Dept Lines: 34 The meaning is summed up in the first chapter ("declarative semantics") on page 24 of the first edition of Lloyd's book. It defines theta to be a correct answer substitution for a program P and goal G if the universal closure of G theta is a logical consequence of P (that is, all instances of G theta are true in all models of P). This definition is given before SLD resolution, the operational semantics of Prolog, is discussed at all. The basic semantics of pure Prolog can be given without any operational concepts. Most functional languages and imperative languages have semantics based on operational concepts such as reduction and assignment. However, this does not necessarily mean that declarative semantics do not exist for such languages. We should therefore be wary of calling such languages non-declarative (or even non- logic programming). Are difference lists (etc) a problem? If you misunderstand them they are, otherwise they are not (after all, they are just terms). Thinking that [1,2,3] \ [3] is the same as [1,2] is like thinking that 3 - 1 is the same as 2. The fact that some people get expressions confused with numbers does not mean that expressions cause a problem for the semantics of the language. Is incompleteness a problem? Unfortunately, there is not yet a theorem prover implementation which is complete (you need an unbounded amount of memory for a start). One of important features of SLD resolution is that queries with correct answers substitutions will not finitely fail. This means that negation as failure is sound. In programming languages, as opposed to theorem proving systems, we want to be able to specify algorithms and completeness is less important. lee