What constitutes denotational semantics?

Question

On a different thread, Andrej Bauer defined denotational semantics as:

the meaning of a program is a function of the meanings of its parts.

What bothers me about this definition is that it doesn't seem to single out what is commonly thought of as denotational semantics from what is commonly thought of as non-denotational semantics, namely structural operational semantics.

More precisely, the key ingredient here is modularity, or compositionality, of the semantics, or put differently, the fact that they are defined according to the abstract structure of the program.

As most (all?) formal semantics nowadays tend to be structural, is this the required definition?

So, my question is: What is denotational semantics?

Meaning can be given in many forms: pre-post conditions, operation of an abstract machine, a mathematical entity, a game strategy. In all modern approaches, these meanings are given as a function of the meaning of the parts. — Ohad Kammar, Dec 06 '10 at 00:00
I am no expert, but if I remember correctly the reason Dana Scott and Christopher Strachey developed domain theory was to get a mathematical meaning satisfying $[D \rightarrow D] \cong D$, i.e. the function space is isomorphic to the space itself. I don't think that works for those you have stated above. (It seems to me that modularity for any kind of meaning simply follows from the fact that the composition of the meanings of two programs should be equal to the meaning of the composition.) — Kaveh, Dec 06 '10 at 00:10
The question of the existence of $[D\rightarrow D]\cong D$ initiated the study of domain theory. It stemmed out of the denotational approach, but does not define it (for example, the language in question might not even have function spaces). As to modularity, as I said above, basically every modern approach to semantics have compositionality in a suitable sense. — Ohad Kammar, Dec 06 '10 at 00:12
Ok, please stop spreading the false opinion that $[D \to D] = D$ initiated or motivated domain theory, because it did not. Dana Scott wanted domain theory to be a mathematical theory suitable for the typed $\lambda$-calculus. The fact that it also gave a model of the untyped $\lambda$-calculus was an accident. I know, he told me so. — Andrej Bauer, Dec 06 '10 at 14:48
Thanks for the correction. What I meant was that in his unpublished "Type Theoretical Alternative to ISWIM", he advocated to abandon looking for $[D\rightarrow D]=D$, and started looking for models for typed $\lambda$-calculus. In the process, he discovered a solution $D$ to the above domain equation. Thus, the question of non-existence of $[D \rightarrow D]\cong D$, which was postulated to be positive (but turned out to be negative), hence led to domains initiated domain theory. Am I being wrong here as well? — Ohad Kammar, Dec 06 '10 at 19:20
Not sure that's helping, but the way I see "current" denotational semantics work is "compilation of the language into some category" -- indeed you could write semantics in term of well-known mathematical objects without insisting on the category structure, but that's a fair characterization of the specific examples I've encountered. — gasche, Feb 26 '12 at 17:43
Since you can see any set as a (trivial) category, it's unclear what constraints your characterisation puts on translation. — Martin Berger, Feb 28 '12 at 15:21
"the meaning of a program is a function of the meanings of its parts" -- that's compositional semantics, at least in natural language semantics. — Sylvain, Mar 02 '12 at 16:12

score 30 · Answer 1 · answered Dec 06 '10 at 03:55

The distinction I personally make between denotational and operational semantics is something like this:

denotational semantics is mathematical and equational. The details of the reduction matter less than the end result, which is a timeless value in some mathematical space.
operational semantics is algorithmic. It unfolds in individual steps in time. The process is part of the the meaning, and the end result is just a distinguished step in that process.

The difference can sometimes be quite subtle, and it can be hard to tell if it is just a difference in style, or in substance.

However, we can see how Andrej's compositional definition follows more naturally from the denotational definition, and we can also easily imagine a non-confluent, non-compositional semantics that still meets the operational definition.

A good example of the algorithmic-vs-mathematical difference is the treatment of nontermination. The denotation of a loop is bottom, but because of the halting problem, it's undecidable whether the denotation of an arbitrary program is bottom. In small-step semantics, instead, you can observe reduction steps, but the theory has no "bottom" value. Undecidability and nontermination move to the metatheory: what's undecidable is whether a sequence of reduction terminates. Similarly, in big-step semantics it's undecidable whether there is a derivation. — Blaisorblade, May 11 '14 at 19:27

score 25 · Answer 2 · answered Dec 06 '10 at 14:53

25

If I were to guess what Dana Scott would say, he'd probably say that denotational semantics is compositional (like what I claimed) and that the meaning of a program must be a genuine mathematical object, not some syntactic or formalist entity. Of course, such a view requires one to differentiate between formal manipulation of syntax and "true" mathematics. This is necessarily a non-mathematical distinction.

As an afterthought, one would presumably want the meaning to be adequate in the sense that two observationally different program do not receive the same meaning. Of course, adequacy of this kind depends on what one admits as "observation".

Under this view it could be argued that structural operational semantics is not denotational semantics because it equates the meaning of a syntactic entity with another syntactic entity (a value or a reduction sequence).

answered Dec 06 '10 at 14:53

Andrej Bauer

28,823
1
80
133

4

From time to time, I'm being told that transition systems are not as mathematical as domains or lattices or orders. I find this view baffling. All can be expressed in ZFC set theory. – Martin Berger Dec 06 '10 at 15:33
1

Considering how precisely a given semantics can model a compuational phenomenon is a more interesting approach, and is indeed crucially dependend on the chosen notion of observation. One of the key advantages of operational semantics (e.g. process theory) is precisely that natural notions of observation are much more easily definable in comparison with order-theoretic semantics. – Martin Berger Dec 06 '10 at 15:36
1

@Martin Berger: The traditions of mathematics are definitely inclined to timelessness, or to treat time as "just" another dimension in some space. Many computational formalisms, such as transition systems, are dependent on a more realistic asymmetric model of time. The difference can be subtle in some cases, but I think it actually has a big impact on how you end about thinking about things. I guess it's not that unusual for there to be discipline-related tastes in such matters. ;-) – Marc Hamann Dec 06 '10 at 16:14
3

@Marc: I agree with you that operational methods don't model computation as a function. But I don't see why that makes order-theoretic approaches "more mathematical". Physics-influenced mathematics like differential equations models the evaluations of certain systems over time. The input-output approach itself uses a rudimentary temporal structure, namely that the output isn't available before the input. – Martin Berger Dec 07 '10 at 12:26
2

@Martin: Mathematicians often complain that what physicists do isn't real math either. ;-) Physics is just a more comfortably established science at this point in time. TCS is still relatively the new kid on the block. I think TCS shouldn't worry about making people in a different discipline (no matter how much we personally like it) happy; we have our own mojo on the go (just like the physicists). – Marc Hamann Dec 07 '10 at 17:19
3

@Marc: arbitrary garbage can be expressed in ZFC, so that's not much of a criterion to rely on. Semantics in which "functions" in a programming language are interpreted as functions in the mathematical sense has at least two advantages. Firstly, it fits well with how people think of functions in a programming language. Secondly, functions are familiar mathematical objects so there is a lot of machinery that one can use. Of course, transition systems have their uses too. – Andrej Bauer Dec 14 '10 at 22:18
1

@Andrej: Just noticed this comment, so am replying now. My one qualm with what you say is that for many people, their intuitive sense of a mathematical function is tied up with at least a naive ZFC sense of what a function is. It can be tricky, as you know, to ensure that only graph expansions that are effective get considered without additional machinery. This is why I appreciate your work, among others. I still think that more overtly computational models are "safer" for most casual purposes, since it is harder to express "arbitrary garbage" that way without sophisticated machinery. – Marc Hamann Feb 26 '12 at 17:38
I'd say our naive, everyday intuitions about functions are insufficiently precise for highly demanding applications in programming languages with advanced effects. – Martin Berger Feb 28 '12 at 15:32
1

@Marc: I don't think Andrez was saying there is anything wrong with ZFC, but he is questioning what is expressed in it. But, note that he is not sticking by the original definition from Dana Scott, viz., the meaning must be an object in a mathematical space. He is making a judgement about which mathematical space is being used. I think it is fine to make such judgements. But he can't deny whether something is denotational on that basis. (This discussion is getting fascinating. Can somebody turn it into a chat so we are not limited by the comment boxes?) – Uday Reddy Feb 29 '12 at 16:54
Andrez privately admitted to me that in his initial comment, which Ohad branded as "definition of denotational semantics", Andrez simply confused denotational and compositional. So please don't take him too seriously. – Andrej Bauer Mar 01 '12 at 07:22
This philosophical paper ("Understanding Programming Languages") explains exactly this point: it suggests that founders of semantics were Platonists, and distinguished "real mathematics" from operational semantics on an ontological basis (the paper then summarizes known challenges to Platonism, together with "it's expressible in ZFC"). I don't like the way it's written (and the definition of operational semantics is mostly wrong, but good enough for the discussion), but maybe it is still spot-on on this discussion: http://scholar.google.com/scholar?cluster=3474869582992230339&hl=en&as_sdt=0,5 – Blaisorblade May 11 '14 at 09:31

score 20 · Answer 3 · edited Apr 13 '17 at 12:32

20

I agree that A. Bauer's identification of denotational semantics with compositionality (in Books on programming language semantics) doesn't really characterise well what has traditionally been meant by denotational semantics, since clearly operational semantics as well as program logics (axiomatics semantics) are compositional.

I'd suggest the term is best understood socio-historically, as referring loosely to a certain theory tradition (started in earnest when Scott produced a lattice-theoretic model of the untyped lambda-calculus) with certain preferred tools (order theory, fixpoint theorems, topology, category theory) and preferred target languages (purely functional and sequential). I imagine that -- apart from pure intellectual interest -- denotational semantics was mostly invented because:

It used to be difficult to reason about operational semantics.
It used to be difficult to give axiomantic semantics to non-trivial languages.

I'd argue that both problems have been ameliorated to a substantial degree, (1) for example by bisimilation based techniques coming from process theory (which can be seen as a specific form of operational semantics) or e.g Pitts work on operational semantics and program equivalence, and (2) by the developments of e.g. separation logic or Hoare logics derived as typed versions of Hennessy-Milner logics via programming language embeddings in typed $\pi$-calculi.

So, in summary, I'd argue that the term "denotational semantics" has become less precise, and thus less useful. It might be helpful for the semantics community to converge towards better terminology.

edited Apr 13 '17 at 12:32

Community

1

answered Dec 06 '10 at 13:38

Martin Berger

11,420
3
39
71

1

To recap my latest post, a "denotational semantics" has to say, "the meaning of this notation is that". "Operational" semantics and "axiomatic" semantics are not semantic definitions of this kind. It is misleading to make them appear so. Note also that what is called the "operational approach" is an approach to reasoning about programs. It is not operational semantics. The operational approach and the axiomatic approach can substitute for the engineering applications of denotational semantics. But they don't become denotational semantics. – Uday Reddy Feb 26 '12 at 15:21
@Uday. I'm not sure that's really a substantial difference. For example if I give the semantics of a language $L$ by compositional translation to $\pi$-calculus, I assign to each $L$-program a process. What that process does is given only operationally. With program logics, you often have characteristic formulae (computable inductively form program syntax), which capture the entire behaviour of a program in a pair of formulae. How does that not say "the meaning of this notation is that"? – Martin Berger Feb 26 '12 at 15:58
A compositional translation is a compositional translation. It is not denotational semantics. If the target language has denotational semantics then you can compose the two and get a denotational semantics for the source language. 2. Program logic. If by "characteristic formulae" you mean something like predicate transformers, they are widely acknowledged to constitute a denotational semantics. Please look up the paper "Dijkstra's predicate transformers and Smyth's power domains" by Plotkin. However, this doesn't mean that the program logic itself is a denotational semantics.

Uday Reddy

Feb 26 '12 at 16:45

This discussion and the one below Uday's post leaves me more confused than edified. An inductively defined language can be given compositional semantics in different mathematical universes, be they transition systems, posets, or games. Patrick Cosuot has a TCS paper showing that denotational and game semantics can be derived from operational semantics using adjunctions. – Vijay D Feb 27 '12 at 06:10

@VijayD If denotational semantics could be produced so easily by turning the wheel, then all the semanticists would have been out of job a long time ago! If the Cousot paper you are referring to is "Constructive design of a hierarchy of semantics", this could exactly be the kind of thing that Martin Berger has been asking for. However, note that Cousot is not inventing new semantic models here. He is showing that existing models can be fit into a certain framework. On the other hand, semanticists are looking for new models that explain new phenomena that were previously not understood. – Uday Reddy Feb 27 '12 at 19:58

Hello Uday. I am aware that Cousot is not inventing new models. What I greatly appreciate is his painting the mathematical landscape in which different semantic models sit. I know no other rigorous mathematical work putting such a range of semantic models in the same picture. Also, denotational/game semantics of a language being abstractions of operational semantics does not mean the abstraction is easy to derive. – Vijay D Feb 27 '12 at 20:05

@ Uday, ad (1) I still don't see why assigning processes in a compositional way does not count as denotations. Ad (2) "characteristic formulae" I simply mean a pair of formulae in the ambient logical language. – Martin Berger Feb 28 '12 at 15:25

@Uday, I'm not sure I can agree that we are looking for new models because the existing ones don't explain. Operational semantics explain everything (at least now -- in the prehistory of computation this was different), otherwise, how could we every have implemented all the programming languages we use? The reason we look for new models is different: we seek unification and abstraction. What does that mean? Unification means that we have many different languages and we wish to know how they relate. (Continued in next message.) – Martin Berger Feb 28 '12 at 15:27

(Continuted from previous message.) Exhibiting different programming languages or language features as variants of a theme is highly instructive and gives new suggestions for language abstractions (e.g. monads and monad transformers as a structuring princible for sequential languages, or the many axes according to which one can structure interaction types (linear, affine, replicated, first/second order, input/output etc) which classify interactive behaviour). (Continued in next message.) – Martin Berger Feb 28 '12 at 15:28

(Continuted from previous message.) By abstraction I mean that for reasoning about this or that class of programs, we may not need the full expressive power of a chosen kind of model (e.g. you model programming languages with continuations/callcc but you want to reason only about linear continuation usage). Then weaker modelling technology might be sufficient. – Martin Berger Feb 28 '12 at 15:31

1

@Martin. Why assigning processes in a compositional way is not denotational. It could be, if you convince all of us that processes are a foundational theory just like set theory and one shouldn't ask for its semantics. I sympathize with the view that there could be a foundational language that models stateful computations. Perhaps process calculus of some form will be accepted as such a foundation some day. But I don't think we are there yet. – Uday Reddy Feb 28 '12 at 19:42

@Martin. Any "pair of formulae" can hardly be called "characteristic formulae". To warrant the "characteristic" label, they have to be unique and canonical. Predicate transformers are the only things I know that fit that bill, and I have already accepted that they constitute a denotational semantics. If you have some other definition of characteristic formulae, please tell us which ones you have in mind. – Uday Reddy Feb 28 '12 at 20:03

@Martin. I have added a new "answer" talking about how denotational semantics models "explain" computational phenomena. – Uday Reddy Feb 28 '12 at 20:55

@UdayReddy, the problem is that these distinctions are highly subjective, to the extent of being philosophical. If someone said "a denotational semantics is a compositional map from programs to domain theoretic objects" I would find it a simple, precise and useful definition. – Vijay D Feb 28 '12 at 21:37

A characteristic formula for a process, given a notion of equivalence is one that is satisfied exactly by equivalent processes. There are characteristic formulae for bisimulation, simulation, etc. I think this is a perfectly appropriate way to assign semantics. I would not call it "denotational" because that word is heavily associated with the domain theoretic approach. But I find nothing less fundamental about characteristic formulae. – Vijay D Feb 28 '12 at 21:39

@VijayD "Compositional map from programs to domain theoretic objects". That might satisfy you but it is wrong. Denotational semantics never dictated what kind of objects you must use. Why not set-theoretic objects? Trace sets? Strategies in a game? Automata? Or, some combination of all of these? Predicate transformers? All these things have been used in denotational semantics. And even domain theory is not a straitjacket as you seem to imagine. There are Winskel's event structures, Girard's coherent spaces, Kahn-Plotkin sequential data structures and so on. – Uday Reddy Feb 28 '12 at 22:00

@VijayD. The correct version of your definition is what Andrez gave originally, which I said I agreed with: compositional map from programs to some mathematical space. He also said that what constitutes a "mathematical space" is a subjective judgement. Giving meanings as formulas wouldn't be "denotational" by that definition, but I would agree that it is close. Predicate transformer people used to use syntactic formulae as "predicates" and got into quite a bit of mess as a result. One purpose of Plotkin's paper was to clear out that shrubbery. – Uday Reddy Feb 28 '12 at 23:36

I am not an expert on denotational semantics, so thank you for being patient. I have a question: I can define an operational semantics for a simple imperative language using a compositional map from program statements to relations over states. Is this a denotational semantics? If so, does that mean an operational semantics can be a denotation semantics, depending on how I define it? – Vijay D Feb 29 '12 at 02:16

@VijayD. If it is a compositional map from program statements to relations over states, then it is a denotational semantics. (On the other hand, calling it an operational semantics may be questionable.) Please feel free to send it me offline, and we can open a chat session, as the system recommends that we do. – Uday Reddy Feb 29 '12 at 15:42

let us continue this discussion in chat – Uday Reddy Feb 29 '12 at 15:52

"clearly operational semantics as well as program logics (axiomatics semantics) are compositional." No, a denotational semantics is a fold on the syntax producing values, and for instance a big-step semantics of a language with mutable state is not expressed as such a fold, because information flows between different parts of the program. If you use a state monad to model this information flow, then you're changing the semantic values.

– Blaisorblade May 09 '14 at 13:04

@Blaisorblade That's an interesting definition. Is it canonical? – Martin Berger May 10 '14 at 04:55

1

@MartinBerger That's the only one I ever learned, but I have a hard time providing a good reference right away. For instance, "Finally Tagless, Partially Evaluated" (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.9287) uses "fold", "compositional" and "primitive recursive" in the intro as obvious synonyms (but this is not discussed much in the paper, it's taken for granted). Viceversa, it would appear that this is a point of debate in philosophy, if Wikipedia is to be trusted here: https://en.wikipedia.org/wiki/Principle_of_compositionality#Critiques – Blaisorblade May 10 '14 at 21:37

1

@Blaisorblade When I was a PhD student, I socialised with denotational semanticists, because I was supposed to be working on denotational semantics. I always asked them what denotational semantics was, if they they could give me an abstract definition, but I only got evasive or vague answers like "denotational semantics is mathematical semantics", see also A. Bauer's explanation. I don't think the concept is well-defined. I also don't see why requiring e.g. primitive recursiveness is constraining enough, because the power of primitive recursion depends on what else is available: (continued) – Martin Berger May 11 '14 at 05:48

for example the Ackermann function can be defined using primitive recursion in the presence of higher-order functions, see e.g. my answer here. So it's really all very vague. – Martin Berger May 11 '14 at 05:52

Yes, but... 1: You can make every function compositional if you add enough info to domain elements (worst case, the program); however, full abstraction requires doing the opposite. So a compositional and fully abstract semantics is something interesting. – Blaisorblade May 11 '14 at 09:21

@Blaisorblade I'm not sure I fully understand what you mean, or how it disagrees with my point. – Martin Berger May 11 '14 at 10:19

@MartinBerger, sorry I was unclear. Your point is right: "compositionality" alone means indeed little if you don't constrain domains. However, full abstraction is a way out of this vagueness because it does constrain the domain. Even for non-fully-abstract semantics, people require you to "get close" to full abstraction, so they would not be happy with a semantics which just returns the program. To make this more precise, I'd need a concept of "closeness to full abstraction", so that one can discuss "optimizing" for it. (I have some ideas, but they don't fit a comment). – Blaisorblade May 11 '14 at 16:18

let us continue this discussion in chat – Blaisorblade May 11 '14 at 16:18

@Blaisorblade I have trouble logging into chat, maybe we can discuss this by email? – Martin Berger May 11 '14 at 16:29

Uday Reddy · Answer 4 · 2012-02-27T03:39:39.733

I am happy with Adrej's answer, but I would like to drill down further.

To start with, denotational semantics wants to say something like "the meaning of this notation is that". A real semanticist would want to imagine that the meanings are what exist in our mind and the notations are just a way of expressing those meanings. The requirement that denotational semantics should be compositional follows from this. If the meanings are primary and the notations secondary, then we have no choice but to define the meanings of bigger notations as functions of the meanings of their constituents.

If we accept this viewpoint then a good denotational semantics needs to capture the meanings we presume we have in our mind. Any compositional semantics wouldn't necessarily fit the bill. If I come up with a compositional semantic definition and nobody agrees that it states any meanings they have in their head, then it is of little use. Games semantics at present is in this situation. It is a compositional definition and technically quite strong, but very few people agree that it has anything to do with the meanings they have in their mind.

That said, any compositional definition has various technical advantages. We can use it to verify equivalences or other properties by induction on the syntax of terms. We can use it to verify the soundness of proof systems, again by induction on the syntax of terms. We can verify the correctness of compilers or program analysis techniques (which, by their nature, are defined by induction on syntax). A fully abstract semantic definition has even more technical advantages. You can use it to show that two programs are not equivalent, which you can't do with any arbitrary compositional semantics. A fully definable semantic definition is even better. Here the semantic domains have exactly what you can express in the programming language (with some provisos). So, you can enumerate the values in the domains to see what values there are, which would be hard to do with syntactic notations. On all these grounds, games semantics scores brilliantly.

However, compositional semantic definitions have been losing their edge over the years. Robin Milner and Andy Pitts have developed a number of "operational reasoning" techniques, which work purely on the syntax but using the operational semantics wherever needed for talking about behaviour. These operational reasoning techniques are low-tech. No fancy mathematics. No infinite objects. We can teach them to undergraduates and anybody can use them. So, many people ask the question why we need denotational semantics at all. (Martin Berger is probably in this camp.)

Personally, I have no problem with having many tools in my tool box. Denotational techniques might score better for some problems and operational techniques for others. The researchers that develop the theory might be better tuned to one approach or the other. Pretty often, we can develop the insights in one approach and transfer those insights to the other approach. (A lot of Andy Pitts's work is of this kind. Relational parametricity was developed in the denotational setting but he is able to figure out how to restate it as operational reasoning. When I look at it, I say "wow, I would have never thought that would be possible." Separation Logic is also going this way. Steve Brookes gave a 60-page soundness proof for Concurrent Separation Logic using denotational semantics. Viktor Vafeiadis recently came up with an operational soundness proof that is only 4-5 pages long.)

Operational approaches also score brilliantly when the programming languages get very fancy, with all kinds of loopy higher-order types. We may have no idea how to model such things mathematically. Or, the standard mathematical models might turn out to be inconsistent under the stress of loopiness. (For example, see "Polymorphism is not set-theoretic" by Reynolds.) Operational approaches that work purely on syntax can neatly side step all these mathematical problems.

Another approach that is intermediate between operational and denotational approaches is realizability. Instead of working with syntactic terms as in operational approaches, we go partly denotational by using some other form of mathematical representatives. These representatives may not qualify as real denotational "meanings" but they would at least be a bit more abstract than syntactic terms. For example, for polymorphic lambda calculus, we can first give meanings to untyped terms (in some model of the untyped lambda calculus) and then use them as the representatives ('realizers') to do some form of "operational reasoning" at a slightly more abstract level.

So, let there be some healthy competition between denotational, operational and realizability approaches. There is no harm.

On the other hand, there might also be some "unhealthy" competition growing between the different approaches. People working with one approach might be so closely wedded to it that they might not see the point of the other approaches. Ideally we should all be aware of the strengths and weaknesses of the different approaches and develop a scientific attitude towards them even if they are not our individual favourites.

One constructive approach towards solving this problem could be to find translations between the different approaches. — Martin Berger, Feb 26 '12 at 14:17
Note that I have no problem with conventional denotational semantics as a tool in the tool box. I just find the implicit or explicit suggestions that they are somehow better to be problematic and lacking coherent justification. — Martin Berger, Feb 26 '12 at 14:24
I would put up the "Algollike Languages" volumes (http://www.eecs.qmul.ac.uk/~ohearn/Algol/algol.html) volumes edited by Peter O'Hearn and Bob Tennent as a model of good practice. They include papers on "conventional denotational semantics" (Strachey, Reynolds, Tennent, Meyer et al), as well as "unconventional" denotational semantics (mine, Abramsky & McCusker, Brookes) and operational approaches (Andy Pitts, Felleisen). Incidentally, two papers of Reynolds in the volumes (Specification Logic and Syntactic Control of Interference) were "axiomatic" when they were written! — Uday Reddy, Feb 26 '12 at 14:43
Finding translations between approaches would be really nice, but also difficult. Very few of us have expertise in multiple approaches. But, I agree that it would be great to see papers that say here is an idea in the denotational approach and the same idea using an operational approach. We could all learn a lot from such papers. — Uday Reddy, Feb 26 '12 at 14:52
Maybe we can collectively think of some promising ideas that might be amenable to such translation. — Martin Berger, Feb 26 '12 at 16:03
About the healthy competition, one key problem is that there are so many approaches, formalisms, researchers and papers, that it's hard to keep up with the development. It might be worth our while as a research community to make a sustained effort to synthesise and unify the existing approaches. — Martin Berger, Feb 26 '12 at 16:06
@MartinBerger, a starting point I am aware of is Patrick Cousot's paper "Constructive Design of a Hierarchy of Semantics" which shows that a very broad range of semantic models, including transition systems, axiomatic semantics, denotational models, can be related using adjunctions, hence viewed as different abstractions. — Vijay D, Feb 27 '12 at 20:07
@Vijay. I have not read the paper, but it looks like it's going in the direction I envision. We do semantics because we want to reason, so a next step could be to try and push different reasoning technology across the adjunctions, e.g. what's bisimulation-up-to in partial orders etc. — Martin Berger, Feb 28 '12 at 15:23
@MartinBerger, there are a few papers about this. Some by the coalgebra folks, and some by abstract interpretation folks. Ranzato and Tapparo's Generalised Strong Preservation paper was useful for me. — Vijay D, Feb 28 '12 at 18:33
It looks like it would be good idea for Martin to open a new question and for Vijay to respond. I would welcome a more comprehensive discussion than possible in these comment boxes. — Uday Reddy, Feb 28 '12 at 19:10
I think the stackexchange style site is not set up for such a discussion - which is a pity. — Vijay D, Feb 28 '12 at 21:35

Uday Reddy · Answer 5 · 2012-03-01T19:47:17.153

[One more answer. It is probably uncool to pile up several answers. But, hey, this is a deep issue.]

I said that I agreed with Andrej's answer, but it seems that I don't agree entirely. There is a difference.

I said that a denotational semantics has to say "the meaning of this notation is that". What I meant is that notations must be assigned meanings, which are some form of conceptual entities, not some other notations. In contrast, Andrej also required, paraphrasing Scott, that the meanings must be "mathematical" objects. I don't believe that the mathematical bit is necessary.

For example, it would be perfectly fine, from my point of view, for meanings of notations to be physical processes. After all computer programs put on brakes in your car, fly airplanes, drop bombs, and what not. These are physical processes, not elements in some mathematical space. You can't drop a bomb, see if it kills somebody, and take it back if it doesn't. Computer programs can't do that. But mathematical functions can. (They are called "snapback" operations.) So, it is not at all clear that mathematical functions will make good meanings for computer programs.

On the other hand, we really don't know yet how to talk about physical processes abstractly. So, we might indeed use some mathematical description of processes in order to articulate our ideas. But these mathematical descriptions would be just that, "descriptions". They are not meanings. The real meanings would be just the physical processes that we imagine conceptually.

In his acceptance speech for the SIGPLAN award (which should be on youtube sometime soon), Hoare said that ACP used an "algebraic approach", CSP used a "denotational approach" and CCS used an "operational approach" to describe processes. Ohad and I were sitting together in the session, we looked at each other and said "that is really interesting". So, there is a lot of conceptual space here that is being explored. I think that a lot of Scott's later work, on neighbourhood systems and information systems etc., was indeed an effort to explain functions as "processes" of some form. Girard's geometry of interaction and the later games semantics are also efforts to explain functions as processes. I would say that developing a solid theory of processes could be the big contribution that Computer Science could make to the 21st century mathematics. I wouldn't accept a belief that mathematics has all the answers and we should attempt to reduce computational phenomena to mathematical concepts in order to understand them.

What amazes me is how beautifully information hiding works in stateful computations (imperative programming as well as process calculi), whereas it is clumsy and complicated in mathematical/functional formalisms. Yes, we have relational parametricity, and it allows us to get around the limitations of mathematical formalisms very nicely. But it does not match the simplicity and elegance of imperative programming. So, I don't believe that the mathematical formalisms are the right answer, though I would admit that they are the best answer we have at the moment. But we should keep looking. There is a nice theory of processes out there which will beat traditional mathematics hands down.

Uday Reddy · Answer 6 · 2012-03-08T01:57:42.803

[Hopefully, this is my last answer to this question!]

Ohad's original question was about how denotational semantics differs from structural operational semantics. He thought that both of them were compositional. Actually, that is untrue. Structural operational semantics is given as sequences of steps. Each step is expressed compositionally (and it is remarkable of Plotkin to make the discovery that this is possible!), but the entire behaviour is not defined compositionally. Here is what Plotkin says in his introduction to the SOS article [emphasis added]:

In denotational semantics one follows an ideal of compositionality, where the meaning of a compound phrase is given as a function of the meaning of its parts. In the case of operational semantics one considers the behaviour of a program phrase, which is just the collection of the transitions it can make. This behaviour is, however, not compositional when thought of as a function of program phrases. However the rules do give it structurally, i.e., primitive recursively, in the syntax;...

The fact that each step is expressed compositionally doesn't mean that the entire behaviour is expressed compositionally.

There is a nice article by Carl Gunter called Forms of Semantic Specification, where the different methods of specifying semantics are compared and contrasted. Much of this material is also reproduced in the first chapter of his "Semantics of Programming Languages" text. This should hopefully clarify the picture.

Another word about "operational semantics". In the early days, the term "operational" was used to refer to any semantic definition that referred to detailed evaluation steps. Both denotational semanticists and axiomatic proponents looked down upon "operational" semantics, regarding it as being low-level and machine-oriented. I think this was really based on their belief that higher level descriptions were possible. These beliefs were shattered as soon as they considered concurrency. de Bakker and Zucker's Processes and denotational semantics of concurrency has these interesting passages:

We shall use the methodology of denotational semantics. "Denotational" should be contrasted here with "operational": The key idea of the former approach is that expressions in a programming langauge denote values in mathematical domains equipped with an appropriate structure, whereas in the latter the operations as prescribed by the language constructs are modelled by steps performed by some suitable abstract machine....

The mathematical model contains various notions which, though denotational in style, are operational in spirit [emphasis added]. These include the "history" feature of the notion of process itself, and the use of so-called silent moves in dealing with synchronization and recursion.

Here we see the authors struggling with the two notions of "operational", one the technical notion - behaviour expressed using syntactic manipulations, and the other, the conceptual notion - being low-level and detailed. The credit largely goes to Plotkin and Milner for rehabilitating "operational" semantics, making it as high-level as possible and showing that it could be elegant and insightful.

Despite all this, the operational notion of process is still quite different from the denotational notion of process, the latter of which was developed by both de Bakker and Hoare and their teams. And, I think there is a lot that is mysterious and beautiful about the denotational process concept which is still to be understood.

Sorry about not replying to the chat request. I am very busy for the next two weeks. Thanks for writing this! It's the first technical answer on the page I understand. — Vijay D, Mar 08 '12 at 04:49
I might take this opportunity to put in a plug for our Midlands Graduate School in Theoretical Computer Science, which is intended to address all these kind of issues. It is open to all PhD students to attend, from anywhere in the world. — Uday Reddy, Mar 08 '12 at 13:56

Uday Reddy · Answer 7 · 2012-03-01T11:58:04.927

This additional response is to amplify the point that denotational semantic models are designed to "explain" computational phenomena. I will give a series of examples from the semantics of imperative programming languages (also called "Algol-like" languages).

First there was the semantic model formulated by Scott and Strachey. (Cf. Gordon: Denotational description of programming languages - my all-time favourite or Winskel's book.) This model posits that there is a global state, made up of the state of all the locations allocated by a program. Every command is interpreted as some sort of a function from global states to global states.

Reynolds said that it didn't model the stack discipline of local variables. When a local scope is entered, its variables are allocated, and they are deallocated when the scope is exited. Basically, this is the question, "in what sense are local variables local?" How does the semantics capture the locality? To explain this, he invented a functor-category model. (Cf. Reynolds: The Essence of Algol and Tennent: Semantics of programming languages).

Tennent wanted to model the reasoning principles formulated in Reynolds's Specification Logic (an extension of Hoare Logic for higher-order procedures). The Logic has ideas like expression-like (read-only) computations, non-interference between command-like and expression-like computations, and some data abstraction reasoning principles. He refined Reynolds's functor-category model to find a new one. This called the "SASL" model, also covered in Tennent's book.

Meyer and Sieber, and also O'Hearn and Tennent, noted that none of these models still captured the locality of local variables fully. When two implementations of an abstract data type or a class differ in their local variables but manipulate them in ways that have the same behaviour when viewed from outside, they are observationally equivalent. The denotational semantics should equate them. To model this, O'Hearn and Tennent added relational parametricity to a variant of the Reynolds's functor-category model.

When I looked at the problem at the same time, I disbelieved in the functor-category approach. I also thought that it was overly technical and believed there must be a simpler model. This led me to invent the "Global state considered unnecessary" model, which is rather like a CSP traces model, but for a higher-order language. As an added bonus, this model also captured the irreversibility of state change, which was not present in the earlier models.

My model only worked for a well-behaved sublanguage of Algol, called Syntactic Control of Interference. Abramsky and McCusker extended my model using games semantics ideas so that it can work for full Algol. So, their model explains the same phenomena as mine does, but for the bigger language.

In each case, we are able to demonstrate that the new models capture observational equivalences (or other forms of logical formulae) exhibiting the computational phenomena mentioned, which were not validated by the earlier models. So, there is a very precise sense in which these models are "explaining" computational phenomena.

[All the work I mentioned here can be found in the "Algol-like Languages" volumes: link and link]

What constitutes denotational semantics?

7 Answers7

Linked

Related