Documentation

Complexity.Computability.TreeEval.Reader.Tuple

The Tree Evaluation read machine on tuples #

The halting test, the address and the step of Cslib.TreeEval.Reader.machine, written on the tuples of Cslib.TreeEval.Reader.State.toTuple as chains of tests on finite tags. In this form they are built from basic functions, which is how their work space is bounded.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.TreeEval.Reader.Tuple.ell (x : Tuple) :
ℕ

The value length.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.TreeEval.Reader.Tuple.height (x : Tuple) :
    ℕ

    The height.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.TreeEval.Reader.Tuple.p (x : Tuple) :
      ℕ

      The prime.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.TreeEval.Reader.Tuple.regs (x : Tuple) :
        Regs

        The registers.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.TreeEval.Reader.Tuple.stack (x : Tuple) :
          List Iter.Frame

          The stack.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.TreeEval.Reader.Tuple.mode (x : Tuple) :
            Iter.Mode

            The mode.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.TreeEval.Reader.Tuple.tag (x : Tuple) :
              Fin 7

              The tag of the control state.

              Instances For
                source
                @[reducible, inline]
                abbrev Cslib.TreeEval.Reader.Tuple.n₁ (x : Tuple) :
                ℕ

                The first number of the control state.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.TreeEval.Reader.Tuple.n₂ (x : Tuple) :
                  ℕ

                  The second number of the control state.

                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Cslib.TreeEval.Reader.Tuple.acc (x : Tuple) :
                    List ℕ

                    The list of the control state.

                    Instances For
                      source
                      @[reducible, inline]
                      abbrev Cslib.TreeEval.Reader.Tuple.withCtl (x : Tuple) (c : Fin 7 × ℕ × ℕ × List ℕ) :
                      Tuple

                      A tuple with a new control state.

                      Instances For
                        source
                        @[reducible, inline]
                        abbrev Cslib.TreeEval.Reader.runCtl :
                        Fin 7 × ℕ × ℕ × List ℕ

                        The control tuple of run.

                        Instances For
                          source
                          def Cslib.TreeEval.Reader.offsetT (x : Tuple) (st : List Iter.Frame) :
                          ℕ

                          The offset in the encoding of the node at the path of a stack.

                          Instances For
                            source
                            def Cslib.TreeEval.Reader.haltT (x : Tuple) :
                            Bool

                            The halting test on tuples.

                            Instances For
                              source
                              def Cslib.TreeEval.Reader.addrT (x : Tuple) :
                              Option ℕ

                              The address on tuples.

                              Instances For
                                source
                                def Cslib.TreeEval.Iter.Mode.isCall :
                                Mode → Bool

                                Whether a mode is a call.

                                Instances For
                                  source
                                  def Cslib.TreeEval.Iter.Mode.neg :
                                  Mode → Bool

                                  The sign of a call.

                                  Instances For
                                    source
                                    def Cslib.TreeEval.Iter.Mode.target :
                                    Mode → Fin 3

                                    The target of a call.

                                    Instances For
                                      source
                                      @[reducible, inline]
                                      abbrev Cslib.TreeEval.Reader.dfr :
                                      Iter.Frame

                                      The default frame, standing for the top of an empty stack.

                                      Instances For
                                        source
                                        @[reducible, inline]
                                        abbrev Cslib.TreeEval.Reader.Tuple.with (x : Tuple) (R : Regs) (st : List Iter.Frame) (m : Iter.Mode) (c : Fin 7 × ℕ × ℕ × List ℕ) :
                                        Tuple

                                        The tuple with new registers, stack, mode and control state.

                                        Instances For
                                          source
                                          def Cslib.TreeEval.Reader.runStepT (x : Tuple) :
                                          Tuple × List Bool

                                          The steps of the iterative procedure on tuples.

                                          Instances For
                                            source
                                            def Cslib.TreeEval.Reader.stepT (y : Tuple × Bool) :
                                            Tuple × List Bool

                                            The step on tuples, given the bit read.

                                            Instances For
                                              source
                                              theorem Cslib.TreeEval.Reader.haltT_toTuple (s : State) :
                                              haltT s.toTuple = machine.halt s

                                              On the tuple of a state, haltT is the halting test of machine.

                                              source
                                              theorem Cslib.TreeEval.Reader.addrT_toTuple (s : State) :
                                              addrT s.toTuple = addr s

                                              On the tuple of a state, addrT is the address addr of the state.

                                              source
                                              theorem Cslib.TreeEval.Reader.stepT_toTuple (s : State) (b : Bool) :
                                              stepT (s.toTuple, b) = ((machine.step s b).1.toTuple, (machine.step s b).2)

                                              On the tuple of a state, stepT is the step of machine: it gives the tuple of the next state and the same output.