Fixed-width packing for linear-bounded tapes

This module packs a bounded number of logical symbols into each physical tape cell. It is independent of any particular grammar or automaton and is used by Aho's row encoding.

@[reducible, inline]

abbrev PackedBlock (α : Type) (W : ℕ) : Type

A width-W block of optional logical symbols stored in one physical tape cell.

Equations

• PackedBlock α W = (Fin W → Option α)

noncomputable instance PackedBlock.instFintype {α : Type} [Fintype α] (W : ℕ) : Fintype (PackedBlock α W)

Equations

• PackedBlock.instFintype W = id inferInstance

instance PackedBlock.instDecidableEq {α : Type} [DecidableEq α] (W : ℕ) : DecidableEq (PackedBlock α W)

Equations

• PackedBlock.instDecidableEq W = id inferInstance

def packedCell {α : Type} (W : ℕ) (xs : List α) (i : ℕ) : PackedBlock α W

The i-th width-W block of a list, padded with none past the list end.

Equations

• packedCell W xs i j = xs[i * W + ↑j]?

def packedTape {α : Type} (W n : ℕ) (xs : List α) : Fin n → PackedBlock α W

Pack a list into n width-W cells. Entries beyond n * W are ignored.

Equations

• packedTape W n xs i = packedCell W xs ↑i

theorem packedTape_lookup {α : Type} {W n k : ℕ} (xs : List α) (hW : 0 < W) (hk : k < n * W) : packedTape W n xs ⟨k / W, ⋯⟩ ⟨k % W, ⋯⟩ = xs[k]?

theorem packedTape_ext_of_length_le {α : Type} {W n : ℕ} {xs ys : List α} (hW : 0 < W) (hxs : xs.length ≤ n * W) (hys : ys.length ≤ n * W) (hpack : packedTape W n xs = packedTape W n ys) : xs = ys

Packing is injective for lists that fit in the advertised physical capacity.