Semantics: Denotational vs. Operational

README.md

Semantics: Operational vs. Denotational

In this document I wish to explain the difference between operational and denotational semantics. It may sound like a dry subject but you and I both will learn plenty from it.

Semantics of a language defines how the language behaves, where as the syntax of a programming language defines how it is formed.

• Syntax is the foundation of a language;
• Semantics give purpose to the syntax;
• Syntax errors often lead to semantic errors, but they don't have much of a 'causual' relationship;

Imagine this piece of C code:

int a = "s";

This is syntactically sound, but it is semantically incorrect. The portion of C syntactic grammar that describes this portion is:

declarator 	::= ID [ '=' rvalue ] ;
decl-stmt	::= type-decl declarator { ',' declarator } ';'

Here, rvalue could be anything ranging from a constant value, to a constant expression, to a designated initializer. So we're not commiting a syntax error. However, this is syntactically incorrect. The type associated with "s" is char[], and we are assigning it to a variable of type int. This is a semanic error.

The semantics of a language is defined by first its authors, and later, its implementors. For example, tcc may not error out with this C example, but gcc will. The authors of tcc have chosen not to implement this semantic check.

That is, because C is an imperative language. With an imperative language like C, only the 'operational semantics' matters. Operational Semantics are formal descriptions of how a program:

• May behave;
• Should behave;
• Shall behave;
• Must behave;

This is related to Rice's theorem; For out purpose, this means exactly why tcc chooses to ignore the semantics, but gcc does not: The are not algorithms that could decide how something non-trivial should affect the output. I asked a model to explin this to me in plain terms:

Operational semantics describes how program constructs change the state of a computation step by step. Rice's Theorem suggests that for any sufficiently powerful programming language, there cannot be a general algorithm to decide whether any arbitrary program written in that language will exhibit a particular behavior (like terminating or accessing a particular variable) based solely on its operational semantics.

This is why we need 'denotational semantic'. A language like C may not have 'stadnard' denotational semantics, because these type of semantics are mostly reserved for languages with a functional syntax. Denotational semantics map the behavior of a language into Church's theorem, in other words, they are way to describe mathematics of a language via Lambda calculus.

Denotational semantics have formulas. This is a simple Markdown document and I cannot use complex equations, so for an example, I present you this denotation:

[n] = λ_.n where n ∈ Z

What this says is:

An integer in this language is a 'null transformation of itself'.

We can present this in Python as:

n: int = lambda n: n

I am using Python here because it's one of those languages which you could 'potentially' write proper denotational semantics for. At the end, Python is mostly imperative.

A 'pure' functional language like Haskell, or even non-pure funcional languages like OCaml and SML, they could have denotational semantics written for them. In fact, that is why it's called 'denotational'.

There's no standard for denotations of such semantics. One way to denote them is S-Expressions:

(eq int (lambda i))

I intend to write fully-compliant denotational semantics for my functional language, Xeph. I would also like to write opertaional semantics. Remember that there's nothing stopping you from writing either for even a tacit/concatative language like UNIX Shell! But alas, it would be a waste of time.

I hope this document has been informative. There's another type of semantics, axiomatic semantics which maybe I shall touch upon later.

~ Chubak

PS: There is no doubt that this document is partly errneous. Please inform me of errors and mistakes.

Not a bad start. Think of semantics as a mapping from a language (syntax) to a domain (modelling). Semantics is what an interpreter provides. Ideally, we would only care about semantics at the end of a compiler pipeline, and use source-to-source transformations (syntax to syntax!) instead.

The secret to understanding "operational" and "denotational" is in their plain dictionary definitions; "operational" means "according to a machine" and "denotational" means "in terms of assigning meaning". An operational semantics maps each piece of syntax to an algorithm (a sequence of machine instructions) such that equivalence of syntax implies equivalence of algorithms. In symbols, let F : C -> D be a functor from syntax to semantics, let ~ be an equivalence relation induced by C's rewrite rules, let ~~ be F's mapping of ~ to D, and then:

For all syntax snippets x, y in C: x ~ y => F(x) ~~ F(y)
Also, x ~ y => y ~ x

Yes, this implies that F maps C's rewrite rules (on syntax) to D's rewrite rules (on algorithms)! Sometimes, folks will only work with a directed equivalence; this happens when we can legally rewrite a piece of syntax in one direction, but we can't legally reverse the rewriting rule. This means that we would drop that second helper equation, and instead have something like:

For all syntax snippets x, y in C: x ~> y => F(x) ~~> F(y)

A denotational semantics maps syntax to arbitrary mathematical objects. All that's really required is that the objects form a category. We could think of denotational semantics as generalizing operational semantics; we're still mapping with a functor and creating rewrite rules, but we no longer are talking about the outputs or behaviors of algorithms.

None of this has anything to do with imperative/functional/etc. paradigms. Every programming language can be seen as a category, by seeing its syntactic equivalences as the foundation of a deductive system and remembering that every deductive system is a category.