Documentation

MIPRE.TM.CookLevin.Local

The local check of the Cook–Levin tableau #

The window of the tableau at a step t and a choice of a position on every tape (planning/succinct-cook-levin.md, S1; answer_reduction.tex def:local-check-circuit): for each tape the five cells and heads around the position at time t, the cell and head at the position at time t + 1, the states at t and t + 1 and the emission flags of the step. Five cells rather than the paper's three, because the input heads of the repository's machine model clamp at both ends of the input (Turing.moveInputPos), and deciding whether a head one cell off the center moves or stays needs the cell beyond it.

The window's bits are one-hot: one variable per cell and cell value, per state. A window is locally consistent (LocallyConsistent) if it is the encoding of a local configuration in which, wherever the local information suffices, the time-t + 1 values are the transition of the time-t ones: if every tape has its head in the central three cells the whole transition is checked, including the state and the emission; a tape whose head is not near the center keeps its cell and has no head at the center; a tape with two heads in the window is accepted unconditionally, an invariant of the tableau excluding it. The predicate checkPred on window bits is what the check circuit computes.

source
inductive MIPRE.TM.CookLevin.CellVal (Symbol : Type u_1) :
Type u_1

The value of a tableau cell: a symbol, the blank, or the boundary marker.

Instances For
    source
    @[instance_reducible]
    instance MIPRE.TM.CookLevin.instDecidableEqCellVal {Symbol✝ : Type u_1} [DecidableEq Symbol✝] :
    DecidableEq (CellVal Symbol✝)
    Equations
    source
    def MIPRE.TM.CookLevin.instDecidableEqCellVal.decEq {Symbol✝ : Type u_1} [DecidableEq Symbol✝] (x✝ x✝¹ : CellVal Symbol✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.TM.CookLevin.instFintypeCellValOfDecidableEq {Symbol : Type u_1} [Fintype Symbol] [DecidableEq Symbol] :
      Fintype (CellVal Symbol)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def MIPRE.TM.CookLevin.CellVal.ofOpt {Symbol : Type u_1} :
      Option Symbol → CellVal Symbol

      The cell value of a tape symbol (none the blank).

      Equations
      Instances For
        source
        def MIPRE.TM.CookLevin.CellVal.toOpt {Symbol : Type u_1} :
        CellVal Symbol → Option Symbol

        The tape symbol of a non-boundary cell value (the boundary reads as blank).

        Equations
        Instances For
          source
          @[simp]
          theorem MIPRE.TM.CookLevin.CellVal.toOpt_ofOpt {Symbol : Type u_1} (o : Option Symbol) :
          (ofOpt o).toOpt = o
          source
          @[reducible, inline]
          abbrev MIPRE.TM.CookLevin.Tape (i w : ℕ) :
          Type

          The tapes: i input tapes and w work tapes.

          Equations
          Instances For
            source
            inductive MIPRE.TM.CookLevin.WinVar (i w : ℕ) (Symbol : Type u_1) (State : Type u_2) :
            Type (max u_1 u_2)

            The variables of a window: for each tape, the five cells and heads at offsets 0..4 around the position at time t, the cell and head at the position at time t + 1; the states at t and t + 1; the emission flags of the step.

            Instances For
              source
              def MIPRE.TM.CookLevin.instDecidableEqWinVar.decEq {i✝ w✝ : ℕ} {Symbol✝ : Type u_1} {State✝ : Type u_2} [DecidableEq Symbol✝] [DecidableEq State✝] (x✝ x✝¹ : WinVar i✝ w✝ Symbol✝ State✝) :
              Decidable (x✝ = x✝¹)
              Equations
              Instances For
                source
                @[instance_reducible]
                instance MIPRE.TM.CookLevin.instDecidableEqWinVar {i✝ w✝ : ℕ} {Symbol✝ : Type u_1} {State✝ : Type u_2} [DecidableEq Symbol✝] [DecidableEq State✝] :
                DecidableEq (WinVar i✝ w✝ Symbol✝ State✝)
                Equations
                source
                @[instance_reducible]
                instance MIPRE.TM.CookLevin.instFintypeWinVarOfDecidableEq {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] :
                Fintype (WinVar i w Symbol State)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                structure MIPRE.TM.CookLevin.LocalCfg (i w : ℕ) (Symbol : Type u_1) (State : Type u_2) :
                Type (max u_1 u_2)

                A local configuration: the decoded content of a window.

                Instances For
                  source
                  def MIPRE.TM.CookLevin.LocalCfg.encode {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] (L : LocalCfg i w Symbol State) :
                  WinVar i w Symbol State → Bool

                  The one-hot bits of a local configuration.

                  Equations
                  Instances For
                    source
                    def MIPRE.TM.CookLevin.LocalCfg.HeadAt {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (L : LocalCfg i w Symbol State) (d : Tape i w) (δ : Fin 5) :
                    Prop

                    The head of tape d is at offset δ and nowhere else in the window.

                    Equations
                    Instances For
                      source
                      def MIPRE.TM.CookLevin.LocalCfg.TwoHeads {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (L : LocalCfg i w Symbol State) (d : Tape i w) :
                      Prop

                      Two heads of tape d in the window.

                      Equations
                      Instances For
                        source
                        def MIPRE.TM.CookLevin.LocalCfg.HeadFar {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (L : LocalCfg i w Symbol State) (d : Tape i w) :
                        Prop

                        No head of tape d in the central three cells.

                        Equations
                        Instances For
                          source
                          def MIPRE.TM.CookLevin.newOffset {Symbol : Type u_1} [DecidableEq Symbol] (isInput : Bool) (cells : Fin 5 → CellVal Symbol) (δ : Fin 5) (m : SignType) :
                          ℕ

                          The new offset of a head at offset δ ∈ {1, 2, 3} after a move m, on an input tape (clamped: a move left from the first position, whose left neighbor is the boundary, and a move right from the position after the input, a blank whose left neighbor is not the boundary, stay) or a work tape (never clamped).

                          Equations
                          Instances For
                            source
                            def MIPRE.TM.CookLevin.FullStep {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) (L : LocalCfg i w Symbol State) (δ : Tape i w → Fin 5) :
                            Prop

                            The full transition check, when every tape has its head at the offset δ d of the central three cells: the time-t + 1 values are those of the machine's transition.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def MIPRE.TM.CookLevin.LocallyConsistent {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) (L : LocalCfg i w Symbol State) :
                              Prop

                              Local consistency of a decoded window.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def MIPRE.TM.CookLevin.checkPred {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) (win : WinVar i w Symbol State → Bool) :
                                Prop

                                The check predicate on window bits: the bits encode a locally consistent local configuration.

                                Equations
                                Instances For