Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: Notesfiles $Revision: 1.6.2.16 $; site ima.UUCP
Path: utzoo!linus!philabs!cmcl2!harvard!bbnccv!ima!compilers
From: compilers@ima.UUCP
Newsgroups: mod.compilers
Subject: Denotational Semantics
Message-ID: <136300039@ima.UUCP>
Date: Thu, 9-Jan-86 14:41:00 EST
Article-I.D.: ima.136300039
Posted: Thu Jan  9 14:41:00 1986
Date-Received: Sat, 11-Jan-86 06:12:21 EST
Lines: 51
Approved: compilers@ima.uucp
Nf-ID: #N:ima:136300039:000:2546
Nf-From: ima!compilers    Jan  9 14:41:00 1986


[from cornell!pavel (Pavel Curtis)]

Organization: Cornell Univ. CS Dept, Ithaca NY

Wendy Thrash writes:
> I'd also like to know what people in the know think about denotational
> semantics.  Deciphering it seems to be about as simple as reading a German
> translation of _Finnegan's Wake_; is it worth the trouble?

As a practitioner of denotational semantics, I suppose I qualify as
being ``in the know''.  I believe that it is ``worth the trouble'' to
anyone who needs to accurately describe the meanings of formal languages.
The major alternatives (operational and axiomatic, attribute grammars falling
into the first category) have their uses, and anyone involved in precise
description should be familiar with them, but there are languages which
cannot reasonably be described with them.  For example, my current work
includes the description of the meanings of type expressions in a certain
polymorphic programming language.  I cannot conceive of a useable axiomatic
or operational meaning for these.

Further, I am using this denotational description of the type language to
show that a certain logic for proving assertions of the types of program
expressions is mathematically sound.  That is, I need to prove that if one
can derive in the logic a statement that an expression E has a type Tau, 
then it is the case that the value resulting from evaluation of E is in
fact a member of the set denoted by Tau.  I see no way to structure such
an argument conveniently using anything but a denotation semantics for
both program expressions E and type expressions Tau.

As a final note, the use of denotational semantics instead of operational
ones avoids the possibility of ``implementation-specific'' idiosyncrasies;
after all, an operational description is really just a high-level interpreter
for the given language.  This is not to say that such idiosyncrasies are
inevitable in operational descriptions, but far harder to avoid than in the
denotational case.

To stave off the inevitable requests for references, here are a paper and a
book on denotational semantics.  You can pick your desired level of detail.

Tennent, R.D., ``The denotational semantics of programming languages'',
    Communications of the ACM, vol. 19, no. 8, pp. 437-453, 1976.

Stoy, J.E., Denotational Semantics: The Scott-Strachey Approach to
    Programming Language Theory, MIT Press, Cambridge, Mass., 1977.

I hope that this makes the issues a bit clearer.

	Pavel Curtis
	Xerox PARC / Computer Science Lab
	decvax!cornell!pavel, or, Pavel.pa@Xerox.arpa