Documentation

Complexitylib.Models.TuringMachine.SpaceTime.Internal.OutputFrontier

Output-frontier invariants — proof internals #

This module records the blank-suffix invariant of a one-way output tape. An initial output tape is blank strictly beyond its head, and a transducer step preserves that property because its output head never moves left.

source
def Complexity.Tape.BlankAfterHead (t : Tape) :
Prop

Every cell strictly beyond the tape head is blank. For a one-way output tape, the head is therefore a frontier beyond which no output has been written.

Equations
Instances For
    source
    theorem Complexity.Tape.BlankAfterHead.init_nil :
    (init []).BlankAfterHead

    The empty initialized tape is blank beyond its initial head.

    source
    theorem Complexity.Tape.BlankAfterHead.writeAndMove {t : Tape} (h : t.BlankAfterHead) (s : Γ) (d : Dir3) (hd : d ≠ Dir3.left) :
    (t.writeAndMove s d).BlankAfterHead

    Writing at the current head and then moving right or staying put preserves the blank suffix beyond the head.

    source
    theorem Complexity.TM.initCfg_output_blankAfterHead {n : ℕ} (tm : TM n) (x : List Bool) :
    (tm.initCfg x).output.BlankAfterHead

    The output tape of an initial configuration is blank beyond its head.

    source
    theorem Complexity.TM.IsTransducer.output_blankAfterHead_step {n : ℕ} {tm : TM n} (htrans : tm.IsTransducer) {c c' : Cfg n tm.Q} (hblank : c.output.BlankAfterHead) (hstep : tm.step c = some c') :
    c'.output.BlankAfterHead

    One step of a transducer preserves the blank output suffix.

    source
    theorem Complexity.TM.IsTransducer.output_blankAfterHead_reachesIn {n : ℕ} {tm : TM n} (htrans : tm.IsTransducer) {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') (hblank : c.output.BlankAfterHead) :
    c'.output.BlankAfterHead

    Exact-step reachability from a configuration with a blank output suffix preserves that suffix for a transducer.

    source
    theorem Complexity.TM.IsTransducer.output_blankAfterHead_reaches {n : ℕ} {tm : TM n} (htrans : tm.IsTransducer) {c c' : Cfg n tm.Q} (hreach : tm.reaches c c') (hblank : c.output.BlankAfterHead) :
    c'.output.BlankAfterHead

    Reachability from a configuration with a blank output suffix preserves that suffix for a transducer.

    source
    theorem Complexity.TM.IsTransducer.initCfg_output_blankAfterHead_reachesIn {n : ℕ} {tm : TM n} (htrans : tm.IsTransducer) {x : List Bool} {t : ℕ} {c : Cfg n tm.Q} (hreach : tm.reachesIn t (tm.initCfg x) c) :
    c.output.BlankAfterHead

    Every output tape reachable in an exact number of steps from an initial configuration of a transducer is blank beyond its head.

    source
    theorem Complexity.TM.IsTransducer.initCfg_output_blankAfterHead_reaches {n : ℕ} {tm : TM n} (htrans : tm.IsTransducer) {x : List Bool} {c : Cfg n tm.Q} (hreach : tm.reaches (tm.initCfg x) c) :
    c.output.BlankAfterHead

    Every output tape reachable from an initial configuration of a transducer is blank beyond its head.