Documentation

Complexity.Computability.USTCON.Reader.Cert

The read machine for undirected connectivity within linear work space #

The halting test, the address and the step of Cslib.USTCON.Reader.machine are tidily computable within work space linear in the length of the encoded state (and the bit read): every step is a bounded number of operations on the numbers and the heads of the lists of the state — comparisons, successors and predecessors, products for the address, divisions by the number of labels, and functions of the finitely many controls, labels and frames. So the step machine simulating the read machine is tidy within space linear in its states and the position of its head (Cslib.USTCON.Reader.tidy_machine).

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.USTCON.Reader.encStepIn :
Tuple × Bool ↪ List Bool

The encoding of the inputs of a step: the tuple and the bit read.

Instances For
    source
    def Cslib.USTCON.Reader.stepBudget (y : Tuple × Bool) :
    ℕ

    The space budget of a step: the length of the encoded tuple and bit.

    Instances For

      Projections #

      Building tuples and lists within the budget #

      The halting test and the address #

      The label of a digit, by a finite-state fold over the binary digits #

      source
      instance Cslib.USTCON.Reader.instNeZeroNatNumLabels :
      NeZero numLabels

      The step of the evaluation #

      The step #

      On states #

      source
      def Cslib.USTCON.Reader.stateBudget (q : State) :
      ℕ

      The space budget of a state: the length of its encoded tuple with a bit.

      Instances For
        source
        theorem Cslib.USTCON.Reader.halt_inSpace :
        Turing.MultiTapeTM.ComputableTidilyInSpace machine.halt encState Turing.MultiTapeTM.encBool stateBudget

        The halting test of machine is tidily computable within the space budget of the state.

        source
        theorem Cslib.USTCON.Reader.addr_inSpace :
        Turing.MultiTapeTM.ComputableTidilyInSpace machine.addr encState (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat) stateBudget

        The address of machine is tidily computable within the space budget of the state.

        source
        theorem Cslib.USTCON.Reader.step_inSpace :
        Turing.MultiTapeTM.ComputableTidilyInSpace (fun (p : State × Bool) => machine.step p.1 p.2) (Turing.MultiTapeTM.encPair encState Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encPair encState Turing.MultiTapeTM.encBits) fun (p : State × Bool) => stateBudget p.1

        The step of machine, on a state and the bit read, is tidily computable within the space budget of the state.

        source
        theorem Cslib.USTCON.Reader.tidy_machine :
        ∃ (T : State → ℕ), machine.toStepMachine.Tidy (Turing.MultiTapeTM.encPair encState Turing.MultiTapeTM.encNat) (Turing.ReadMachine.stateT encState T stateBudget) (Turing.ReadMachine.stateS encState stateBudget)

        The step machine simulating the read machine is tidy, within the space of its states together with the position of its head.