ZeroParse Proofs
The runtimes reuse results to bound the cost of a parse. Each mechanism of reuse is stated in the Parser and Runtime Specification, and a reuse is correct only if it gives the result that evaluating again would give. The proofs here show that, and the cost bounds that the mechanisms claim, as lemmas over the definitions of the specifications that they cite.
Each proof names its author and the date of its last revision under its title. A change to a statement or a proof updates the date. From the first release on, each proof also lists the releases that changed it. To cite a proof, cite ZeroParse and name the proof.
Contents
| Proof | Shows |
|---|---|
| Skip Runs | A reused record of a skip run gives what the rest of the walk would, and the walks of a site evaluate its element a linear number of times |
| Memoization | Answering a call from a memo entry, including the members of a left-recursion cycle and results that depend on the order of evaluation, gives the outcome that evaluating it again would give |
| Documents | A parse of a Document after edits, reusing carried memo entries and recorded runs, gives the result of a fresh parse of its text |
| Linear Cost | An outline of how the Conditions for Linear Cost bound the cost of a parse, with its lemmas and the steps still open |
| Constant-Cost Text | Taking the text of a node is a step of constant cost given the guarantee of Cost, so the conditions need not count it as a copy, and a comparison of strings may count only one operand |