`{x : #false x = #true x}`: equal-count / "balanced" language #

The balanced language contains every string with as many falses as trues — any interleaving, not just the blocked form 0ⁿ 1ⁿ. The TM generalizes anbnTM by tracking which bit is currently in excess in the control state, while using the single work tape as a unary counter for the size of the excess.

Invariant: after consuming a prefix p, the work head position equals |#false(p) - #true(p)|, and the control state records whether #false > #true (scanExcess0), #true > #false (scanExcess1), or equality (either state with head at cell 0).

Emptiness (h = 0) is detected structurally by the work head reading ▷ at cell 0 — the same trick as in anbnTM.

Main definitions #

TM.balancedTM — 5-state 1-work-tape push-down machine.
Language.balanced — {x | x.count false = x.count true}.

Main results #

TM.balancedTM_reachesIn — halts in |x| + 3 steps on every input.
balanced_in_DTIME, balanced_mem_P.

source

inductive Complexity.TM.BalancedPhase :

Type

Control states of balancedTM.

start : initial state. Moves all heads from cell 0 (▷) to cell 1.
initWork : rewinds the work head back to cell 0.
scanExcess0 : scanning; the stack (unary counter) holds #false - #true. h = 0 (work reads ▷) means equality so far.
scanExcess1 : scanning; the stack holds #true - #false.
done : halted.

start : BalancedPhase
initWork : BalancedPhase
scanExcess0 : BalancedPhase
scanExcess1 : BalancedPhase
done : BalancedPhase

Instances For

source

@[implicit_reducible]

instance Complexity.TM.instDecidableEqBalancedPhase :

DecidableEq BalancedPhase

Equations

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

source

@[implicit_reducible]

instance Complexity.TM.instFintypeBalancedPhase :

Fintype BalancedPhase

Equations

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

source

def Complexity.TM.balancedTM :

TM 1

Push-down TM deciding the balanced language. One work tape is used as a unary counter. The sign (which bit is in excess) is encoded in the control state; the stack height is the absolute difference.

Equations

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

Instances For

source

def Complexity.TM.balancedExpected :

BalancedPhase → ℕ → List Bool → Γw

The output that balancedTM produces when run from scan state s with stack height h and remaining input rest. Structurally recursive on rest.

Equations

Instances For

source

structure Complexity.TM.BalancedScanInv (c : Cfg 1 balancedTM.Q) (x : List Bool) (k h : ℕ) :

Prop

Invariants for a configuration during the scan phase. Identical shape to AnBn.BalancedScanInv: the input is a suffix of x.map Γ.ofBool starting at position k + 1, the work head equals the stack height h, and the output tape is pristine at head position 1.

ic : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells
ih : c.input.head = k + 1
wh : (c.work 0).head = h
wstart : (c.work 0).cells 0 = Γ.start
wns (j : ℕ) : j ≥ 1 → (c.work 0).cells j ≠ Γ.start
oh : c.output.head = 1
ons : c.output.cells 1 ≠ Γ.start

Instances For

source

theorem Complexity.TM.balancedTM_reachesIn (x : List Bool) :

∃ (c' : Cfg 1 balancedTM.Q), balancedTM.reachesIn (x.length + 3) (balancedTM.initCfg x) c' ∧ balancedTM.halted c' ∧ c'.output.cells 1 = (balancedExpected BalancedPhase.scanExcess0 0 x).toΓ

balancedTM halts in |x| + 3 steps on every input, writing the correct answer (Γ.one iff x.count false = x.count true, else Γ.zero) to output cell 1.

source

def Complexity.Language.balanced :

Language

The balanced language — strings with equal numbers of falses and trues. Generalizes anbn to arbitrary interleavings.

Equations