Denotational Semantics

9 Jan 86 19:41:00 GMT

          From comp.compilers

Related articles
Re: denotational semantics compilers@ima.UUCP (1986-01-07)
Denotational Semantics compilers@ima.UUCP (1986-01-09)
denotational semantics compilers@ima.UUCP (1986-01-10)
Re: denotational semantics compilers@ima.UUCP (1986-01-15)
Denotational semantics compilers@ima.UUCP (1986-01-16)
| List of all articles for this month |

Relay-Version: version B 2.10.2 9/12/84; site mit-hermes.ARPA
Posting-Version: Notesfiles $Revision: $; site ima.UUCP
From: compilers@ima.UUCP
Newsgroups: mod.compilers
Date: 9 Jan 86 19:41:00 GMT
Article-I.D.: ima.136300039
Posted: Thu Jan 9 14:41:00 1986
Date-Received: 11 Jan 86 11:24:04 GMT
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,

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.