The preorder encoding of ranked terms

A symbol is spelled by its block followed by its children's spellings, in index order. The encoding is a bijection onto the words a single right-to-left scan accepts, the scan carrying an incomplete block, the count of pending subterms and a liveness flag.

The idea is that of prefix notation, in which a symbol is followed by exactly as many operands as its arity. RankedAlphabet.Binary is the case of one symbol of arity zero and one of arity two.

Validity is stated as three conditions, in the manner of mathlib's DyckWord, whose fields count_U_eq_count_D and count_D_le_count_U play the roles the pending count and the liveness flag play here, and in the direction a single right-to-left pass carrying a counter can scan. valid_iff_scanFinal adds a third, that the incomplete block is empty: at a general width that condition is not implied by the other two, so stating validity as only the first two, as DyckWord does, would be false here.

A boundedRec of a Cobham-style function algebra processes a list from its far end, so in that reading a symbol's block is read before the blocks of its children and the symbol is applied after them: prefix notation in list order is postfix notation in processing order.

Main definitions

RankedAlphabet.spell — the encoding.

RankedAlphabet.decodeBlock, RankedAlphabet.parseChildren, RankedAlphabet.parseStep, RankedAlphabet.parseAux, RankedAlphabet.parse — the fuel-bounded recursive-descent decoding.

RankedAlphabet.encoding — the two as a Computability.Encoding.

RankedAlphabet.Scan, RankedAlphabet.scanStep, RankedAlphabet.scanFrom, RankedAlphabet.scanFinal — the scan.

RankedAlphabet.validBool, RankedAlphabet.Valid — what it accepts.

DecidablePred RankedAlphabet.Valid — the instance deciding it.

Main statements

RankedAlphabet.parse_spell — the retraction law.

RankedAlphabet.parse_eq_some_iff — the decoding inverts the encoding.

RankedAlphabet.spell_injective — distinct terms have distinct spellings.

RankedAlphabet.valid_spell — every spelling is valid.

RankedAlphabet.valid_iff_exists_spell — the valid words are exactly the spellings.

RankedAlphabet.valid_iff_isSome_parse — the descent decides validity.

RankedAlphabet.length_buf_scanFinal_of_live — a live scan's incomplete block holds the word's length modulo the width.

RankedAlphabet.length_buf_scanFinal_lt — the incomplete block never fills.

RankedAlphabet.depth_scanFinal_le_length — the pending count is at most the word's length.

RankedAlphabet.valid_iff_scanFinal — validity as three conditions on the final state.

Implementation notes

parseAux recurses on an explicit ℕ bound rather than on its input: each child is parsed from a remainder the previous call computes, which is not a structural subterm. parse supplies the input's length, and length_spell with width_pos shows that bound admits every word spell emits.

Fuel exhaustion is not a rejection mechanism of its own. Each parseStep layer consumes a whole block, which width_pos makes at least one bit, so the invariant that the fuel is at least the remaining length holds from parse's initial w.length down to wherever the descent stops. The descent's own rejections are decodeBlock's two — the input falls short of a block, or the block spells no symbol — together with a child's failure and the trailing input parse rejects.

parseChildren is a Nat.rec and decodeBits a List.rec, so neither has generated equation lemmas; parseChildren_succ and decodeBits_cons are stated for the rewrites that need them.

scanStep matches on Bool values and Valid is a Bool equation rather than an equation of Scan. Both are required by kernel reduction: an equation of Scan would be decided through a derived DecidableEq, which at a symbolic fold leaves decide stuck on the instance rather than reducing it, so Scan derives none. A decidable test is not itself the obstruction, as decodeBlock shows by branching on one and reducing.

exists_spell_append_of_live_of_buf_nil_of_one_le_depth is likewise bounded by an explicit ℕ and driven by Nat.rec. Its step applies the hypothesis once per child of the head symbol, through exists_children_append_of_le_depth, which takes that hypothesis as an argument; every use sits at the same bound, so no well-founded recursion is needed. The step splits off the word's leading block rather than its trailing one: spell is prefix notation while the scan reads right to left, so the head symbol's block is read last, from the state the scan of everything after it leaves.

The base case ascribes w.length ≤ 0 to hzero before appealing to omega: Nat.rec's base case presents the bound as w.length ≤ Nat.zero, and omega treats the unreduced Nat.zero as an opaque atom, so the ascription at the literal 0 is what makes the hypothesis usable.

spell_injective is derived from Computability.Encoding.encode_injective through encoding rather than proved directly, the encoding and its descent being exactly that structure's three fields.

Tags

ranked alphabet, preorder, prefix notation, encoding, retraction, scan

The preorder encoding: a symbol's block followed by its children's spellings, in index order.

A spelling's length is the alphabet's width times the term's node count, so the input length is fuel enough for the descent to read anything spell emits.

Read one block: the symbol it spells and the unconsumed remainder, absent when the word is short of a block or the block spells no symbol.

Read n children in index order, delegating each to child.

parseChildren unfolded on a positive count. parseChildren is a bare Nat.rec, for which Lean generates no equation lemma.

One layer of the recursive descent: read one block, then as many children as its symbol's arity.

Recursive descent bounded by an explicit ℕ.

The decoding, rejecting trailing input.

A block followed by anything is read as its own symbol, leaving what follows.

Reading n children off the concatenation of their spellings returns them and the remainder.