Path: utzoo!utgpu!water!watmath!clyde!att!osu-cis!tut.cis.ohio-state.edu!rutgers!pyrnj!pyrdc!uunet!mcvax!enea!kth!sics!sics.se!alf
From: alf@sics.se (Thomas Sj|land)
Newsgroups: comp.lang.prolog
Subject: Re: The meaning of "declarative"
Message-ID: <ALF.88Oct17171258@hathor.sics.se>
Date: 17 Oct 88 16:12:58 GMT
Sender: news@sics.se
Distribution: comp
Organization: Swedish Institute of Computer Science, Kista
Lines: 89


Some comments to the text by lee@munnari.oz (Lee Naish) 
<2452@munnari.oz>:

>The meaning is summed up in the first chapter ("declarative
>semantics") on page 24 of the first edition of Lloyd's book.

The definition of the word "declarative" is not found on this page.

There are definitions of the concepts "correct answer substitution",
"relation" and "partial order". The adjective "declarative" is used
in the following phrases:
	"This definition of correct answer substitution captures
	 the intuitive meaning of a 'correct answer'. It provides a 
	 declarative understanding of the desired output 
	from a program and a goal. ... showing the equivalence between 
	this declarative concept and the corresponding procedural one, 
	which is defined by the refutation procedure used by the system."

It seems that an "understanding" and a "concept" can be "declarative".
What a "procedural" concept is I don't even dare to ask...:-)

I didn't really want to argue about Lloyd's book which explains many
things about the semantics of "logic programs" in a reasonable way
(even though some logicians I know claim that the notions used are
unnecessarily complex for the task).  The task of proving this
equivalence is important if you want to say that programs can be read
as logical axioms, where results follow logically from the program and
the query seen as a specification.  (I don't really understand why you
need to prove this for ALL MODELS, though, since the least Herbrand
model is the only one a "logic programmer" is interested in, but
perhaps it is not more difficult.)

The natural reading of "declarative" in this context becomes "model
theoretic": "model theoretic understanding", "model theoretic concept".

But what is a "model theoretic language" ?

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

Exactly so. I can't think of a language that cannot be given a
"declarative reading". I think that the point originally made by
advocates of logic programming is perhaps that this reading is so
evidently natural. As long as you do not add intension to the program,
i.e., e.g. difference structures, which are NOT a part of the
"declarative reading", but may make perfect sense given a proper
methodology, just like other features of the language. Problems arise
in program transformation, though.

>The fact that some people get
>expressions confused with numbers does not mean that expressions
>cause a problem for the semantics of the language.

Let me just refer to the result discussed by Soendergaard and Marriot 
in another entry. If things were so trivial as you imply, they wouldn't
have a result to present.

>Is incompleteness a problem? 
Well no, I guess I said something unclear about that earlier. I was
trying to relate the notion of "declarativeness" to "completeness"
and various forms of correctness (partial, total), but that line
of thought seems unfruitful. 

Just two concluding citations from your text:

>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.
Doesn't this say that completeness of SLD-resolution is necessary
for the understanding of negation as failure ?

>In programming languages, as opposed to theorem proving systems,
>we want to be able to specify algorithms and completeness is less
>important.

So what does SLD-resolution have to do with a programming language
anyway ? 

(This can go on and on. Shall we stop now ?  People will get bored. 
 I am sure they all have some important hacks to finish. :-)

	/Thomas
--
Thomas Sj|land
SICS, PO Box 1263, S-164 28 KISTA, SWEDEN
Tel: +46 8 752 15 42	Ttx: 812 61 54 SICS S	Fax: +46 8 751 72 30
Internet: alf@sics.se or {mcvax,munnari,ukc,unido}!enea!sics.se!alf