Binary Name Dictionary Lookup

Abstract

Whole-name lookup restores the serialized dictionary and reports its dense position.

Theorem 1.1 (Actual finite execution, exact restored words and paid scan clock).

$$\forall query\in \mathrm{List}\left(Bool\right),\forall names\in \mathrm{List}\left(\mathrm{List}\left(Bool\right)\right),\forall frame\in \mathrm{List}\left(Bool\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(dictionaryMachine\right),\mathrm{lookupCfg}\left(start,query,nil,nil,nil,frame,\mathrm{dictionaryStream}\left(names\right),nil,nil,false\right),\mathrm{some}\left(\mathrm{dictionaryCfg}\left(none,((none,none,true),none,false),\mathrm{compareStacks}\left(query,nil,nil,nil,nil,frame\right),\mathrm{dictionaryStream}\left(names\right),nil,\mathrm{cons}\left(\mathrm{decide}\left(query\in names\right),\mathrm{replicate}\left(\mathrm{idxOf}\left(query,names\right),true\right)\right)\right)\right),\left(2\cdot \mathrm{length}\left(query\right)+12\right)\cdot \mathrm{length}\left(names\right)+4\cdot \mathrm{length}\left(\mathrm{dictionaryStream}\left(names\right)\right)+3\right)\right)$$

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

Source. Repository-derived.

Commentary.

For an arbitrary query name, list of dictionary names and caller frame, the nine-stack machine scans the private serialized dictionary. Each entry stores its reversed binary spelling in escaped pairs. Real pushes extract the candidate, the included comparison program backs up and restores both operands, and cleanup drains the candidate stack.

The final index stack contains the membership flag followed by the unary first-occurrence index; absence uses the dictionary length sentinel. The query and entire dictionary stream are restored literally, all backups and comparison output are empty, and the caller frame is preserved. The bound is (2 times query length plus 12) times the number of names, plus four times serialized dictionary length, plus three.

This is a routine boundary for arbitrary names and dictionary order. The theorem does not supply the preceding raw-source parser, rightmost deduplication or count-preserving complete converter. Those stages must establish the actual dictionary used by this scan.

References

• Truth anchor: D5/S0/Computability/BinaryNameDictionary.dictionary_lookup_run
• Dependency: D5/S0/Computability/BinaryNameComparison
• Dependency: D5/S0/Computability/ConventionalClauseWords