Finite tree excursions

A Łukasiewicz tree word has integer increments at least -1, total sum -1, and nonnegative sums at every strict prefix. The increment decoder checks the lower bound before converting increments to natural outdegrees.

def BGW.IsTreeExcursion (xs : List ℤ) : Prop

Integer increment words of finite plane trees, with the empty prefix included and the terminal prefix excluded from the nonnegativity condition.

Equations

• BGW.IsTreeExcursion xs = ((∀ x ∈ xs, -1 ≤ x) ∧ xs.sum = -1 ∧ ∀ i < xs.length, 0 ≤ (List.take i xs).sum)

def BGW.PlaneTree.ofIncrements? (xs : List ℤ) : Option PlaneTree

Reconstruct a tree from integer increments, rejecting values below -1 before converting them to outdegrees. The degree decoder accepts one tree only.

Equations

• BGW.PlaneTree.ofIncrements? xs = if ∀ x ∈ xs, -1 ≤ x then BGW.PlaneTree.ofDegrees? (List.map (fun (x : ℤ) => (x + 1).toNat) xs) else none

theorem BGW.PlaneTree.isTreeExcursion_increments (t : PlaneTree) : IsTreeExcursion t.increments

The forward DFS code satisfies exactly the finite-excursion conditions.

@[simp]

theorem BGW.PlaneTree.ofIncrements?_increments (t : PlaneTree) : ofIncrements? t.increments = some t

Decoding the increment word of a tree recovers that tree.

theorem BGW.PlaneTree.increments_ofIncrements? {xs : List ℤ} {t : PlaneTree} (h : ofIncrements? xs = some t) : t.increments = xs

A successful increment parse reproduces the entire input word.

theorem BGW.PlaneTree.ofIncrements?_eq_some_iff {xs : List ℤ} {t : PlaneTree} : ofIncrements? xs = some t ↔ t.increments = xs

theorem BGW.PlaneTree.increments_injective : Function.Injective increments

theorem BGW.PlaneTree.exists_ofIncrements?_eq_some (xs : List ℤ) (h : IsTreeExcursion xs) : ∃ (t : PlaneTree), ofIncrements? xs = some t

Every valid tree excursion parses successfully as one tree.

theorem BGW.PlaneTree.isTreeExcursion_iff_existsUnique (xs : List ℤ) : IsTreeExcursion xs ↔ ∃! t : PlaneTree, t.increments = xs

Integer Łukasiewicz excursions are precisely the codes of unique finite plane trees.