The problem catalog

Umbrella file importing every decision problem of the library. Each problem lives in its own file (or directory) under DescriptiveComplexity/Problems/, containing its vocabulary, its semantic definition, the bundled DescriptiveComplexity.DecisionProblem, its first-order reductions, and its completeness theorems.

Job sequencing is in NP but not yet proved NP-hard, so its umbrella carries only the membership half. Alternating machine acceptance (DescriptiveComplexity.ATMAccept) is the machine bridge for the polynomial hierarchy, complete at every level (DescriptiveComplexity.atmAccept_sigmaP_complete, DescriptiveComplexity.atmAccept_piP_complete) – see DescriptiveComplexity.Problems.MachineAlt. The halting problem (DescriptiveComplexity.HALT, the same machine with the tape unbounded) is RE-complete (DescriptiveComplexity.halt_RE_complete, hardness being the machine bridge of DescriptiveComplexity.Problems.Machine.HaltHard); its membership half alone already gives DescriptiveComplexity.halt_le_finsat, Trakhtenbrot's theorem in the form it is usually stated. The halting of a partial recursive code drawn as a syntax tree (DescriptiveComplexity.CODEHALT) is RE-complete (DescriptiveComplexity.codehalt_RE_complete), and is the problem the undecidability of the development goes through: it is undecidable outright (DescriptiveComplexity.not_computablePred_codehalt), whence DescriptiveComplexity.finsat_not_computable. Its hardness reduction draws the instance as the program that runs a semi-decision procedure on it, which is general enough to identify the class with its machine reading (DescriptiveComplexity.mem_RE_iff_rePred) and to separate it from its complement (DescriptiveComplexity.RE_ne_coRE). Post's correspondence problem (DescriptiveComplexity.PCP) is RE-complete too (DescriptiveComplexity.pcp_RE_complete): membership invents the slots of the sequence of dominoes together with a matching between the two parses of the word it spells, and hardness is the computation-history dominoes from HALT (DescriptiveComplexity.Problems.Pcp.Hardness), whence the undecidability of Post's problem (DescriptiveComplexity.pcp_not_computable).