Documentation

Complexity.Computability.Machines.Turing.MultiTape.Universal.Machine

The universal machine #

The universal function takes a description of a multi-tape machine, an input given by symbol numbers, and a number of steps in binary, and returns the output of the described machine after that many steps and whether it has halted by then. One machine computes it for every multi-tape machine, whatever its number of work tapes, states and symbols (Turing.MultiTapeTM.Universal.universal_desc).

For t steps, a description of encoded length D, an input of encoded length N, and a binary clock of length L, the time certificate is O((t + 1) * (stepBound D N t + runBound D N t + (L + 1)^2) + (I + 1)^2), where I is the complete encoded input length. The space certificate is O(runBound D N t + I). The simulation iterates a step, counting down t in binary, and keeps the description, the input, the configuration and the output so far. The setup term is included even when the clock is zero.

Main definitions #

Main results #

source
def Turing.MultiTapeTM.Universal.universal (i : Desc × List ℕ × ℕ) :
List ℕ × Bool

The universal function: the output of the machine described by i.1 on the input i.2.1 after i.2.2 steps, and whether it has halted.

Instances For
    source
    @[reducible, inline]
    abbrev Turing.MultiTapeTM.Universal.eIn :
    Desc × List ℕ × ℕ ↪ List Bool

    The encoding of inputs of the universal function, with the number of steps in binary.

    Instances For
      source
      @[reducible, inline]
      abbrev Turing.MultiTapeTM.Universal.eOut :
      List ℕ × Bool ↪ List Bool

      The encoding of outputs of the universal function.

      Instances For
        source
        @[reducible, inline]
        abbrev Turing.MultiTapeTM.Universal.eRun :
        Ctx × List ℕ ↪ List Bool

        The state of the simulation: the context of a step and the output so far.

        Instances For
          source
          def Turing.MultiTapeTM.Universal.round (s : Ctx × List ℕ) :
          Ctx × List ℕ

          A round of the simulation: a step, collecting the emitted symbol.

          Instances For
            source
            theorem Turing.MultiTapeTM.Universal.init_inO :
            ComputableTidilyInO init eDesc eCfg (fun (d : Desc) => ((eDesc d).length + 1) ^ 2) fun (d : Desc) => (eDesc d).length + 1

            The initial configuration, within time quadratic and space linear in the length of the description.

            source
            @[reducible, inline]
            abbrev Turing.MultiTapeTM.Universal.runBound (D N t : ℕ) :
            ℕ

            The bound on the state of the simulation after t steps: the context and the output.

            Instances For
              source
              theorem Turing.MultiTapeTM.Universal.computableTidilyInO_universal :
              ComputableTidilyInO universal eIn eOut (fun (i : Desc × List ℕ × ℕ) => (i.2.2 + 1) * (stepBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + runBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + ((encNat i.2.2).length + 1) ^ 2) + ((eIn i).length + 1) ^ 2) fun (i : Desc × List ℕ × ℕ) => runBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + (eIn i).length

              The time and space of the universal function, for a description of length D, an input of encoded length N and t steps: time O((t + 1) * (stepBound D N t + runBound D N t)) and space O(runBound D N t), plus terms in the length of the encoded input.

              source
              theorem Turing.MultiTapeTM.Universal.universal_desc {k : ℕ} {Symbol S : Type} [Fintype S] [Fintype Symbol] (eS : S ↪ ℕ) (eY : Symbol ↪ ℕ) (tm : MultiTapeTM k Symbol S) (x : List Symbol) (t : ℕ) :
              universal (desc eS eY tm, List.map (⇑eY) x, t) = (List.map (⇑eY) (runFrom (tm.initCfg x) t).output, (runFrom (tm.initCfg x) t).state.isNone)

              On the description of a machine, the universal function returns the numbered output of the machine after the given number of steps, and whether it has halted.