Documentation

Complexitylib.Encoding.Stack

Exact nested-pair stack encoding #

A stack is encoded top first: the empty stack is [], and pushing a frame pairs its encoding with the encoded tail. Empty frame encodings are permitted; the pair separator still distinguishes a nonempty stack from an empty one. The frame encoder need not be injective for the projection and length laws.

The raw stack operations are the existing pair, pairFst, and pairSnd, including their total behavior on malformed strings. Their polynomial-time closure rules live in Classes.P.Pairing, outside this machine-independent module. Return values and algorithm-specific frame semantics are not encoded here.

source
def Complexity.StackEncoding.encode {α : Type u_1} (frame : α → List Bool) :
List α → List Bool

Encode a stack with its top frame first, using the supplied frame encoding.

Equations
Instances For
    source
    @[simp]
    theorem Complexity.StackEncoding.encode_nil {α : Type u_1} (frame : α → List Bool) :
    encode frame [] = []
    source
    @[simp]
    theorem Complexity.StackEncoding.encode_cons {α : Type u_1} (frame : α → List Bool) (f : α) (fs : List α) :
    encode frame (f :: fs) = pair (frame f) (encode frame fs)
    source
    theorem Complexity.StackEncoding.pairFst_encode_cons {α : Type u_1} (frame : α → List Bool) (f : α) (fs : List α) :
    pairFst (encode frame (f :: fs)) = frame f

    Reading the top of an encoded nonempty stack recovers its frame encoding.

    source
    theorem Complexity.StackEncoding.pairSnd_encode_cons {α : Type u_1} (frame : α → List Bool) (f : α) (fs : List α) :
    pairSnd (encode frame (f :: fs)) = encode frame fs

    Popping an encoded nonempty stack recovers the encoded tail.

    source
    theorem Complexity.StackEncoding.encode_eq_nil_iff {α : Type u_1} (frame : α → List Bool) (fs : List α) :
    encode frame fs = [] ↔ fs = []

    Even an empty frame encoding has a separator, so only an empty stack encodes to [].

    source
    @[simp]
    theorem Complexity.StackEncoding.length_encode {α : Type u_1} (frame : α → List Bool) (fs : List α) :
    (encode frame fs).length = List.foldr (fun (f : α) (n : ℕ) => 2 * (frame f).length + 2 + n) 0 fs

    Exact length, including the doubled frame and two separator bits at every push.

    source
    theorem Complexity.StackEncoding.length_encode_le {α : Type u_1} (frame : α → List Bool) (fs : List α) (B : ℕ) :
    (∀ (f : α), f ∈ fs → (frame f).length ≤ B) → (encode frame fs).length ≤ fs.length * (2 * B + 2)

    A uniform frame-length bound gives a linear bound in the number of live frames.