compilers@ima.UUCP (01/07/86)
[from ] When I read a denotational semantics, I think of it as an operational semantics written in Scheme (a small Lisp dialect closely resembling the lambda calculus). Such games as making up statically-scoped functions on the fly and passing multiple continuations are standard coding practice in Scheme, but appear nearly inpenetrable, I would imagine, to a person trained solely in traditional algorithmic languages. One neat aspect of looking at things this way is that it is conceivably possible to write a meta-interpreter that can interpret any language, given its denotational semantics. (I believe that this has sort of been done: Peter Mosses' SIS (Semantic Interpretation System)?) -- Richard Schooler Intermetrics, Inc.
compilers@ima.UUCP (01/09/86)
[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
compilers@ima.UUCP (01/10/86)
[from uiucdcs!b.CS.UIUC.EDU!liberte (Daniel LaLiberte)] Do you have a reference for Peter Mosses' SIS? I want to build an incremental compiler based on a denotational specification. Dan LaLiberte liberte@uiucdcs.Uiuc.ARPA ihnp4!uiucdcs!liberte
compilers@ima.UUCP (01/15/86)
[from harvard!seismo!utah-cs!utah-gr!peter (Peter S. Ford)] Organization: University of Utah CS Dept If you are interested in using a denotational specification to build a compiler you might be interested in Lawrence Paulson's Stanford PhD. thesis on "semantic grammars" which are an agglomeration of attribute grammars and denotational semantics. At one point he was distributing his work (several large pascal programs). See Stanford CS report 82-893 for his thesis and look in the 1982 POPL for a short paper. Moses SIS system is documented in a report from Aarhus University, published as a refernce guide in 1979. I believe the report is numbered as DAIMI MD-30. Peter S. Ford (peter@utah-cs)
compilers@ima.UUCP (01/16/86)
[from harvard!seismo!mcvax!euroies.UUCP!rshepherd] Ideally the denotational semantics of a languages supplies its underpinning, for practical purposes there are better techniques around for dealing with language semantics. For example with OCCAM we have an underpinning based on both denotational semantics (for the sequential part of the language) and on a CSP-like failure set model (for the concurrent part). For practical purposes it is best to use an algebraic semantics; for example, in occam there is an equivalence between message passing and assignment, CHAN c : is equivalant to PAR c ! e c ? v v := e this algebraic law is underpinned (mathematically). Roger Shepherd INMOS (...!euroies!rshepherd)