Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!rex!caesar!fs
From: fs@caesar.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.functional
Subject: Re: Define "Declarative" (was:  A question on Semantics)
Keywords: Declarative, Denotational and Operational Semantics
Message-ID: <5492@rex.cs.tulane.edu>
Date: 19 Dec 90 19:49:24 GMT
References: <663@rocksanne.WRC.XEROX.COM>
Sender: news@rex.cs.tulane.edu
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 89


Surya Mantha:	 <663@rocksanne.WRC.XEROX.COM> mantha.wbst128@xerox.com 
>	When is a syntax declarative?

Some will call a language declarative if it has
a declarative subset (regardless how weak :-) ).
I consider a language declarative if programs
can easily (to whom?) be viewed as assertions of fact,
alternative to the conventional view that a program is a command.


>	Note that we talk about the declarative semantics
>	of Horn clauses (cut-free, first order restriction of Prolog).
>	In this case, the terms "denotational" and "declarative"
>	can be used interchangeably.
>	We, however, do not talk of the declarative semantics
>	of C or Pascal, for instance.

For these languages, there is no clear declarative reading.
That's why their denotational semantics are so complicated.

With a referentially-transparant functional language
(free of side-effects) you can argue that certain expressions
denote functions, function arguments, function applications, and so on.
One argues that the entire program can be viewed
as a mathamatical assertion, and thus that the language is declarative.

To be sure, the assertion that such-and-such expression
_denotes_ a function is, by definition, a (possibly informal)
claim about the language's _denotational_ semantics,
and therefore, investigation into the denotational semantics
is required to support such claims.  Furthermore,
until we define the mathamatical domains of discourse,
we cannot even begin to speak about functions
(which are, by definition, `1-to-1' and `onto' domain mappings).
Thus the importance of domain theory.


>	In Mathematical Logic, primacy is given to model theory
>	We prove the *soundness* and *completeness* of the axioms
>	and inference rules of the proof theory wrt the model theory
>	(i.e. notions of validity -- true in all models and so forth).
>	For definite Horn clauses we have the machine independent
>	denotational semantics given by the minimal Herbrand model.
>	Then, the operational semantics via SLD-resolution
>	is proposed, and the soundness and completeness results follow.
>	This is in the general tradition of mathematical logic.
>
>	Consider the analogous enterprise in programming language semantics.
>	Here, the idea is to show the *equivalence* between the operational
>	and denotational semantics of a language.
>	But the direction is reversed.
>	Some kind of a relation (either an equivalence relation
>	or a partial ordering) on program *behaviours* is assumed.
>	The models that we then build are said to be *adequate*
>	and/or *fully abstract*. The burden of *full abstraction*
>	or the stigma of being too *concrete* lies with the models
>	that are constructed to give the denotational semantics. 
>	The operational semantics is, in some sense,
>	prior to the denotational semantics.
>	Why is it not the other way around?
>	Why don't we start with machine independent semantics
>	and then show that the corresponding operational models
>	are sound and complete with respect to them?


Practical declarative language designs are limited to
that which is reasonable for a computer to do,
i.e., the operational semantics.  Therefore,
the operational semantics is thought about first.
Once the denotational semantics are understood,
however, _I_ believe we should make it normative,
at least for the purpose of teaching the language.

The theory of logic developed analogously.
First came the "operational semantics",
as ancient philosophers collected rules of inference.
The model-theory was developed much later,
as understanding increased.  In today's
logic programming community, the typical order is:

	1) propose a useful extension to Prolog,
	   giving the operational semantics;

	2) ignore the model-theoretic implications of the new feature.
   	   :-)

Frank Silbermann	fs@cs.tulane.edu
Tulane University	New Orleans, Louisianna  USA