Documentation

Complexity.Computability.Machines.Turing.MultiTape.Counting.Alternative

Choosing between native counting machines #

A single native instruction has two ordered occurrences, entering either component without changing the input, tapes or output. Each component then retains its own occurrences and first halt. The inner optional control state denotes the selector; the outer optional configuration state denotes actual halting. They must not be identified.

Main definitions #

Main results #

References #

The sum-of-path-counts construction is standard in counting complexity [Val79b]. The native occurrence semantics and shared program interpreter are credited in MultiTape.Counting.

source
def Turing.MultiTapeCTM.Alternative.mapAction {k : ℕ} {Symbol State State' : Type} (f : State → State') (action : Action k Symbol State) :
Action k Symbol State'

Relabel control while preserving the native halting action.

Instances For
    source
    def Turing.MultiTapeCTM.Alternative.jump {k : ℕ} {Symbol State : Type} (state : State) :
    Action k Symbol State

    A control transfer that leaves every tape, head and output unchanged.

    Instances For
      source
      def Turing.MultiTapeCTM.Alternative.config {k : ℕ} {Symbol State State' : Type} {input : List Symbol} (f : State → State') (cfg : Cfg k Symbol State input) :
      Cfg k Symbol State' input

      A component configuration in the selector's state space.

      Instances For
        source
        theorem Turing.MultiTapeCTM.Alternative.apply_mapAction {k : ℕ} {Symbol State State' : Type} {input : List Symbol} (f : State → State') (action : Action k Symbol State) (cfg : Cfg k Symbol State input) :
        (mapAction f action).apply (config f cfg) = config f (action.apply cfg)
        source
        def Turing.MultiTapeCTM.alternative {k : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapeCTM k Symbol State₀) (second : MultiTapeCTM k Symbol State₁) :
        MultiTapeCTM k Symbol (Option (State₀ ⊕ State₁))

        Choose one of two components in one instruction, preserving both transition occurrences.

        Instances For
          source
          theorem Turing.MultiTapeCTM.Nonblocking.alternative {k : ℕ} {Symbol State₀ State₁ : Type} {first : MultiTapeCTM k Symbol State₀} {second : MultiTapeCTM k Symbol State₁} (hfirst : first.Nonblocking) (hsecond : second.Nonblocking) :
          (first.alternative second).Nonblocking

          The selector and both component phases have an occurrence at every running local view.

          source
          theorem Turing.MultiTapeCTM.runList_alternative_left {k : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (first : MultiTapeCTM k Symbol State₀) (second : MultiTapeCTM k Symbol State₁) (fuel : ℕ) (cfg : Cfg k Symbol State₀ input) :
          (first.alternative second).runList fuel (Alternative.config (some ∘ Sum.inl) cfg) = List.map (Alternative.config (some ∘ Sum.inl)) (first.runList fuel cfg)

          Entering the first component preserves its complete occurrence list.

          source
          theorem Turing.MultiTapeCTM.runList_alternative_right {k : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (first : MultiTapeCTM k Symbol State₀) (second : MultiTapeCTM k Symbol State₁) (fuel : ℕ) (cfg : Cfg k Symbol State₁ input) :
          (first.alternative second).runList fuel (Alternative.config (some ∘ Sum.inr) cfg) = List.map (Alternative.config (some ∘ Sum.inr)) (second.runList fuel cfg)

          Entering the second component preserves its complete occurrence list.

          source
          theorem Turing.MultiTapeCTM.runList_alternative {k : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapeCTM k Symbol State₀) (second : MultiTapeCTM k Symbol State₁) (fuel : ℕ) (input : List Symbol) :
          (first.alternative second).runList (fuel + 1) (Cfg.init (first.alternative second).initial input) = List.map (Alternative.config (some ∘ Sum.inl)) (first.runList fuel (Cfg.init first.initial input)) ++ List.map (Alternative.config (some ∘ Sum.inr)) (second.runList fuel (Cfg.init second.initial input))

          The selector contributes exactly one occurrence of each component, including equal outputs.

          source
          theorem Turing.MultiTapeCTM.branchCount_alternative {k : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapeCTM k Symbol State₀) (second : MultiTapeCTM k Symbol State₁) (verdict : List Symbol → Bool) (fuel : ℕ) (input : List Symbol) :
          (first.alternative second).branchCount verdict (fuel + 1) (Cfg.init (first.alternative second).initial input) = first.branchCount verdict fuel (Cfg.init first.initial input) + second.branchCount verdict fuel (Cfg.init second.initial input)

          Native terminal counts add, even at clocks too short for some component branches.

          source
          theorem Turing.MultiTapeCTM.HaltsWithin.alternative {k : ℕ} {Symbol State₀ State₁ : Type} {first : MultiTapeCTM k Symbol State₀} {second : MultiTapeCTM k Symbol State₁} (hnonfirst : first.Nonblocking) (hnonsecond : second.Nonblocking) (fuel : ℕ) (input : List Symbol) (hfirst : first.HaltsWithin fuel (Cfg.init first.initial input)) (hsecond : second.HaltsWithin fuel (Cfg.init second.initial input)) :
          (first.alternative second).HaltsWithin (fuel + 1) (Cfg.init (first.alternative second).initial input)

          A common sufficient component clock gains exactly one selector instruction.