Determinacy checking

A functional predicate, one declared with func (Type declarations), is one the checker can prove leaves no choice point: every call has at most one solution. Its type is (func) where a relation’s is (pred). What the checker does with that promise is a static, best-effort analysis: not every non-deterministic call is caught. See Fissore & Tassi, PADL 2026 for the full formal treatment; elpi -no-det turns the analysis off.

The check is worth having because the code it applies to is overwhelmingly functional: the HDR thesis measures around 96% of the predicates in Elpi’s own code and in coq-elpi as computing a function rather than a relation. A left-over choice point in one of them is almost always a bug, and one that surfaces far from its cause.

What a functional signature promises

map is the running example (Fissore & Tassi, PADL 2026 opens with it). Its basic signature says only that map relates a higher-order argument and two lists:

pred map (pred A -> B), list A -> list B.       % basic
func map (func A -> B), list A -> list B.        % better (this checker)
map _ [] [].
map F [X|XS] [Y|YS] :- F X Y, map F XS YS.

The better signature says more: if the higher-order argument F is a function, then map F is a function too. A call map F L R with a functional F produces a single R. That is the whole content of writing func here: a promise about map’s determinacy conditional on its argument’s.

What the checker requires

For a func to be accepted, three things must hold, and each has its own error message so a rejection says which one failed:

  • its rules are mutually exclusive: no two can fire for the same call without one of them cutting. Two overlapping heads with no cut give Mutual exclusion violated for rules of predicate ….

  • every atom in its body is itself functional: a relational call in a func body is Found relational atom (…) in the body of function …, unless a ! after it collapses the choice point.

The checker does not run the body; it reasons from the signatures. A call it cannot prove functional it rejects, even when the program would in fact be deterministic. elpi -no-det, or a wider pred signature, is the way out when that happens.

Wrongly called predicates

A predicate is wrongly called when an argument passed to it is weaker than its signature asks for, the usual case being a relation passed where a function was expected. Three one-line definitions of a meal predicate, building a list of dishes for a list of guests, show what the checker does with that (likes is relational, since a guest may like several dishes; likes! is likes with a trailing cut, so functional):

func meal list guest -> list dish.
meal Gs Ds :- map likes! Gs Ds.        % accepted: likes! is a function
meal Gs Ds :- map likes  Gs Ds, !.     % accepted: the cut makes the body one
meal Gs Ds :- map likes  Gs Ds.        % rejected

The first is fine: likes! is a function, so map likes! is, so meal’s body is. The second wrongly calls map, since likes is only a relation, but then commits with !, which is enough. The third gets no such compensation, and the checker rejects it:

DetCheck: Found relational atom (likes) in the body of function meal.
Offending term: (likes)
 - Inferred: (pred any -> any)
 - Expected: (func any -> any)
Contained in: (map likes Gs Ds)
 - Inferred: (pred)
 - Expected: (func)

Nothing forces the fix to be a cut in meal’s own body. A wrapper whose signature says “the argument may be any predicate, but the result is a function” packages the commit safely:

func commit (pred A -> B), A -> B.
commit P X R :- P X R, !.
meal Gs Ds :- map (commit likes) Gs Ds.     % accepted

The signature is the interesting part: commit’s input is a plain pred, so passing likes is not a wrong call, yet commit likes is a func. commit is a two-argument analogue of the standard library’s std.once, which commits a whole goal rather than a predicate applied to its arguments.

The body of a pred is still traversed, but the comparison that would reject a relational atom in it is vacuous (a pred body is allowed to be relational), so a relational meal may call map likes freely: the call runs, it just quietly leaves a choice point. The output signatures of a pred are checked all the same. This is how a codebase adopts determinacy checking incrementally: leave the relations alone, mark func only what is ready.

../code/wrongly-called.elpi:

 1% map's better signature promises: if F is a function, map F is a function.
 2% `meal` is a func, so its body must be functional -- calling map with the
 3% deterministic `likes!` keeps the promise. `wrong-meal` is only a pred, so
 4% the checker lets it call map with the plain relation `likes`: the call
 5% still runs, it just leaves a choice point that backtracking walks into.
 6
 7data guest.
 8data dish.
 9symb mario, anna guest.
10symb pizza, pasta, gelato dish.
11
12pred likes guest -> dish.            % relational: mario likes two dishes
13likes mario pizza.
14likes mario pasta.
15likes anna gelato.
16
17func likes! guest -> dish.           % functional: commit to the first
18likes! G D :- likes G D, !.
19
20func map (func A -> B), list A -> list B.
21map _ [] [].
22map F [X|XS] [Y|YS] :- F X Y, map F XS YS.
23
24func meal list guest -> list dish.
25meal Gs Ds :- map likes! Gs Ds.
26
27pred wrong-meal list guest -> list dish.
28wrong-meal Gs Ds :- map likes Gs Ds.
29
30main :-
31  meal [mario, anna] Ds, print "meal:" Ds,
32  ( wrong-meal [mario, anna] Ds1, print "wrong-meal:" Ds1, fail
33  ; true ).

meal: [pizza, gelato]
wrong-meal: [pizza, gelato]
wrong-meal: [pasta, gelato]

meal is a func and passes likes!; wrong-meal is a pred and gets away with the plain relation likes, whose extra solutions backtracking then walks into.

A function that extends the program

A func may add rules to itself at run time and stay a func. The standard shape is a HOAS traversal that goes under a binder: copy copies a term, and under lam it needs a copy x x rule for the fresh bound variable. Added with plain ==> that rule overlaps the structural ones and mutual exclusion fails; added with =!=> (Inference rules and queries) it carries a cut at the end of its body, so the checker still sees a single-valued copy:

../code/functional-hoas.elpi:

 1data tm.
 2symb app tm -> tm -> tm.
 3symb lam (tm -> tm) -> tm.
 4
 5% `copy` is a function: one output per input. Going under `lam`, it adds a
 6% `copy x x` rule for the fresh bound variable. Written with =!=> so a cut is
 7% appended to that rule's body -- the determinacy checker still sees `copy` as
 8% a func, where plain ==> would flag the two overlapping `copy` rules.
 9func copy tm -> tm.
10copy (app A B) (app A1 B1) :- copy A A1, copy B B1.
11copy (lam F) (lam F1) :- pi x\ copy x x =!=> copy (F x) (F1 x).
12
13main :-
14  copy (lam x\ app x x) T,
15  print "copied:" T.

copied: lam c0 \ app c0 c0

This is what =!=> is for: a rule known only at run time, meant to fire once, in a predicate the checker must keep treating as deterministic.

Signatures as a subtyping relation

A functional signature is stronger than a relational one: whatever a func can do, a pred can do too, but not the other way round. The checker compares signatures with a subtyping relation ⊆, read “is at least as strong as”, contravariant on inputs and covariant on outputs: a function expecting a weaker (more relational) predicate as an input argument accepts a stronger (more functional) one in its place, and a function promising a stronger output may be used wherever a weaker one is expected. map’s better signature is exactly the ⊆-smallest one above the basic one that still carries the conditional-determinacy promise.

Functional status of outputs

A signature’s output being functional is itself information a caller can use. For instance func id A -> A (with the single rule id X X) promises whoever receives its output a value, not a choice among values.

The code below turns a two-argument relation into a one-argument function by picking the first solution and cutting:

func make-deterministic (pred A -> B) -> (func A -> B).
make-deterministic P (x\y\ P x y, !).

make-deterministic likes F gives an F the checker can treat as a func A -> B from then on, for instance as the argument to map, now correctly called. Passing likes itself in that position, with no make-deterministic around it, is the wrong call of the previous section.