Formal semantics

A reference-level formalization of the previous three chapters: an abstract syntax, the runtime objects the interpreter manipulates, and the big-step rules that define how a query is run. It follows the HDR thesis §2.5.1; the operational semantics of dynamic predicates specifically (rules added and retracted while running, as Rocq-Elpi does) is due to Fissore & Tassi, PADL 2026. Read the previous three chapters first; this one names things rather than motivating them.

Abstract syntax

\[\begin{split}\begin{array}{rll} p, q, f, g & \in \mathrm{Pred} & \text{functors (predicate / term constructors)} \\ X, Y \ldots x, y & \in \mathrm{Var} & \text{unification variables, bound variables} \\ \mathrm{App} & ::= p\ \vec t \mid X\ \vec t & \text{applicative term} \\ \mathrm{Atom} & ::= \mathrm{cut} \mid \mathrm{delay}\ (\mathrm{App})\ \vec X \mid \mathrm{App} & \text{goal atom} \\ & \ \ \mid\ \mathtt{pi}\ x{\backslash}\ \mathrm{Atom} \mid \mathrm{Clause} \Rightarrow \mathrm{Atom} & \\ \mathrm{Term} & ::= \mathrm{App} \mid \lambda x.\ \mathrm{Term} & \text{term} \\ \mathrm{Clause} & ::= \mathrm{App} \mathrel{{:}{-}} \vec{\mathrm{Atom}} & \text{rule} \\ \mathrm{Chr} & ::= \vec{\mathrm{App}} \mathrel{\backslash} \vec{\mathrm{App}} \mid \mathrm{App} \Leftrightarrow \vec{\mathrm{App}} & \text{constraint rule} \end{array}\end{split}\]

\(\mathrm{cut}\) is the cut. \(\mathrm{delay}\ c\ \vec X\) is the abstract form of \(\mathtt{declare\_constraint}\): it carries the applicative term \(c\) to suspend and the variables \(\vec X\) that trigger its resumption. A \(\mathrm{Chr}\) rule is a list of patterns to match, a list of patterns to match and remove, a guard (defaulting to “always true” in the concrete syntax) and a list of new goals; its concrete-syntax spelling is described in Constraint handling rules.

Runtime objects

A substitution \(\sigma\) is a partial map from unification variables to terms; \(\sigma\ t\) applies it to \(t\), and \(\mathrm{dom}(\sigma)\) is the set of variables it assigns. Two functions extend a substitution:

\[\begin{split}\begin{aligned} \mathrm{unify} &: \mathrm{Term} \times \mathrm{Term} \times \Sigma \rightharpoonup \Sigma \\ \mathrm{match} &: \mathrm{Term} \times \mathrm{Term} \times \Sigma \rightharpoonup \Sigma \end{aligned}\end{split}\]

\(\mathrm{unify}(t_1, t_2, \sigma) = \sigma'\) is the most general extension of \(\sigma\) such that \(\sigma' t_1 = \sigma' t_2\) (Miller, 1992). \(\mathrm{match}(t, p, \sigma) = \sigma'\) is the most general extension of \(\sigma\) such that \(\sigma' p = \sigma t\); it only ever assigns variables of the pattern \(p\), never ones already in \(t\), and this is what makes a signature’s input arguments matched rather than unified (Constraints). Both are partial: on failure they return \(\bot\).

A program \(\pi = (N, I)\) pairs a set of names \(N\) (the constants introduced by \(\mathtt{pi}\)) with an index \(I\) mapping each predicate to an ordered list of rules. \(h + \pi\) prepends the rules \(h\) to that index, giving them top priority; this is how \({\Rightarrow}\) extends the program for one goal.

A constraint store \(\kappa\) is a multiset of triples \((\pi, c, t)\): a program, a constraint (an applicative term), and a trigger (a list of variables). The store’s semantics is covered in detail in The constraint store.

A goal is a triple \((\pi, \mathrm{atom}, a)\): the program to solve the atom against, and the list of cut-to alternatives, what \(\mathrm{cut}\) restores. An alternative is itself a triple \((\kappa, \sigma, gs)\): a constraint store, a substitution, and the list of goals still to solve along that branch.

The semantics

\[\mathrm{run} : \mathrm{Alt} \times [\mathrm{Alt}] \rightharpoonup K \times \Sigma \times [\mathrm{Alt}]\]

\(\mathrm{run}\) takes the current alternative (its pending goals, store and substitution) and the list of alternatives still available, and either returns an updated store, substitution and remaining alternatives, or \(\bot\) when every alternative has been exhausted. We write a configuration \(\langle gs \mid a \mid \sigma \mid \kappa\rangle\) for one pending goal list together with the rest of that state, and \(\longrightarrow\) for one step of \(\mathrm{run}\); repeating \(\longrightarrow\) until it gets stuck at \(\mathrm{stop}\) or \(\mathrm{abort}\) below is what \(\mathrm{run}\) computes. To keep the rules narrow we write a goal at the head of \(gs\) as its program paired with its atom, \((\pi, \mathrm{atom})\), eliding the goal’s own cut-to alternatives except in \(\mathrm{cut}\), the one rule that reads them.

The rules that touch the constraint store (\(\mathrm{delay}\), \(\mathrm{resume}\)) take priority and are tried first; the rest are syntax-directed on the goal at the head of \(gs\). The \(\mathrm{resume}\) rule follows Michaylov & Pfenning, 1993, which reads a higher-order logic programming language as a constraint logic programming one.

\(\mathrm{stop}\)

\[\dfrac{}{\langle [\,] \mid a \mid \sigma \mid \kappa\rangle\ \to\ (\kappa,\ \sigma,\ a)}\]

an empty goal list returns the current store, substitution and alternatives.

\(\mathrm{call}\) (and \(\mathrm{backtrack}\), \(\mathrm{abort}\))

\(\mathrm{backchain}\) (below) produces one alternative per rule that applies to the goal at the head of \(gs\):

\[\dfrac{\mathrm{backchain}(\kappa, \pi, p\,\vec t, gs, \sigma, a) = (\kappa, \sigma_1, gs_1) :: rest} {\langle (\pi, p\,\vec t) :: gs \mid a \mid \sigma \mid \kappa\rangle \longrightarrow \langle gs_1 \mid rest \mathbin{+\!+} a \mid \sigma_1 \mid \kappa\rangle}\]

the first alternative becomes the new configuration, its own leftover rules \(rest\) pushed in front of \(a\). If \(\mathrm{backchain}\) is empty and \(a = a_0 :: a_s\), pop \(a_0\) instead, chronological backtracking to the most recent choice point, undoing every assignment made since. If it is empty and \(a = [\,]\), the computation stops.

\(\mathrm{cut}\)

\[\dfrac{}{\langle (\pi, \mathrm{cut}, a_{cut}) :: gs \mid a \mid \sigma \mid \kappa\rangle \longrightarrow \langle gs \mid a_{cut} \mid \sigma \mid \kappa\rangle}\]

\(\mathrm{cut}\) at the head of the goal list discards every alternative created since the enclosing rule was selected, by replacing the current alternatives \(a\) with the goal’s own cut-to alternatives \(a_{cut}\); the \(\mathrm{cut}\) goal is the one place a goal’s third component is read. This is why the cut is hard: alternatives left over from premises solved earlier in the same rule are discarded too, not only the untried rules for the predicate.

\(\beta\)

\[\dfrac{\sigma\,(X\,\vec t) \;=_{\beta\eta}\; p\,\vec u} {\langle (\pi, X\,\vec t) :: gs \mid a \mid \sigma \mid \kappa\rangle \longrightarrow \langle (\pi, p\,\vec u) :: gs \mid a \mid \sigma \mid \kappa\rangle}\]

if the head of the goal is a unification variable and \(\sigma X\) applied to \(\vec t\) \(\beta\)/\(\eta\)-reduces to an applicative term \(p\,\vec u\), the goal is replaced by it. This is what lets a unification variable stand for a predicate, as in \(P = \mathtt{true},\ P\).

\(\mathtt{pi}\)

\[\dfrac{y \mathbin{\#} \pi} {\langle (\pi, \mathtt{pi}\ x{\backslash}\ g) :: gs \mid a \mid \sigma \mid \kappa\rangle \longrightarrow \langle (y{+}\pi, g[x/y]) :: gs \mid a \mid \sigma \mid \kappa\rangle}\]

\(\mathtt{pi}\ x{\backslash}\ g\) picks a name \(y\) fresh for the program (\(y \mathbin{\#} \pi\), HDR’s notation for “fresh in”), adds it to \(\pi\), and continues with \(g[x/y]\), the body with the fresh name put in for the bound variable.

\({\Rightarrow}\)

\[\dfrac{}{\langle (\pi, h \Rightarrow g) :: gs \mid a \mid \sigma \mid \kappa\rangle \longrightarrow \langle (h{+}\pi, g) :: gs \mid a \mid \sigma \mid \kappa\rangle}\]

\(h \Rightarrow g\) continues with \(g\) under \(h + \pi\): the extra rules \(h\) prepended to the program, for the duration of \(g\) only.

\(\mathrm{delay}\)

\(\mathrm{delay}\ c\ \vec X\), the abstract form of \(\mathtt{declare\_constraint}\), adds \((\pi, c, \vec X)\) to the store. Because a new constraint may immediately enable a constraint handling rule, \(\mathcal{CHR}\) (below) runs right away; whatever goals it produces are solved before the rest of the current branch:

\[\dfrac{\mathcal{CHR}(\kappa, \pi, c, \vec X, a) = (gs', \kappa')} {\langle (\pi, \mathrm{delay}\ c\ \vec X) :: gs \mid a \mid \sigma \mid \kappa\rangle \longrightarrow \langle gs' \mathbin{+\!+} gs \mid a \mid \sigma \mid \kappa'\rangle}\]

\(\mathrm{resume}\)

whenever the store holds a constraint \((\pi, c, t)\) some variable of which is now in \(\mathrm{dom}(\sigma)\), it is removed from the store and \(c\) is solved next, ahead of every pending goal, under program \(\pi\) and the current alternatives as its cut-to list (irrelevant there, since \(c\) is an applicative term, never \(\mathrm{cut}\)):

\[\dfrac{(\pi, c, t) \in \kappa \quad \exists X \in t,\ X \in \mathrm{dom}(\sigma)} {\langle gs \mid a \mid \sigma \mid \kappa\rangle \longrightarrow \langle (\pi, c) :: gs \mid a \mid \sigma \mid \kappa - (\pi, c, t)\rangle}\]

Backchain

\(\mathrm{backchain}\) builds one alternative per rule of \(p\) that applies to the goal \(p \vec t\):

\[\begin{split}\begin{aligned} \mathrm{backchain}(\kappa, \pi, p\,\vec t, gs, \sigma, a)\ = \Big[\ &(\kappa,\ \sigma',\ [(\pi, g, a) \mid g \in \vec b] \mathbin{+\!+} gs) \\ \text{for}\ &(p\ \vec u \mathrel{{:}{-}} \vec b) \in \pi\ p \\ \text{if}\ &\mathrm{select}({\vec t\ \vec u},\, \sigma) = \sigma' \neq \bot\ \Big] \end{aligned}\end{split}\]

in the order the rules appear in \(\pi\ p\). Every new goal of every alternative carries the same cut-to list \(a\), the alternatives that existed right before backchaining, not any created by it or by exploring its results.

Select

\(\mathrm{select}\) is what makes a signature’s inputs matched and its outputs unified: given the pairs of a rule’s head arguments with the goal’s, it folds \(\mathrm{match}\) over the input pairs and \(\mathrm{unify}\) over the output pairs:

\[\begin{split}\begin{aligned} \mathrm{select}({\vec t\ \vec u},\, \sigma) =\ &\mathrm{fold}\ \mathrm{unify}\ {\vec t\ \vec u}_{\,\mathrm{out}} \\ &\ \big(\mathrm{fold}\ \mathrm{match}\ {\vec t\ \vec u}_{\,\mathrm{in}}\ \sigma\big) \end{aligned}\end{split}\]

folding \(\bot\) through either step aborts the whole rule, as does a failed \(\mathrm{match}\) or \(\mathrm{unify}\) on any one pair.

The \(\mathcal{CHR}\) procedure

A constraint rule \(G_1 \mathrel{\backslash} G_2 \mid T \Leftrightarrow G_3\) has a logical reading, \(T \land G_1 \Rightarrow (G_2 \Leftrightarrow G_3)\): when the guard \(T\) holds, \(G_2\) may be replaced by \(G_3\), provided \(G_1\) still needs to be solved. \(\mathcal{CHR}\) computes this for one freshly declared or resumed constraint, the active constraint, following the refined operational semantics of Duck, Stuckey, García de la Banda & Holzbaur, 2004, as formalized by Guidi, Sacerdoti Coen & Tassi, 2019 (The constraint store gives the informal, 8-step version of exactly this procedure):

\[\mathcal{CHR}(\kappa, \pi, c, t, a) = (g', \kappa')\ \text{where}\]

the active constraint \((\pi, c, t)\) is added to \(\kappa\) to get \(\kappa'\), and \(g'\) starts empty;
for each rule \(P_1 \ldots P_x \mathrel{\backslash} P_{x+1} \ldots P_n \mid Q \Leftrightarrow G\) of the active constraint’s clique, in declaration order;
for each position \(0 < j \le n\), in increasing order;
for each permutation \(C_1 \ldots C_n\) of constraints in \(\kappa'\) with \(C_j = (\pi, c, t)\);
match every \(C_i\) against \(P_i\), and run the guard \(Q\) in the program the top-level query was launched against, not in the \(\pi\) carried by any matched constraint (HDR §2.5.1); on success, committing to this rule, this position and this permutation, remove \(C_{x+1} \ldots C_n\) from \(\kappa'\), discard every remaining permutation that mentions any of them, and add the (substituted) \(G\) to \(g'\);
continue with the next rule at step 2.

Two refinements make this tractable. First, unless a constraint’s trigger is the shared wildcard that opts it out (The constraint store), step 4 only considers permutations whose constraints have a trigger overlapping \(t\), clustering the store instead of considering every constraint against every other one. Second, step 1 actually freshens \((\pi, c, t)\)’s own names before adding it, so that the names of every constraint in the store stay pairwise disjoint; this is the “frozen into its own space of names” of The constraint store.