Documentation

Complexity.Computability.Circuit.Boolean.Tableau.Correct

Correctness of the uniform tableau circuit #

The tableau circuit of a multi-tape machine (Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean) computes the run: on an input x of length n, for T steps with n < 2 T, the wire of each feature at time t ≤ T carries the value of that feature in the configuration after t steps (Cslib.Circuits.Boolean.Tableau.invariant_le). In particular the output wire is true exactly when the output written after T steps is [true] (Cslib.Circuits.Boolean.Tableau.evalOutput_gates), and the tableau circuit outputs this value (Cslib.Circuits.Boolean.Tableau.eval_circuit).

The proof follows the blocks. In block t + 1, the scan accumulates the symbols under the heads across the columns, the global gates compute the situation and the attributes of the action, and the gadget of each feature computes the disjunction of its terms, which is the step equation of the feature.

Main definitions #

Main results #

References #

Values of wires #

source
noncomputable def Cslib.Circuits.Boolean.Tableau.val {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (T : ℕ) (x : List Bool) (w : ℕ) :
Bool

The value of wire w of the tableau of tm for T steps, on the input x.

Instances For

    The features of configurations #

    source
    def Cslib.Circuits.Boolean.Tableau.colSem {k : ℕ} {State : Type} (T : ℕ) {input : List Bool} (cfg : Turing.Cfg k Bool State input) (c : ℕ) :
    ColFeat k → Bool

    The value of a column feature in column c of a configuration: the input head at c, the work heads and the work cells at c - T.

    Instances For
      source
      def Cslib.Circuits.Boolean.Tableau.gfSem {k : ℕ} {State : Type} [DecidableEq State] {input : List Bool} (cfg : Turing.Cfg k Bool State input) :
      GFeat State → Bool

      The value of a global feature of a configuration.

      Instances For
        source
        def Cslib.Circuits.Boolean.Tableau.Invariant {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) (T : ℕ) (x : List Bool) (t : ℕ) :
        Prop

        The invariant at time t: the wire of every feature carries its value after t steps.

        Instances For

          Values of references #

          The scan #

          Situations and attributes #

          The gadgets of the features #

          The step equations of the features #

          source
          theorem Cslib.Circuits.Boolean.Tableau.invariant_le {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {T : ℕ} {x : List Bool} (hn : x.length < 2 * T) (t : ℕ) :
          t ≤ T → Invariant tm T x t

          The tableau computes the run: on an input of length n < 2 T, the wire of each feature at time t ≤ T carries the value of that feature after t steps.

          source
          theorem Cslib.Circuits.Boolean.Tableau.evalOutput_gates {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {T : ℕ} {x : List Bool} (hn : x.length < 2 * T) :
          evalOutput x (gates tm x.length T) (outWire k State x.length T) = decide (Turing.OutView.ofList (Turing.MultiTapeTM.runFrom (tm.initCfg x) T).output = Turing.OutView.one true)

          The output wire of the tableau carries the answer: on an input of length n < 2 T, it is true exactly when the output written after T steps is [true].

          source
          theorem Cslib.Circuits.Boolean.Tableau.eval_circuit {k : ℕ} {State : Type} [Fintype State] [DecidableEq State] (tm : Turing.MultiTapeTM k Bool State) {n T : ℕ} (hn : n < 2 * T) (y : BitString n) :
          (circuit tm n T).eval interpretation y 0 = decide (Turing.OutView.ofList (Turing.MultiTapeTM.runFrom (tm.initCfg (List.ofFn y)) T).output = Turing.OutView.one true)

          The tableau circuit outputs the answer: on inputs y of length n < 2 T, it outputs whether tm, started on y, has written exactly [true] after T steps.