Definition. Horn clauses - Semantics [004w]

December 15, 2025

Context

VU-VFS-2025. Lecture 8 - Horn Clauses [004u]

December 15, 2025

Introduction & Syntax

December 15, 2025

Definition. Horn clauses - Syntax [004v]

December 15, 2025

A Horn clause is a disjunctive clause (disjunction of literals) with at most one positive, i.e. unnegated literal. Often written in implication form as a conjunction of literals implying some literal called the head.

\[ \underbrace {\underbrace {p(x_1, x_2) \land q(x_1, x_2, x_3) \land \ldots }_\text {queries} \land \underbrace {\phi }_\text {constraint}}_\text {body} \to \underbrace {H}_\text {head} \]

Here:

queries are relations over some vector of variables
\(\phi \) represents a formula in a first-order theory which does not contain queries
\(H\) is called the head and represents either a query in which case we also call the horn clause a definite class if it has the following shape \[ (p \land q \land \ldots \land \phi ) \to H \] or a fact if it has the following shape \[ \top \to H \] \(H\) can also be \(\bot \) in which case we refer to the horn clause as a gloal clause with the shape \[ (p \land q \land \ldots \land \phi ) \to \bot \] with the idea being that as opposed to assuming the query holds we now show that it holds

Free variables are implicitly universally quantified over, so a horn clause like

\[ \texttt {mortal}(X) \to \texttt {human}(X) \]

stands for

\[ \forall X.\ \texttt {mortal}(X) \to \texttt {human}(X) \]

Definition. Horn clauses - Semantics [004w]

December 15, 2025

Definition. Horn clause - Solution [0050]

December 16, 2025

A solution is a function \(\Sigma \) that maps queries to formulas in the background theory over the same variables. Formally we write \(\Sigma \vDash C\) and say that \(\Sigma \) satisfies \(C\), if \(C\) is true if we replace all queries by their solutions, written as an inference rule:

We write \(\Sigma \vDash \mathcal {C}\) and say that \(\Sigma \) satisfies the set of clauses \(\{C_1, C_2, \ldots , C_n\}\), if it satisfies all individual clauses, i.e:

\[ \Sigma \vDash C_1 \land \Sigma \vDash C_2 \land \ldots \land \Sigma \vDash C_n \]

We say that \(\mathcal C\) is satisfiable, if \(\exists \Sigma .\ \Sigma \vDash \mathcal C\)

Quiz. Finding recursive Horn clauses [004z]

December 16, 2025

Is the following set of horn clauses recursive?

\[ \begin {align} q(x) \land r(x) &\to p(x) \\ p(x) \land (x < n) &\to \bot \end {align} \]
\[ \begin {align} q(x) \land r(x) &\to p(x) \\ p(x) \land (x > 0) &\to r(x) \\ p(x) \land (x < n) &\to \bot \end {align} \]

Solution.

December 16, 2025

No, we can draw the dependency graph as follows
Yes, because the head \(p\) depends on the query \(r\) and vv. again as a graph we can draw it as follows

Application of Horn clauses

December 15, 2025

Definition. Normalizing Horn clauses [0059]

December 19, 2025

Something of note when dealing with weakets preconditions in terms of horn clauses is that we have to first normalize them to ensure they are in the correct horn format, which is to say we commonly have some horn clause in the form

\[ p(e_1, e_2) \land \ldots \land \phi \to H(e_3) \]

where \(e_i\) represents an expression, to normalize these clauses we lift the expressions out of the parameters for the predicates and into the list of conjuncts, i.e.:

\[ p(x_1, x_2) \land x_1 = e_1 \land x_2 = e_2 \land x_3 = e_3 \land \ldots \land \phi \to H(x_3) \]

So we create fresh variables \(x_1, x_2, x_3\) and assign these to the respective expressions then use them in place of the expressions themselves.

Definition. Strongest Postcondition [005c]

December 22, 2025

In the most straightforward sense the strongest postcondition, denoted \(\texttt {sp}\) or \(\texttt {post}\), denotes the exact or least set of final states which we land in after a successful execution. Set theoretically we can denote it as.

\[ \texttt {sp}(s, P) = \{\sigma \in \Sigma \mid \exists \sigma ' \in \Sigma : \sigma ' \vDash P \land (s, \sigma ') \Downarrow \sigma \} \]

We can also use a more logic way of expressing it as follows

\[ \texttt {sp}(s, P) \triangleq \exists \sigma '.\ P(\sigma ') \land (s, \sigma ') \Downarrow \sigma \]

But the idea is in principle the same, it represents the set of states corresponding to some evaluated result based on some existing safe state.

Quiz. Computing the strongest post-condition [005k]

December 25, 2025

Consider the following set of Horn clauses

\[ \begin {align} x = 0 &\to q(x) \\ (q(y) \land y < 6 \land x = y + 1) \to q(x) \end {align} \]

Abstraction

December 15, 2025

Definition. Abstraction & Concretization function [005d]

December 22, 2025

In the most general sense we consider two domains, an abstract domain \(A\) and a concrete domain \(C\). We have two functions the abstraction function

\[ \alpha : C \to A \]

and the concretization function

\[ \gamma : A \to C \]

Naturally we often instantiate these two domains for different scenarios.

Example: Interval abstraction

December 22, 2025

Let's consider a basic instance of abstraction where we think of the concrete domain as set's of numbers and the abstract domain as rangers or intervals of numbers which characterize these sets. So formally we say

Our concrete domain is the power set \(\mathcal P(\mathbb {R})\) of the natural real numbers \(\mathbb {R}\) ordered by set-inclusion so \(\sqsubseteq \equiv \subseteq \)
Our abstract domain is represented by intervals in addition to the symbols for true and false, so \[ A = \textrm {Intervals} \cup \{\top , \bot \} \]
Our concretization function maps from an interval to all those numbers contained within the interval, so as an example \[ \gamma ([l, u]) \equiv \{x \mid l \leq x \leq u\} \]
Our abstraction function which takes a concrete element \(c\) then maps this to the meet or conjunct of all abstract element in which the ordering with the concretization function holds, i.e. \[ \alpha (c) = \bigwedge \{a \in A \mid c \subseteq \gamma (a)\} \] the idea is that it represents the most precise abstract representation which can capture the concrete element c. Operationally we can express this equivalently as \[ \alpha(c \equiv \{x_1, x_2, \ldots, x_n\}) = \begin{cases} [\textrm{min}\ c, \textrm{max}\ c] & \textrm{if bounded} \\ [\textrm{min}\ c, +\infty) & \textrm{if only lb} \\ (-\infty, \textrm{max}\ c] & \textrm{if only ub} \\ \top & \textrm{if unbounded} \\ \bot & \textrm{if}\ = \emptyset \end{cases} \] so more plainly we can understand the abstraction function of just being the most exact combination i.e. meet / conjunction of intervals to express our concrete element.

Example: Predicate abstraction

December 22, 2025

A common application within the domain of logic and computer science is to consider the concrete domain as referring to formulas or equivalently set's of states, not too much unlike our power-set of numbers. With our abstract state then being a conjunct of predicates from some finite set \(P\) which best characterize our concrete formulas.

Each element in the abstract domain is some permutation of our finite predicate set \(P\), so we have \[ A = \mathcal P(P) \quad P_1 \sqsubseteq P_2 \iff P_2 \subseteq P_1 \] each abstract element \(a \in P\) is defined by the conjunction \[ \bigwedge _{p \in a} p \] hence our concretization function yields those set's of concrete states (or predicates representing these states) which satisfy \(a\). \[ \gamma (a) = \{\sigma \in \Sigma \mid \forall p \in a.\ p(\sigma ) = \top \} \equiv \llbracket \bigwedge _{p \in a} p \rrbracket \]
The abstraction function is then defined more or less the usual way, we take in a concrete set of states \(c\) then aggregate those predicates which describe our concrete set of states most precisely. \[ \alpha (c) = \bigcap \{a \in A \mid c \subseteq \gamma (a)\} \] can equivalent formulation is \[ \alpha (c) = \bigwedge \{p \in P \mid c \to p\} \]

Let's consider as an example

\[ P = \{x \geq 0, x \geq 5, x \leq 10\} \quad c = \{x = 7\} \]

Here we can define the abstraction function as follows

\[ \alpha (x = 7) = \bigwedge \{x \geq 0, x \geq 5, x \leq 10\} \]

Definition. Abstract strongest postcondition [005e]

December 22, 2025

The idea

December 22, 2025

Our usual strongest postcondition can be understood as a mapping from a concrete domain to a concrete domain, i.e.

\[ \begin {align} \texttt {sp} : \texttt {Stmt} \times \texttt {C} \to C \end {align} \]

Where \(C\) represents our concrete domain, in the world of program logic this is typically assertions on the state of some memory environment. The idea behind the abstract \(\texttt {sp}\), is that we have a function

\[ \begin {align} \texttt {sp}^\# : \texttt {Stmt} \times \texttt {A} \to \texttt {A} \end {align} \]

In other words we are considering the strongest postcondition from within the abstract domain. Intuitively this just means that our predicates or assertions on the memory states (or equivalently the set of states we characterize) will be expressed in abstract terms.

In more detail

December 22, 2025

The abstract strongest postcondition, denoted \(\texttt {sp}^\#\) or \(\textrm {post\#}\) is defined as

\[ \texttt {sp}^\# (s, a) = \alpha (\texttt {sp}(s, \gamma (a))) \]

Let's explain a bit on how we can derive this, we begin with the idea that for each \(a \in A\) and each statement \(s\) we want:

\[ \texttt {sp}(s, \gamma (a)) \subseteq \gamma (\texttt {sp}^\#(s, a)) \]

This expresses soundness in other words, the resulting set of states, generated by concretizing the abstraction \(a\) must be contained within the prediction of the abstract transformer predicate \(\texttt {sp}^\#\). Then using the Galois connection we have between \(\alpha \) and \(\gamma \)

\[ \forall a \in A, c \in C.\ \alpha (c) \subseteq a \iff c \leq \gamma (a) \]

which expresses the notion that \(c\) is approximated by \(a\). We can rewrite our earlier soundness condition as:

\[ \alpha (\texttt {sp}(s, \gamma (a))) \sqsubseteq \texttt {sp}^\# (s, a) \]

two again denote the same conceptual thing that our abstract predicate transformer \(\texttt {sp}^\#\) is an over-approximation of the analogous transformer for the concrete domain. As we would preferably like to have the most precise approximation we choose equality. Or stated differently by definition the most precise abstracted approximation of the strongest post-condition we can have for some abstracted state is literally just this state concretized, and the resulting set abstracted.

\[ \texttt {sp}^\# (s, a) = \alpha (\texttt {sp}(s, \gamma (a))) \]

Correctness

December 22, 2025

The most important property to remember about the abstract strongest post-condition is that if we do over-approximate an error state it does not allow us to conclude that the program is wrong.