Persistent Horn composition with selective fact routing

1 October 2026. Written construction and proofs; finite corroboration, not proof-assistant verification. Novelty is unestablished.

The question and a decisive example

The preceding eager engine delivers a new boundary fact to every leaf. For m empty leaves, even a balanced composition therefore performs m-1 internal propagation events. But no rule in those leaves can use the fact. Can we retain it once and avoid visiting those leaves?

Yes. Store it in a global boundary set, and route it only toward leaves with a rule that reads that variable. Importantly, keep the fact even when no present rule reads it: joining a new fragment containing x implies y must still discover y if x was supplied earlier. This note proves a persistent construction with that behavior, and charges construction of its routing information.

1. Model, observations and representation

Use the explicit bounded-record model, normalized Horn3CNF programs and length-l bit names of persistent Horn closure. All operands belong to a typed family with the same boundary B and name length l >= 1. Validity of supplied boundary names is checked against its prepared trie in O(l+1) work per name. Preparing that trie is charged. No pointer equality, address arithmetic, hash oracle or unbounded scalar is available. An identifier is an immutable bit list; finite tuples are fixed-size record encodings.

Operations are preparation of leaves, arbitrary retained Join, positive Pin, SAT query, and boundary-membership/enumeration. Negative requirements can be prepared as false-headed rules and joined. There is no deletion, forgetting, renaming, unrestricted rule mutation or free materialization of an assignment. Private names are disjoint by unfolded leaf occurrence, including Join(h,h).

A public handle contains:

1. The unchanged exact syntax DAG, with Pin facts and occurrence binding.
2. A global boundary truth trie Z and enumeration list, plus a failure flag.
3. An immutable binary routing tree. A leaf contains a prepared Horn index and a persistent local closure state. An internal node contains two child roots. Every routing node also has a static support trie.

For leaf i define its input support S_i to be the boundary variables appearing in any rule body, including false-headed rules. Internal supports are unions of descendant supports. These are directly computable from rule syntax; no semantic equivalence or satisfiability oracle is used. Safe supersets also work, but can cause extra delivery. Omitting a true dependency is unsound in general.

A local state need not contain every fact in Z. Only the public handle exposes Z as the least forced boundary set. A subtree state is not an independently exportable handle; it may contain facts obtained from the surrounding context.

2. The dependency projection lemma

Write cl_P(S) for the least set of true variables of a consistent Horn program P under positive boundary seeds S, and let S_P contain all boundary body names. For any S subset B for which the closures are consistent,

cl_P(S) = cl_P(S intersect S_P) union S.

Consistency is also identical for these two seed choices.

Proof. Extra seeds in S outside S_P do not occur in a rule body. Thus they can neither enable a positive-headed rule nor fire a false-headed rule. Every rule derivation from S is already a derivation from S intersect S_P, except for the extra seed facts themselves. Conversely every derivation from the smaller seed set is a derivation from S. This proves the identity and the conflict claim. The statement concerns rule evaluation, not equality of the two boundary outputs.

Consequently a completed local state can omit globally true facts outside its input support without losing private consequences or failing to detect a local conflict. The global set must still retain those facts for public observations and future composition.

3. Algorithm

Leaf preparation builds its ordinary immutable rule indexes, its support trie, and closure under its own zero-body facts. Its initial Z consists of the resulting boundary facts. A failed leaf gives an absorbing failed handle.

A global operation has a pending stack. seed(v) checks the global truth trie; if v is new it inserts v, appends it to the enumeration list and pushes v. For each popped name v, perform a depth-first traversal of the router:

route(node, v):
    if v not in node.support: return the unchanged node
    if node is a leaf:
        resume its local Horn engine on v
        report its new boundary facts to the global seed routine
        return a leaf holding the new immutable state
    route its left child and then its right child on v
    return a new node holding the resulting children and the old support

Any local conflict ends the operation with failure. Newly reported global facts are queued; finish the current routing traversal before routing the next name. Do not recursively start a whole new global traversal inside a leaf call.

Pin: retain old Z and the old router, seed the supplied names, and drain. Even if a name is absent from the entire router support, it remains in Z.

Join: create the syntax Join, union the two static root support tries, and make a router node with the two old operand routers. Start the new global Z empty; enumerate and seed both old Z lists, then drain. Thus old facts are replayed against the new router even when they were irrelevant in their original operand. Replays to already informed leaves are harmless truth-trie lookups. Leaf indexes and counters are not merged or rebuilt. A failed operand makes the result failed immediately, while retaining the exact syntax Join; no valid closure cache is promised for failed handles.

The prototype returns lists recursively; the bounded-record implementation uses explicit immutable traversal frames and a global output/pending stack. Each reported name is consumed once by seed, rather than copying concatenated lists at each ancestor. After a child returns, replace its pointer in the pending frame; a completed frame constructs one immutable parent. This charges each descent, return and replacement once. It does not repeatedly copy an entire root path for every primitive leaf step.

4. Correctness theorem

For every finite sequence of valid preparations, joins and positive pins, including branches from old handles, this construction returns exact satisfiability and least-boundary answers, preserves old versions and exact syntax, and terminates. It does not preserve arbitrary observations of the old eager solver’s internal graph.

Maintain the following quiescent invariant for each successful public handle: Z is its least boundary set, and local engine i is the completed closure of its fixed P_i under Z intersect S_i. Its marked boundary facts are included in Z. Positive Pin facts in the syntax contribute to global seeds, not to hidden unconditional assumptions of each P_i. The local full assignment may omit boundary variables outside S_i, exactly as the lemma permits.

Proof by induction on operations. Leaf preparation establishes the invariant: feeding back boundary facts already derived by that leaf changes no closure. During Pin or Join, every retained or supplied global fact is a consequence of the new whole formula. Old local facts remain consequences because only positive facts or conjuncts are added. Every new local derivation is consequently sound, and a fired false-headed rule proves inconsistency.

There are finitely many boundary variables; each enters the new global pending stack at most once per operation. Every routing traversal is finite. Each local Horn extension terminates by its truth/counter invariant. Thus draining ends. At successful termination, each leaf has received every globally true fact in its support: routing visits all such leaves, both for replayed Join facts and for newly discovered facts. It is therefore closed under precisely the required inputs. By soundness and the preceding local closure theorem its state is cl_Pi(Z intersect S_i).

Combine Z with all the local private assignments. Consider any clause. Its true boundary body variables belong to S_i and have reached that leaf; its private body variables are local. Local closure therefore satisfies the head or would have reported conflict. So the combined assignment is a model of every leaf and every supplied Pin. All of its facts were soundly derived, making it the least model. In particular Z is exact. Private occurrence namespaces are separate, so this model union introduces no extra identifications.

Path copying preserves every input handle. If a router is shared twice, routing updates each occurrence independently; the same immutable starting state may be reused, but no state change in one occurrence mutates the other. This completes the induction for arbitrary retained histories, not only one growing version.

5. Charged cost, including routing construction

Build a leaf support by inserting its boundary body names into a binary trie; this fits the existing O(N_i(l+1)) leaf preparation bound. At Join, merge the root support tries structurally: if one is missing return the other; otherwise recurse on the two corresponding child pairs and construct their union node. No equality test on non-null pointers is used. Let W count all visited pairs in this merge, including terminal cases. Both work and fresh records are O(1+W). In particular W can be large even when no new boundary fact results. It is bounded by a constant times the total nodes of the two input tries, not by the number of leaf rule indexes. Subsequent Pins reuse these static tries.

For one operation define:

• k: supplied Pin names, including repetitions;
• z: boundary names enumerated from operand Z lists for Join, with repetitions;
• V: routing-node visits across all popped global facts, including rejected nodes;
• A: newly marked local variables over all leaf occurrences;
• E: local antecedent-occurrence visits;
• W: support-trie union visits (zero for Pin).

Then work and fresh records are bounded by

O(1 + W + (z+k+V+A+E)(l+1)).

Proof. Trie membership, insertion, local truth/counter operations and boundary validation take O(l+1) per charged name/event. Every popped global name triggers at least one router visit, so V pays its scheduling. New boundary reports are charged to A; initial replay is charged to z. There are O(V) traversal frames and parent reconstructions. The preceding leaf theorem pays its remaining local work by A+E and by delivered seeds, the latter bounded by V. The union work was charged separately. These arguments also upper-bound early failure.

For a successful fixed-tree Pin, let I_v count internal routing occurrences whose support contains v. If Delta = Z’ minus Z, the specified traversal has

V = sum over v in Delta of (1 + 2 I_v).

Each name visits the root once; each visited subscribing internal node makes exactly two child calls. A subscribing descendant always has subscribing ancestors, so none is skipped. This proves the identity. If t_v leaves subscribe to v and height is h, then I_v <= h*t_v, by covering subscribing internal nodes with root-to-subscriber paths. Hence sparse dependencies can benefit from balanced routing, although building or changing support summaries remains charged. Unlike the earlier rotations, a rotation here needs a new support union for its newly grouped subtree; it is not automatically constant-cost.

If all leaves omit a new name from their bodies, a Pin routes it once and never calls a leaf engine. For k such names the bound is O((1+k)(l+1)), independent of the number of leaf occurrences. Conversely, if every leaf subscribes to v, all router nodes are visited. No general improvement over dense propagation is claimed. Along a fixed-tree positive lineage each local variable is marked at most once and each local antecedent occurrence processed at most once; Join replay and independent branches have their separately charged budgets.

SAT is available from the handle flag. Boundary membership takes O(l+1), and enumeration is charged by output length. Queries do not discharge hidden pending work: every returned successful handle is fully drained under the new invariant.

6. Meaningful failures and checks

Dropping irrelevant facts from global Z loses a later join interaction: Pin(empty,x) joined with {x implies y} must force y. The router skips delivery to the empty leaf but keeps x globally. A false-headed rule x implies false must subscribe just like a positive-headed rule. An unseeded cycle does not justify its own facts. Private chains and duplicate leaf occurrences must retain their separate local states. The executable tests include these concerns through random examples and explicit retained-handle, cross-fragment and conflict cases.

Checker and output compare 161 random joins and 260 random pins against a truth-assignment oracle, using three-variable leaves, two boundary variables, and at most five leaf occurrences for the random cases. A separate 64-empty-leaf example takes one router visit and zero leaf deliveries, then a later join correctly derives y. This finite semantic prototype uses host sets for supports and recursive list concatenation; it does not implement or certify the pointer-cost construction. The quantified bounds rest on the written trie/frame argument above. No proof assistant or complete compiler extraction was run.

7. Classical theory and research assessment

Dependency-directed fixed-point scheduling is established mathematics. Apt’s The Rough Guide to Constraint Propagation (1999), Theorem 1 and section 3, gives generic iteration, component dependency schemes, and scheduling by changed components. We use that as the conceptual framework; our Horn proof separately establishes exact satisfiability, rather than assuming that arbitrary constraint propagation decides satisfiability. The local engine is classical Horn forward chaining, and immutable trie/path copying is standard persistence. The additional argument here specifies retained Join, global fact retention, projected local states and the charged support-routing implementation. An original fixed-point calculus or novel Horn algorithm is not established.

The application now distinguishes four quantities: exact contextual information, communication across a boundary, local derivation work, and dependency-routing work. The preceding SAT note studies the first two; the persistent constructions make the latter two explicit. This is a useful application of the foundations, but does not yet characterize all behaviors with bounded local realizations. In particular, improving a scheduler is not itself a new language-class boundary. Further routine Horn scheduler refinements should not become the main program.

The next foundational checkpoint is to audit and formalize the strongest common semantic statement, equality of boundary relations versus all allowed future contexts, keeping it separate from the independent-fragment access lower bound. That proof should make the allowed contexts, private renaming and observations explicit before any broader characterization is proposed.

The existing bounded-record transfer applies to the local steps of this construction when their execution is scheduled and paid for. This note does not establish a new unpadded real-time scaffold language or an equal-cost ordinary TM simulation. Syntax-size, unfolded-size and name-length charges survive transfer; scaffold-to-PEG language transfer still requires reversal.