Documentation

Complexity.Computability.TreeEval.Reader.Encode

Encodings of the states of the Tree Evaluation read machine #

The states of Cslib.TreeEval.Reader.machine are encoded as tuples: the value length, the height and the prime in binary, the registers as lists of binary naturals, the stack as a list of frames, each a binary round with finitely many other fields, the mode as a finite tag, and the control state as a tag with two binary naturals and a list of them.

Main definitions #

source
def Cslib.TreeEval.Reader.Frame.equiv :
Iter.Frame ≃ ℕ × Fin 4 × Bool × Fin 3

A frame as a tuple.

Instances For
    source
    def Cslib.TreeEval.Reader.encFrame :
    Iter.Frame ↪ List Bool

    The encoding of frames.

    Instances For
      source
      def Cslib.TreeEval.Reader.Mode.equiv :
      Iter.Mode ≃ Option (Bool × Fin 3)

      A mode as an option.

      Instances For
        source
        @[instance_reducible]
        instance Cslib.TreeEval.Reader.instFinEnumMode :
        FinEnum Iter.Mode
        source
        def Cslib.TreeEval.Reader.encMode :
        Iter.Mode ↪ List Bool

        The encoding of modes.

        Instances For
          source
          def Cslib.TreeEval.Reader.Ctl.toTuple :
          Ctl → Fin 7 × ℕ × ℕ × List ℕ

          The control state as a tuple: a tag, two naturals and a list.

          Instances For
            source
            theorem Cslib.TreeEval.Reader.Ctl.toTuple_injective :
            Function.Injective toTuple
            source
            @[reducible, inline]
            abbrev Cslib.TreeEval.Reader.encCtlTuple :
            Fin 7 × ℕ × ℕ × List ℕ ↪ List Bool

            The encoding of tuples of control states.

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

              The encoding of control states.

              Instances For
                source
                @[reducible, inline]
                abbrev Cslib.TreeEval.Reader.encRegs :
                Regs ↪ List Bool

                The encoding of registers.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.TreeEval.Reader.Tuple :
                  Type

                  The tuples of states.

                  Instances For
                    source
                    def Cslib.TreeEval.Reader.State.toTuple (s : State) :
                    Tuple

                    A state as a tuple.

                    Instances For
                      source
                      theorem Cslib.TreeEval.Reader.State.toTuple_injective :
                      Function.Injective toTuple
                      source
                      @[reducible, inline]
                      abbrev Cslib.TreeEval.Reader.encTuple :
                      Tuple ↪ List Bool

                      The encoding of tuples of states.

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

                        The encoding of states.

                        Instances For
                          source
                          @[simp]
                          theorem Cslib.TreeEval.Reader.encState_apply (s : State) :
                          encState s = encTuple s.toTuple
                          source
                          @[simp]
                          theorem Cslib.TreeEval.Reader.encCtl_apply (c : Ctl) :
                          encCtl c = encCtlTuple c.toTuple