Documentation

Complexitylib.Languages.ZeroPrefix

{0ⁿ 1ᵐ : n ≥ m}: a push-down language with inequality counter #

A small variant of AnBn: the input is 0ⁿ 1ᵐ with the extra condition n ≥ m. The machine structurally mirrors anbnTM — a single work tape is used as a unary counter (push on 0, pop on 1) — but the end-of-input branches accept unconditionally: after scanning the full input without hitting a mismatch, the remaining stack height is exactly n − m ≥ 0, which we accept.

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.ZeroPrefixPhase :
Type

Control states of zeroPrefixTM.

  • 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.instDecidableEqZeroPrefixPhase :
    DecidableEq ZeroPrefixPhase
    Equations
    source
    @[implicit_reducible]
    instance Complexity.TM.instFintypeZeroPrefixPhase :
    Fintype ZeroPrefixPhase
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Complexity.TM.zeroPrefixTM :
    TM 1

    Push-down TM deciding {0ⁿ 1ᵐ : n ≥ m}. 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). End-of-input is accepted in both scan states — reaching a blank means we consumed the input without a mismatch, so n ≥ m.

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

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

      Differs from anbnExpected only in end-of-input branches: scanZeros and scanOnes at end of input always accept (output .one).

      Equations
      Instances For
        source
        theorem Complexity.TM.zeroPrefixTM_reachesIn (x : List Bool) :
        ∃ (c' : Cfg 1 zeroPrefixTM.Q), zeroPrefixTM.reachesIn (x.length + 3) (zeroPrefixTM.initCfg x) c' ∧ zeroPrefixTM.halted c' ∧ c'.output.cells 1 = (zeroPrefixExpected ZeroPrefixPhase.scanZeros 0 x).toΓ

        zeroPrefixTM halts in |x| + 3 steps on every input, writing the correct answer to output cell 1.

        source
        def Complexity.Language.zeroPrefix :
        Language

        The language {0ⁿ 1ᵐ : n ≥ m} — strings of some zeros followed by at most that many ones.

        Equations
        Instances For
          source
          theorem Complexity.TM.zeroPrefixTM_decidesInTime :
          zeroPrefixTM.DecidesInTime Language.zeroPrefix fun (n : ℕ) => n + 3

          zeroPrefixTM decides Language.zeroPrefix in time |x| + 3.

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

          zeroPrefix ∈ DTIME(n + 3).

          source
          theorem Complexity.zeroPrefix_mem_P :
          Language.zeroPrefix ∈ P

          zeroPrefix ∈ P.