Dense Parser Instruction Refinement

Abstract

The translated finite parser restores raw words and identifies complete accepted syntax.

Theorem 1.1 (Dense Parser Instruction Refinement).

$$\forall w\in \mathrm{List}\left(Bool\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(denseMachine\right),\mathrm{initList}\left(denseMachine,w\right),\mathrm{some}\left(\mathrm{Cfg}\left(\mathrm{some}\left(parseReturn\right),denseLocal,\mathrm{denseParserStacks}\left(\mathrm{parseStacks}\left(w,nil,\mathrm{decodedOccurrences}\left(w\right),\mathrm{singleton}\left(\mathrm{isSome}\left(\mathrm{readWord}\left(w\right)\right)\right),nil\right)\right)\right)\right),4\cdot \mathrm{length}\left(w\right)+5\right)\right)\wedge \left(\forall F\in ConventionalFormula,\mathrm{readWord}\left(w\right)=\mathrm{some}\left(F\right)\Rightarrow \left(w=\mathrm{formulaWord}\left(F\right)\wedge \left(\forall c\in Clause,c\in F\Rightarrow \mathrm{length}\left(c\right)\le 3\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every raw Boolean word, instruction translation executes the actual parser to the parseReturn boundary within four times input length plus five steps. The input is restored, saved stacks are empty, and the decoder determines the occurrence stream and result flag. A grammar induction on that same word shows that every accepted formula reproduces the complete original spelling and has clauses of width at most three. The endpoint is a parser phase boundary, before dictionary construction and dense output.

References

• Truth anchor: D5/S0/Computability/DenseClauseMachine.dense_parser_run
• Dependency: D5/S0/Computability/BinaryNameDeduplication
• Dependency: D5/S0/Computability/ClauseWordCodec