2026-01-20
This survey is written around Łukasz Stafiniak’s PhD thesis GADTs for Reconstruction of Invariants and Postconditions (University of Wrocław, 2015), focusing on Section 4.2 (“Constraint Abduction”), especially Section 4.2.4.1 (“Abduction for Terms”) and the JCAQP over the free term algebra \(\mathcal{T}(\mathcal{F})\) problem. The bibliography and appendix pointers (A.2.2, B.2.2, B.2.3) are aligned to the thesis’ full PDF.
Constraint abduction asks for “missing hypotheses” \(A\) such that \((D \land A) \Rightarrow C\) holds in a fixed model \(\mathcal{M}\), while \(D \land A\) remains satisfiable. In verification and type inference, the missing hypotheses are not arbitrary formulas but constraints drawn from a solver domain (e.g. equations over a term algebra, Presburger arithmetic, or combinations thereof). Stafiniak (2015, Section 4.2) introduces Joint Constraint Abduction under a Quantifier Prefix (JCAQP), motivated by type-inference-driven invariant generation and by implication constraints in GADT typing. This survey focuses on the hard core case where the background model is the free term algebra \(\mathcal{T}(\mathcal{F})\) and the abducted constraints are (existentially quantified) conjunctions of equations. We review the landscape of Herbrand constraint abduction (Maher; Maher & Huang), the jump from simple to joint abduction, the extra complications caused by quantifier prefixes, and the delicate role of Herbrandization/Skolemization in a fixed-model setting. We then address the thesis-motivated question of how closely the JCAQP\(_{\mathcal{T}(\mathcal{F})}\) existence problem relates to Simultaneous Rigid \(E\)-Unification (SREU) (Degtyarev–Voronkov; Voronkov), and what can (and likely cannot) be reduced to what. Finally, we summarize 2014–2026 follow-up work on closely related forms of abduction—especially SMT/SyGuS “abduction as a service” and verification-oriented abduction—and discuss what (if anything) this implies for inference problems more expressive than OutsideIn-style approaches to GADTs.
Classical (logical) abduction is usually phrased as: given a background theory \(\Gamma\) and a goal \(C\), find an explanation \(A\) such that \(\Gamma \cup \{A\} \models C\) and \(A\) is consistent with \(\Gamma\), subject to syntactic restrictions on \(A\). In constraint abduction, the background is not an abstract theory but a fixed model \(\mathcal{M}\) and the objects of interest are constraints interpreted in that model. A typical instance is a pair \((D, C)\) and we seek \(A\) such that:
Stafiniak (2015) adopts this fixed-model stance explicitly and emphasizes that it interacts nontrivially with quantifiers (Section 4.2 intro; see also the example in Section 4.2.4.1 on why Herbrandization can be unsound for a fixed model).
Many applications do not present a single implication, but a family of implications that must all be satisfied by a single abducted hypothesis \(A\). This is Joint (Simultaneous) Constraint Abduction (JCA) in Maher’s terminology, and it already behaves differently from “just solve each implication and conjoin” (e.g. Example 12 in Maher, “Herbrand Constraint Abduction”, shows JCA cannot be reduced to SCA in general).
In verification and typing, we also routinely face quantification:
These pressures lead to the thesis’ central formulation:
A JCAQP problem is \(Q:\bigwedge_i (D_i \Rightarrow C_i)\) where \(Q\) is a quantifier prefix and \(D_i,C_i\) are conjunctions of atoms. A candidate answer is an existentially quantified conjunction of atoms \(\exists \bar\beta.\,A\) satisfying relevance/validity/consistency/no-escaping. (Your thesis, Def. 4.1)
The free term algebra \(\mathcal{T}(\mathcal{F})\) over signature \(\mathcal{F}\) interprets function symbols as constructors and equality as syntactic identity of ground terms. It is the canonical model underlying unification-based HM typing and the Herbrand constraint domain used in the Maher/Sulzmann lines of work.
Two distinct “hardness boundaries” are easy to conflate here:
It is the second boundary that is at the core of JCAQP\(_{\mathcal{T}(\mathcal{F})}\).
Maher’s “Herbrand constraint abduction” line, and the follow-on “On computing constraint abduction answers” (Maher & Huang), study the Herbrand constraint domains:
Key takeaways (see Maher, “Herbrand Constraint Abduction”, and Maher & Huang, “On Computing Constraint Abduction Answers”):
Sulzmann–Schrijvers–Stuckey propose to model GADT typing via implication constraints \(D \supset C\) and then solve them by Herbrand constraint abduction, producing conjunctions of type equations as solutions (“Type Inference for GADTs via Herbrand Constraint Abduction”). The paper’s central empirical punchline is that even for small GADT programs, there can be infinitely many maximal types, establishing that unrestricted GADT inference is not the Hindley–Milner story.
The methodological linkage to Section 4.2 of your thesis is:
However, the thesis’ JCAQP focus is strictly broader: it targets quantifier prefixes and multi-sorted combination, motivated by invariant generation and richer constraint domains than pure type equations.
Stafiniak (2015) distinguishes (implicitly but crucially) between:
Even if the decision problem is decidable, the abduction problem can remain open/undecidable/ill-behaved because abduction quantifies over candidate hypotheses \(A\) (a synthesis space), and because “good” answers are usually constrained by admissibility conditions that are not purely semantic (e.g. avoiding escaping parameters, avoiding non-intuitive solutions, etc.).
Section 4.2 of Stafiniak (2015) makes a sharp point that is easy to miss if one comes from automated deduction rather than fixed-model constraints:
Stafiniak’s illustrative counterexample (Section 4.2.4.1) shows that Herbrandization can change a formula’s meaning when interpreted in \(\mathcal{T}(\mathcal{F})\): a premise that is unsatisfiable in \(\mathcal{T}(\mathcal{F})\) (“\(a \doteq b(x)\)”) collapses an implication away, while Herbrandization/Skolemization can turn it into a statement that effectively forces a particular instantiation (e.g. \(\varphi(a)\)).
For invariant synthesis, this is the core reason you typically want to reason under the quantifier prefix rather than Skolemize it away: Skolem functions represent witnesses that may depend on universals; but invariants (and types) are usually required to live in a constraint language that does not admit arbitrary fresh function symbols, and—in the fixed-model reading—adding such symbols changes the model and thus changes what it means for an abduction answer to be relevant/consistent.
Even if one could justify Skolemization in a given setting (e.g. by switching to a proof-theoretic rather than fixed-model reading, or by extending the signature intentionally), it can still be counterproductive for synthesis tasks:
This is exactly Stafiniak’s motivation for keeping quantification explicit and adding “no escaping variables” constraints to control dependency.
Simultaneous rigid \(E\)-unification (SREU) arose in proof search for first-order logic with equality (tableaux, connection method, model elimination, etc.). Intuitively, it asks for a single substitution that makes multiple “rigid equations” solvable under their respective (rigid) equational assumptions. Classic results include:
Stafiniak (2015, Section 4.2.4.1) states: the JAQP problem for first-order logic with function symbols and equality is undecidable because it is equivalent—via Herbrandization—to SREU; moreover the existence of (JCAQP/JAQP-style) answers coincides with intuitionistic satisfiability.
The important nuance for the present survey is that this equivalence is not an immediate statement about JCAQP over the fixed model \(\mathcal{T}(\mathcal{F})\). It is about a proof-theoretic/logical reading where Herbrandization is admissible as part of the meta-theory.
Your question (“Can SREU be reduced to JCAQP over \(\mathcal{T}(\mathcal{F})\)?”) is exactly where the fixed-model vs proof-theoretic split matters.
What we can say with high confidence from the material at hand:
So: as stated (fixed model \(\mathcal{T}(\mathcal{F})\), fixed signature \(\mathcal{F}\), abducted constraints are equations over that algebra), a clean published reduction SREU \(\leq\) JCAQP\(_{\mathcal{T}(\mathcal{F})}\) is not something Stafiniak (2015) establishes, and it is plausibly open.
There are two ways one might try to get a reduction “in spirit”, each with a cost:
If we restrict to “plain” Herbrand JCA where:
then we are squarely in the Maher/Maher–Huang world. This world already exhibits severe combinatorial blowups and unknown decidability for some joint problems, but it lacks the explicit quantifier alternation and the proof-theoretic strength that drives SREU’s connection to intuitionistic provability.
Heuristically:
From the excerpts at hand, a conservative conclusion is:
A reduction SREU \(\leq\) JCA\(_{\mathcal{T}(\mathcal{F})}\) with existential variables only is not supported by the provided sources, and would be surprising without additional machinery that reintroduces universal/rigid structure.
Your question frames a common tension: “Do we really need to avoid Herbrandization/Skolem constraints and reason under the quantifier prefix?”
In the fixed-model constraint-abduction setting of Stafiniak (2015, Section 4.2), the answer is: yes, if the goal is to preserve semantics and keep solutions in the intended constraint language. More concretely:
So, in Stafiniak’s fixed-model setting you are not “wrong” to avoid Herbrandization; rather, the avoidance is a principled response to the fixed-model semantics and the intended language of solutions.
Mostly no, at least not in the same way.
Sulzmann et al. work inside the Herbrand constraint domain and give a normalization/elimination procedure that removes universal quantifiers from solved forms without introducing Skolem function symbols (their “elim” construction). The transformations are justified as equivalences in the intended semantics of Herbrand constraints (their Theorem 4).
That said, your thesis’ warning becomes relevant again if one tries to:
In other words: Sulzmann et al. do not appear to rely on “Skolemization introduces fresh uninterpreted functions” as a core step; but the thesis’ caution is still relevant to generalizing the approach to JCAQP-style multi-sorted, quantifier-prefix problems for invariant generation.
The 2014–2026 period does not (to the best of what is visible from the sources consulted here) deliver a universally accepted, fully automatic, strictly more expressive alternative to OutsideIn for general GADT inference—largely because the underlying inference problem remains fundamentally ill-behaved (infinite maximal types / undecidability phenomena already documented by Sulzmann et al.). What does evolve substantially is the ecosystem around abduction as solver functionality, especially in SMT and verification.
Work in the SyGuS/SMT community turns abduction into a first-class query to solvers:
--sygus-abduct). (CVC4 1.7 release notes, 2019)get-abduct / get-abduct-next.
(cvc5 documentation, continuously updated; accessed 2026)From the JCAQP perspective, this direction is interesting because it makes abduction a composable back-end service: one can imagine decomposing a multi-sorted JCAQP instance into multiple abduct subqueries (as your thesis proposes via a combination procedure), while letting the solver handle substantial fragments of each domain.
Abduction continues to play a role in verification beyond the classic interpolant-based toolkit:
These verification uses often operate in arithmetic or decidable background theories and focus on generating helpful auxiliary assertions. The bridge back to JCAQP\(_{\mathcal{T}(\mathcal{F})}\) is methodological: if term equalities and their quantifier-prefix discipline are part of the invariant language (e.g. symbolic heaps, inductive data structures, or type-level invariants), then JCAQP becomes a natural organizing abstraction.
Although classic bi-abduction for separation logic predates 2014, work continues on extending bi-abduction to richer domains. For example, a 2020 paper studies bi-abduction in a fragment of separation logic with ordered data. This matters to the present survey mainly as evidence that abduction remains a viable lens even in domains where constraints include inductive structure and nontrivial theories.
Post-2014 practical type inference work in mainstream compilers largely continues to rely on constraint solving with carefully designed restrictions and with user-provided annotations in hard cases. From the perspective of this survey:
This section tries to make the “is it obviously undecidable by SREU?” question as crisp as possible. The outcome is not a proof, but (i) a concrete reduction attempt and (ii) a clear explanation of where it breaks under the fixed-model semantics of Section 4.2. The punchline is that the standard SREU \(\leftrightarrow\) prenex intuitionistic provability route goes through transformations (Herbrandization/Skolemization and “assumptions as derivability”) that do not have a straightforward counterpart in satisfaction over the free term algebra.
There are at least three “nearby” problems with similar syntax but different semantics:
The SREU equivalences in Voronkov’s account live squarely in (1). Your Open Problem 1 is about (2).
An SREU instance can be seen as a finite family of rigid equations \[ \{E_i \vdash^\forall s_i \approx t_i\}_{i=1}^n \] and asks for a single substitution \(\theta\) (shared across all \(i\)) such that for each \(i\), \[ E_i\theta \vdash s_i\theta \approx t_i\theta \] holds in the intended “rigid/equational” derivability relation (Voronkov’s survey discusses several equivalent formulations and their links to intuitionistic provability).
Two semantic features matter for the reduction attempt:
Try to translate each rigid equation \(E_i \vdash s_i \approx t_i\) into an implication constraint \[ D_i \Rightarrow C_i \quad\text{where}\quad D_i := \bigwedge E_i,\; C_i := (s_i \doteq t_i), \] and let the abducted hypothesis \(A\) encode the substitution \(\theta\) as a conjunction of equations (e.g. \(x_j \doteq u_j\) for each substitution variable \(x_j\)).
If this worked, the target would be a JCA instance in \(\mathcal{T}(\mathcal{F})\) asking for \(A\) such that for all \(i\): \[ \mathcal{T}(\mathcal{F}) \models (D_i \land A) \Rightarrow C_i. \]
But this immediately runs into the “premises are assumptions, not satisfiable constraints” problem:
This is the same phenomenon highlighted by the thesis’ Section 4.2.4.1 counterexample: antecedents that are false in \(\mathcal{T}(\mathcal{F})\) make implications trivially true, collapsing the intended meaning.
So the naive encoding does not even get off the ground: it cannot faithfully represent “derivability under assumptions” using only satisfaction of implications in the free term algebra.
One might try to repair the previous failure by choosing a model in which each \(E_i\theta\) is true—e.g. a quotient term algebra modulo the congruence generated by \(E_i\theta\). Then \((E_i\theta \Rightarrow s_i\theta = t_i\theta)\) being true in that quotient looks more like equational consequence.
This does not yield a reduction to JCAQP\(_{\mathcal{T}(\mathcal{F})}\) for two reasons:
Thus “quotienting to make premises true” is incompatible with the JCAQP definition you use for invariants (and would also undermine the multi-sorted combination story, where a single shared base model matters).
What SREU needs is not the truth of \(E_i\theta\) as equations, but the ability to use them as rewrite/derivation axioms to show \(s_i\theta \approx t_i\theta\). To capture that inside a fixed model, one would need to internalize a relation like: \[ \mathrm{Derive}_E(s,t) \;\; \text{meaning “\(s=t\) is derivable from \(E\)”}. \]
However, once \(\mathrm{Derive}_E\) is part of the object language, the problem is no longer “JCAQP over \(\mathcal{T}(\mathcal{F})\) with equations as atoms” (the Herbrand constraint domain). It becomes abduction over a richer structure that includes (at least) a reachability / congruence-closure predicate parameterized by a set of equations.
There are ways to represent derivability (e.g. via explicit proof objects, or via a rewriting-step predicate plus transitive closure), but these generally push you beyond first-order equations over a term algebra and into:
So this “internalize derivability” route would be a reduction to a different abduction problem than the one in Section 4.2.4.1.
Your thesis’ statement that (a suitable) JAQP problem in first-order logic with equality is undecidable “because it is equivalent, by Herbrandization, to SREU” is consistent with the rigid-unification literature:
But that line of reasoning targets semantics (1), not fixed-model semantics (2). The reduction does not automatically transfer because JCAQP\(_{\mathcal{T}(\mathcal{F})}\) is not “provability in LJ\(^=\)”; it is “truth in a particular structure”, and (crucially) the antecedents must be satisfiable in that structure to avoid vacuity (the consistency condition in Def. 4.1).
To actually reduce SREU to your JCAQP\(_{\mathcal{T}(\mathcal{F})}\), one would need to address both gaps:
The analysis above suggests that doing both while staying inside the pure Herbrand constraint language is nontrivial and may be impossible—at least without enriching the constraint language with an explicit derivability/reachability predicate or changing the model away from the free term algebra.
This reduction attempt fails in a structurally informative way: it fails not due to a missing trick, but due to a semantic mismatch between:
So your thesis’ “open question” stance looks defensible: SREU-undecidability does not simply carry over “for free” to JCAQP\(_{\mathcal{T}(\mathcal{F})}\) as defined for constraint abduction in a model.
That said, none of the above is a proof of decidability or undecidability. To firm up the status, the next actionable step is to precisely fix (in the write-up) which variant of JCAQP is meant:
Given the full thesis PDF (incl. appendices) is available, the natural next step is to tighten Section 9 into explicit lemmas keyed to your formal definitions (in particular, to make the role of the consistency condition and the fixed-model semantics completely explicit in each failed encoding).
This subsection records the “academic curiosity” angle: even if SREU does not reduce cleanly, is full JCAQP\(_{\mathcal{T}(\mathcal{F})}\) nevertheless likely undecidable, and if so, does that automatically imply undecidability of existential-only JCA over \(\mathcal{T}(\mathcal{F})\)?
It helps to separate two statements that can easily get conflated:
Conjecture B does not follow from Conjecture A without an additional theorem showing that the quantifier-prefix discipline can be eliminated (or simulated) inside the same fixed model and the same answer language—exactly the kind of move that is delicate in Stafiniak (2015, Section 4.2.4.1).
Even under fixed-model semantics, full JCAQP has several “undecidability-friendly” ingredients:
However, the earlier sections show why importing SREU-hardness wholesale is not straightforward: classic rigid unification uses assumptions as derivability, while JCAQP\(_{\mathcal{T}(\mathcal{F})}\) insists that \(D_i \land A\) be satisfiable in the free term algebra and evaluates \((D_i \land A) \Rightarrow C_i\) by truth in that model.
So if Conjecture A is true, the proof likely needs a different source problem or a different encoding strategy than “rigid assumptions as false antecedents”.
To prove Conjecture A, a reduction must:
One plausible strategy template is:
Whether this can be done while keeping all antecedents satisfiable—and without smuggling in an implicit derivability predicate—is exactly the crux.
If a proof of Conjecture A uses the quantifier alternation in an essential way (for example, to express “for all contexts/steps/positions, some equality must hold”), then eliminating universals is nontrivial:
So, even if Conjecture A were settled as “undecidable”, Conjecture B could remain open (or require a separate reduction).
Existential-only JCA is still “second-order-ish” because the unknown \(A\) is a synthesized conjunction of equations, and jointness can force nonlocal interactions. So Conjecture B is not implausible; but its proof would likely require a source problem whose hardness does not rely on universal quantification/rigidity (e.g. a purely existentially quantified unification-like synthesis problem that can be phrased as “does there exist a conjunction of equations \(A\) such that …”).
At the moment, Section 9’s reduction attempt should be read as evidence that SREU is not an obvious source of such a proof for either conjecture under fixed-model semantics.
Łukasz Stafiniak. GADTs for Reconstruction of Invariants and Postconditions. PhD thesis, Institute of Computer Science, University of Wrocław, 2015.
Hubert Comon. “Disunification: a survey.” In Computational Logic: Essays in Honor of Alan Robinson, 1991.
Isil Dillig, Thomas Dillig, Boyang Li, Ken McMillan. “Inductive invariant generation via abductive inference.” OOPSLA 2013.
Anatoli Degtyarev, Andrei Voronkov. “Simultaneous rigid \(E\)-unification is undecidable.” CSL 1996.
Anatoli Degtyarev, Andrei Voronkov. “Reduction of Second-Order Unification to Simultaneous Rigid \(E\)-Unification.” UPMAIL Technical Report 109, 1995.
Michael Maher. “Herbrand constraint abduction.” LICS 2005.
Michael Maher, Ge Huang. “On computing constraint abduction answers.” LPAR 2008.
Martin Sulzmann, Tom Schrijvers, Peter J. Stuckey. “Type Inference for GADTs via Herbrand Constraint Abduction.”
Andrei Voronkov. “Simultaneous Rigid \(E\)-Unification and Other Decision Problems Related to the Herbrand Theorem.” Theoretical Computer Science 224, 1999.
Isil Dillig, Thomas Dillig, Boyang Li, Ken McMillan, Mooly Sagiv. “Synthesis of Circular Compositional Program Proofs via Abduction.” STTT, 2017.
Haniel Barbosa et al. “CVC4 1.7 release notes” (SyGuS abduction option).
cvc5 documentation: abducts (get-abduct,
get-abduct-next).
Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli. “Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis.” Automated Reasoning (LNCS), 2020.
Mnacho Echenim, Nicolas Peltier, Yanis Sellami. “Ilinva: Using Abduction to Generate Loop Invariants.” 2019.
Christopher Curry, Quang Loc Le. “Bi-Abduction for Shapes with Ordered Data.” 2020.