Let \(Q\) quantify all free variables in the instance. An answer \(\exists\bar\beta: A\) (conjunction of equations) must satisfy:
Maher shows a simple JCA instance whose set of answers cannot be captured by any single
SCA instance (even over Herbrand constraints). This indicates that jointness is a genuine source of complexity and cannot be eliminated by “solve each implication separately and conjoin.”
For SCA over Herbrand constraints, recognizing maximally general or fully maximal answers is co-NP complete, even though checking that a candidate is an answer is easy (linear-time unification). This suggests that even the shape of the answer space is algorithmically hard to control, which partly explains why JCA/JCAQP decision status remains open.
node(tag, args) or
pair) by encoding symbols as ground terms (strings over a
fixed alphabet). This removes the “growing signature” concern.From standard definitions (e.g., the MSR/Veanes survey), a rigid
equation is written E |- s ≈ t with E a
finite set of equations. An SREU instance is a finite set
{ E_i |- s_i ≈ t_i }_i. A substitution θ is a
solution if:
E_i θ and (s_i ≈ t_i) θ are
ground, andE_i θ entails
s_i θ ≈ t_i θ in equational logic (i.e., s_i θ
and t_i θ are in the congruence closure generated by the
ground equations E_i θ).Thus SREU relies on derivability under axioms (ground equations as rewrite/congruence axioms), not on truth in the free term algebra.
Let D be a conjunction of equations in the free term
algebra. If D is satisfiable and σ is an mgu
of D, then for any terms s,t:
T(F) |= D -> (s ≈ t) iff
sσ and tσ are syntactically identical.So entailment in the free term algebra collapses to unification
w.r.t. D; it does not
use D as rewrite axioms in the sense of equational logic
with a quotient.
Given SREU instance: finite family \(E_i \vdash s_i \approx t_i\). Try to encode:
Then relevance says: \(\mathcal{T}(\mathcal{F}) \models E_i \land A \Rightarrow s_i \approx t_i\).
Conclusion: the direct SREU reduction collapses because rigid derivability is not the same as truth in \(\mathcal{T}(\mathcal{F})\).
R_Σ(t) that forces
\(t\) to be ground (in LJ\(^=\)), highlighting how rigid derivability
can express properties far beyond free-term entailment.These points reinforce: SREU’s power comes from proof-theoretic entailment with equality, not model-theoretic truth in \(\mathcal{T}(\mathcal{F})\).
Again, this is a further illustration that SREU encodes properties (like groundness of higher-order instantiations) that are not directly expressible with finite conjunctions of equations evaluated in \(\mathcal{T}(\mathcal{F})\).
Idea: add equations to encode a “proof object” witnessing that \(s_i\theta\) rewrites to \(t_i\theta\) using equations in \(E_i\theta\).
Obstacle:
step or proof does not
help: in \(\mathcal{T}(\mathcal{F})\),
they are uninterpreted constructors, so equations cannot enforce the
semantics of rewriting.Conclusion: encoding derivability requires extending the language/model beyond pure Herbrand equations. That leaves the JCAQP setting.
Idea: let the abduced answer \(A\) assert the existence of a term encoding a full computation (e.g., a list of configurations). Use implication constraints to enforce local transitions.
Obstacle:
Conclusion: the equational language is too weak to express “every adjacent pair is a valid step” without additional predicates or axioms.
Idea: view abduced \(A\) as an unknown conjunction of equations, i.e., a partial substitution, and encode a known undecidable unification-style problem.
Issues:
Conclusion: I do not yet see a faithful encoding of second-order or semi-unification into JCAQP with only equations.
Maher’s Herbrand Constraint Abduction explicitly notes that, despite semi-unification being undecidable, “the status of the JCA decision problem is unknown (though it appears more tractable).” This supports the interpretation that undecidability of JCA (let alone JCAQP over \(\mathcal{T}(\mathcal{F})\)) is not settled by the classical reductions and remains open.
If the answer \(A\) fully pins down variables via equations (i.e., encodes a substitution), then each implication \(D_i \land A \Rightarrow C_i\) becomes “ground-truth”:
either \(D_i \land A\) is inconsistent or, when consistent, the fixed substitution makes \(C_i\) syntactically true. This suggests a (very rough) idea that existence of A
could reduce to checking whether there is a substitution compatible with all implications and with the dependency/no-escaping constraints. That looks closer to unification with dependency restrictions than to classic rigid-derivability problems.
However:
I do not have a precise reduction either way; this is only a possible route if one tries to prove decidability rather than undecidability.
With a prefix like \(\forall x.\exists
y\), an equation in \(A\) of the
form y = t(x, p̄) makes \(y\) a definable function
of \(x\) (with parameters \(p̄\)). This resembles higher-order
unification where function variables are restricted to first-order
definable functions (a.k.a. context terms / patterns).
If JCAQP effectively only allows such “pattern” dependencies, the problem could be closer to higher-order pattern unification (decidable) rather than full second-order unification (undecidable). This is not a proof, but it suggests that undecidability is not automatic even with quantifier alternation.
In the free term algebra, a satisfiable conjunction of equations \(E\) induces a single most general unifier \(\sigma\) (up to renaming). Entailment reduces to checking syntactic identity after \(\sigma\). Thus any implication of the form \(E \Rightarrow s \approx t\) can only constrain finitely many positions—those reachable through the finitely many equations in \(E\) and the two terms \(s,t\).
This suggests a meta-lemma: there is no way, using only finitely many equations, to enforce a local “transition” property at every depth of a recursively nested term, because every such enforcement would require a definable traversal/predicate not present in pure equational logic.
This is not formalized, but it explains why the TM/PCP “trace term” idea repeatedly stalls.