Unary input-length transducer — definitions

This module defines a deterministic transducer that scans its Boolean input once and writes one true bit per input bit. Its output is therefore the unary representation List.replicate x.length true of the input length.

inductive Complexity.TM.UnaryLengthPhase : Type

Control states for unaryLengthTM: scan the input, then halt at its first trailing blank.

• copying : UnaryLengthPhase
• done : UnaryLengthPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqUnaryLengthPhase : DecidableEq UnaryLengthPhase

Equations

• Complexity.TM.instDecidableEqUnaryLengthPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeUnaryLengthPhase : Fintype UnaryLengthPhase

Equations

• Complexity.TM.instFintypeUnaryLengthPhase = { elems := {Complexity.TM.UnaryLengthPhase.copying, Complexity.TM.UnaryLengthPhase.done}, complete := ⋯ }

def Complexity.TM.unaryLengthTM {n : ℕ} : TM n

Scan the Boolean input from left to right and emit one true bit per input bit. The first step skips the left-end markers, and the machine halts when the input head reaches its first trailing blank.

Equations

• One or more equations did not get rendered due to their size.