Persistent Horn joins without rebuilding leaf indexes

1 October 2026. Written construction; finite corroboration; novelty unestablished.

Suppose a retained fragment asserts x and another contains x -> y. Merely combining their indexes and waiting for a newly inserted fact misses y: x was already processed before the join. This is a failure of that update scheme, not an impossibility of incremental composition.

We instead leave every prepared leaf index intact. A composite stores two child solver states and its own set of forced boundary variables. Joining two retained composites introduces one more such node, then propagates boundary facts through the existing structure. The cost counts this propagation. It need not revisit every rule or copy the operands’ indexes.

1. Values and observations

Fix a common finite boundary B with b variables, represented by l-bit names, l >= 1. The name width is a parameter of a family of handles, not an unbounded scalar register. All leaves have the same declared boundary; their private variables are local. A leaf is a normalized finite Horn 3CNF program with n variables and p antecedent occurrences, prepared by the persistent closure construction. Preparation and its O(N(l+1)) cost remain charged once per supplied leaf.

Values are finite terms generated by

Leaf(P), Join(T,U), Pin(T,S),

where S is a finite list of positive boundary facts. Join identifies exactly B and alpha-renames all private variables of its two operands apart. Pin conjoins the listed unit clauses. Terms can be stored as persistent DAGs, but their interpretation is by occurrences in the unfolded term. In Join(h,h), the two private namespaces remain separate even if both pointers initially share all their stored records. No address identity is observed.

The public operations are prepare, Join, Pin and satisfiability query. Operations are typed by the common declared boundary and name width. Pin names are checked against its prepared boundary map in O(l+1) each; invalid names are rejected. No uncharged comparison of arbitrarily different boundary lists is included in a Join. Query returns an exact Boolean after the operation finishes. A successful state also exposes its least model’s boundary set by membership or enumeration. The formulas themselves remain in a separate immutable syntax DAG. Solver updates do not overwrite that DAG or pretend derived facts were original clauses. Retained handles can be queried or used in later operations.

This is arbitrary retained-handle Join within the fixed-boundary Horn family. It does not include Forget, boundary renaming, negative pin insertion as a primitive update, retraction or arbitrary mutation of a leaf program. A negative unit clause can be supplied as a prepared leaf and joined normally.

2. The semantic contract needed for reuse

For a term T and positive boundary assumptions S, let c_T(S) be the boundary of the least model of T with S true, or a distinguished failure value if no model exists. A solver state for (T,S) represents that conditional computation. Extending it by Q must produce a state for (T,S union Q), preserving the old state, and return exactly the newly true boundary names unless it fails.

A public handle for Pin(T,S) can export that state: its assumptions are now part of its value. In contrast, a temporary conditional state for (T,S) must not be exported as an unconditional state for T. For example T=(x -> y) is compatible with (y -> false), but T under temporary assumption x is not. Forgetting the scope of x would change the satisfiability answer.

Within a composite, assumptions sent to a child are justified by the parent computation. They need not follow from that child in isolation. This is why internal conditioned child states are not independently exported as handles for their original syntax. The parent retains its own exact syntax and owns the conditional-state invariant.

Horn least-model semantics gives two facts used below. All derived positive facts hold in every model extending the assumptions. Also, after adding positive assumptions, previously derived facts stay true. A closed child state can consequently be resumed without invalidating its leaf counters.

3. Composite representation and algorithm

A consistent quiescent composite has child states L,R and a cached boundary set Z. Its invariant is that both children have boundary set Z and jointly represent the least model under the node’s accumulated assumptions. Store Z as a persistent binary trie plus an immutable list of its true names. Failed states expose only failure and remain absorbing under further joins/pins.

The following procedure updates a composite. Its incoming names may already be true. extend on a leaf is the previous persistent counter engine; on an internal node it is this same procedure. Each child call finishes before the next one. Child-returned deltas contain only newly true boundary names.

seed(v):
    if v is absent from Z:
        insert v into Z and its true-name list
        push v onto pending
        append v to this call's returned delta

extend-composite(Q):
    seed every name in Q
    while pending is nonempty:
        pop v
        (L, DL) := extend(L, [v]); fail if L failed
        seed every name in DL
        (R, DR) := extend(R, [v]); fail if R failed
        seed every name in DR
    return new composite and returned delta

If Q contains only names already in the old Z, this returns the unchanged solver state after membership checks. During draining, Z may temporarily be larger than one child’s boundary set; the quiescent equality is restored only when pending is empty. Conflating these two invariants would be an error.

To Join two consistent public handles, create a new composite with those solver states, empty Z and empty pending; call seed on every name in both children’s cached true-name lists and drain. If either child is inconsistent, return an inconsistent handle immediately. Preserve the operands’ syntax in a new Join record even when the query result is already known. A Pin operation similarly stores a syntax record and applies positive extension to the solver.

No leaf receives a new rule. A fact that was already true in one operand is explicitly delivered to the other operand, whose truth lookup decides whether it is new there. This avoids both uninitialized new-rule counters and replay of already processed facts against old counters.

4. Correctness theorem

Theorem 1. For every finite well-formed term over prepared Horn leaves, the algorithm terminates, computes its exact satisfiability and (if consistent) least boundary model, and supports persistent extension and reuse. Leaf indexes are never rebuilt or modified by Join or Pin. All old syntax and solver records are preserved.

Proof. Induct on the composition tree, counting occurrences if the physical representation shares nodes. Leaves satisfy the prior closure theorem. For an internal node, every seeded name is either an incoming assumption or a fact returned by a child under already justified assumptions. Induction on the sequence of these derivations shows that every name in Z holds in every model of the parent’s formula and assumptions. Child failure therefore proves parent inconsistency.

A name enters a given node’s pending list at most once during this monotone update. There are at most b names. Recursive calls descend to a strict child, so induction on height proves termination even for cyclic implication rules inside leaves. No fairness or infinite scheduling premise is needed.

At the end, every name in Z has been sent to both children. Every boundary fact returned by either child was inserted into Z, so the two quiescent child boundaries equal Z. Their private-variable sets are disjoint by occurrence. Their models therefore combine into a model of the parent’s conjunction. All its derived variables were forced by the derivation invariant; induction on child semantics makes the combined model least. This also proves the conditional extension contract and the initial Join case, which starts from the two valid child models and explicitly synchronizes their boundary facts.

All changes use persistent maps and fresh fixed-size records. Shared child roots in Join(h,h) are initially legitimate snapshots. Updating one child produces a new root in that position only; the other occurrence keeps its own state until its own call. Sharing immutable base records never identifies the private variables in the semantic decoding. A separate unchanged syntax DAG preserves exact constructor values rather than only satisfiability. ∎

5. Charged bound, including tree propagation

Let an operation start with already prepared, quiescent handles. Define:

• z: names enumerated from the two operand root caches when creating a Join (at most 2b); zero for Pin;
• k: supplied seed-list length for Pin; zero for Join;
• D: total pending-name pops at internal composition-node occurrences during this operation, including the newly created Join root;
• A: newly marked leaf variables, counted separately at different occurrences;
• E: leaf antecedent occurrences processed during this operation.

Theorem 2. With opaque pointers, finite labels and immutable binary records, the operation takes time and fresh records bounded by

$$O\big((1+z+k+D+A+E)(l+1)\big).$$

The implied constant is independent of leaf sizes, tree height, boundary size and version history. This is a construction bound, not an optimum or a bound solely in the number of changed output facts.

Proof. Trie membership, insertion and each leaf name/counter action cost O(l+1). Every internal pending pop makes two child calls. Returning deltas costs one list action per returned name; each such name is charged either to a leaf activation or an internal insertion/pending event. Duplicate seed checks are charged to incoming names, initial z+k, or those returns. A failed call has at most the same work before its failure.

Use an explicit immutable continuation stack for descent: a frame holds the parent’s fixed-size local state, the chosen child position and the continuation phase. Push/pop and rebuilding a parent record cost O(1) per child call. In particular, do not independently copy a complete root-to-leaf path for each primitive leaf update. The suspended frame retains the path while the child call finishes. The number of entered internal routines is bounded by the number of child calls plus one, hence O(D+1). The implementation uses a fixed number of registers and finite tags; unbounded depth lives in the frame stack. Combine these charges with the leaf theorem. ∎

For one fixed unfolded composition tree with I internal occurrences, along a single positive-extension lineage each existing internal node processes a boundary name at most once after its initial synchronization. Thus D <= bI for those lifetime events; analogous totals are A <= sum n_leaf and E <= sum p_leaf. Creating additional Join roots adds their synchronization charges. Branches and repeated occurrences have separate budgets. A compact DAG may have exponentially many unfolded occurrences: no polynomial bound in physical DAG size is asserted.

Examples. If both operands have empty least boundary sets and are consistent, Join does O(1) work: z=D=A=E=0, even if their private indexes are large. For a chain of composite nodes, delivering one new boundary variable may enter every level even when only one new boundary fact is observed at the root. The D term records that traversal. This explains the benefit and the limit of sharing: index reuse does not make communication through a deep stored structure free.

6. Failed alternatives and scope

1. Union indexes and do no replay. Fact x in one operand and x -> y in the other leave y unmarked. The missing work is a cross-operand notification.
2. Add counters with the same rule ID. For (x and z) -> y, two independently conditioned copies where only x is true each have counter one. Adding the counters spuriously fires y although z is false. IDs are local, and the two semantic rule occurrences are distinct.
3. Take the maximum counter and do no replay. For the same two-premise rule, one operand with x true and another with z true each has counter one; the maximum misses the conclusion forced after their boundary facts combine.
4. Reuse temporary assumptions as facts of an exported value. The example in Section 2 changes a satisfiable conjunction into a reported contradiction.

These refute those schemes. They do not prove a representation-independent obstruction to faster Join, nor a lower bound for every representation of Horn SAT. The successful construction keeps leaf rule sets fixed while the composite formula grows; it does not magically retrofit a single counter array to an arbitrary new program.

The finite-rule implementation uses the instruction calculus from clocked Horn transfer. Each primitive has bounded access/allocation, but one Join takes the charged number of primitives above. There is no new constant-clock input-language theorem here. A transfer to PEGs would still reverse the chosen scaffold language and retain its actual clocks.

7. Established ingredients and verification

Least-fixed-point composition is classical. Cousot and Cousot’s constructive study of closure operators provides the lattice-theoretic setting for composing closure conditions. The finite Horn argument above is proved directly; no transfinite convergence or stronger imported complexity bound is needed. Forward-chaining counters come from Dowling and Gallier. Persistent path copying and the fixed-size record encoding are the previously credited ingredients of our leaf construction.

The additional statement here is the persistent composite-state invariant and its explicit accounting for propagation through an occurrence tree. It extends the fixed-pair result to arbitrary retained Join terms without rebuilding leaf indexes. Novelty of that combination is unestablished; it should be assessed against incremental constraint/dataflow solvers before being called a new algorithmic result.

The checker and output compare finite retained Join/Pin histories against independent truth-assignment semantics, check old snapshots, and exhibit the failed counter combinations. Its high-level recursive sets are a semantic reference, not a verified compiler or a measured pointer implementation. Written proofs supply the unbounded correctness and cost argument. No new Lean verification is claimed.

Next decisive question: can the D term be controlled by a maintained balanced composition representation without losing exact syntax, private-variable separation or the reusable conditional-state invariant? First distinguish a bound in unfolded occurrences from a bound in physical DAG size; balancing alone does not remove duplicate occurrences or cross-branch propagation.