Every semi-decidable problem reduces to CODEHALT

DescriptiveComplexity.orderedReduction_codehalt: a decision problem whose concrete instances form a recursively enumerable set – in Mathlib's sense, REPred – reduces to DescriptiveComplexity.CODEHALT by an ordered first-order reduction.

This is the pivot of the library's undecidability results: it makes CODEHALT RE-hard (instantiate at a problem already known to be RE-hard) and it makes “RE is exactly the recursively enumerable properties of finite structures” a theorem (instantiate at an arbitrary problem and push membership forward along the reduction). Both readings are drawn in DescriptiveComplexity.Computability.CodeHaltComplete.

Why the code model, and not a machine

The reduction has to produce a program. For a machine that would mean writing a transition table and proving its run correct – the evaluator with addressed storage, the expensive object the library has so far always avoided. Here the program is a Nat.Partrec.Code, and “a program semi-deciding this problem exists” is a theorem of Mathlib (Nat.Partrec.Code.exists_code): the reduction names the procedure cP instead of building it, and only has to write the instance beside it, as the argument of one comp.

The three pieces

• the value the instance is written as, and its decoding (DescriptiveComplexity.structVal, DescriptiveComplexity.structOf, in DescriptiveComplexity.Problems.CodeHalt.Hardness.Value);
• the drawing of comp cP (pair numeral nest) as a first-order interpretation (DescriptiveComplexity.codeProgInterp, in DescriptiveComplexity.Problems.CodeHalt.Hardness.Interp) and its correctness (DescriptiveComplexity.decodesTo_rootPt, DescriptiveComplexity.codeWF_codeProg, in DescriptiveComplexity.Problems.CodeHalt.Hardness.Draw);
• the two lines this file adds: evaluating the drawn code is running cP on the value, and decoding the value gives the instance back.

The drawn code computes the value of the instance

theorem DescriptiveComplexity.eval_drawnCode {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (cP.comp ((numCode (Nat.card A)).pair (codeNestFrom (blockCode V (Nat.card A) (⇑(ordEnum A)) (botTup V A)) 0))).eval 0 = cP.eval (structVal V (Nat.card A) (⇑(ordEnum A)) (botTup V A))

The drawn code runs the procedure on the value of the instance. Every branch is evaluated at input 0, so the argument of the comp is a constant: the pair of the numeral of the universe size with the nest of the tables.

theorem DescriptiveComplexity.codehalt_codeProg {L : FirstOrder.Language} (V : L.FinVocab) (cP : Nat.Partrec.Code) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : CODEHALT.Holds ((codeProgInterp V cP).Map A) ↔ (cP.eval (structVal V (Nat.card A) (⇑(ordEnum A)) (botTup V A))).Dom

The instance is a yes-instance of CODEHALT exactly when the procedure halts on the value of the instance.

The value is decoded back into the instance

theorem DescriptiveComplexity.toPred_structOf_structVal {L : FirstOrder.Language} [L.IsRelational] (V : L.FinVocab) {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (P : DecisionProblem L) : P.toPred V (structOf V (structVal V (Nat.card A) (⇑(ordEnum A)) (botTup V A))) ↔ P.Holds A

Decoding the value of an instance answers about the instance.

The reduction

theorem DescriptiveComplexity.orderedReduction_codehalt {L : FirstOrder.Language} [L.IsRelational] {V : L.FinVocab} (P : DecisionProblem L) (h : REPred (P.toPred V)) : Nonempty (OrderedFOReduction P CODEHALT)

A semi-decidable problem reduces to CODEHALT. The reduction draws the instance as the program comp cP (pair numeral nest), where cP is a code semi-deciding the problem – which Nat.Partrec.Code.exists_code supplies – and the rest is a constant the first-order formulas can write.