|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)|
|Relay-Version:||version B 2.10.2 9/12/84; site mit-hermes.ARPA|
|Posting-Version:||Notesfiles $Revision: 184.108.40.206 $; site ima.UUCP|
|Date:||9 Jan 86 19:41:00 GMT|
|Posted:||Thu Jan 9 14:41:00 1986|
|Date-Received:||11 Jan 86 11:24:04 GMT|
|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
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.
Xerox PARC / Computer Science Lab
decvax!cornell!pavel, or, Pavel.pa@Xerox.arpa
Return to the
Search the comp.compilers archives again.