Documentation

Complexity.Computability.Machines.Turing.MultiTape.Internal.CodecWordMachines

Shared codec word machines #

The original head and emptiness transducers, moved unchanged from Encodings.Basic.

Transducers for the word operations #

source
def Turing.MultiTapeTM.Encodings.headT (drop : Option Bool) :
Transducer Bool Bool

Emits a word determined by its input's first symbol, if any, and by drop: [true] followed by the input (drop = none), the input without its first symbol (drop = some false), or just the first symbol (drop = some true).

Instances For
    source
    theorem Turing.MultiTapeTM.Encodings.headT_step (drop : Option Bool) (x✝ x✝¹ : Bool) :
    (headT drop).step x✝ x✝¹ = match x✝, x✝¹ with | false, b => (true, match drop with | none => [true, b] | some false => [] | some true => [b]) | true, b => (true, match drop with | none => [b] | some false => [b] | some true => [])
    source
    theorem Turing.MultiTapeTM.Encodings.headT_final (drop : Option Bool) (x✝ : Bool) :
    (headT drop).final x✝ = match x✝ with | false => match drop with | none => [true] | x => [] | true => []
    source
    theorem Turing.MultiTapeTM.Encodings.headT_q₀ (drop : Option Bool) :
    (headT drop).q₀ = false
    source
    theorem Turing.MultiTapeTM.Encodings.headT_run_true (drop : Option Bool) (v : List Bool) :
    (headT drop).run true v = if drop = some true then [] else v
    source
    theorem Turing.MultiTapeTM.Encodings.headT_none_run (v : List Bool) :
    (headT none).run (headT none).q₀ v = true :: v

    headT none prepends true.

    source
    theorem Turing.MultiTapeTM.Encodings.headT_some_false_run (v : List Bool) :
    (headT (some false)).run (headT (some false)).q₀ v = v.tail

    headT (some false) drops the first symbol.

    source
    theorem Turing.MultiTapeTM.Encodings.headT_some_true_run (v : List Bool) :
    (headT (some true)).run (headT (some true)).q₀ v = List.take 1 v

    headT (some true) keeps just the first symbol.

    source
    def Turing.MultiTapeTM.Encodings.isEmptyT :
    Transducer Bool Bool

    Emits [true] on the empty word and [false] on every other word.

    Instances For
      source
      theorem Turing.MultiTapeTM.Encodings.isEmptyT_step (q x✝ : Bool) :
      isEmptyT.step q x✝ = (true, if q = true then [] else [false])
      source
      theorem Turing.MultiTapeTM.Encodings.isEmptyT_q₀ :
      isEmptyT.q₀ = false
      source
      theorem Turing.MultiTapeTM.Encodings.isEmptyT_final (q : Bool) :
      isEmptyT.final q = if q = true then [] else [true]
      source
      theorem Turing.MultiTapeTM.Encodings.isEmptyT_run_true (v : List Bool) :
      isEmptyT.run true v = []
      source
      theorem Turing.MultiTapeTM.Encodings.isEmptyT_run (v : List Bool) :
      isEmptyT.run isEmptyT.q₀ v = [v.isEmpty]

      isEmptyT emits the emptiness test of its input.