<figure><img src="image_1.png" /></figure>

HAL
open science

# Determinacy Checking for Elpi: an Higher-Order Logic Programming language with Cut

Davide Fissore, Enrico Tassi

► To cite this version:

Davide Fissore, Enrico Tassi. Determinacy Checking for Elpi: an Higher-Order Logic Programming language with Cut. 2025. hal-05026472v3

HAL Id: hal-05026472

https://inria.hal.science/hal-05026472v3

Preprint submitted on 14 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Determinacy Checking for Elpi: an Higher-Order Logic Programming Language with Cut *

Davide Fissore¹[0009-0002-5934-8776] and Enrico Tassi¹[0000-0002-7783-528X]

Université Côte d'Azur, Inria

**Abstract.** Elpi is a higher-order logic programming language derived from λProlog and widely used to extend the Rocq interactive theorem prover. Typical users are familiar with types and functional programming but often lack experience with backtracking.

We introduce a language of signatures to declare that a predicate is operationally deterministic, meaning that calling the predicate does not leave any choice points. The signature language handles higher-order programs and dynamic programs.

We present a static analyzer that verifies these signatures and report its application to the majority of public Elpi code in the Rocq ecosystem.

**Keywords:** Determinacy Analysis, Higher Order, Logic Programming, Cut

## 1 Introduction

Elpi is a higher-order logic programming language, a dialect of λProlog, particularly well suited for manipulating syntax trees with binders (see [23,24,10,16]). It is used as an extension language for the Rocq Prover (formerly the Coq proof assistant) and has become an important piece of infrastructure: several projects and libraries depend on Elpi [19,4,7,21,11,12]. Examples include the Hierarchy-Builder library-structuring tool [8], which supports the Mathematical Components ecosystem [22] and mechanizations such as the Odd Order and Four Color theorems [14,13], and Derive, a program-and-proof synthesis framework with industrial applications at BlueRock systems [30,31,15].

Over the years Elpi was put in the hands of quite a number of Rocq users and the most widely cited barrier to entry has been the paradigm shift to a logic programming one. Rocq users are comfortable with typed and functional programming but often lack experience with backtracking and its control. Uncontrolled backtracking can produce slower programs and complicate debugging.

To lower this barrier we design a system of determinacy signatures that allows programmers to declare when a predicate behaves like a function: at most one result is produced and the runtime will not consider alternative results. This

<footnote>* This work has been supported by the French government, through the France 2030 investment plan managed by the Agence Nationale de la Recherche, as part of the "UCA DS4H" project, reference ANR-17-EURE-0004.</footnote>
notion of determinism is called *semidet* by Henderson et al. [18] and named *operationally deterministic* by Nakamura [26]. Alternative notions exist, for example Warren [9] considers predicates *observably deterministic* when they produce the same result multiple times or diverge. We chose operational determinacy since it matches the behavior of functions in mainstream functional languages.

The annotation language covers Elpi's higher-order features, including higher-order predicates (for example map and fold) and dynamic predicates that extend themselves at runtime.

We apply these annotations to a large portion of publicly available Elpi code in the Rocq ecosystem and report our experience. Our findings indicate that most Elpi programs are intended to be backtracking-free and require only minimal annotations for the static analyzer we implemented to verify determinacy.

*Contributions* 1) we design a language of signatures to assert the determinacy of predicates that covers higher-order logic programming constructs such as first-class predicates and dynamic predicates; 2) we implement a static analyzer for that language; 3) we apply the static analyzer to most of the Elpi code available in the Rocq ecosystem.

## 2 Elpi and determinacy signatures by examples

As in most logic programming languages, Elpi programs are organized in rules. When rules are not *mutually exclusive*, i.e. multiple rules apply on the same query, the runtime continues the computation using the rule with highest priority. Moreover it stores the other rules as a *choice point* and can backtrack to that point to continue the computation. What makes backtracking tricky to Elpi users is that it is an opt-out feature of logic programming: it is left to the programmer to tell the runtime to commit to one rule and discard the choice point, rather than the other way around. If the user forgets to commit to a rule, his program still works but becomes much harder to debug and typically slower to run in case of failures.

The simplest example is the list-membership *relation* that can succeed more than once if the element we are looking for occurs multiple times in the list:

1. `mem X [Y|_] :- X = Y. % the head is the X we are looking for, or`

2. `mem X [_|YS] :- mem X YS. % recurse on the tail`

In the code above each line represents a rule. By convention, unification variables are capitalized, and following the λ-calculus tradition application is written without parentheses, i.e. `f x` rather than `f(x)`. Square brackets are used for lists with pipe separating the head from the tail. The `:-` symbol separates the head of a rule from its premises. Rules are tried in the order of their declaration by unifying their head with the current query.

The first rule for `mem` is the base case: it succeeds if the head of the list is equal to the X we are looking for. The second one discards the list's head and continues
looking for X in the tail. A query such as `mem 2 [2,3,2]` can be solved in two different ways: either using rule 1 immediately, or using rule 2 twice to discard the first two items, and then conclude with rule 1.

Elpi users often have a background in functional programming and simply do expect `mem` to be a *function* testing membership, and not a relation. Moreover one needs to look, carefully, at how `mem` is implemented in order to see the peril. This misconception becomes a problem when they use `mem` in a larger piece of code and observe its execution.

```
main L :- code_before L, mem 1 L, code_after L.
```

For example, in the code above, one may see `code_after` being executed multiple times: each choice point left by `mem` enables the runtime to backtrack to that point in time and continue from there. Even worse, if `code_after` is expensive and fails, one pays its cost multiple times.

It must be said that backtracking can be very useful in some situations and that a programmer with experience in logic programming can take advantage of that. We want the Elpi casual user to be able to write code without mastering all that, and simply declare that they expect their code to compute functions.

```
func main list int -> . % the signature for main
```

The signature starts by a keyword declaring the determinacy of the predicate: `func` for deterministic predicates, that we also call functions, and `pred` for any predicate, including both functions and relations. Inputs are separated from outputs by the arrow symbol, and in the case of `main` there is no output.

```
main L :- code_before L, mem 1 L, code_after L.
%                 error: non-deterministic atom
```

Since `main` was declared as a function, our static analysis invites the user to discard the choice points left by `mem`, for example by inserting a `!` (a `cut` directive) after it. Assuming `code_after` is a function, this code is accepted, since the cut discards all choice points generated by `mem` and `code_before L`.

```
main L :- code_before L, mem 1 L, !, code_after L. % OK
```

Note that the programmer may also write a functional membership test as follows, and use it in functional code with no additional safeguard. In this case the cut discards the second rule as soon as `X = Y` succeeds.

```
func in int, list int -> .
in X [Y|_] :- X = Y, !. % commit to this rule, discard the next one
in X [_|YS] :- in X YS.
```

```
main L :- code_before L, in 1 L, code_after L. % OK
```

Tracking the use of backtracking code statically is a well known technique in logic programming called determinacy analysis [9,29]. What the literature lacks is a treatment of Elpi features not available in plain Prolog, see 2.1 and 2.2.
## 2.1 Higher-order programs

A notable higher-order program is the one turning relations into functions.

```
func once (pred) -> . % a function taking a predicate in input
```

```
once P :- P, !. % the ! commits to the first success
```

We say that the signature of the once predicate marks it as unconditionally a function: once leaves no choice points, no matter what it receives as the higher-order argument P.

An example of a conditional function is the predicate to map over a list:

```
func map (func A -> B), list A -> list B.
```

```
map _ [] [].
```

```
map F [X|XS] [Y|YS] :- F X Y, map F XS YS.
```

We say that the signature of map has a precondition, namely that F is a function, and a postcondition, namely that map is a function, i.e., the call map F L L' leaves no choice points. If the precondition is not met the postcondition is not guaranteed to hold and we say that map is miscalled. In this case we weaken its signature to:

```
pred map (func A -> B), list A -> list B.
```

Our static analysis tracks miscalled functions and considers them as relations for the analysis of the surrounding code. This is important to avoid code duplication, i.e., we can just have one copy of map in our library. We give an example of four scenarios involving calls and miscalls to map.

```
% a function
```

```
func incr int -> int.
```

```
incr 1 2.
```

```
% a relation
```

```
pred pdiv int -> int.
```

```
pdiv 6 3. pdiv 6 2.
```

```
% four predicates calling map or miscalling map
```

```
func p list int -> list int.
```

```
p L R :- map incr L R. % OK
```

```
pred q list int -> list int.
```

```
q L R :- map pdiv L R. % OK
```

```
func r list int -> list int.
```

```
r L R :- map pdiv L R.
```

```
func r1 list int -> list int.
```

```
r1 L R :- map pdiv L R, !. % OK
```

```
% error: non-deterministic atom
```

Here p is a function because the precondition of map is respected (incr is a function). The body of q contains a miscall to map; as a consequence q may leave choice points. This is not an error because q is declared to be a relation. The body of q and r are identical, but r should be a function and hence the static analyzer complains. The predicate r1 has the same signature of r but it compensates the miscall to map by discarding choice points via a cut. The static analyzer accepts this last declaration.
## 2.2 Dynamic programs

The domain where Elpi really shines is the manipulation of higher-order data represented via the so-called λ-tree syntax [25] also called HOAS in [27]. Such data is pervasive in interactive provers based on Type Theory such as Rocq. In the paradigmatic example below `tm` is the data type for λ-terms.

<table><tr><td>kind tm type.</td><td>% datatype of λ-terms in HOAS form</td></tr><tr><td>type app tm -> tm -> tm.</td><td>% - binary application</td></tr><tr><td>type lam (tm -> tm) -> tm.</td><td>% - λ-abstraction</td></tr></table>

In the HOAS encoding of syntax with binders we do not find a node for variables: we re-use the notion of bound variable of the programming language to encode the one of the syntax tree. At the level of types we see that the `lam` node carries an Elpi function over terms. It is by applying this function that one can recover the body of the λ-abstraction. A simple program manipulating higher-order data is the function performing a deep copy of a term:

```
func copy tm -> tm.
copy (app A B) (app C D) :- copy A C, copy B D.
copy (lam F) (lam G) :- pi x\ copy x x => copy (F x) (G x).
```

The copy of an application is built from the copies of the subterms. What is more interesting is how one copies under a binder. The `pi x\ copy x x =>` instruction generates a fresh constant `x` and adds to the program the rule `copy x x` for the rest of the execution of `copy`. That rule explains how to copy the new constant `x`. Intuitively `pi x\.. => ..` amounts to a well-bracketed use of Prolog's `assert/1` and `retract/1`. Finally the code performs a recursive call over `F x`: by applying the Elpi function `F` to the fresh symbol `x` one obtains the body of the λ-abstraction where the bound variable is replaced by the new symbol `x`.

We say that the predicate `copy` is *dynamic*, or open, since its code is dynamically augmented with rules. Even so `copy` is a function because no two rules can apply to the same input: `lam` and `app` are different constants, and each constant `x` generated dynamically is guaranteed to be fresh by the `pi` operator, hence each `copy x x` rule is mutually exclusive with the other rules.

The `copy` predicate, as given, implements the identity and may seem rather useless, but it is not! Since the program is open, one can add new rules for `copy` and change its behavior. For example the code below computes the weak head normal form of a λ-term by contracting the application of a λ-abstraction to an argument and uses `copy` to perform the substitution:

```
func whd tm -> tm.
whd (app H A) R :- whd H (lam F), !, % we fire the redex
pi x\ copy x A => copy (F x) S, whd S R. % and we continue
whd X X. % or we stop
```

The argument `A` is put in place of the (previously) bound variable in `F` by replacing that variable with `x` and by running `copy` with the addition of a special
rule copying x to A. Our static analysis understands this programming pattern and is able to recognize that `whd` is also a function. In particular the first rule, if taken, discard the second rule (due to the cut) and only calls functions.

## 3 Elpi's abstract syntax and rule selection

Any static analysis to rule out non-determinism must depend on the operational semantics of the language. In particular the order in which rules are applied and the order in which rule premises are executed directly impact the scope of the cut directive.

Here we specify the relevant aspects of Elpi. Its abstract syntax is given below.

<table><tr><td>Kp ::= p, q, ...</td><td>predicate</td><td>C ::= Kp | V | C Tm</td><td>callable</td></tr><tr><td>Kd ::= f, g...x, y, ...</td><td>constant</td><td>H ::= Kp | H Tm</td><td>head</td></tr><tr><td>V ::= X, Y ...</td><td>variable</td><td>A ::= C | CUT | PI Kd R A</td><td>atom</td></tr><tr><td>Tm ::= Kp | Kd | V | Tm Tm</td><td>term</td><td>R ::= H :- A*</td><td>rule</td></tr></table>

We assume a set Kp of predicate names, a set Kd of term constructors, and a set V of unification variables. We call the union of these three syntactic categories *symbols*. In the syntax of atoms A we find predicate calls (C), the `CUT` operator (explained in section 4) and the `PI` operator.<fnref n="1" /> The arguments of predicate calls are in the Tm nonterminal, for terms, that includes predicate calls along with first order data construction. For space constraint we omit from the syntax the construction of data with binders since it plays no interesting role in the static analysis of determinacy. We reserve s for symbols (`Kp` `∪` `Kd` `∪` V), v for variables, k for terms in `Kp` `∪` `Kd`, a and b for atoms, c for callables and r for rules. Given a rule h :- `b₁`...`bₙ` we call h the *head*, `b₁`...`bₙ` the *body* and each `bᵢ` a *body atom*. We use non-terminal as types, e.g., Tm is the type of terms. We use P for the type of programs, being lists of rules in R, and we reserve t for terms and P for programs.

**Definition 1 (Rule and atom selection).** Each rule has a *priority* and *rules* are applied following their *priority*. When a rule is applied, its *body atoms* are executed in order.

This selection strategy is called SLD and is the standard one for logic programs. In this strategy non-determinism arises when: 1) at least two rules can be used (successfully) to the *same query* (i.e., lack of mutual exclusion between rules, see section 4); 2) the call to a non-deterministic predicate, or the miscall of a deterministic one, is not followed by a cut (see section 5).

<footnote n="1">¹ In reality, in Elpi, `pi` and `=>` are two separate operators, generating a fresh symbol and loading a rule respectively, but for simplicity we only consider their combination.</footnote>
# 4 Hard Cut and Mutual Exclusion

We focus on how to address the first source of non-determinism.

In order to precisely describe `cut`, we need to introduce the notion of choice points, or alternatives. The type of an alternative $\mathcal{L}$ is equal to $\Sigma \times \mathcal{G}$, that is a substitution and a list of goals. The type of a goal $\mathcal{G}$ is equal to $\mathcal{P} \times \mathcal{A}$, that is a program and a query (an atom). Since the program can dynamically change due to $\mathcal{P}$, each (sub)goal must contain the program in which it should be solved. A substitution $\sigma$ is a mapping from unification variables $\mathcal{V}$ to terms $\mathfrak{Tm}$. We call this function space $\Sigma$ and we write $\varepsilon$ for the empty substitution. We write $\sigma \cdot t$ for the application of a substitution $\sigma$ to a term $t$.

**Definition 2 (Hard cut).** Given a rule for predicate $k$ with priority $p$ and body $b_1...b_i \subset \mathcal{U}T \dots$, the effect of reaching $\mathcal{U}T$ is that the runtime discards all alternatives generated by $b_1...b_i$ and all rules for $k$ with lower priority than $p$.

Unlike most logic programming languages, Elpi applies rules by matching the input arguments, rather than unifying them.

**Definition 3 (Unification / Matching).** Two terms $t$ and $u$ unify, as per [23], if there exists a substitution $\sigma$ such that $\sigma \cdot t = \sigma \cdot u$. We say that a term $t$ matches (the pattern) $u$ if there exists a substitution $\sigma$ such that $\sigma \cdot u = t$ and $\sigma \cdot t = t$.

Finally, in the next definition we distinguish between global rules, i.e., rules that are part of the program $\mathcal{P}$, and local rules that are loaded via the $\mathcal{P}$-operator. For example, the `copy` predicate from section 2.2 has two global rules and one local rule.

**Definition 4 (Mutual exclusion (mut_excl $\mathcal{P}$ $\mathcal{R}$))).** Given a program $\mathcal{P}$ and a rule $r$, we say that $r$ is mutually exclusive with the rules in $\mathcal{P}$ if it has the highest priority and one of the following additional conditions holds:

(a) there is a $\subset \mathcal{U}T$ in the body of $r$, or

(b) $r$ is a `gloabl` rule and all rules $r'$ in $\mathcal{P}$ have an input argument not unifying with the corresponding input in $r$, or

(c) $r$ is a local rule introduced via $\mathcal{P}$, $x$ and $b$, $x$ is an input of $r$ and for all rule $r'$ in the program, the corresponding input is not a variable

For example, the rules for predicate $p$ below are not mutually exclusive, so choice points may remain after a query resolution, hence introducing non-determinism. For instance, $p \ 1 \ X$ has two solutions, namely $X = 3$ and $X = 2$.

pred p int -> int.

p 1 3.

p 1 2.

func q int -> int.

q 1 3.

q 2 4.

func r int -> int.

r X R :- p X R, !.

r X R :- q X R.

Conversely, $q$ satisfies mutual exclusion: no query can trigger both rules. Note that, since inputs are matched, a query like `q X Y` has no solution in Elpi. Standard Prolog implementation would reject the query as not well moded since the
input X is not ground. Both rules for r match any input. If the first rule succeeds, the `CUT` removes the alternatives created by the call to `p` and also discards the other rule `r X R :- q X R`. If the first rule fails, the `CUT` is not reached hence the second rule is not discarded. Thus, at most one rule can succeed for `q`.

The predicates `s` and `s1` below illustrate the role of `pi`.

```
func s int -> int.       func s1 int -> int.
s X R :- pi y\ q y 3 => q X R. s1 X R :- pi y\ q 1 5 => q X R.
% error: mxecl violated ^^^^^
```

The local rule `q y 3` is mutually exclusive with the rules for `q` above since `y` is fresh: each time the rule is loaded `y` is different from `1` and `2` and any other fresh constants generated before. On the contrary the local rule `q 1 5` is not mutually exclusive: the query `s1 1 R` has two results, namely `R = 5` and `R = 3`.

# 5 Static analysis of determinacy signatures

The abstract syntax of signatures is given below. Predicate signatures `T`y start with input arguments from the `$S_i$` non-terminal, continue with output arguments from the `$S_o$` non-terminal and end with a determinacy marker `$D$`: `FUN` for functions and `REL` for relations (respectively `func` and `pred` in the concrete syntax).

```
S_i ::= S_o | S_i' -> S_i | ☆ i' -> S_i sign. start      D ::= FUN | REL determinacy
S_o ::= D | S_i' -> S_o | ☆ i' -> S_o sign. stop          ☆ ::= * all data
T_y ::= S_i signature
```

We collapse all data types into a single type `☆` and we disallow to store predicate into data, i.e., one cannot form a list of predicates. Note that the grammar of `T`y forces all input arguments to come first. We reserve `d` for instances of type `☆`, `ρ` and `τ` for signatures and `$D$` for instances of `$D$`. For example the signature `func map (func A -> B), list A -> list B` corresponds to `(★ ↦★ ◦► FUN) i' -> ★ i' -> ★ ◦► FUN`.

We denote booleans `$B$` = `{⊤, ⊥}`; contexts `Γ` being partial maps from symbols to signatures. We use `Ø` for the empty list and `x :: xs` for prepending the element `x` to a list `xs`. We reserve `Γ` for contexts.

**Operations on signatures.** We compare signatures using the standard subtyping relation of functional languages. In particular, we compare inputs contravariantly and outputs covariantly. It is similar to [17], except for the absence of the `Any` terminal. `FUN` is smaller than `REL` since functions generate a “smaller number of results” than relations.

$$ \begin{array}{ccc} * \subseteq * & D \subseteq D & FUN \subseteq REL \\ \rho \stackrel{i}{\rightarrow} \tau \subseteq \rho' \stackrel{i}{\rightarrow} \tau' & \text{iff} & \rho' \subseteq \rho \wedge \tau \subseteq \tau' \\ \rho \stackrel{o}{\rightarrow} \tau \subseteq \rho' \stackrel{o}{\rightarrow} \tau' & \text{iff} & \rho \subseteq \rho' \wedge \tau \subseteq \tau' \end{array} $$
The static analysis needs often to keep the stronger or weaker signature among two. We hence derive from $\subseteq$ a min and max operators defined below.

$$
\begin{align*}
\min * * = * & \quad \min \mathcal{D} \mathcal{D} = \mathcal{D} & \max * * = * & \quad \max \mathcal{D} \mathcal{D} = \mathcal{D} \\
\min \mathbf{FUN} \mathbf{REL} = \min \mathbf{REL} \mathbf{FUN} = \mathbf{FUN} & & \max \mathbf{FUN} \mathbf{REL} = \max \mathbf{REL} \mathbf{FUN} = \mathbf{REL} \\
\min (\rho \xrightarrow{i} \tau) (\rho' \xrightarrow{i} \tau') & = \max \rho \rho' \xrightarrow{i} \min \tau \tau' & \max (\rho \xrightarrow{i} \tau) (\rho' \xrightarrow{i} \tau') & = \min \rho \rho' \xrightarrow{i} \max \tau \tau' \\
\min (\rho \xrightarrow{\circ} \tau) (\rho' \xrightarrow{\circ} \tau') & = \min \rho \rho' \xrightarrow{\circ} \min \tau \tau' & \max (\rho \xrightarrow{\circ} \tau) (\rho' \xrightarrow{\circ} \tau') & = \max \rho \rho' \xrightarrow{\circ} \max \tau \tau'
\end{align*}
$$

When a predicate is miscalled we need to weaken its signature. For example in section 2.1 we have weakened the signature of `map` to `(★ i → ★ ◦→ FUN) i → ★ i → ★ ◦→ REL`. We define strong and weak as follows:

$$
\begin{align*}
\text{strong } ★ = ★ & \qquad \text{weak } ★ = ★ \\
\text{strong } REL = FUN \quad \text{strong } FUN = FUN & \qquad \text{weak } FUN = REL \quad \text{weak } REL = REL \\
\text{strong } (\rho \xrightarrow{i} \tau) = \text{weak } \rho \xrightarrow{i} \text{strong } \tau & \qquad \text{weak } (\rho \xrightarrow{i} \tau) = \text{strong } \rho \xrightarrow{i} \text{weak } \tau \\
\text{strong } (\rho \xrightarrow{\circ} \tau) = \text{strong } \rho \xrightarrow{\circ} \text{strong } \tau & \qquad \text{weak } (\rho \xrightarrow{\circ} \tau) = \text{weak } \rho \xrightarrow{\circ} \text{weak } \tau
\end{align*}
$$

**The idea.** The static analyzer accumulates knowledge on variables in a context $\Gamma$ initially only containing the signature of predicates. The checking algorithm considers one rule at a time. It begins by updating $\Gamma$ using the preconditions on the *inputs* of the head, then it scans all body atoms and finally checks the postconditions: the *determinacy* of the body and the *determinacy* of the *outputs* of the head.

For example, consider the predicates `comp` and `compose` below: `comp` is a function that takes as input two functions `F` and `G`, and calls them in sequence, whereas `compose` builds a new function from the two received in input.

```
func comp (func int -> int), (func int -> int), int -> int.
comp F G X Z :- F X Y, G Y Z.
```

```
func compose (func int -> int), (func int -> int) -> (func int -> int).
compose F G (comp F G).
```

After updating $\Gamma$ w.r.t. the preconditions of `comp`, $\Gamma$ flags `F` and `G` as functions. Then the algorithms scans all body atoms computing the max of their determinacies: since both `F X Y` and `G Y Z` are `FUN`, also their max is. Finally the analyzer checks that the determinacy of the body matches the declared one. The analysis for `compose` needs to check two postconditions: 1) the *output* term `comp F G` is a function, since the two arguments of `comp` match its signature; 2) the body of `compose` is deterministic since empty.

We now move to an example that involves a non-deterministic body atom.

```
func r (func int -> int), (pred int -> int), int -> int.
r F G X Y :- map G [X] [Z], !, compose F F H, H Z Y.
```

After analyzing the head the context asserts that `F` (resp. `G`) is a function (resp. a relation). In the body of `r`, the first atom is non-deterministic, since `G` violates the preconditions of `map`. The signature of `map G [X] [Z]` is hence weakened to
$$
\begin{array}{l}
x \text{ fresh in } \Gamma \qquad \mathcal{P}, \Gamma + \{x \mapsto \star\} \Big|_{\tau} r \\
\text{mut\_excl} \quad \mathcal{P} \Gamma x r \qquad (r :: \mathcal{P}), \Gamma + \{x \mapsto \star\}, \mathcal{D}|_{\bar{a}} a = \mathcal{D}', \Gamma' \\
\hline
\mathcal{P}, \Gamma, \mathcal{D}|_{\bar{a}} \pi_1 x r a = \mathcal{D}', \Gamma' \\
\hline
\mathcal{P}, \Gamma, -|_{\bar{a}} \text{cut} = \text{fun}, \Gamma \quad (\mathbf{a}_1) \qquad \frac{\Gamma|_{\text{tm}}^{\frac{i}{\text{tm}}} c = \text{rel}, \perp}{\mathcal{P}, \Gamma, -|_{\bar{a}} c = \text{rel}, \Gamma} \quad (\mathbf{a}_{\perp}) \\
\hline
\frac{\Gamma|_{\text{tm}}^{\frac{i}{\text{tm}}} c = \mathcal{D}', \tau}{\mathcal{P}, \Gamma, \mathcal{D}|_{\bar{a}} c = \max \mathcal{D} \mathcal{D}', \Gamma'} \quad (\mathbf{a}_c)
\end{array}
$$

<caption>Fig. 1: $\mathbb{P}$, $\Gamma$, $\mathcal{D}|_{\bar{a}} A = \mathcal{D}$, $\Gamma$ (check atom)</caption>

REL. Even if this atom could generate multiple alternatives, the cut commits to the first one restoring the determinism of the body of r up to that point. The call to **compose** satisfies its preconditions, so its postconditions apply: the entire atom **compose** F F H is considered deterministic and H is marked as a function in Γ. The final atom H Z Y is also deterministic because of the knowledge about H accumulated so far in Γ.

**The algorithm.** We present the static analyzer using derivation rules. Each procedure has an associated entails-like symbol, e.g., context $|_{\text{flag name}}$ intake = result. We use the equal sign to “mode” the rule, i.e., separate what is given to the rule from what is generated by it. The static analyzer is composed of seven procedures for a total of 24 rules. Here we list only the interesting ones, leaving the rest to the appendix.

The main entry point is **check rule** ($\mathbb{P}, \Gamma|_{\tau} \mathbb{R}$), that verifies if a rule validates the signature ascribed to its predicate. The procedure stores in $\Gamma$ all the knowledge available on variables in $\mathcal{V}$ and it verifies the precondition made by the signature entails the postcondition.

$$
\frac{\Gamma \big|_{\text{hd}}^{\frac{i}{\text{hd}}} c = \mathcal{D}_1, \Gamma_1 \quad \forall i \in 1 \dots n \text{ do } \mathcal{P}, \Gamma_i, \mathcal{D}_i|_{\bar{a}} b_i = \mathcal{D}_{i+1}, \Gamma_{i+1} \quad \Gamma_{n+1} \big|_{\text{hd}}^{\frac{o}{\text{hd}}} c : \mathcal{D}_{n+1}}{\mathcal{P}, \Gamma|_{\tau} c :- b_1 \dots b_n} (r)
$$

In particular the **assume head input** ($\Gamma \big|_{\text{hd}}^{\frac{i}{\text{hd}}} \mathbb{Tm} = \mathbb{Ty}, \Gamma$) procedures loads in $\Gamma_1$ the information assumed from the head inputs while **check head output** ($\Gamma \big|_{\text{hd}}^{\frac{o}{\text{hd}}} \mathbb{Tm} : \mathbb{Ty}$) verifies that $\Gamma_{n+1}$ entails the postcondition. Each of the $n$ body atoms $b_i$ is processed by **check atom** (fig. 1, $\mathbb{P}, \Gamma, \mathcal{D}|_{\bar{a}} A = \mathcal{D}, \Gamma$) that updates the context and computes the determinacy of the entire body $\mathcal{D}_{n+1}$.

We now focus on the analysis of an atom. The **check atom** procedure has two rules to handle cut (a!) and pi (a_∀), and two more rules to handle predicate calls (a_c) and predicate miscalls (a_⊥). The cut operator resets the current determinacy to Fun, while pi introduces a fresh symbol, checks the hypothetical rule and proceeds after adding r to P. Rule (a_c) verifies the preconditions for c are met, and assumes its postcondition generating an updated Γ'. The determi-
$$ \frac{\Gamma s = \tau \qquad (\mathbf{tm}_k^i)}{\Gamma \mathbf{|}_{\mathbf{tm}}^i s = \tau, \top} \qquad \frac{\Gamma \mathbf{|}_{\mathbf{tm}}^i f = \rho \mathbf{|} \to \tau, \top \qquad \Gamma \mathbf{|}_{\mathbf{tm}}^i t = \rho', \top \qquad \rho' \subseteq \rho \qquad (\mathbf{tm}_\top^i)}{\Gamma \mathbf{|}_{\mathbf{tm}}^i f t = \tau, \top} $$ $$ \frac{\Gamma \mathbf{|}_{\mathbf{tm}}^i f = \rho \mathbf{|} \to \tau, b_1 \qquad \Gamma \mathbf{|}_{\mathbf{tm}}^i t = \rho', b_2 \qquad b_1 = \bot \lor b_2 = \bot \lor \rho' \notin \rho \qquad (\mathbf{tm}_\bot^i)}{\Gamma \mathbf{|}_{\mathbf{tm}}^i f t = \text{weak } \tau, \bot} $$

Fig. 2: $\Gamma \mathbf{|}_{\mathbf{tm}}^i \mathbf{TM} = \mathbf{Ty}, \mathbb{B}$ (check input)

$$ \frac{\tau' = \text{if } X \in \Gamma \text{ then } \Gamma X \text{ else } \tau \qquad (\mathbf{tm}_X^\circ)}{\Gamma \mathbf{|}_{\mathbf{tm}}^\circ X : \tau = \Gamma + \{X \mapsto \min \tau \tau'\}} \qquad \frac{\Gamma k = \tau' \quad \tau' \subseteq \tau \qquad (\mathbf{tm}_k^\circ)}{\Gamma \mathbf{|}_{\mathbf{tm}}^\circ k : \tau = \Gamma} $$ $$ \frac{\Gamma \mathbf{|}_{\mathbf{tm}}^\circ f : \rho \mathbf{|} \to \tau = \Gamma' \qquad \Gamma' \mathbf{|}_{\mathbf{tm}}^\circ t : \rho = \Gamma'' \qquad (\mathbf{tm}_i^\circ)}{\Gamma \mathbf{|}_{\mathbf{tm}}^\circ f t : \tau = \Gamma''} $$

Fig. 3: $\Gamma \mathbf{|}_{\mathbf{tm}}^\circ \mathbf{TM} : \mathbf{Ty} = \Gamma$ (assume output)

nacy is set to the maximum of current determinacy and the one of the predicate. When precondition are not met the context is left untouched and the current determinacy is set to REL.

The most interesting procedure is the one to check if the preconditions of a predicate call are met, that is **check input** (fig. 2, $\Gamma \mathbf{|}_{\mathbf{tm}}^i \mathbf{TM} = \mathbf{Ty}, \mathbb{B}$). The procedure ignores data arguments and output arguments and simply fetches from the context the signature of constants and variables ($\mathbf{tm}_k^i$). Rule ($\mathbf{tm}_\top^i$) is the standard typing rule for application: if the input argument matches the expected signature it computes the return type, signaling no miscalls (i.e. $\top$). When the head or the argument contain a miscall, or when the argument does not match the expected signature, the rule ($\mathbf{tm}_\bot^i$) signals a miscall and computes the return type by weakening the one obtained from the head, i.e., the predicate call is considered as a relation, and the signature of the output arguments is also recursively weakened.

The procedure to update the context when an atom is found to be a good call is **assume call output** ($\Gamma \mathbf{|}_{\mathbf{ca}}^\circ \mathbf{TM} : \mathbf{Ty} = \Gamma$). Other than ignoring input arguments it calls **assume output** on output arguments.

$$ \frac{\Gamma \mathbf{|}_{\mathbf{ca}}^\circ f : \rho \mathbf{|} \to \tau = \Gamma' \qquad \Gamma' \mathbf{|}_{\mathbf{tm}}^\circ t : \rho = \Gamma'' \qquad (\mathbf{a}_o^\circ)}{\Gamma \mathbf{|}_{\mathbf{ca}}^\circ f t : \tau = \Gamma''} $$

The **assume output** procedure (fig. 3, $\Gamma \mathbf{|}_{\mathbf{tm}}^\circ \mathbf{TM} : \mathbf{Ty} = \Gamma$) updates the context when it encounters variables ($\mathbf{tm}_X^\circ$). When variable is already ascribed a signature in the context, we keep the stronger signature. Data and output arguments are skipped, while input arguments are recursively traversed: the signature of variables in their input positions are also updated in the context.

The processing of the head of a rule is akin to the one of body atoms, but symmetric in which arguments are used to strengthen the context and which are
checked for conformance. The **assume head input** procedure ($\Gamma|_{hd}^i \mathbb{Tm} = \mathbb{Ty}$, $\Gamma$) called at the very beginning of (r), ignores outputs and calls **assume output** on inputs.

The **check head output** ($\Gamma|_{hd}^\circ \mathbb{Tm} : \mathbb{Ty}$) procedure is called at the very end.

$$ \frac{\Gamma|_{hd}^\circ f : \rho \stackrel{\tau}{\to} \tau \qquad \Gamma|_{\mathbb{Tm}}^i t = \rho', \tau \qquad \rho' \subseteq \rho \quad (\mathbf{hd}^\circ)}{\Gamma|_{hd}^\circ f t : \tau} $$

It ignores input arguments but checks that the output ones satisfy the ascribed signature in the current context, that is the result of assuming the rule preconditions and all the postconditions of well called body atoms.

# 6 Determinism guarantees

In order to express operational determinacy we need to use an operational semantics for Elpi. That semantics, for its higher-order logic-programming part, is essentially the one given by [28] using a last-in-first-out goal selection. However it must be complemented with a treatment of choice points to describe the behavior of the cut operator following [5]. Moreover Elpi has a peculiar runtime threatment of input arguments, that are matched rather than unified (see definition 3).

For space constraints we omit the rules defining run, they can be found in the appendix or in [3].

**Definition 5 (Operational semantics (run : $\mathbb{L} \times \overrightarrow{\mathbb{L}} \to \Sigma \times \overrightarrow{\mathbb{L}}$)).** Run is a partial function from a non-empty list of alternatives to a solution consisting in a substitution and a list of yet-to-be-explored alternatives. The properties of run relevant to the current paper are:

1. $\mathbf{CUT}$ behaves as per definition 2

2. $\mathbf{PI} x r b$ generates a fresh constant for $x$ available in $r$ and $b$

3. $\mathbf{PI} x r b$ loads $r$ in the program giving it the highest priority

4. input arguments are matched against the query as per definition 3

**Definition 6 (Operationally deterministic execution (deterministic<sub>a</sub> P A)).** We say that a query atom $b$ is operationally deterministic in a program $\mathcal{P}$ iff

$$ run (\varepsilon, (\mathcal{P}, b) :: \emptyset) \emptyset = (-, a) \Rightarrow a = \emptyset $$

In other words a deterministic query leaves no alternatives when it succeeds. We now link the static check to the deterministic execution of a query.

**Definition 7 (Checked program (checked<sub>p</sub> Γ P)).** A program $\mathcal{P}$ is checked against a context of signatures $\Gamma$ iff it validates these rules:

$$ \frac{\text{checked}_p \Gamma \mathcal{P} \quad \text{mut_excl} \mathcal{P} r \quad \mathcal{P}, \Gamma|_r r}{\text{checked}_p \Gamma \emptyset} $$
The intuition is that we build the program from the end, always adding new rules with highest priority.

**Definition 8 (Checked query atom (checked<sub>a</sub> ⊢ A)).** An atom b is checked against a context of signatures Γ iff

$$ \emptyset, \Gamma, FUN|_{\sigma} b = FUN, - $$

**Theorem 1 (Static analysis).** Given program *P*, a context of signatures Γ and a query atom b, checked<sub>p</sub> Γ *P* ∧ checked<sub>a</sub> Γ b ⇒ deterministic<sub>a</sub> *P* b.

The proof of theorem 1 has been mechanized in the Rocq proof assistant, formerly known as Coq, for the first-order part [2]. The mechanization for the higher-order part is ongoing.

# 7 Experience report

The static analyzer we describe was integrated in the Elpi language version 3.0. It consists of about 200 lines of OCaml code for the implementation of mut_excl and about 800 lines of code for the implementation of check rule, along with all the related auxiliary functions. We have ported some Rocq libraries written using Elpi: Rocq-Elpi, Hierarchy Builder, Algebra Tactics, Trocq, and BRiCk.

We can divide the porting of these libraries into two categories: libraries in which we have traversed all the predicates and carefully changed pred markers to func (Elpi, Rocq-Elpi, and Hierarchy Builder), and libraries that have been ported to just pass the static analyzer. We summarize these results in table 1. In the Elpi standard library, we annotated 272 predicates out of 281 as functions, with 37 occurrences of higher-order arguments, as in map, filter, fold, etc. We identified 1 error, i.e., a missing cut. In Rocq-Elpi, we have 928 functions out of 1181, with 62 higher-order predicates. We added 91 cuts to please the static analyzer, 78 of which were clearly bugs in the code. The remaining 13 cuts are due to mut_excl, which is not powerful enough to discriminate rules; the problem is in general undecidable. An example of this problem is given below:

<table><caption>Table 1: Experience report</caption><thead><tr><th>Software</th><th>LOC</th><th>% FUN</th><th>CUT added</th><th>CUT needed (bugs)</th></tr></thead><tbody><tr><td>Elpi</td><td>1448</td><td>97%</td><td>1</td><td>1 (100%)</td></tr><tr><td>Rocq-Elpi</td><td>13164</td><td>79%</td><td>91</td><td>78 (85%)</td></tr><tr><td>Hierarchy Builder</td><td>5326</td><td>94%</td><td>33</td><td>30 (90%)</td></tr><tr><td>Algebra Tactics</td><td>1799</td><td>—</td><td>1</td><td>1 (100%)</td></tr><tr><td>Trocq</td><td>2918</td><td>—</td><td>4</td><td>4 (100%)</td></tr><tr><td>BRiCk (public)</td><td>2500</td><td>—</td><td>11</td><td>11 (100%)</td></tr><tr><td>BRiCk (private)</td><td>7500</td><td>—</td><td>6</td><td>6 (100%)</td></tr><tr><td>Total</td><td>34655</td><td>85%</td><td>147</td><td>131 (89%)</td></tr></tbody></table>
```python
func fact int -> int.

fact 0 1.

fact N R :- N > 0, N' is N - 1, fact N' R', R is N * R'.
```

The two rules for `fact` are in mutual exclusion: the input cannot be `0` and `greater than 0` at the same time. But a complete algorithm identifying all of these scenarios does not exist, and we require an explicit `cut` in the first rule.

In Hierarchy Builder, we have 460 functions out of 488, with 33 higher-order arguments, and we have corrected 30 bugs in the code.

Overall, we can conclude that 85% of the predicates were functions.

The numbers from the second category of libraries measure the minimal cost for adapting code to the changes we made to the Elpi and Rocq-Elpi standard libraries. The typical example of code requiring a fix is code that loads a local rule containing no cut, typically `copy`. In Algebra Tactics, we added 1 cut over 1799 lines of codes; in Trocq, we added 4 cuts over 2918 lines of code. None of these libraries were using `copy` as a relation, i.e. to generate all possible copies of a term. The BRiCk application has some public code we ported ourselves and some closed source code ported by the BlueRock company, that we thank for sharing these numebrs. In the public code we added 11 cuts over 2500 lines of code, while in the private one they added 11 cuts over 7500 lines.

## 8 Related work and concluding remarks

We summarize several related works in table 2.

One key difference between our work and [9,29,20,17]. is that they focus on closed predicates, that do not evolve during execution, while λProlog, hence Elpi, allows rules to be dynamically loaded. For closed predicates, programs can be transformed into *super-homogeneous* form by merging all rules into one with disjunctions. This simplifies determinacy inference and may allow to compile the code to a faster binary. However, this transformation is not feasible in our dynamic setting (section 2.2) and in particular the check for mutual exclusion needs a higher degree of sophistication.

Regarding modes, Elpi's matching procedure over input arguments allows us to dispense with explicit mode checking – an essential component in [9,29,20].

<table><caption>Table 2: Comparison with related work</caption><thead><tr><th></th><th>Mode check</th><th>Dynamic prog.</th><th>HO prog.</th><th>Miscalls</th></tr></thead><tbody><tr><td>Warren et al. [9]</td><td>required</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>RedAlert [20]</td><td>required</td><td>✗</td><td>✗</td><td>✗</td></tr><tr><td>Mercury [29]</td><td>required</td><td>✗</td><td>✓‡</td><td>✗†</td></tr><tr><td>Curry [17]</td><td>no need</td><td>✗</td><td>✓</td><td>✓</td></tr><tr><td>Elpi (this paper)</td><td>no need</td><td>✓</td><td>✓</td><td>✓</td></tr></tbody></table>
We differ from Red Alert [20] in that we pick an operational semantics that explicitly represents choice points as a list of alternatives, and that hence is very close to the actual behavior of Elpi's runtime. They pick a denotational semantics over the super-homogeneous form that in turn lets them formulate the static analyzer as an abstract interpreter. It is unclear if a denotational semantics can be written without transforming the program in super-homogeneous form.

Some of the higher-order features of the Elpi language are available in Mercury [29], although in a more constrained way (‡). For example `once` from section 2.1 is considerably more useful if the input relation is allowed to be non-ground, e.g., `once (map pdiv [6] L)`. We allow higher-order predicates to be miscalled, while Mercury does not. Instead, it requires higher-order functions to be annotated with explicit mode and determinacy signatures for each possible behavior. As a result, Mercury ascribes 11 signatures to the `foldr` predicate and any call that does not match exactly one of these signatures results in a compilation failure (†). Elpi targets less technically inclined users, more familiar with functional programming languages than logic ones, hence we strive for simplicity, defining only one determinacy class and immediately classifying wrong calls as non-deterministic. As a result the signature for `foldr` is just `func foldr (func L, A -> A), list L, A -> A`, familiar to our audience.

The “determinism types” of Curry [17] are much more similar to our signatures, and Curry supports miscalled functions as well. In the work of Hanus and Prott the Any type stands for non-determinism and like a black hole it absorbs the determinism of the surrounding sub-terms. This is a convenient way to capture all miscalls and treat them uniformly. In our presentation, we have no equivalent; instead, we use weak to change the signature of a term when a miscall is detected (`tm_⊥`) (or atom calls (`a_⊥`)). The advantage is that weak only changes the leaves (`D`) of the signature while leaving its structure intact. Although we do not analyze data in this paper, our set of rules can be complemented to perform full type checking (in addition to determinacy checking) in one pass.
In Curry the `allValues` builtin can be used to turn a relation into a function. Prolog, and also Elpi, provide a similar `findall` builtin, but in addition to that they also let one commit to the first result by either using `once`, or by placing a `cut` after the non-deterministic call. It is this “after the fact” commitment that make the analysis a bit more complex. In fact, in the body of a deterministic predicate we can have calls to relations (or miscalled functions) and still consider the rules valid with respect to determinacy (see (`a!`)). The notion of functional context in [9] is closely related to this difficulty.

Our experience report confirms most of the Elpi code out there is made of functional predicates and that the static analyzer accepts the vast majority of it requiring no changes. The main improvement we will consider is about mode subtyping for higher-order arguments. In the definition of $\subseteq$ we currently accept only arrows that have the same input/output mode. However, it seems possible to relax this condition. For example we could allow passing to `map` a function of type $★ \circled{→} ★ \circled{→} FUN$, since the modes of higher-order arguments seem to play no role in the determinacy of code that receives and calls them.
References

1. Andrews, J.H.: The witness properties and the semantics of the prolog cut. vol. 3, p. 1–59. Cambridge University Press (Jan 2003). https://doi.org/10.1017/S1471068402001540, https://doi.org/10.1017/S1471068402001540

2. Anonymous for blind review: https://github.com/gares/elpi-formalization, Note for the reviewer: the repository is not anonymized

3. Anonymous for blind review: Elpi: rule-based extension language. https://github.com/gares/HDR/blob/main/hdr.pdf, Note for the reviewer: the repository is not anonymized

4. Blot, V., Cousineau, D., Crance, E., de Prisque, L.D., Keller, C., Mahboubi, A., Vial, P.: Compositional pre-processing for automated reasoning in dependent type theory. In: Krebbers, R., Traytel, D., Pientka, B., Zdancewic, S. (eds.) Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2023, Boston, MA, USA, January 16-17, 2023. pp. 63–77. ACM (2023). https://doi.org/10.1145/3573105.3575676, https://doi.org/10.1145/3573105.3575676

5. de Bruin, A., de Vink, E.P.: Continuation semantics for prolog with cut. In: Díaz, J., Orejas, F. (eds.) TAPSOFT ’89. pp. 178–192. Springer (1989)

6. de Bruin, A., de Vink, E.P.: Retractions in comparing prolog semantics. In: Mathematical Foundations of Computer Science. pp. 180–186. Springer (1990)

7. Cohen, C., Crance, E., Mahboubi, A.: Trocq: Proof transfer for free, with or without univalence. In: Weirich, S. (ed.) Programming Languages and Systems. pp. 239–268. Springer Nature Switzerland, Cham (2024)

8. Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi. In: Proceedings of FSCD. LIPIcs, vol. 167, pp. 34:1–34:21 (2020). https://doi.org/10.4230/LIPIcs.FSCD.2020.34, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.34

9. Debray, S.K., Warren, D.S.: Functional computations in logic programs. vol. 11, p. 451–481. Association for Computing Machinery (Jul 1989). https://doi.org/10.1145/65979.65984, https://doi.org/10.1145/65979.65984

10. Dunchev, C., Guidi, F., Coen, C.S., Tassi, E.: ELPI: fast, embeddable, λProlog interpreter. In: Proceedings of LPAR. LNCS, vol. 9450, pp. 460–468. Springer (2015). https://doi.org/10.1007/978-3-662-48899-7_32, https://inria.hal.science/hal-01176856v1

11. Fissore, D., Tassi, E.: A new Type-Class solver for Coq in Elpi. In: The Coq Workshop (Jul 2023), https://inria.hal.science/hal-04467855

12. Fissore, D., Tassi, E.: Higher-order unification for free!: Reusing the meta-language unification for the object language. In: Proceedings of PPDP. pp. 1–13. ACM (2024). https://doi.org/10.1145/3678232.3678233, https://doi.org/10.1145/3678232.3678233

13. Gonthier, G.: A computer-checked proof of the Four Color Theorem. Tech. rep., Inria (Mar 2023), https://inria.hal.science/hal-04034866

14. Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7998, pp. 163–179. Springer (2013). https://doi.org/10.1007/978-3-642-39634-2_14, https://inria.hal.science/hal-00816699v1
15. Grégoire, B., Léchenet, J.C., Tassi, E.: Practical and sound equality tests, automatically. In: Proceedings of CPP. p. 167–181. Association for Computing Machinery (2023). https://doi.org/10.1145/3573105.3575683, https://doi.org/10.1145/3573105.3575683

16. Guidi, F., Coen, C.S., Tassi, E.: Implementing type theory in higher order constraint logic programming. In: Mathematical Structures in Computer Science. vol. 29, pp. 1125–1150. Cambridge University Press (2019). https://doi.org/10.1017/S0960129518000427

17. Hanus, M., Prott, K.O.: Determinism Types for Functional Logic Programming. In: Proceedings of PPDP. pp. 47–59

18. Henderson, F., Somogyi, Z., Conway, T.: Determinism analysis in the mercury compiler. In: Proceedings of Australian Computer Science Conference. pp. 337–346 (08 1996)

19. Krebbers, R., van der Maas, L., Tassi, E.: Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. In: Forster, Y., Keller, C. (eds.) 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol. 352, pp. 27:1–27:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2025). https://doi.org/10.4230/LIPIcs.ITP.2025.27, https://drops.dagstuhl.de/ entities/document/10.4230/LIPIcs.ITP.2025.27

20. Kriener, J., King, A.: Redalert: Determinacy inference for prolog. vol. 11, pp. 537–553. Cambridge University Press (2011)

21. van der Maas, L.: Extending the Iris Proof Mode with Inductive Predicates using Elpi. Master’s thesis, Radboud University Nijmegen (2024). https://doi.org/10.5281/zenodo.12568604

22. Mahboubi, A., Tassi, E.: Mathematical Components. Zenodo (Sep 2022). https://doi.org/10.5281/zenodo.7118596, https://doi.org/10.5281/zenodo.7118596

23. Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Extensions of Logic Programming. pp. 253–281. Springer (1991)

24. Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press (2012)

25. Miller, D.A.: Mechanized metatheory revisited. In: Journal of Automated Reasoning. vol. 63, pp. 625–665. Springer (2018)

26. Nakamura, K.: Control of logic program execution based on the functional relations. In: Proceedings of ICLP. p. 505–512. Springer (1986)

27. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of PLDI. p. 199–208. Association for Computing Machinery (1988). https://doi.org/10.1145/53990.54010, https://doi.org/10.1145/53990.54010

28. Qi, X.: An Implementation of the Language Lambda Prolog Organized around Higher-Order Pattern Unification. Ph.D. thesis, Graduate School of the University of Minnesota (2009), https://arxiv.org/abs/0911.5203

29. Somogyi, Z., Henderson, F., Conway, T.: The execution algorithm of mercury, an efficient purely declarative logic programming language. vol. 29, pp. 17–64 (1996). https://doi.org/10.1016/S0743-1066(96)00068-4, https://www.sciencedirect.com/science/inproceedings/pii/S0743106696000684, high-Performance Implementations of Logic Programming Systems

30. Tassi, E.: Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect). In: The Fourth International Workshop on Coq for Programming Languages (Jan 2018), https://inria.hal.science/hal-01637063
31. Tassi, E.: Deriving proved equality tests in Coq-Elpi. In: Proceedings of ITP. LIPIcs, vol. 141, pp. 29:1–29:18 (Sep 2019). https://doi.org/10.4230/LIPIcs.CVIT.2016.23, https://inria.hal.science/hal-01897468
## A Operational semantics

We use $\emptyset$ for the empty list and $x :: xs$ for prepending an element $x$ to a list $xs$; @ for list concatenation; $[e \text{ if } p \mid x \in \bar{x}]$ for list comprehension.

We denote with $\times$ and $\to$ the product, disjoint union, list and function space of types, respectively. We denote $f \vdash$ the first projection of a product.

A substitution $\sigma$ is a mapping from unification variables $\mathcal{V}$ to terms $\mathfrak{Tm}$ (we refer to this function space as $\mathfrak{S}$). We write $\sigma \cdot t$ to denote the application of a substitution $\sigma$ to a term $t$. This application recursively replaces variables in $t$ with their assignment in $\sigma$ if any, then recursively performs $\beta$-reduction on the given term.

We assume a function unify of type $\mathfrak{Tm} \times \mathfrak{Tm} \times \mathfrak{S} \to \mathfrak{S}$ such that if unify $t_1 t_2 \sigma = \sigma'$, then $\sigma'$ is the most general extension of $\sigma$ such that $\sigma' \cdot t_1 = \sigma' \cdot t_2$, as described in [23]. We also assume a function match of type $\mathfrak{Tm} \times \mathfrak{Tm} \times \mathfrak{S} \to \mathfrak{S}$ such that if match $t p \sigma = \sigma'$, then $\sigma'$ is the most general extension of $\sigma$ such that $\sigma \cdot t = \sigma' \cdot p$ and $\sigma' \cdot t = \sigma \cdot t$. In other words, match does not assign variables in $t$ but only in $p$, which acts as the pattern.

We write $t[y/x]$ for the usual, capture avoiding, operation of replacing the variable $x$ with $y$ inside $t$.

A program $\mathcal{P}$ of type $\mathcal{P}$ consists of an ordered list of rules, where rules appearing earlier have higher priority than those appearing later.

The type of a goal $\mathcal{G}$ is $\mathcal{P} \times \mathcal{A}$, which is a pair consisting of a program and an atom. The type of an alternative $\mathcal{L}$ is $\mathcal{S} \times \mathcal{G}$, which is a substitution and a list of goals. The $\mathcal{CUT}$ operator is annotated with a list of alternatives, allowing the interpreter to jump to a previous point in time. These alternatives are referred to as *cut-to* alternatives. The notation $\mathcal{CUT}^a$ represents the $\mathcal{CUT}$ atom with $a$ as its cut-to alternatives.

The select function, denoted as $S_\Gamma$, is used to verify whether the arguments of a query atom can unify with the arguments in the head of a rule. The context $\Gamma$ is used to recover the mode of predicate's arguments. This context is fixed, it does not change at runtime.

**Definition 9 (Select, $S_\Gamma : \mathcal{C} \times \mathcal{C} \times \mathfrak{S} \to \mathfrak{S})$.** $S_\Gamma(k_1, k_2, \sigma) = f \vdash S^\Gamma(c_1, c_2, \sigma)$ where $S^\Gamma : \mathcal{C} \times \mathcal{C} \times \mathfrak{S} \to \mathfrak{S} \times \mathfrak{Ty}$ is defined by the following rules:

$$ \frac{\overline{S^\Gamma(k, k, \sigma) = (\sigma, \Gamma k)} \qquad S_b^\Gamma}{\frac{S^\Gamma(h_1, h_2, \sigma) = (\sigma', \neg \to B) \qquad \text{match}(b_1, b_2, \sigma') = \sigma''}{S_m^\Gamma}} \qquad S_m^\Gamma \\ \frac{S^\Gamma(h_1, h_2, \sigma) = (\sigma'', B)}{S^\Gamma(h_1, h_2, \sigma) = (\sigma', \neg \to B) \qquad \text{unify}(b_1, b_2, \sigma') = \sigma''}{S_u^\Gamma} \qquad S_u^\Gamma $$

The match (resp. unify) procedure is used for arguments in input (resp. output) positions. The select function works in conjunction with the backchain
$$
\begin{array}{r@{\quad}l@{\quad}l@{\quad}l}
\frac{\sigma \cdot c = c'}{\text{run } (\sigma, (\mathcal{P}, c) :: gs) as = r} & \text{run}_\sigma & & \\
\frac{c \neq c'}{\text{run } (\sigma, (\mathcal{P}, c) :: gs) as = r} & & & \\
\cline{2-4}
\frac{\mathcal{B}(\mathcal{P}, \sigma, c, gs, (a :: as)) = \emptyset}{\text{run } (\sigma, (\mathcal{P}, c) :: gs) as = r} & \text{run } a \ as = r & \text{run}_\sigma & \\
\frac{\mathcal{B}(\mathcal{P}, \sigma, c, gs, as) = a' :: as'}{\text{run } (\sigma, (\mathcal{P}, c) :: gs) as = r} & \text{run } a' \ (as' @ as) = r & \text{run}_\sigma & \\
\frac{y \ \text{fresh}}{\text{run } (\sigma, (r[y/x] :: \mathcal{P}, g[y/x]) :: gs) as = r} & \text{run } (\sigma, (\mathcal{P}, (\pi_1 x r g)) :: gs) as = r & \text{run}_{\pi_1} & \\
\cline{2-4}
\end{array}
$$

<caption>Fig. 4: run : $\mathbb{L} \times \vec{\mathbb{L}} \to \vec{\mathbb{L}} \times \Sigma$</caption>

function, denoted as $\mathcal{B}$. The $\mathcal{B}$ function takes a program $\mathcal{P}$ and selects only the rules that can be used on a given callable under a certain substitution. The notation $g^{+as}$ is used to add the alternatives $as$ to the atom $g$ if $g$ is a $\subset \cup \tau$.

**Definition 10 (Backchain, $\mathcal{B} : \mathcal{P} \times \Sigma \times \mathcal{C} \times \vec{\mathcal{G}} \times \vec{\mathbb{L}} \to \vec{\mathbb{L}}$).**

$$
\mathcal{B}(\mathcal{P}, \sigma, c, gs, as) = \left[ \sigma', \left( \left( (\mathcal{P}, g^{+as}) \mid g \in \vec{b} \right] @ gs \right) \text{ if } \mathcal{S}_{\Gamma}(c, c_1, \sigma) = \sigma' \mid \left( c_1 :- \vec{b} \right) \in \mathcal{P} \right]
$$

The operational, big-step semantics of Elpi is defined by the function run in fig. 4. We write run (σ, gs) as = (σ', as') to indicate that a goal list gs under a substitution σ and alternatives as terminates with a substitution σ' and a remaining list of (still unexplored) alternatives as'. We write run (σ, gs) as = ⊥ to indicate that the execution halts, either because it fails to solve one of the given goals or because it runs out of alternatives. An initial query is written as run (ε, [(P, c)]) ∅ = -.

The first rule to examine is the one for cut (`run_1`): if the atom in the goal is a `subset` of alternatives, then the global alternatives are shortened to `as`, which are referred to as the cut-to alternatives.

The cut rule works in conjunction with `run_@`, which stores the current alternatives `as` in all the subgoals using the `B` function. This function is responsible for creating new alternatives `a' :: as'`, where the first alternative is directly evaluated, and the rest are prepended to the existing list of alternatives. The `S_Γ` function filters applicable clauses by unifying their heads with the goal. If no clause can be used, then rule `run_@` moves to the next alternative (backtracking to the most recent choice point, if any).

The stop rule `run_τ` terminates the goal with success as there are no more goals to be solved and returns the current substitution and the yet to be explored alternatives.

Rule `run_{\pi_1}` postulates a fresh symbol `y` and replaces the bound `x` for `y` everywhere, then it loads the new clause `r` into the program.
The last rule run<sub>σ</sub> deals with the fact that an atom can be a variable. If that variable is assigned in σ to a term that happens to be a predicate, then it proceeds.

The operational semantics we present is essentially an extension of the one
described in [6], adapted to accommodate the higher-order constructs of λProlog
and the input-matching behavior specific to Elpi. It is also worth mentioning [28],
where the author proposes a semantics for an implementation of a higher-order
pure λProlog. This implementation lacks an equivalent for the cut operator and
does not support the notion of clause priority.

Our semantics describes an SLD search strategy with a *hard-cut* operator, as
defined in [1]. This operator not only prunes later clauses of the same predicate
but also eliminates alternatives for subgoals that appear earlier in the clause
premise.

B The full algorithm

<figure><img src="image_3.png" /></figure>

The three relations above were introduced at the beginning of section 5.
They define a subtyping relation between signatures, as well as two pairs of
mutually recursive functions that compute the minimum and maximum between
two signatures, and the supremum and infimum of a signature within its lattice.

$$
\frac{\Gamma \Big|_{\text{hd}}^{\text{i}} c = \mathcal{D}_1, \Gamma_1 \quad \forall i \in 1 \dots n \text{ do } \mathcal{P}, \Gamma_i, \mathcal{D}_i \Big|_{\text{\textbf{a}}} b_i = \mathcal{D}_{i+1}, \Gamma_{i+1} \quad \Gamma_{n+1} \Big|_{\text{hd}}^{\text{o}} c : \mathcal{D}_{n+1}}{\mathcal{P}, \Gamma \Big|_{\tau}^{c} :- b_1 \dots b_n} \quad (r)
$$

<caption>Fig. 5: $\mathcal{P}$, $\Gamma \Big|_{\tau} \mathbb{R}$ (check rule)</caption>
The **check rule** above, was explained in section 5. Using the **assume head input** procedure (fig. 11, noted $|_{hd}^i$), it first assumes that the input terms of the clause head have the expected signature, producing the new context $\Gamma_1$.

Next, **check atom** (fig. 6, noted $|_a^\circ$) iterates over the body atoms, updating the context and tracking the determinacy of the body. Finally, **check head output** (fig. 11, noted $|_{hd}^\circ$) verifies that the postconditions of the rule are satisfied.

$$
\frac{
  \begin{array}{l}
    x \text{ fresh in } \Gamma \qquad \mathcal{P}, \Gamma + \{x \mapsto \star\} |_r r \\
    \text{mut\_excl} \quad \mathcal{P} \Gamma x r \quad (r :: \mathcal{P}), \Gamma + \{x \mapsto \star\}, \mathcal{D}|_a^\circ a = \mathcal{D}', \Gamma' \\
    \hline
    \mathcal{P}, \Gamma, \mathcal{D}|_{\underline{a}}^\circ \Gamma x r a = \mathcal{D}', \Gamma'
  \end{array}
}{
  \begin{array}{l}
    \mathcal{P}, \Gamma, -|_{\underline{a}}^\circ \text{ CUT} = \text{FUN}, \Gamma \quad (\mathbf{a}_!)
  \end{array}
} \quad (\mathbf{a}_\vee)
$$
$$
\frac{
  \begin{array}{l}
    \Gamma |_{\underline{tm}}^i c = \text{REL}, \perp \\
    \hline
    \mathcal{P}, \Gamma, -|_{\underline{a}}^\circ c = \text{REL}, \Gamma \quad (\mathbf{a}_\perp)
  \end{array}
}{
  \begin{array}{l}
    \Gamma |_{\underline{tm}}^i c = \mathcal{D}', \top \\
    \hline
    \mathcal{P}, \Gamma, \mathcal{D}|_{\underline{a}}^\circ c = \max \mathcal{D} \mathcal{D}', \Gamma' \quad (\mathbf{a}_c)
  \end{array}
} \quad (\mathbf{a}_\perp)
$$

<caption>Fig. 6: $\mathcal{P}$, $\Gamma$, $\mathcal{D}|_{\underline{a}}^\circ A = \mathcal{D}$, $\Gamma$ (check atom)</caption>

The **check atom** procedure has also been fully explained in section 5. We briefly summarize the main ideas behind this procedure. **check atom** takes the atom to be analyzed in a program $\mathcal{P}$, context $\Gamma$, and with an expected determinacy $\mathcal{D}$. Its role is to return a new context and a new determinacy obtained after the dynamic execution of the atom. In particular, by definition 2, the $\mathrm{CUT}$ operator does not change the context and simply restores the determinacy to $\mathrm{FUN}(\mathbf{a}_!)$.

The $\mathrm{PI}$ operator is treated by $(\mathbf{a}_\vee)$. Since $\mathrm{PI}$ introduces a fresh name $x$ and a new rule $r$ in the program, we need to verify that the new rule $r$ guarantees mutual exclusion and that it does not break the signature of the predicate it is extending. Then the atom beneath $\mathrm{PI}$ is recursively checked.

The determinacy check of predicate calls is delegated to $(\mathbf{a}_\perp)$ and $(\mathbf{a}_c)$. We use the **check input** (fig. 7, noted $|_{\underline{tm}}^i$) procedure to identify miscalls to the predicate. If a miscall is found, $(\mathbf{a}_\perp)$ returns an unmodified context and sets the determinacy of the execution to $\mathrm{REL}$. In the case of a valid call to a predicate $(\mathbf{a}_c)$, we assume its postconditions using **assume call output** (fig. 8, $|_{\underline{ca}}^\circ$), which returns an updated context $\Gamma'$ and the determinacy of the atoms $\mathcal{D}'$. The determinacy returned by $(\mathbf{a}_c)$ is the $\max \mathcal{D} \mathcal{D}'$.

The **check input** procedure receives a context $\Gamma$ and a term $t$. It traverses $t$ and its input terms recursively, excluding sub-terms of type $\star$ ($\vdash m_*^i$) and sub-terms in output positions ($\vdash m_o^i$). Then it returns the signature of $t$ together with a boolean indicating whether the predicate contains a miscall.

The base case is for constants and variables ($\vdash m_k^i$), where it fetches their signature in $\Gamma$.
$$ \frac{\Gamma s = \tau}{\Gamma |_{\mathfrak{t}m}^{i} s = \tau, \tau} (\mathfrak{t}m_k^i) \qquad \frac{\Gamma |_{\mathfrak{t}m}^{i} f = * \stackrel{i}{\rightarrow} \tau, b}{\Gamma |_{\mathfrak{t}m}^{i} f d = \tau, b} (\mathfrak{t}m_*^i) \qquad \frac{\Gamma |_{\mathfrak{t}m}^{i} f = - \stackrel{\circ}{\rightarrow} \tau, b}{\Gamma |_{\mathfrak{t}m}^{i} f t = \tau, b} (\mathfrak{t}m_o^i) $$

$$ \frac{\Gamma |_{\mathfrak{t}m}^{i} f = \rho \stackrel{i}{\rightarrow} \tau, \tau \qquad \Gamma |_{\mathfrak{t}m}^{i} t = \rho', \tau \qquad \rho' \subseteq \rho}{\Gamma |_{\mathfrak{t}m}^{i} f t = \tau, \tau} (\mathfrak{t}m_{\perp}^{i}) \\ \frac{\Gamma |_{\mathfrak{t}m}^{i} f = \rho \stackrel{i}{\rightarrow} \tau, b_1 \qquad \Gamma |_{\mathfrak{t}m}^{i} t = \rho', b_2 \qquad b_1 = \perp \lor b_2 = \perp \lor \rho' \notin \rho}{\Gamma |_{\mathfrak{t}m}^{i} f t = \text{weak } \tau, \perp} (\mathfrak{t}m_{\perp}^{i}) $$

<caption>Fig. 7: $\Gamma |_{\mathfrak{t}m}^{i} \mathfrak{t}m = \mathfrak{t}y, \mathfrak{B}$ (check input)</caption>

Rule $(\mathfrak{t}m_{\perp}^{i})$ is the standard typing rule for application: if the input argument matches the expected signature, it computes the return type, signaling no miscalls (i.e., $\tau$).

When the head or the argument contains a miscall, or when the argument does not match the expected signature, the rule $(\mathfrak{t}m_{\perp}^{i})$ signals a miscall and computes the return type by weakening the one obtained from the head. In this case, the predicate call is considered a relation, and the signature of the output arguments is also recursively weakened.

$$ \frac{\Gamma s = \tau}{\Gamma |_{\mathfrak{ca}}^{\mathfrak{o}} s : \tau = \Gamma} (\mathfrak{a}_k^{\circ}) \qquad \frac{\Gamma |_{\mathfrak{ca}}^{\mathfrak{o}} f : \rho \stackrel{\circ}{\rightarrow} \tau = \Gamma' \qquad \Gamma' |_{\mathfrak{t}m}^{\mathfrak{o}} t : \rho = \Gamma''}{\Gamma |_{\mathfrak{ca}}^{\mathfrak{o}} f t : \tau = \Gamma''} (\mathfrak{a}_o^{\circ}) \\ \frac{\Gamma |_{\mathfrak{ca}}^{\mathfrak{o}} f : - \stackrel{i}{\rightarrow} \tau = \Gamma}{\Gamma |_{\mathfrak{ca}}^{\mathfrak{o}} f t : \tau = \Gamma} (\mathfrak{a}_i^{\circ}) $$

<caption>Fig. 8: $\Gamma |_{\mathfrak{ca}}^{\mathfrak{o}} \mathfrak{t}m : \mathfrak{t}y = \Gamma$ (assume call output)</caption>

The **assume call output** is an iterator. It takes a context $\Gamma$, a term $t$, and a signature $\tau$. It aims to update $\Gamma$ by assuming signatures of variables appearing in the output position in $t$. The interesting case is rule $(\mathfrak{a}_o^{\circ})$. This rule calls **assume output** (fig. 9, $|_{\mathfrak{t}m}^{\mathfrak{o}}$) to recursively update the signature in the output term.

The **assume output** procedure (fig. 9, $\Gamma |_{\mathfrak{t}m}^{\mathfrak{o}} \mathfrak{t}m : \mathfrak{t}y = \Gamma$) updates the context when it encounters variables $(\mathfrak{t}m_{\perp}^{\circ})$. When a variable is already ascribed a signature in the context, we keep the stronger signature. Data and output arguments are skipped, while input arguments are recursively traversed: the signature of variables in their input positions is also updated in the context.

The processing of the head of a rule is similar to that of body atoms but symmetric in terms of which arguments are used to strengthen the context and which are checked for conformance. The **assume head input** procedure
$$ \frac{\tau' = \text{if } X \in \Gamma \text{ then } \Gamma X \text{ else } \tau}{\Gamma |_{\text{tm}}^{\circ} X : \tau = \Gamma + \{X \mapsto \min \tau \tau'\}} \quad (\text{tm}_X^{\circ}) \qquad \frac{\Gamma k = \tau' \quad \tau' \subseteq \tau}{\Gamma |_{\text{tm}}^{\circ} k : \tau = \Gamma} \quad (\text{tm}_k^{\circ}) $$

$$ \frac{\Gamma |_{\text{tm}}^{\circ} f : * \xrightarrow{\cdot} \tau = \Gamma'}{\Gamma |_{\text{tm}}^{\circ} f : d : \tau = \Gamma'} \quad (\text{tm}_*^{\circ}) \qquad \frac{\Gamma |_{\text{tm}}^{\circ} f : \cdot \xrightarrow{\cdot} \tau = \Gamma'}{\Gamma |_{\text{tm}}^{\circ} f : t : \tau = \Gamma'} \quad (\text{tm}_o^{\circ}) $$

$$ \frac{\Gamma |_{\text{tm}}^{\circ} f : \rho \xrightarrow{\cdot} \tau = \Gamma'}{\Gamma |_{\text{tm}}^{\circ} f : t : \tau = \Gamma''} \qquad \frac{\Gamma' |_{\text{tm}}^{\circ} t : \rho = \Gamma''}{\Gamma' |_{\text{tm}}^{\circ} f : t : \tau = \Gamma''} \quad (\text{tm}_i^{\circ}) $$

Fig. 9: $\Gamma |_{\text{tm}}^{\circ} \mathfrak{T}m : \mathfrak{T}y = \Gamma$ (assume output)

$$ \frac{\Gamma k = \tau}{\Gamma |_{\text{hd}}^{\text{i}} k = \tau, \Gamma} \quad (\text{hd}_k^{\text{i}}) \qquad \frac{\Gamma |_{\text{hd}}^{\text{i}} f = \cdot \xrightarrow{\cdot} \tau, \Gamma' \quad \Gamma |_{\text{hd}}^{\text{i}} f = * \xrightarrow{\cdot} \tau, \Gamma'}{\Gamma |_{\text{hd}}^{\text{i}} f : t = \tau, \Gamma'} \quad (\text{hd}_o^{\text{i}}) $$

$$ \frac{\Gamma |_{\text{hd}}^{\text{i}} f = \rho \xrightarrow{\cdot} \tau, \Gamma' \quad \Gamma' |_{\text{tm}}^{\circ} t : \rho = \Gamma''}{\Gamma |_{\text{hd}}^{\text{i}} f : t = \tau, \Gamma''} \quad (\text{hd}_i^{\text{i}}) $$

Fig. 10: $\Gamma |_{\text{hd}}^{\text{i}} \mathfrak{T}m = \mathfrak{T}y, \Gamma$ (assume head input)

$$ \frac{\Gamma k = \tau' \quad \tau \subseteq \tau'}{\Gamma |_{\text{hd}}^{\circ} k : \tau} \quad (\text{hd}_k^{\circ}) \qquad \frac{\Gamma |_{\text{hd}}^{\circ} f : \cdot \xrightarrow{\cdot} \tau \quad \Gamma |_{\text{hd}}^{\circ} f : * \xrightarrow{\cdot} \tau}{\Gamma |_{\text{hd}}^{\circ} f : t : \tau} \quad (\text{hd}_o^{\circ}) $$

$$ \frac{\Gamma |_{\text{hd}}^{\circ} f : \rho \xrightarrow{\cdot} \tau \quad \Gamma |_{\text{tm}}^{\text{i}} t = \rho', \tau \quad \rho' \subseteq \rho}{\Gamma |_{\text{hd}}^{\circ} f : t : \tau} \quad (\text{hd}_o^{\circ}) $$

Fig. 11: $\Gamma |_{\text{hd}}^{\circ} \mathfrak{T}m : \mathfrak{T}y$ (check head output)

($\Gamma |_{\text{hd}}^{\text{i}} \mathfrak{T}m = \mathfrak{T}y, \Gamma$), called at the very beginning of (r), ignores outputs and calls **assume output** on inputs.

The **check head output** procedure is called at the very end of **check rule**. It ignores input arguments but checks that the output ones satisfy the ascribed signature in the current context. This context results from assuming the rule preconditions and all the postconditions of well-called body atoms.