In programming language semantics, it is often heard that people talking about meaning and denotation. They seem not to be the same. What is the difference? Is the former associated with operational semantics while the latter with denotational semantics? Thanks.
$\begingroup$ Can you cite a source that does this, please? In my experience, meaning and denotation are used to refer to the same concept in programming language semantics literature (though, in Philosophy, they are used in different ways, as Neel explains below). $\endgroup$– Uday ReddyNov 6, 2012 at 22:48
$\begingroup$ @UdayReddy: The question happened to come to my mind. I can not recall where I got it, probably from philosophical texts. $\endgroup$– dayNov 9, 2012 at 11:34
"Meaning" is used in a broader way than denotation is.
The original dichotomy, inherited from logic and philosophy, is between "sense" and "denotation" (which philosophers call "reference").
This distinction can be illustrated by Frege's original example. He noted that phrases "the morning star" and "the evening star" referred to the same object --- the planet Venus --- but that the sentence "the morning star and the evening star are the same planet" actually conveys some information to a reader. He suggested that the meaning of a noun phrase can go beyond the actual object it denotes, including something about how it presents the object it denotes.
Similarly, in a programming language, the expression $8 \times 7$ is not the same as the expression $56$, even though they may be (ought to be!) completely indistinguishable by any client program. But even though they are indistinguishable, they are not the same -- when evaluating the two programs, your machine does a multiplication in the first case, and doesn't in the second.
When building a denotational semantics, we try to build a model of a language in which indistinguishable programs denote --- refer to --- the same mathematical object. The goal is to simplify reasoning about the behavior of programs, since we can reason about the denotations, the mathematical objects, without having to worry about the details of how the program is presented. This lets us avoid having to deal with aspects of the meaning of programs that are not of interest to us.
The way sense and denotation relate to operational semantics is more complicated, and different. I may extend my answer later to cover this, but I have to run now. :)
EDIT: Okay, I'm extending this answer now.
The connection between "denotation" and "reference" is pretty much exact, and it's exact because the people who invented denotational semantics (e.g., Scott and Strachey) were quite consciously appropriating ideas from philosophical logic as part of their project.
To understand how meaning and operational semantics relate, it's helpful to recall the philosopher Michael Dummett's notion of a "meaning theory" and how it differs from a "semantic theory".
In Dummett's terminology, a semantic theory is a compositional way of relating sentences to determinate mathematical objects. In logic, the meaning of a sentence is its truth-value, and it is determined from the truth-values of its constituents. Denotational semantics of programming languages uses a much wider variety of mathematical objects, but it works the same way -- we give the meaning of a program term in terms of the meaning of its subterms. So in Dummett's terminology, denotational semantics offer semantic theories of programming languages.
A meaning-theory is also a compositional way of relating sentences to mathematical objects, but in addition it contains an account of what justifies the relationship between the sentence and the mathematical object. He developed this idea in order to understand how intuitionistic mathematicians understood the notion of truth. In particular, they had a compositional account of the meaning of logical connectives, but did not give them semantic values in the same way that classical logicians do. For example, in the Brouwer-Heyting-Kolmogorov account of intuitionistic logic, truth is defined in the following way:
- A canonical proof of $A \land B$ is a pair $(p_1, p_2)$, where $p_1$ is a canonical proof of $A$ and $p_2$ is a canonical proof of $B$.
- A canonical proof of $A \vee B$ is a pair $(i, p)$, where $i$ is either $0$ or $1$, and if $i$ is $0$, then $p$ is a canonical proof of $A$, and if $i$ is $1$, then $p$ is a canonical proof of $B$.
- A canonical proof of $A \to B$ is an effective procedure, that takes any canonical proof of $A$ and computes a canonical proof of $B$.
- A canonical proof of $\forall x.\;A(x)$ is an effective procedure which takes a numeral $n$, and computes a canonical proof of $A(n)$.
- A canonical proof of $\exists x.\;A(x)$ is a pair $(n, p)$, where $n$ is a numeral and $p$ is a proof of $A(n)$.
A proposition $A$ is said to be true when it is possible to give a canonical proof of $A$.
Now, note that this definition connects propositions and truth values, but the connection must be justified by the possibility of giving a canonical proofs.
Operational semantics enters the picture via this notion of justification. An operational semantics is just a description of what an abstract machine does. After we give a denotational semantics, we generally want to show that the denotational semantics is faithful to the operational semantics. This property is called adequacy (along with its big brother full abstraction), and it exactly amounts to giving a meaning-theory that connects abstract machine states with denotational objects, which is closed under the reduction of the abstract machine.
This is actually not the whole story, since what I've laid out here is how to connect operational and denotational approaches via a realizability model. Type theories can also have proof-theoretic semantics (indeed, this prospect was what Dummett was most interested in), but I have not explained that connection in this post.
$\begingroup$ Thanks for the nice explanation. Looking forward to the expansion covering their relations to operational semantics. $\endgroup$– dayNov 3, 2012 at 14:16
$\begingroup$ Great explanation, Neel. Thank you very much. So if I understand correctly, the so-called meaning theory is more formal. In the case of intuitionistic logic, truth is defined proof-theoratically. $\endgroup$– dayNov 9, 2012 at 11:32
$\begingroup$ Meaning-theories aren't necessarily more formal; a denotational semantics is completely formal mathematics! A semantic theory says an "$X$ equals a $Y$", and a meaning theory says "$X$ is related to $Y$, because of $Z$". If you say $X$ is $Y$, you don't supply a justification because it's an equation. Anyway, The Logical Basis of Metaphysics is a really fantastic book, and it's well worth persevering through Dummett's ponderous philosopher-English to read it. $\endgroup$ Nov 9, 2012 at 13:55