Documentation

Complexitylib.Languages.Trivial

Trivial languages: ∅ and Set.univ #

The two easiest languages to decide, along with their complexity. Both are decided by writeTM — a machine that writes a fixed symbol to the output tape and halts in constant time — and therefore belong to every standard complexity class.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Complexity.Language.empty :
Language

The empty language (no strings accepted).

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.Language.univ :
    Language

    The universal language (all strings accepted).

    Equations
    Instances For
      source
      theorem Complexity.TM.Tape.init_nil_wf :
      (Tape.init []).cells 0 = Γ.start ∧ (∀ j ≥ 1, (Tape.init []).cells j ≠ Γ.start) ∧ (Tape.init []).head ≤ 0

      Tape.init [] is the canonical output-tape initial value: cell 0 is ▷, every other cell is □, and the head is at position 0. This is exactly the well-formedness precondition of writeTM_hoareTime with B = 0.

      source
      theorem Complexity.TM.writeTM_decidesInTime_const {n : ℕ} (sym : Γw) (x : List Bool) :
      ∃ (c' : Cfg n (writeTM sym).Q), ∃ t ≤ 3, (writeTM sym).reachesIn t ((writeTM sym).initCfg x) c' ∧ (writeTM sym).halted c' ∧ c'.output.cells 1 = sym.toΓ

      writeTM halts on every input in 3 steps with sym on output cell 1.

      Specialization of writeTM_hoareTime (B = 0) to the initial configuration, packaged in the exact form required by DecidesInTime.

      source
      theorem Complexity.empty_in_DTIME :
      Language.empty ∈ DTIME fun (x : ℕ) => 3

      The empty language is decidable in constant time. writeZeroTM always writes 0 to output cell 1 and halts in at most 3 steps.

      source
      theorem Complexity.univ_in_DTIME :
      Language.univ ∈ DTIME fun (x : ℕ) => 3

      The universal language is decidable in constant time. writeOneTM always writes 1 to output cell 1 and halts in at most 3 steps.

      source
      theorem Complexity.empty_mem_P :
      Language.empty ∈ P

      ∅ ∈ P.

      source
      theorem Complexity.univ_mem_P :
      Language.univ ∈ P

      Set.univ ∈ P.

      source
      theorem Complexity.empty_mem_NP :
      Language.empty ∈ NP

      ∅ ∈ NP.

      source
      theorem Complexity.univ_mem_NP :
      Language.univ ∈ NP

      Set.univ ∈ NP.

      source
      theorem Complexity.empty_mem_BPP :
      Language.empty ∈ BPP

      ∅ ∈ BPP.

      source
      theorem Complexity.univ_mem_BPP :
      Language.univ ∈ BPP

      Set.univ ∈ BPP.

      source
      theorem Complexity.empty_mem_PSPACE :
      Language.empty ∈ PSPACE

      ∅ ∈ PSPACE.

      source
      theorem Complexity.univ_mem_PSPACE :
      Language.univ ∈ PSPACE

      Set.univ ∈ PSPACE.

      source
      theorem Complexity.empty_mem_EXP :
      Language.empty ∈ EXP

      ∅ ∈ EXP.

      source
      theorem Complexity.univ_mem_EXP :
      Language.univ ∈ EXP

      Set.univ ∈ EXP.