Binary Name Dictionary Construction

Abstract

Occurrence-driven construction writes the rightmost-deduplicated dictionary.

Theorem 1.1 (Actual lookup, insertion and a quadratic charged clock).

$$\forall names\in \mathrm{List}\left(\mathrm{List}\left(Bool\right)\right),\forall frame\in \mathrm{List}\left(Bool\right),\forall dimension\in \mathrm{List}\left(Bool\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(builderMachine\right),\mathrm{buildCfg}\left(start,nil,nil,nil,\mathrm{dictionaryStream}\left(\mathrm{reverse}\left(names\right)\right),dimension,frame,false\right),\mathrm{some}\left(\mathrm{builderCfg}\left(none,((none,none,true),none,false),\mathrm{dictionaryStacks}\left(\mathrm{compareStacks}\left(nil,nil,nil,nil,nil,frame\right),\mathrm{dictionaryStream}\left(\mathrm{dedup}\left(names\right)\right),nil,nil\right),nil,\mathrm{append}\left(\mathrm{replicate}\left(\mathrm{length}\left(\mathrm{dedup}\left(names\right)\right),true\right),dimension\right)\right)\right),20\cdot \mathrm{pow}\left(\mathrm{length}\left(\mathrm{dictionaryStream}\left(names\right)\right)+1,2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Computability/BinaryNameDeduplication.dictionary_build_run (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every list of binary names, the eleven-stack machine scans its serialized occurrences in reverse order. It extracts each whole name with real pops and invokes the included finite dictionary-lookup program. The resulting membership flag selects an actual discard or insertion branch.

Every unseen name is written to the head of the dictionary in escaped reversed spelling; the dimension stack receives one true symbol. The final dictionary equals the pinned rightmost-occurrence deduplication of the original list. All comparison backups, candidates, history, index and occurrence stacks are empty at return. The arbitrary caller frame and dimension suffix are preserved.

The clock is at most twenty times (serialized occurrence length plus one) squared. It charges extraction, comparison, operand and dictionary restoration, index draining and insertion. This routine does not yet parse arbitrary conventional clause words or relabel their literals.

References

• Truth anchor: D5/S0/Computability/BinaryNameDeduplication.dictionary_build_run
• Dependency: D5/S0/Computability/BinaryNameDictionary