Documentation

Complexity.Computability.USTCON.Reader.Encode

Encoding the states of the read machine for undirected connectivity #

The states of Cslib.USTCON.Reader.machine are encoded through tuples of the control, numbers in binary, and lists of labels and frames, every label and frame by its rank among the finitely many (Turing.MultiTapeTM.encFinEnum). The machines simulating the read machine keep the encoded state on their work tapes, so its length bounds their work space, up to a constant factor and the position of the input head.

Main definitions #

Main results #

source
@[instance_reducible]
instance Cslib.USTCON.Reader.instFintypeCtl :
Fintype Ctl
source
@[instance_reducible]
instance Cslib.USTCON.Reader.instFinEnumCtl :
FinEnum Ctl
source
@[instance_reducible]
instance Cslib.USTCON.Reader.instFinEnumReingoldPc :
FinEnum RotationMap.ReingoldPc
source
@[instance_reducible]
instance Cslib.USTCON.Reader.instFinEnumZMod (n : ℕ) [NeZero n] :
FinEnum (ZMod n)

Concrete enumeration of a positive modular ring.

source
@[reducible, inline]
abbrev Cslib.USTCON.Reader.Tuple :
Type

The states as tuples: the control and the header counter, the parameters of the instance and of Reingold's graph, and the counters of the walks with the state of the evaluation.

Instances For
    source
    def Cslib.USTCON.Reader.State.toTuple (q : State) :
    Tuple

    A state as a tuple.

    Instances For
      source
      def Cslib.USTCON.Reader.State.ofTuple (x : Tuple) :
      State

      The state of a tuple.

      Instances For
        source
        @[simp]
        theorem Cslib.USTCON.Reader.State.ofTuple_toTuple (q : State) :
        ofTuple q.toTuple = q
        source
        @[simp]
        theorem Cslib.USTCON.Reader.State.toTuple_ofTuple (x : Tuple) :
        (ofTuple x).toTuple = x
        source
        def Cslib.USTCON.Reader.encLab :
        Reachability.Reingold.Label ↪ List Bool

        Labels, by their ranks.

        Instances For
          source
          def Cslib.USTCON.Reader.encFrame :
          RotationMap.ReingoldPc × Reachability.Reingold.Label ↪ List Bool

          Frames, by their ranks.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.USTCON.Reader.encNat3 :
            ℕ × ℕ × ℕ ↪ List Bool

            Three numbers.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.USTCON.Reader.encEval :
              (ℕ × ℕ) × List Reachability.Reingold.Label × List (RotationMap.ReingoldPc × Reachability.Reingold.Label) ↪ List Bool

              The state of the evaluation: the slot, the labels and the frames.

              Instances For
                source
                def Cslib.USTCON.Reader.encCtl :
                Ctl ↪ List Bool

                The control, by its rank.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.USTCON.Reader.encTuple :
                  Tuple ↪ List Bool

                  The encoding of tuples.

                  Instances For
                    source
                    def Cslib.USTCON.Reader.encState :
                    State ↪ List Bool

                    The encoding of the states, through their tuples.

                    Instances For
                      source
                      @[simp]
                      theorem Cslib.USTCON.Reader.encState_apply (q : State) :
                      encState q = encTuple q.toTuple
                      source
                      theorem Cslib.USTCON.Reader.length_encState_le (q : State) :
                      (encState q).length ≤ 64 * ((encCtl q.ctl).length + (Turing.MultiTapeTM.encNat q.cnt).length + (Turing.MultiTapeTM.encNat q.n).length + (Turing.MultiTapeTM.encNat q.s).length + (Turing.MultiTapeTM.encNat q.t).length + (Turing.MultiTapeTM.encNat q.depth).length + (Turing.MultiTapeTM.encNat q.len).length + (Turing.MultiTapeTM.encNat q.c).length + (Turing.MultiTapeTM.encNat q.w).length + (Turing.MultiTapeTM.encNat q.j).length + (Turing.MultiTapeTM.encNat q.ev.vertex.1).length + (Turing.MultiTapeTM.encNat q.ev.vertex.2).length + ((Turing.MultiTapeTM.encList encLab) q.ev.lower).length + ((Turing.MultiTapeTM.encList encFrame) q.ev.frames).length + 1)

                      The length of an encoded state: the framing doubles the encodings of the components, a bounded number of times.