Documentation

DescriptiveComplexity.Problems.Machine.HaltHard.Tags

The alphabet of the machine simulating a ToPartrec code #

The static data of the RE-hardness of DescriptiveComplexity.HALT (PCP-HARDNESS.md §2): the machine M(c) that the reduction draws simulates the sequential semantics Turing.ToPartrec.step of a fixed code c, so its states and symbols are indexed by the positions of the syntax tree of c – a finite type built by recursion on c, the SubPos pattern of the CODEHALT reduction – and by nothing else. This file carries those positions (DescriptiveComplexity.HaltHard.CPos), the continuations restricted to subcodes (DescriptiveComplexity.HaltHard.PCont), the tape alphabet (DescriptiveComplexity.HaltHard.SimSym) and the encoding of a configuration as a tape word:

bk … bk endL ⟦TOP⟧ gap ⟦…⟧ gap ⟦BASE⟧ gap mid gap ⟦value, mirrored⟧ endR bk …

Every code in a continuation frame reached from stepNormal c … /stepRet is a subcode of c, so the positioned continuations PCont mirror Turing.ToPartrec.Cont with positions for codes; DescriptiveComplexity.HaltHard.PCont.toCont projects back, and the simulation is stated over PCont throughout.

The positions of the syntax tree of a code #

source
def DescriptiveComplexity.HaltHard.CPos :
Turing.ToPartrec.Code → Type

The positions of the syntax tree of a ToPartrec code, by recursion on the code: one tag per node, so that drawing the machine of a fixed code costs nothing at any instance size.

Equations
Instances For
    Dependency graph
    source
    instance DescriptiveComplexity.HaltHard.instFiniteCPos (c : Turing.ToPartrec.Code) :
    Finite (CPos c)
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.HaltHard.instDecidableEqCPos (c : Turing.ToPartrec.Code) :
    DecidableEq (CPos c)
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.HaltHard.cRoot (c : Turing.ToPartrec.Code) :
    CPos c

    The root position.

    Equations
    Instances For
      Dependency graph
      source
      instance DescriptiveComplexity.HaltHard.instNonemptyCPos (c : Turing.ToPartrec.Code) :
      Nonempty (CPos c)
      Dependency graph
      source
      def DescriptiveComplexity.HaltHard.codeAt {c : Turing.ToPartrec.Code} :
      CPos c → Turing.ToPartrec.Code

      The subcode sitting at a position.

      Equations
      Instances For
        Dependency graph
        source
        @[simp]
        theorem DescriptiveComplexity.HaltHard.codeAt_cRoot (c : Turing.ToPartrec.Code) :
        codeAt (cRoot c) = c
        Dependency graph
        source
        def DescriptiveComplexity.HaltHard.child₁ {c : Turing.ToPartrec.Code} :
        CPos c → Option (CPos c)

        The positions of the immediate subterms: the first child of a binary node.

        Equations
        Instances For
          Dependency graph
          source
          def DescriptiveComplexity.HaltHard.child₂ {c : Turing.ToPartrec.Code} :
          CPos c → Option (CPos c)

          The positions of the immediate subterms: the second child of a binary node.

          Equations
          Instances For
            Dependency graph

            The codes at the children #

            The step function dispatches on the code at a position and moves to its children, so the simulation needs to read the child positions' codes off the parent's. The two functions below are the code-level shadows of DescriptiveComplexity.HaltHard.child₁/child₂, and the lemmas identify the two readings.

            source
            def DescriptiveComplexity.HaltHard.lchild? :
            Turing.ToPartrec.Code → Option Turing.ToPartrec.Code

            The left immediate subterm of a code.

            Equations
            Instances For
              Dependency graph
              source
              def DescriptiveComplexity.HaltHard.rchild? :
              Turing.ToPartrec.Code → Option Turing.ToPartrec.Code

              The right immediate subterm of a code.

              Equations
              Instances For
                Dependency graph
                source
                theorem DescriptiveComplexity.HaltHard.codeAt_child₁ {c : Turing.ToPartrec.Code} (p : CPos c) :
                Option.map (fun (q : CPos c) => codeAt q) (child₁ p) = lchild? (codeAt p)

                The code at the first child is the first subterm of the code at the position.

                Dependency graph
                source
                theorem DescriptiveComplexity.HaltHard.codeAt_child₂ {c : Turing.ToPartrec.Code} (p : CPos c) :
                Option.map (fun (q : CPos c) => codeAt q) (child₂ p) = rchild? (codeAt p)

                The code at the second child is the second subterm of the code at the position.

                Dependency graph
                source
                def DescriptiveComplexity.HaltHard.c₁ {c : Turing.ToPartrec.Code} (p : CPos c) :
                CPos c

                The first child of the code at p, defaulting to the root – the default is never taken at the positions the machine visits.

                Equations
                Instances For
                  Dependency graph
                  source
                  def DescriptiveComplexity.HaltHard.c₂ {c : Turing.ToPartrec.Code} (p : CPos c) :
                  CPos c

                  The second child of the code at p.

                  Equations
                  Instances For
                    Dependency graph
                    source
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₁ {c : Turing.ToPartrec.Code} {p : CPos c} {f : Turing.ToPartrec.Code} (h : lchild? (codeAt p) = some f) :
                    codeAt (c₁ p) = f

                    The code at the first child, when the position holds a code with a first subterm.

                    Dependency graph
                    source
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₂ {c : Turing.ToPartrec.Code} {p : CPos c} {g : Turing.ToPartrec.Code} (h : rchild? (codeAt p) = some g) :
                    codeAt (c₂ p) = g

                    The code at the second child, when the position holds a code with a second subterm.

                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₁_cons {c : Turing.ToPartrec.Code} {p : CPos c} {f fs : Turing.ToPartrec.Code} (h : codeAt p = f.cons fs) :
                    codeAt (c₁ p) = f
                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₂_cons {c : Turing.ToPartrec.Code} {p : CPos c} {f fs : Turing.ToPartrec.Code} (h : codeAt p = f.cons fs) :
                    codeAt (c₂ p) = fs
                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₁_comp {c : Turing.ToPartrec.Code} {p : CPos c} {f g : Turing.ToPartrec.Code} (h : codeAt p = f.comp g) :
                    codeAt (c₁ p) = f
                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₂_comp {c : Turing.ToPartrec.Code} {p : CPos c} {f g : Turing.ToPartrec.Code} (h : codeAt p = f.comp g) :
                    codeAt (c₂ p) = g
                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₁_case {c : Turing.ToPartrec.Code} {p : CPos c} {f g : Turing.ToPartrec.Code} (h : codeAt p = f.case g) :
                    codeAt (c₁ p) = f
                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₂_case {c : Turing.ToPartrec.Code} {p : CPos c} {f g : Turing.ToPartrec.Code} (h : codeAt p = f.case g) :
                    codeAt (c₂ p) = g
                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.HaltHard.codeAt_c₁_fix {c : Turing.ToPartrec.Code} {p : CPos c} {f : Turing.ToPartrec.Code} (h : codeAt p = f.fix) :
                    codeAt (c₁ p) = f
                    Dependency graph

                    Continuations over positions #

                    Every code stored in a continuation reached from stepNormal c/stepRet is a subcode of c, so the simulation works with continuations carrying positions and projects back to Turing.ToPartrec.Cont when it meets the library semantics.

                    source
                    inductive DescriptiveComplexity.HaltHard.PCont (c : Turing.ToPartrec.Code) :
                    Type

                    A continuation whose codes are positions of the syntax tree of c.

                    Instances For
                      Dependency graph
                      source
                      def DescriptiveComplexity.HaltHard.PCont.toCont {c : Turing.ToPartrec.Code} :
                      PCont c → Turing.ToPartrec.Cont

                      The continuation a positioned continuation stands for.

                      Equations
                      Instances For
                        Dependency graph

                        The tape alphabet #

                        source
                        inductive DescriptiveComplexity.HaltHard.SimSym (c : Turing.ToPartrec.Code) :
                        Type

                        The tape alphabet of the simulating machine: the blank, the unary digit and the block separator (each with a primed copy for the one non-destructive copy loop), the three markers – the movable endL and endR and the fixed mid – and one header letter per continuation frame shape, the ones carrying a code carrying its position.

                        Instances For
                          Dependency graph
                          source
                          instance DescriptiveComplexity.HaltHard.instFiniteSimSym {c : Turing.ToPartrec.Code} :
                          Finite (SimSym c)
                          Dependency graph

                          Words #

                          source
                          def DescriptiveComplexity.HaltHard.encNum {c : Turing.ToPartrec.Code} (n : ℕ) :
                          List (SimSym c)

                          The word of one number: its unary digits, closed by a separator.

                          Equations
                          Instances For
                            Dependency graph
                            source
                            def DescriptiveComplexity.HaltHard.encVal {c : Turing.ToPartrec.Code} (v : List ℕ) :
                            List (SimSym c)

                            The word of a value, head block leftmost. The value region of the tape holds (encVal v).reverse – blocks in reverse order, each separator before its digits – so that the head block ends at the movable marker endR and every operation on it has the blank half-tape to grow into.

                            Equations
                            Instances For
                              Dependency graph
                              source
                              def DescriptiveComplexity.HaltHard.encFrame {c : Turing.ToPartrec.Code} :
                              PCont c → List (SimSym c)

                              The word of one continuation frame: its header, then its stored value – straight in a cons₁ frame (what the marked copy loop writes), mirrored in a cons₂ frame (what the destructive move of the exchange writes).

                              Equations
                              Instances For
                                Dependency graph
                                source
                                @[simp]
                                theorem DescriptiveComplexity.HaltHard.encNum_ne_nil {c : Turing.ToPartrec.Code} (n : ℕ) :
                                encNum n ≠ []
                                Dependency graph
                                source
                                @[simp]
                                theorem DescriptiveComplexity.HaltHard.length_encNum {c : Turing.ToPartrec.Code} (n : ℕ) :
                                (encNum n).length = n + 1
                                Dependency graph
                                source
                                @[simp]
                                theorem DescriptiveComplexity.HaltHard.encVal_nil {c : Turing.ToPartrec.Code} :
                                encVal [] = []
                                Dependency graph
                                source
                                @[simp]
                                theorem DescriptiveComplexity.HaltHard.encVal_cons {c : Turing.ToPartrec.Code} (n : ℕ) (v : List ℕ) :
                                encVal (n :: v) = encNum n ++ encVal v
                                Dependency graph
                                source
                                theorem DescriptiveComplexity.HaltHard.length_encVal {c : Turing.ToPartrec.Code} (v : List ℕ) :
                                (encVal v).length = v.sum + v.length
                                Dependency graph