45
$\begingroup$

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?

$\endgroup$
  • 4
    $\begingroup$ 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. $\endgroup$ – Ohad Kammar Dec 6 '10 at 0:00
  • 1
    $\begingroup$ 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. $\endgroup$ – Ohad Kammar Dec 6 '10 at 0:12
  • 10
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Dec 6 '10 at 14:48
  • 2
    $\begingroup$ 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? $\endgroup$ – Ohad Kammar Dec 6 '10 at 19:20
  • 1
    $\begingroup$ 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. $\endgroup$ – gasche Feb 26 '12 at 17:43
30
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Blaisorblade May 11 '14 at 19:27
23
$\begingroup$

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).

$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – Martin Berger Dec 6 '10 at 15:33
  • 1
    $\begingroup$ 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. $\endgroup$ – Martin Berger Dec 6 '10 at 15:36
  • 3
    $\begingroup$ @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. $\endgroup$ – Martin Berger Dec 7 '10 at 12:26
  • 2
    $\begingroup$ @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). $\endgroup$ – Marc Hamann Dec 7 '10 at 17:19
  • 2
    $\begingroup$ @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. $\endgroup$ – Andrej Bauer Dec 14 '10 at 22:18
19
$\begingroup$

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:

  1. It used to be difficult to reason about operational semantics.

  2. 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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Uday Reddy Feb 26 '12 at 15:21
  • $\begingroup$ @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"? $\endgroup$ – Martin Berger Feb 26 '12 at 15:58
  • 1
    $\begingroup$ @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. $\endgroup$ – Uday Reddy Feb 28 '12 at 19:42
  • 1
    $\begingroup$ @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" (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: en.wikipedia.org/wiki/Principle_of_compositionality#Critiques $\endgroup$ – Blaisorblade May 10 '14 at 21:37
  • 1
    $\begingroup$ @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) $\endgroup$ – Martin Berger May 11 '14 at 5:48
16
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ One constructive approach towards solving this problem could be to find translations between the different approaches. $\endgroup$ – Martin Berger Feb 26 '12 at 14:17
  • 1
    $\begingroup$ 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. $\endgroup$ – Martin Berger Feb 26 '12 at 14:24
  • $\begingroup$ I would put up the "Algollike Languages" volumes (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! $\endgroup$ – Uday Reddy Feb 26 '12 at 14:43
  • 1
    $\begingroup$ 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. $\endgroup$ – Martin Berger Feb 26 '12 at 16:06
  • 2
    $\begingroup$ @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. $\endgroup$ – Vijay D Feb 27 '12 at 20:07
12
$\begingroup$

[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.

$\endgroup$
10
$\begingroup$

[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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Vijay D Mar 8 '12 at 4:49
  • $\begingroup$ 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. $\endgroup$ – Uday Reddy Mar 8 '12 at 13:56
9
$\begingroup$

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]

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.