What is denotational semantics?

Question

I am looking for an accurate and understandable definition. The ones I have found differ from each other:

• From a book on functional reactive programming

Denotational semantics is a mathematical expression of the formal meaning of a programming language.

• However, wikipedia refers to it as an approach and not a math expression

Denotational semantics is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages

Answer 1

The term "denotational semantics" refers to both the mathematical meanings of programs and the approach of giving such meanings to programs. It is like, say, the word "history", which means the history of something as well as the entire research field on histories of things.

Answer 2

I've never found the definitions of the term "denotational semantics" useful for understanding the concept and its significance. Rather, I think it's best approached instead by considering the forms of reasoning that denotational semantics enables.

Specifically, denotational semantics enables equational reasoning with referentially transparent programs. Wikipedia gives this introductory definition of referential transparency:

An expression is said to be referentially transparent if it can be replaced with its value without changing the behavior of a program (in other words, yielding a program that has the same effects and output on the same input).

But a more precise definition wouldn't talk about replacing an expression with a "value", but rather replacing it with another expression. Then, referential transparency is the property where, if your replace parts with replacements that have the same denotation, then the resulting wholes also have the same denotation.

So IMHO, as a programmer, that's the key thing to understand: denotational semantics is about how to give mathematical "teeth" to the concept of referential transparency, so we can give principled answers to claims about correctness of substitution. In the context of functional programming, for example, one of the key applications is: when can we say that two function-valued expressions actually denote "the same" function, and thus either can safely substitute for the other? The classic denotational answer is extensional equality: two functions are equal if and only if they map the same inputs to the same outputs, so we just have to prove whether the expressions in question denote extensionally equivalent functions. So for example, Quicksort and Bubblesort are notably different arguments, but denotationally they are the same function.

In the context of reactive programming, the big question would be: when can we say that two different expressions nevertheless denote the same event stream or time-dependent value?