Documentation

DescriptiveComplexity.Computability.CodeHalt

Drawing a partial recursive code as a concrete instance #

The computable half of the undecidability bridge: a primitive recursive map

Nat.Partrec.Code → FirstOrder.Language.FinStruct codeVocab

whose image is a yes-instance of DescriptiveComplexity.CODEHALT exactly when the code halts on 0 (DescriptiveComplexity.codehalt_toPred_codeStruct).

Nothing here simulates anything: the code is the instance, so the map is a plain tree flattening. DescriptiveComplexity.codeNodes lists the nodes of a code in preorder, each node carrying its constructor tag and the relative offsets of its children – relative, so that the flattening of a subterm is literally a segment of the flattening of the whole (DescriptiveComplexity.Seg), which is what makes the correctness proof an induction on the code and nothing more.

This is exactly what the machine route could not deliver. Mathlib's universal machine Turing.PartrecToTM2.tr is not finite-state, so code ↦ machine instance is not available; code ↦ syntax tree is trivially primitive recursive, and pushes the whole difficulty into CODEHALT ∈ RE, an ordinary membership proof of the catalog (DescriptiveComplexity.Problems.CodeHalt.Membership).

Whence the two results the layer exists for: DescriptiveComplexity.not_computablePred_of_RE_hard, every RE-hard problem is undecidable, and its first instance DescriptiveComplexity.finsat_not_computable, Trakhtenbrot's theorem.

source
@[instance_reducible]
instance DescriptiveComplexity.instDecidableEqSigmaNatRelationsCode :
DecidableEq ((n : ℕ) × FirstOrder.Language.code.Relations n)
Equations
Dependency graph
source
def DescriptiveComplexity.codeVocab :
FirstOrder.Language.code.FinVocab

The vocabulary of code instances, presented: eleven symbols, nine unary and two binary.

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

    Flattening a code into a list of nodes #

    source
    def DescriptiveComplexity.nodeNone :
    ℕ × ℕ × ℕ

    The reading of an index outside the flattening: a tag no constructor carries, and no children.

    Equations
    Instances For
      Dependency graph
      source
      def DescriptiveComplexity.codeNodes :
      Nat.Partrec.Code → List (ℕ × ℕ × ℕ)

      The nodes of a code, in preorder. Each node carries its constructor tag and the offsets of its children relative to itself, 0 meaning “no such child”. Relative offsets are what make the flattening of a subterm a segment of the flattening of the whole.

      Equations
      Instances For
        Dependency graph

        Segments #

        The instance a code draws #

        source
        def DescriptiveComplexity.tagAt (L : List (ℕ × ℕ × ℕ)) (i : ℕ) :
        ℕ

        The constructor tag of the node at index i.

        Equations
        Instances For
          Dependency graph
          source
          def DescriptiveComplexity.off1At (L : List (ℕ × ℕ × ℕ)) (i : ℕ) :
          ℕ

          The offset of the first child of the node at index i, 0 for none.

          Equations
          Instances For
            Dependency graph
            source
            def DescriptiveComplexity.off2At (L : List (ℕ × ℕ × ℕ)) (i : ℕ) :
            ℕ

            The offset of the second child of the node at index i, 0 for none.

            Equations
            Instances For
              Dependency graph
              source
              def DescriptiveComplexity.codeRelBool (L : List (ℕ × ℕ × ℕ)) {n : ℕ} :
              FirstOrder.Language.code.Relations n → (Fin n → Fin (L.length + 1)) → Bool

              The relations a list of nodes denotes.

              Equations
              Instances For
                Dependency graph
                source
                def DescriptiveComplexity.listStruct (L : List (ℕ × ℕ × ℕ)) :
                FirstOrder.Language.FinStruct codeVocab

                The instance a list of nodes draws. One element per node, and one spare element at the end which carries no mark – out-of-range readings return DescriptiveComplexity.nodeNone, whose tag is no constructor's.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Dependency graph
                  source
                  def DescriptiveComplexity.codeStruct (c : Nat.Partrec.Code) :
                  FirstOrder.Language.FinStruct codeVocab

                  The instance a code draws.

                  Equations
                  Instances For
                    Dependency graph
                    source
                    @[simp]
                    theorem DescriptiveComplexity.card_listStruct (L : List (ℕ × ℕ × ℕ)) :
                    (listStruct L).card = L.length + 1
                    Dependency graph

                    The instance a code draws does draw it #

                    The instance a code draws is well formed #

                    The instance draws the code, and nothing else #

                    source
                    theorem DescriptiveComplexity.codehalt_toPred_codeStruct (c : Nat.Partrec.Code) :
                    CODEHALT.toPred codeVocab (codeStruct c) ↔ (c.eval 0).Dom
                    Dependency graph

                    The map is primitive recursive #

                    Undecidability #

                    source
                    theorem DescriptiveComplexity.not_computablePred_codehalt :
                    ¬ComputablePred (CODEHALT.toPred codeVocab)

                    CODEHALT is undecidable. Mathlib's halting problem maps into it by the tree encoding, which is primitive recursive, so a decision procedure for the concrete instances would decide whether a partial recursive code halts. Registered in the Lax archive as Lax624099.HaltingUndecidable.codehalt_not_computable.

                    Dependency graph
                    source
                    theorem DescriptiveComplexity.not_computablePred_of_RE_hard {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (hP : RE.Hard P) (V : L.FinVocab) :
                    ¬ComputablePred (P.toPred V)

                    An RE-hard problem is undecidable. Hardness in this library is cofinal, so an RE-hard problem is in particular a target of CODEHALT, which is undecidable; and a first-order reduction is a computable many-one reduction of the induced sets (DescriptiveComplexity.not_computablePred_of_relOrderedReduction).

                    This is the leverage the whole DescriptiveComplexity.Computability layer exists for: every completeness theorem for RE now yields undecidability with no computability work of its own. Registered in the Lax archive as Lax624099.REHardUndecidable.not_computablePred_of_RE_hard.

                    Dependency graph
                    source
                    theorem DescriptiveComplexity.finsat_not_computable :
                    ¬ComputablePred (FINSAT.toPred finsatVocab)

                    Trakhtenbrot's theorem: whether a first-order sentence has a finite model is undecidable. Registered in the Lax archive as Lax624099.Trakhtenbrot.finsat_not_computable.

                    Dependency graph