Preliminaries
Course participants are expected to be familiar with basics of mathematical logic and program semantics. The necessary background can, for example, be obtained in the DTU courses 02141 and 02156.
In particular, throughout the course we will
- read and write formulas in first-order predicate logic,
- formally reason about the satisfiability and validity of such formulas,
- read and write formal definitions (of terms, formulas, expressions, etc.) using recursive (or inductive) definitions and sets of inference rules, and
- prove properties of such formal definitions, particularly using structural induction.
We give a few pointers to standard textbooks for students looking for a refresher of or an introduction to the above topics. Our notation will be close to these books. All of the listed books are available online for DTU students.
First-order Predicate Logic
A thorough introduction to first-order predicate logic is found in chapters II and III of the following standard textbook:
Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Mathematical logic (3. ed.). Graduate texts in mathematics, Springer 2021, available online.
The syntax of first-order predicate logic is discussed in chapter II.3. The semantics of the logic via the satisfaction relation $\models$ is covered in chapters III.1 - III.3 Satisfiability and validity of predicate logic formulas is defined in chapter III.4.
Notation
Throughout the course, we will write logical formulas using two notations: the (easier typable) notation used by verification tools and the (more concise, perhaps easier readable) notation commonly known from mathematics (as in the book referenced above).
The table below compares both notations and summarizes the semantics of formulas $F,G,H$ in first-order predicate logic for a structure $\mathfrak{A}$ and an interpretation $\mathfrak{I}$.
Here, t, t1, ..., tn are terms, that is, expressions constructed from constants, variables $x$, and function applications (interpreted by the structure $\mathfrak{A}$, e.g. standard arithmetical operations). $\mathfrak{I}(t)$ denotes the valuation of term $t$ using interpretation $\mathfrak{I}$. R denotes a relational symbol (interpreted as the relation $R^{\mathfrak{A}}$ by the structure $\mathfrak{A}$) that takes some finite number n >= 0 of terms as argument. An example is the relational symbol =, which is interpreted as the equality relation between terms by every structure under consideration. For binary relations such as =, we often use infix notation t1 = t2 instead of =(t1, t2).
We also give the semantics of $F$ using the satisfaction (or model) relation $\mathfrak{I} \models F$ (read: interpretation $\mathfrak{I}$ satisfies formula $F$); details are found in the above textbook, chapter III.3. We denote by $\mathfrak{I}[x \texttt{:=} a]$ the update of interpretation $\mathfrak{I}$ in which we assign value $a$ (taken from the universe of structure $\mathfrak{A}$) to variable $x$.
Formula F in tool notation | Formula $F$ in mathematical notation | Read as | $\mathfrak{I} \models F$ if and only if |
|---|---|---|---|
true | $\texttt{true}$ | true | always |
false | $\texttt{false}$ | false | never |
R(t1, ..., tn) | $R t_1 ... t_n$ | relation R of t1, ..., tn | $(\mathfrak{I}(t_1), \ldots, \mathfrak{I}(t_n)) \in R^{\mathfrak{A}}$ |
t1 == t2 | $t_1 = t_2$ | t1 equals t2 | $\mathfrak{I}(t_1) = \mathfrak{I}(t_2)$ |
t2 != t2 | $t_1 \neq t_2$ | t1 does not equal t2 | $\mathfrak{I}(t_1) \neq \mathfrak{I}(t_2)$ |
G && H | $G \wedge H$ | conjunction | $\mathfrak{I} \models G$ and $\mathfrak{I} \models H$ |
G \|\| H | $G \vee H$ | disjunction | $\mathfrak{I} \models G$ or $\mathfrak{I} \models H$ |
!G | $\neg G$ | negation | not $\mathfrak{I} \models G$ |
G ==> H | $F \rightarrow G$ | implication | if $\mathfrak{I} \models G$ then $\mathfrak{I} \models H$ |
exists x :: G | $\exists x (G)$ | existential quantifier | there is an a in the universe of $\mathfrak{A}$ such that $\mathfrak{I}[x \texttt{:=} a] \models G$ |
forall x :: G | $\forall x (G)$ | universal quantifier | for all a in the universe of $\mathfrak{A}$, we have $\mathfrak{I}[x \texttt{:=} a] \models G$ |
Furthermore, a formula $F$ is satisfiable if there exists an interpretation $\mathfrak{I}$ such that $\mathfrak{I} \models F$. The formula is called valid if $\mathfrak{I} \models F$ holds for every interpretation $\mathfrak{I}$.
Operational Program Semantics & Structural Induction
We recommend two standard textbooks:
Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science, Springer 2007, available online.
Chapter 1 gives an overview, including a brief introduction to structural induction. Chapter 2 discusses operational semantics in a style similar to the one used in the lecture.
Glynn Winskel: The formal semantics of programming languages - an introduction. Foundation of computing series, MIT Press 1993, available online.
Operational program semantics is covered in chapter 2. Chapters 3 and 4 give a detailed discussion of inductive definitions, inference rules, and proving properties about such definitions using various induction principles.