Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!udel!rochester!rocksanne!mum.wrc.xerox.com!mantha
From: mantha@mum.wrc.xerox.com (S. Mantha (co-op))
Newsgroups: comp.lang.functional
Subject: Re: Define "Declarative" (was:  A question on Semantics)
Keywords: Declarative, Denotational and Operational Semantics
Message-ID: <673@rocksanne.WRC.XEROX.COM>
Date: 20 Dec 90 20:37:03 GMT
References: <663@rocksanne.WRC.XEROX.COM> <5492@rex.cs.tulane.edu>
Sender: news@WRC.XEROX.COM
Reply-To: mantha.wbst128@xerox.com
Lines: 86

In article <5492@rex.cs.tulane.edu>, fs@caesar.cs.tulane.edu (Frank
Silbermann) writes:
|>
|>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.

	Are you saying -- please correct me if I am wrong -- that referential
transparency (R.T.) is a *necessary* condition for "declarativeness"? I
don't think 
that (that R.T. is a necessary condition for declarativeness) is a
correct assertion.
It is too strong a requirement to place upon the language. I agree that it is a
sufficient condition for declarativeness.
	Consider intensional sentences such as "I believe that X" or "I know that Y".
Any logic that models such sentences 
(and thus any language whose operational semantics mimics the proof theory for
such a logic) violates the property of referential transparency. I
would, however, not
venture to claim that such a language was not declarative. I feel we
need a sharper notion
of what we mean by declarative programming. 

	As far as functional languages (FL) are concerned, I agree with you
that referential
transparency is a key property. One compromises on the compositionality
of FL by introducing
even such seemingly benign entities as logical variables (consequently
full unification).
While one gets a richer notion of communication--synchronization (with
the logical variables
acting as channels of C and S) than in traditional functional languages
and the ability to
reason with partially instantiated data structures there are several
disadvantages. 
Characterizing the behaviour of logical variables semantically is a
problem. In the presence
of "laziness", one has to deal very carefully with unification. The
semantics should not only
be bottom-avoiding, it should also be top(error)-avoiding. 
	We (Gary Lindstrom and I) have, however, arrived at a somewhat
satisfactory account of
lazy functional languages with logical variables. We use the notion of
Information Systems
(introduced by Scott to give an alternative formulation of domain
theory) to capture the notion
of "constraint solving" inherent in unification. Instead of viewing
programs as plain 
mathematical functions, we view them as entities that impose constraints
on the values of 
logical variables in a *global* logical store -- a term introduced by
Saraswat in his 
thesis. We can show compositionality (modulo the logical store). It
seems plausible that
such a model can be generalized to functional programming with other
kinds of constraint
solving, as in the Constraint Logic Programming model. "Laziness"  would
be of real 
importance as constraints would not have to be reduced to a normal form
at each step of the
computation.

|>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.
|>   	   :-)
	
	I couldn't agree with you more. There is another class of logic programmers
who are exclusively engaged in the enterprise of providing "semantics"
(on an incremental basis) but whose work has little computational content. 
	The worst are those who palm off EXTRA-LOGICAL features as being
*meta-logical*.

cheers
Surya Mantha
University of Utah and
Xerox, Webster Research Center