Horn composition with linear clock padding

1 October 2026. Written proof and finite specification checks. The construction uses classical Horn propagation, immutable path copying and the reviewed scaffold compiler. Novelty is unestablished.

Overview

A Horn program consists of facts and rules such as p, p -> q, and q -> false. The first two rules are satisfiable, but joining them with the third creates a contradiction. Forward chaining detects this efficiently once the variables, rules, and incidence lists have been indexed. The issue here is who pays to build those indexes when the program itself arrives as input.

This note makes that work visible. The recognizer reads an ordinary encoded pair of Horn programs, a separator, exactly $C(|x|+1)$ clock symbols, and a finish marker. During the clock block it reverses the stored input, validates names, builds immutable trie indexes, and runs Horn propagation. Some fixed constant $C$ suffices for every valid or malformed description. The reviewed compiler then gives a scaffolding automaton, and hence a PEG for the reversed padded language.

The result shows that this explicit Horn composition can be scheduled with linear padding in the total encoded length. It does not remove the padding, give a scaffold for the raw unpadded descriptions, or solve arbitrary joins of previously retained Horn fragments. Horn propagation, path copying, padding, and the scaffold transfer are established ingredients; novelty of this specialization is not established.

1. An explicit finite alphabet and input language

Use data alphabet

{u, :, B, F, G, D, R, E, ;, 0, 1, a, b, c, d, +, -}.

The fresh symbols #, t and ! are separator, clock and finish. Case matters. A valid description x has the following grammar, interpreted with a common name length l determined by its initial nonempty unary header:

u^l : B (key ;)*
F D (key ;)* R rule*
G D (key ;)* R rule* E

Here key is exactly l bits. The B list declares shared boundary variables. The D list for each side declares that side’s private variables. The R list contains its rules. A rule has syntax

ruleID arity head bodyKey_1 ... bodyKey_a ;

The four arity symbols a,b,c,d mean 0,1,2,3 respectively. A head is either - (false) or +key. A variable-headed rule must have arity at most two. Rule IDs use the same l-bit width but a separate namespace on each side.

Validity also requires: no repeated declaration in B or either D list; a private declaration cannot duplicate a B name; rule IDs are unique within each side; every rule name is declared in B or that side’s D list; body names are distinct; a variable head is not in its body. These last two restrictions make the representation normalized. Ill-formed descriptions are rejected, not silently normalized. Private bit strings may coincide across the sides; they remain different variables. Boundary declarations are implicit variable declarations in both programs. The empty program pair, with positive l and empty lists, is valid and satisfiable. The empty description is invalid.

Let H be the set of valid descriptions whose two programs have a satisfying joint assignment when exactly their declared boundary variables are shared. For any positive integer C, define

$$e_C(x)=x\#t^{C(|x|+1)}!,\qquad L_C=\{e_C(x):x\in H\}.$$

This is a language over one fixed finite alphabet, with unbounded variable count, rule count and name width. C is fixed for the recognizer, not supplied as part of an instance or advice.

2. A small source instruction calculus

A program has finite control, a fixed finite set of pointer registers, and immutable binary records with labels in a fixed finite alphabet. Null is explicitly distinguishable from a record. Its primitive instructions are:

Every target and guard uses the pre-instruction registers. No equality test between two nonnull pointers is available. Constants are finite labels; unbounded data, including names, live in linked records. Finite tuples use fixed binary layouts. Finite flags and arities can live in control or record labels. An instruction sees radius at most one, allocates at most one record, and never modifies a record.

Straight-line combinations expand into several primitives. A finite flowchart with pointer-controlled loops is therefore a finite program in this calculus. All loops below iterate a stored list, a key, an explicit path stack or a worklist. None requires an unbounded integer register. The subroutine call graph is acyclic; inlining call sites leaves a finite flowchart. Trie recursion is replaced by the explicit path stack described next.

3. Loader and algorithm certificate

The certificate below describes a finite expansion, rather than asserting that a unit-cost map implementation exists. Register names in each row stand for a fixed number of registers, independent of the instance. Fixed tuples and the maximum of three body positions are expanded syntactically.

A trie branch has two children and a branch label. A leaf has a payload pointer. Descent frames can be two binary cells: one labeled by the direction and pointing to the saved old node, followed by a list cell pointing to that frame and its predecessor. These are two separate new instructions. During ascent, move a saved old node to a register before reading its sibling field. Thus no frame operation hides a two-edge observation in one primitive. A payload of bounded tuple length is similarly traversed in several primitives. Each newly allocated node points only to current registers.

The loader reads the entire grammar in order. It creates a boundary map/list, then builds F and G in separate variable and rule maps. Populate each variable map from the B list before its D list. On a D declaration, test the variable map to exclude duplicate private names and boundary collisions. On a rule, check all body/head names against that side’s variable map and its ID against the rule map. Even if an earlier empty negative clause makes the formula inconsistent, finish syntax/identifier validation before selecting the final answer. Store the conflict flag and skip propagation if desired. Any detected syntax error halts with no; truncated input is detected by a null cursor. Trailing symbols after E also halt with no.

After validation and index construction, retain the original index roots, initialize each side’s zero-body rules and run the two notification stacks from the preceding theorem. Preserve independent base versions by copying their fixed tuples into immutable version records before delivering messages. Only a fixed number of such handles is needed for this one-composition language.

Lemma 1 (linear primitive bound). There is a finite program P_H in the above calculus, starting with only an input-list register, that decides H and halts within C_H(M+1) primitive instructions on every description of length M, for some fixed effectively obtainable integer C_H.

Proof. The table gives finite expansions with a uniform constant per visited cell. Grammar phases and body positions are finite control. Read-key uses a copy of the unary ruler pointer, not a scalar length. On valid input, all declaration and rule operations make only constantly many length-l passes per syntactic field. Each such field contributes l bits to M. Copying the boundary declarations into both local maps only multiplies this charge by two. The unary ruler is itself part of M.

There are n_F+n_G variable activations, at most p_F+p_G incidence visits and at most 2b notifications. Each costs O(l+1). Variable declarations, rule bodies and boundary declarations already contribute their corresponding key lengths to M. Hence all propagation costs are O(M+1), including an input with no rules. The previous least-model proof supplies semantic correctness.

For invalid input, each complete field pays for its own validation. A final truncated or malformed key reads at most its present bits plus one failure check; it does not finish traversing the ruler after failure. An arity or undeclared-name error rejects after the corresponding bounded work. No semantic propagation occurs before all validation succeeds. Thus malformed input also has the linear bound. Multiplying the finite routine-expansion constants by these constant visit multiplicities yields an effective C_H. This is a written construction proof, not an extracted decimal instruction bound. An assembled instruction listing and a smallest C_H are not claimed. ∎

4. Exact clock padding and scaffold transfer

Lemma 2 (buffer-and-clock lifting). Let P be any program in the above calculus deciding a language J from a forward input list in at most c(M+1) primitive steps on all inputs. Then for some fixed integer C, the language {x#t^{C(|x|+1)}!: x in J} has a finite-rule immutable source with binary records, A=1, radius r=1 and a fixed number s of roots, from empty initialization.

Proof. While reading data symbols, allocate one cell carrying the symbol and pointing to the previous input head. Input order is reversed in this list. On #, copy the head into the reversal cursor, and allocate one extra sentinel whose next pointer is that head. A separate fuel root points to this sentinel. The fuel list has exactly M+1 nodes and shares the untouched reverse input. A finite phase register initially holds C. No arithmetic on M is performed.

Each t runs one primitive of list reversal followed by P. Once P halts, retain its yes/no flag and idle. Independently on the same t, decrement the finite phase; when it reaches one, advance the fuel root one edge and reset the phase to C. Combining this fixed root movement with a P primitive adds no allocation. Reject a clock when fuel is already null. A ! accepts exactly if fuel is null and P has halted yes. An early ! rejects. Any data symbol after #, any separator repetition, and any symbol after ! reject. Before ! all states are nonaccepting, including empty input. A clock before # also rejects.

The reversal routine costs at most a fixed multiple of M+1. Choose C to cover it, the runner’s fixed setup and c. Then exactly C(M+1) clocks suffice and are required by fuel consumption. Reversal never mutates the input cells shared with fuel. Each transition reads root labels/one-edge fields, creates at most one record, and changes only finitely many roots and finite control. There is no input-dependent initial graph. ∎

Theorem 3 (linearly padded Horn recognition). For some fixed positive integer C, L_C is recognized by a scaffolding automaton of finite degree

$$d=\max(1,s+2),\qquad k=2,$$

where s is the fixed register count of the expanded loader, Horn program and clock wrapper. Its decoded source run preserves the immutable records and retained handles. Its language is exactly L_C, with no erasure of clocks. A PEG recognizes exactly

$$L_C^R=\{!t^{C(|x|+1)}\#x^R:x\in H\}.$$

Proof. Apply Lemmas 1 and 2, then the reviewed simultaneous-record compiler with q=2,A=1,r=1. All guards factor through bounded rooted unfoldings; null is explicit and nonnull identity is never tested. The initial heap is empty. Old endpoints are roots or one-edge children and new endpoints are the single fresh slot. The compiler preserves prefix acceptance and decoded source behavior. The native observation repair gives distance r+1=2. The scaffold-to-PEG sufficient direction introduces exactly one reversal. ∎

The register count and C are constants independent of n,m,b,l,M. This is an existence construction with a syntactic expansion procedure, not a claim to have emitted a minimized scaffold, a decimal degree, or a concrete PEG file.

5. Why the clocks cannot be quietly erased

The map e_C is a linear-size encoding, but deleting its clocks is a different language transformation. The theorem does not say that raw H has a scaffold or that a strict real-time ordinary TM recognizes L_C. Linked heap navigation is the primitive of the source calculus; it is not one tape-head move. The ordinary-TM-to-scaffold theorem goes in the other direction and does not supply a reverse simulation with the same time bound.

A simple counterexample to a tempting inference is a program that ignores its input and idles for M squared steps before answering yes. The same clock wrapper with C(M+1) clocks fails on sufficiently large inputs. Totality alone is insufficient for linear clock padding. A runtime bound in the specified primitive model, checked before transfer, is essential.

The input loader above consumes ordinary symbols while storing them, then works on the explicit t symbols. It therefore does not establish worst-case constant work per Horn clause or real-time answers at declaration boundaries. It preserves a one-composition execution; the stronger retained-version extension interface remains in the preceding data-structure theorem.

6. Literature and scope of assurance

Loff, Moreira and Reis, The computational power of parsing expression grammars, Section 4.3, supply the scaffold/PEG characterization. Their Section 5.1 already uses padding for computational universality and obtains a P-complete PEG language. Padding and powerful clocked PEG examples are established ideas. Our narrow addition is a linear budget for this explicit Horn-pair encoding, together with a fixed-initialization loader and an immutable-source certificate. Novelty of this specialization is unestablished.

The closure engine is classical Horn forward chaining, as credited to Dowling and Gallier in the preceding note. Immutable tries use elementary path copying, not an unproved constant-time mutable array or a blanket application of a persistence conversion theorem. The Lab’s imported compiler contract is recorded in Foundational contracts, Section 3, and its timing and reversal scope in review run 09.

The finite checker and output exercise the concrete grammar, malformed-input cases, private-name separation, Horn answers against truth assignments, and the exact fuel wrapper on small primitive runners. They do not extract P_H, compute C_H, verify its full primitive schedule, or prove the infinite statements. The proofs here are written mathematical arguments; there is no new Lean verification.

This closes the saved loader/schedule question at the written-construction level. The next substantive question is whether arbitrary retained Horn fragments can be joined without rebuilding their indexes, with an explicit cost bound in changed information rather than total operand size. Do not infer this from monotone seed extension: adding rules changes incidence lists and the meaning of existing propagation counters.