Documentation

Complexitylib.Languages.AnBn

{0ⁿ 1ⁿ : n ≥ 0}: the canonical push-down language #

The first non-regular language formalized here: the TM uses its single work tape as a counter (push on 0, pop on 1). Demonstrates a textbook push-down construction with an O(n) time bound.

The machine has six control states (start, initWork, scanZeros, scanOnes, reject, done) and maintains the invariant that the work head equals the current stack size. Emptiness is detected structurally via the permanently-▷ cell 0.

Main definitions #

Main results #

source
inductive Complexity.TM.AnBnPhase :
Type

Control states of anbnTM.

  • start : initial state. Moves all heads from cell 0 (▷) to cell 1.
  • initWork: rewinds work head back to cell 0 (where ▷ marks emptiness).
  • scanZeros: scanning the 0-prefix; pushes on 0, transitions on 1.
  • scanOnes : scanning the 1-suffix; pops on 1, rejects on 0.
  • reject : sink state; consumes remaining input then halts with 0.
  • done : halted.
Instances For
    source
    @[implicit_reducible]
    instance Complexity.TM.instDecidableEqAnBnPhase :
    DecidableEq AnBnPhase
    Equations
    source
    @[implicit_reducible]
    instance Complexity.TM.instFintypeAnBnPhase :
    Fintype AnBnPhase
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Complexity.TM.anbnTM :
    TM 1

    Push-down TM deciding {0ⁿ 1ⁿ}. One work tape used as a unary counter: the work head holds the current stack size (0 means empty, detected by reading ▷ at cell 0).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.TM.anbnExpected :
      AnBnPhase → ℕ → List Bool → Γw

      The output that anbnTM produces when run from scan state s with work head h (= stack size) and remaining input rest. Structurally recursive on rest.

      Equations
      Instances For
        source
        structure Complexity.TM.ScanInv (c : Cfg 1 anbnTM.Q) (x : List Bool) (k h : ℕ) :
        Prop

        Common invariants for a configuration during the scan phase.

        Instances For
          source
          structure Complexity.TM.RejectInv (c : Cfg 1 anbnTM.Q) (x : List Bool) (k : ℕ) :
          Prop

          Simpler invariant for the .reject state. Work head is not tracked.

          Instances For
            source
            theorem Complexity.TM.anbnTM_reachesIn (x : List Bool) :
            ∃ (c' : Cfg 1 anbnTM.Q), anbnTM.reachesIn (x.length + 3) (anbnTM.initCfg x) c' ∧ anbnTM.halted c' ∧ c'.output.cells 1 = (anbnExpected AnBnPhase.scanZeros 0 x).toΓ

            anbnTM halts in |x| + 3 steps on every input, writing the correct answer (Γ.one if x = 0ⁿ 1ⁿ, else Γ.zero) to output cell 1.

            source
            def Complexity.Language.anbn :
            Language

            The language {0ⁿ 1ⁿ : n ≥ 0} — the canonical context-free but non-regular language. A string x is in anbn iff it consists of some n copies of false followed by the same number of copies of true.

            Equations
            Instances For
              source
              theorem Complexity.TM.anbnTM_decidesInTime :
              anbnTM.DecidesInTime Language.anbn fun (n : ℕ) => n + 3

              anbnTM decides Language.anbn in time |x| + 3.

              source
              theorem Complexity.anbn_in_DTIME :
              Language.anbn ∈ DTIME fun (n : ℕ) => n + 3

              anbn ∈ DTIME(n + 3).

              source
              theorem Complexity.anbn_mem_P :
              Language.anbn ∈ P

              anbn ∈ P.