Semantics
Notes on Types & Programming Languages by Benjamin Pierce (2002)
The design of a programming language can be divided into two parts: syntax and semantics.
The syntax describes how it looks like.
The semantics describes what it should do.
There are many ways a program can be written with valid syntax but turn nonsensical when evaluated. These nonsensical evaluations are known as runtime errors.
Semantics formally describes how programs should be evaluated. Programs that are well-formed according to its semantics do not get stuck.
There are three main styles of describing semantics: operational, denotational, and axiomatic.
Operational semantics
Operational semantics uses the idea that languages are abstract machines and evaluation of a program is a series of state transitions from an initial to a final state.
Transition functions define how states transit to the next, if there is one. If there is no such next state, the machine either completed its evaluation successfully or faced a runtime error and got stuck. The program halts in both cases.
Every term in the computer program has some meaning, and its form finalizes when the state transitions are complete. State transitions may be single or multi-step.
There are two major ways to write operational semantics: small-step or big-step.
Small-step semantics breaks down behaviour into granular simplification steps. A simplication step might not guarantee evaluation to a finalized form; sometimes multiple steps are needed.
Big-step semantics composes multiple small-step rules that evaluate into a finalized form into a single rule. Such a rule is equivalent with its multi-step counterpart.
Since operational semantics is styled after abstract machine behaviour, they’re useful as a reference for implementation.
Origins: John McCarthy on Semantics of Lisp (1960)
Denotational semantics
Denotational semantics uses the idea that languages are mathematical objects. Unlike operational semantics, evaluation and implementation details are abstracted away.
An interpretation function is defined to map terms in a program to elements in semantic domains (also known as its denotation), removing any occurrences of the original syntax.
Semantic domains are designed to model after specific language features and this study is called domain theory.
Checking whether two programs are the same is achievable by comparing their denotations.
Laws can be derived from the semantic domains and are used for language specifications to verify correctness of an implementation.
The properties of the semantic domains can be used to show impossible instances in a language.
Origins: Christopher Strachey, Dana Scott on “Toward a mathematical semantics for computer languages” (1970, 1971)
Axiomatic semantics
Intuitively related to Hoare Logic. Instead of deriving laws from operational or denotational behaviour definitions, the laws themselves define the semantics of the language.
This reversal simplifies reasoning about a program, leading to developments in software verification.
Two different program implementations with the same set of initial and final assertions (laws) are considered to have the same semantics.
The terms that happen between assertions are just used to prove the assertions themselves and do not contribute to the semantics.
Assertions define relationships between variables and other moving parts in a program, and some of these assertions remain invariant throughout execution. This is the important invariance concept that underlies axiomatic semantics.
Origins: Tony Hoare on Hoare Logic (1969)