Documentation

DescriptiveComplexity.Problems.Machine.HaltHard.Bridge

The simulating machine as rewriting, and the transport to a drawn machine #

Two bridges. The first identifies runs of the zipper semantics (DescriptiveComplexity.HaltHard.lstep) with derivations of the rewriting system DescriptiveComplexity.HaltPcp.MRule of the machine packaged as a DescriptiveComplexity.TMData (DescriptiveComplexity.HaltHard.simTM, over the three-block universe DescriptiveComplexity.HaltHard.SimU – states, symbols, and one transition per applicable state–symbol pair; the machine is deterministic, so the pair is the transition). A zipper configuration is a configuration word (DescriptiveComplexity.HaltHard.wordOf), one lstep is one rewriting step, and the boot and halting phases close the two ends: DescriptiveComplexity.HaltHard.derives_startWord_iff_evalDom states the result directly against Turing.ToPartrec.Cont.eval, through DescriptiveComplexity.HaltHard.reach_acc_iff_evalDom.

The second bridge is the rule-correspondence transport: a machine whose predicates are the images of simTM's along an injection (DescriptiveComplexity.HaltHard.TMEmbed – the shape of the machine the interpretation of Interp.lean draws, whose universe also carries the tape positions and the junk) derives the halting word from an image word exactly when simTM does from its preimage (DescriptiveComplexity.HaltHard.TMEmbed.derives_halt_iff). Together with DescriptiveComplexity.HaltPcp.acceptsU_iff_derives on the drawn side, this turns DescriptiveComplexity.TMData.AcceptsU of the drawn machine into termination of the abstract evaluation, with no tape-function bookkeeping.

The universe of the simulating machine #

source
@[reducible, inline]
abbrev DescriptiveComplexity.HaltHard.SimU (c : Turing.ToPartrec.Code) :
Type

The universe of the simulating machine as a DescriptiveComplexity.TMData: states, symbols, and one transition per state–symbol pair the table acts on.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    @[reducible, inline]
    abbrev DescriptiveComplexity.HaltHard.stq {c : Turing.ToPartrec.Code} (q : SimQ c) :
    SimU c

    A state, as an element of the machine universe.

    Equations
    Instances For
      Dependency graph
      source
      @[reducible, inline]
      abbrev DescriptiveComplexity.HaltHard.sts {c : Turing.ToPartrec.Code} (σ : SimSym c) :
      SimU c

      A symbol, as an element of the machine universe.

      Equations
      Instances For
        Dependency graph
        source
        @[reducible, inline]
        abbrev DescriptiveComplexity.HaltHard.stt {c : Turing.ToPartrec.Code} (τ : SimQ c × SimSym c) :
        SimU c

        A transition – a state–symbol pair – as an element of the machine universe.

        Equations
        Instances For
          Dependency graph
          source
          def DescriptiveComplexity.HaltHard.simTM (c : Turing.ToPartrec.Code) :
          TMData (SimU c)

          The simulating machine as machine data: one transition per pair on which the table acts, its attributes read off simStep. The position block is empty – the rewriting system of a machine never mentions positions, and the bridge to a drawn machine goes through words alone.

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

            Zipper configurations as words #

            source
            def DescriptiveComplexity.HaltHard.symsOf {c : Turing.ToPartrec.Code} (l : List (SimSym c)) :
            List (HaltPcp.TapeLetter (SimU c))

            The symbol letters of a run of tape letters.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Dependency graph
              source
              @[simp]
              theorem DescriptiveComplexity.HaltHard.symsOf_nil {c : Turing.ToPartrec.Code} :
              symsOf [] = []
              Dependency graph
              source
              @[simp]
              theorem DescriptiveComplexity.HaltHard.symsOf_cons {c : Turing.ToPartrec.Code} (σ : SimSym c) (l : List (SimSym c)) :
              symsOf (σ :: l) = HaltPcp.TapeLetter.sym (sts σ) :: symsOf l
              Dependency graph
              source
              @[simp]
              theorem DescriptiveComplexity.HaltHard.symsOf_append {c : Turing.ToPartrec.Code} (l l' : List (SimSym c)) :
              symsOf (l ++ l') = symsOf l ++ symsOf l'
              Dependency graph

              Locating the unique marked letter #

              Decoding the attributes of a transition #

              One machine step is one rewriting step #

              Whole runs #

              The boot phase, and the abstract statement #

              source
              theorem DescriptiveComplexity.HaltHard.derives_startWord_iff_evalDom {c : Turing.ToPartrec.Code} {k : PCont c} {fr : List (SimSym c)} (hfr : FrameSeg k fr) (v : List ℕ) (j t : ℕ) :
              Pcp.History.Derives (HaltPcp.MRule (simTM c)) (HaltPcp.startWord (List.map sts (SimSym.endL :: (fr ++ SimSym.mid :: valR v j t)))) [HaltPcp.TapeLetter.halt] ↔ (k.toCont.eval v).Dom

              The abstract bridge: the rewriting system of the simulating machine derives the halting word from the spelled resting configuration of k and v exactly when the abstract evaluation of k on v terminates.

              Dependency graph

              Transport along an injection #

              The machine the interpretation draws has the same states, symbols and transitions, embedded in a larger universe that also carries the tape positions and the junk. Its predicates are the images of the abstract ones, and derivations of the halting word correspond exactly.

              source
              def DescriptiveComplexity.HaltPcp.TapeLetter.map {A B : Type} (f : A → B) :
              TapeLetter A → TapeLetter B

              Mapping the machine elements of a tape letter.

              Equations
              Instances For
                Dependency graph
                source
                structure DescriptiveComplexity.HaltHard.TMEmbed {A B : Type} (f : A → B) (M : TMData A) (N : TMData B) :
                Prop

                A machine embedded in a larger universe: an injection under which every predicate of the target is the image of the corresponding predicate of the source.

                • inj : Function.Injective f

                  The embedding is injective.

                • tr (b : B) : N.Tr b ↔ ∃ (a : A), b = f a ∧ M.Tr a

                  Transitions correspond.

                • start (b : B) : N.Start b ↔ ∃ (a : A), b = f a ∧ M.Start a

                  Start states correspond.

                • acc (b : B) : N.Acc b ↔ ∃ (a : A), b = f a ∧ M.Acc a

                  Accepting states correspond.

                • blank (b : B) : N.Blank b ↔ ∃ (a : A), b = f a ∧ M.Blank a

                  Blanks correspond.

                • right (b : B) : N.Right b ↔ ∃ (a : A), b = f a ∧ M.Right a

                  Directions correspond.

                • src (b b' : B) : N.Src b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Src a a'

                  Source states correspond.

                • read (b b' : B) : N.Read b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Read a a'

                  Read symbols correspond.

                • dst (b b' : B) : N.Dst b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Dst a a'

                  Destination states correspond.

                • write (b b' : B) : N.Write b b' ↔ ∃ (a : A) (a' : A), b = f a ∧ b' = f a' ∧ M.Write a a'

                  Written symbols correspond.

                Instances For
                  Dependency graph

                  Decomposing image words #

                  source
                  theorem DescriptiveComplexity.HaltHard.TMEmbed.derives_halt_iff {A B : Type} {f : A → B} {M : TMData A} {N : TMData B} (h : TMEmbed f M N) {w : List (HaltPcp.TapeLetter A)} :
                  Pcp.History.Derives (HaltPcp.MRule N) (List.map (HaltPcp.TapeLetter.map f) w) [HaltPcp.TapeLetter.halt] ↔ Pcp.History.Derives (HaltPcp.MRule M) w [HaltPcp.TapeLetter.halt]

                  Derivations of the halting word transport along an embedding.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.HaltHard.TMEmbed.derives_iff_evalDom {c : Turing.ToPartrec.Code} {B : Type} {f : SimU c → B} {N : TMData B} (h : TMEmbed f (simTM c) N) {k : PCont c} {fr : List (SimSym c)} (hfr : FrameSeg k fr) (v : List ℕ) (j t : ℕ) :
                  Pcp.History.Derives (HaltPcp.MRule N) (HaltPcp.startWord (List.map f (List.map sts (SimSym.endL :: (fr ++ SimSym.mid :: valR v j t))))) [HaltPcp.TapeLetter.halt] ↔ (k.toCont.eval v).Dom

                  The whole bridge, for a drawn machine: a machine whose predicates are the images of simTM's derives the halting word from the image of the spelled resting configuration exactly when the abstract evaluation terminates.

                  Dependency graph