Documentation

Complexitylib.Interop.Cslib.FromMultiTape.Defs

Simulating CSLib multi-tape machines on Complexitylib machines #

This file defines a Complexitylib machine (TM k) that simulates a binary CSLib multi-tape machine (Turing.MultiTapeTM k Bool S) with the same number of work tapes. It is the converse direction of Complexitylib.Interop.Cslib.MultiTape.

The simulator bridges the two models as follows.

Main definitions #

source
def Complexity.Γ.toCell :
Γ → Option Bool

Read one of our symbols as a binary CSLib cell: □ and ▷ are blank.

Equations
Instances For
    source
    def Complexity.Γw.ofCell :
    Option Bool → Γw

    Store a binary CSLib cell as a writable symbol, with CSLib's blank as □.

    Equations
    Instances For
      source
      def Complexity.Γ.keep :
      Γ → Γw

      The writable symbol that rewrites s unchanged (off the left-end marker).

      Equations
      Instances For
        source
        def Complexity.Dir3.guard (r : Γ) (d : Dir3) :
        Dir3

        Guard a head direction: a head reading ▷ moves right, as TM.δ_right_of_start requires; otherwise it moves in direction d.

        Equations
        Instances For
          source
          inductive Complexity.FromMultiTape.Plan :
          Type

          What a folded work tape still has to do in phases 1 and 2 of a simulated step.

          • idle : Plan

            Nothing more; the head is in place.

          • out : Plan

            One more move right (a move away from the fold, begun in phase 0).

          • inPos : Plan

            On the nonnegative half, moving toward the fold: one more left move, unless the head bumped into ▷, in which case it crosses the fold.

          • inNeg : Plan

            On the negative half, moving toward the fold: one more left move, then a check for ▷ in phase 2.

          • cross : Plan

            Crossing from CSLib cell 0 to cell -1: one more move right.

          Instances For
            source
            @[instance_reducible]
            instance Complexity.FromMultiTape.instDecidableEqPlan :
            DecidableEq Plan
            Equations
            source
            @[instance_reducible]
            instance Complexity.FromMultiTape.instFintypePlan :
            Fintype Plan
            Equations
            • One or more equations did not get rendered due to their size.
            source
            inductive Complexity.FromMultiTape.St (k : ℕ) (S : Type) :
            Type

            The simulator's states, for a CSLib machine with k work tapes and state type S. The sign flags say, for each work tape, whether the CSLib head is at a negative position.

            • init {k : ℕ} {S : Type} : St k S

              Move every head off ▷.

            • run {k : ℕ} {S : Type} (q : S) (sign : Fin k → Bool) : St k S

              Phase 0: simulate one step of CSLib state q.

            • mid1 {k : ℕ} {S : Type} (q : S) (sign : Fin k → Bool) (plan : Fin k → Plan) (inDir : Dir3) : St k S

              Phase 1: continue the moves; CSLib is now in state q.

            • mid2 {k : ℕ} {S : Type} (q : S) (sign : Fin k → Bool) (plan : Fin k → Plan) (inDir : Dir3) : St k S

              Phase 2: finish the moves, including the input head move inDir.

            • halt {k : ℕ} {S : Type} : St k S

              CSLib halted.

            Instances For
              source
              @[instance_reducible]
              instance Complexity.FromMultiTape.instDecidableEqSt {k✝ : ℕ} {S✝ : Type} [DecidableEq S✝] :
              DecidableEq (St k✝ S✝)
              Equations
              source
              def Complexity.FromMultiTape.instDecidableEqSt.decEq {k✝ : ℕ} {S✝ : Type} [DecidableEq S✝] (x✝ x✝¹ : St k✝ S✝) :
              Decidable (x✝ = x✝¹)
              Equations
              Instances For
                source
                def Complexity.FromMultiTape.St.equivSum (k : ℕ) (S : Type) :
                St k S ≃ Unit ⊕ S × (Fin k → Bool) ⊕ S × (Fin k → Bool) × (Fin k → Plan) × Dir3 ⊕ S × (Fin k → Bool) × (Fin k → Plan) × Dir3 ⊕ Unit

                The simulator's states as a sum of finite types.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance Complexity.FromMultiTape.instFintypeSt {k : ℕ} {S : Type} [Fintype S] :
                  Fintype (St k S)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  def Complexity.FromMultiTape.plan0 (s : Bool) :
                  SignType → Plan × Dir3

                  Phase 0 of a folded work-tape move m, on the negative half when s holds: the remaining plan and the first head move.

                  Equations
                  Instances For
                    source
                    def Complexity.FromMultiTape.plan1 (p : Plan) (s : Bool) (r : Γ) :
                    Plan × Bool × Dir3

                    Phase 1 of a folded work-tape move with plan p, sign flag s, and symbol r under the head: the next plan, the next sign flag, and the move.

                    Equations
                    Instances For
                      source
                      def Complexity.FromMultiTape.plan2 (p : Plan) (s : Bool) (r : Γ) :
                      Bool × Dir3

                      Phase 2 of a folded work-tape move with plan p, sign flag s, and symbol r under the head: the next sign flag and the move.

                      Equations
                      Instances For
                        source
                        def Complexity.FromMultiTape.inputPlan (r : Γ) (m : SignType) :
                        Dir3

                        The input head move made in phase 2 to simulate CSLib input move m, where r is the input symbol read in phase 0. On ▷ the head already moved right in phase 0; elsewhere a right move off the right blank is clamped.

                        Equations
                        Instances For
                          source
                          def Complexity.FromMultiTape.writeSym (r : Γ) :
                          Option (Option Bool) → Γw

                          The symbol written in phase 0 for a CSLib write wr over symbol r.

                          Equations
                          Instances For
                            source
                            def Complexity.FromMultiTape.outSym (o : Γ) :
                            Option Bool → Γw

                            The symbol written on our output tape over symbol o when CSLib emits e.

                            Equations
                            Instances For
                              source
                              def Complexity.FromMultiTape.outDir :
                              Option Bool → Dir3

                              The output head move when CSLib emits e: right after each emitted bit.

                              Equations
                              Instances For
                                source
                                def Complexity.FromMultiTape.δ {k : ℕ} {S : Type} (M : Turing.MultiTapeTM k Bool S) (q : St k S) (i : Γ) (w : Fin k → Γ) (o : Γ) :
                                St k S × (Fin k → Γw) × Γw × Dir3 × (Fin k → Dir3) × Dir3

                                The simulator's transition function. Every direction is passed through Dir3.guard, so heads on ▷ always move right.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  theorem Complexity.FromMultiTape.Dir3.guard_start (d : Dir3) :
                                  Dir3.guard Γ.start d = Dir3.right

                                  Guarded directions move right off ▷.

                                  source
                                  def Complexity.FromMultiTape.toTM {k : ℕ} {S : Type} [DecidableEq S] [Fintype S] (M : Turing.MultiTapeTM k Bool S) :
                                  TM k

                                  The Complexitylib machine simulating the binary CSLib machine M, with one folded work tape per CSLib work tape.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For