Coq Library of Undecidability Proofs

The Coq Library of Undecidability Proofs contains mechanised reductions to establish undecidability results in Coq. The undecidability proofs are based on a synthetic approach to undecidability, where a problem P is considered undecidable if its decidability in Coq would imply the decidability of the halting problem of single-tape Turing machines in Coq. As in the traditional literature, undecidability of a problem P in the library is often established by constructing a many-one reduction from an undecidable problem to P.

For more information on the structure of the library, the synthetic approach, and included problems see Publications below, our Wiki, look at the slides or the recording of the talk on the Coq Library of Undecidability proofs at CoqPL '20.

The library is a collaborative effort, growing constantly and we invite everybody to contribute undecidability proofs!

Problems in the Library

The problems in the library can mostly be categorized into seed problems, advanced problems, and target problems.

Seed problems are simple to state and thus make for good starting points of undecidability proofs, often leading to easier reductions to other problems.

Advanced problems do not work well as seeds, but they highlight the potential of our library as a framework for mechanically checking pen&paper proofs of potentially hard undecidability results.

Target problems are very expressive and thus work well as targets for reduction, with the aim of closing loops in the reduction graph to establish the inter-reducibility of problems.

Seed Problems

• Post correspondence problem (PCP in PCP/PCP.v)
• Halting problem for two counters Minsky machines (MM2_HALTING in MinskyMachines/MM2.v)
• Halting problem for FRACTRAN programs (FRACTRAN_REG_HALTING in FRACTRAN/FRACTRAN.v)
• Satisfiability of elementary Diophantine constraints of the form x = 1, x = y + z or x = y · z (H10C_SAT in DiophantineConstraints/H10C.v)
• Satisfiability of uniform Diophantine constraints of the form x = 1 + y + z · z (H10UC_SAT in DiophantineConstraints/H10C.v)
• One counter machine halting problem (CM1_HALT in CounterMachines/CM1.v), good seed
• Finite multiset constraint solvability (FMsetC_SAT in SetConstraints/FMsetC.v), good seed

Advanced Problems

Halting Problems for Traditional Models of Computation

• Halting problem for the call-by-value lambda-calculus (HaltL in L/L.v)
• Halting problem for multi-tape Turing machines (HaltMTM in TM/TM.v)
• Halting problem for single-tape Turing machines (HaltTM 1 in TM/TM.v)
• Halting problem for simple binary single-tape Turing machines (HaltSBTM) in TM/SBTM.v
• Halting problem for Binary Stack Machines (BSM_HALTING in StackMachines/BSM.v)
• Halting problem for Minsky machines (MM_HALTING in MinskyMachines/MM.v)
• Halting problem for FRACTRAN programs (FRACTRAN_REG_HALTING in FRACTRAN/FRACTRAN.v)

Problems from Logic

• Provability in Minimal, Intuitionistic, and Classical First-Order Logic (FOL*_prv_intu, FOL_prv_intu, FOL_prv_class in FOL/FOL.v)
• Validity in Minimal and Intuitionistic First-Order Logic (FOL*_valid, FOL_valid_intu in FOL/FOL.v)
• Satisfiability in Minimal and Intuitionistic First-Order Logic (FOL*_satis, FOL_satis_intu in FOL/FOL.v)
• Finite satisfiability in First-Order Logic, known as "Trakhtenbrot's theorem" (FSAT in TRAKHTENBROT/red_utils.v)
• Entailment in Elementary Intuitionistic Linear Logic (EILL_PROVABILITY in ILL/EILL.v)
• Entailment in Intuitionistic Linear Logic (ILL_PROVABILITY in ILL/ILL.v)
• Entailment in Classical Linear Logic (CLL_cf_PROVABILITY in ILL/CLL.v)
• Entailment in Intuitionistic Multiplicative Sub-Exponential Linear Logic (IMSELL_cf_PROVABILITY3 in ILL/IMSELL.v)
• Provability in Hilbert-style calculi (HSC_PRV in HilbertCalculi/HSC.v)
• Recognizing axiomatizations of Hilbert-style calculi (HSC_AX in HilbertCalculi/HSC.v)

Other Problems

• Acceptance problem for two counters non-deterministic Minsky machines (ndMM2_ACCEPT in MinskyMachines/ndMM2.v)
• String rewriting in Semi-Thue and Thue-systems (SR and TSR in StringRewriting/SR.v)
• String rewriting in Post canonical systems in normal form (PCSnf in StringRewriting/PCSnf.v)
• Hilbert's 10th problem, i.e. solvability of a single diophantine equation (H10 in H10/H10.v)
• Solvability of linear polynomial (over N) constraints of the form x = 1, x = y + z, x = X · y (LPolyNC_SAT in PolynomialConstraints/LPolyNC.v)
• One counter machine halting problem (CM1_HALT in CounterMachines/CM1.v),
• Finite multiset constraint solvability (FMsetC_SAT in SetConstraints/FMsetC.v)
• Uniform boundedness of deterministic, length-preserving stack machines (SMNdl_UB in StackMachines/SMN.v)
• Semi-unification (SemiU in SemiUnification/SemiU.v)
• System F Inhabitation (SysF_INH in SystemF/SysF.v), System F Typability (SysF_TYP in SystemF/SysF.v), System F Type Checking (SysF_TC in SystemF/SysF.v)

Target Problems

• Halting problem for the call-by-value lambda-calculus (HaltL in L/L.v)
• Provability or satisfiability in First-Order Logic (all problems in FOL/FOL.v)

Installation Instructions

If you can use opam 2 on your system, you can follow the instructions here. If you cannot use opam 2, you can use the noopam branch of this repository, which has no dependencies, but less available problems.

Install from opam

We recommend creating a fresh opam switch:

opam switch create coq-library-undecidability 4.07.1+flambda
eval $(opam env)

Then the following commands install the library:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-library-undecidability.1.0.0+8.12

Manual installation

You need Coq 8.12 built on OCAML >= 4.07.1, the Smpl package, the Equations package, and the MetaCoq package for Coq. If you are using opam 2 you can use the following commands to install the dependencies on a new switch:

opam switch create coq-library-undecidability 4.07.1+flambda
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only

Building the undecidability library

• make all builds the library
• make TM/TM.vo compiles only the file theories/TM/TM.v and its dependencies
• make html generates clickable coqdoc .html in the website subdirectory
• make clean removes all build files in theories and .html files in the website directory

Troubleshooting

Windows

If you use Visual Studio Code on Windows 10 with Windows Subsystem for Linux (WSL), then local opam switches may cause issues. To avoid this, you can use a non-local opam switch, i.e. opam switch create 4.07.1+flambda.

Coq version

Be careful that this branch only compiles under Coq 8.12. If you want to use a different Coq version you have to change to a different branch. Due to compatibility issues, not every branch contains exactly the same problems. We recommend to use the newest branch if possible.

Publications

Papers and abstracts on the library

A Coq Library of Undecidable Problems. Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, Maximilian Wuttke. CoqPL '20. https://popl20.sigplan.org/details/CoqPL-2020-papers/5/A-Coq-Library-of-Undecidable-Problems

Papers and abstracts on problems and proofs included in the library

• Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. Dominik Kirst and Dominique Larchey-Wendkling. IJCAR 2020. Subdirectory TRAKTHENBROT. https://www.ps.uni-saarland.de/extras/fol-trakh/
• Undecidability of Semi-Unification on a Napkin. Andrej Dudenhefner. FSCD 2020. Subdirectory SemiUnification. https://www.ps.uni-saarland.de/Publications/documents/Dudenhefner_2020_Semi-unification.pdf
• Undecidability of Higher-Order Unification Formalised in Coq. Simon Spies and Yannick Forster. Technical report. Subdirectory HOU. https://www.ps.uni-saarland.de/Publications/details/SpiesForster:2019:UndecidabilityHOU.html
• Verified Programming of Turing Machines in Coq. Yannick Forster, Fabian Kunze, Maximilian Wuttke. Technical report. Subdirectory TM. https://github.com/uds-psl/tm-verification-framework/
• Hilbert's Tenth Problem in Coq. Dominique Larchey-Wendling and Yannick Forster. FSCD '19. Subdirectory H10. https://uds-psl.github.io/H10
• A certifying extraction with time bounds from Coq to call-by-value lambda-calculus. ITP '19. Subdirectory L. https://github.com/uds-psl/certifying-extraction-with-time-bounds
• Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines. Yannick Forster and Dominique Larchey-Wendling. CPP '19. Subdirectory ILL. http://uds-psl.github.io/ill-undecidability/
• On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. Yannick Forster, Dominik Kirst, and Gert Smolka. CPP '19. Subdirectory FOL. https://www.ps.uni-saarland.de/extras/fol-undec
• Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. Fabian Kunze, Gert Smolka, and Yannick Forster. APLAS 2018. Subdirectory L/AbstractMachines. https://www.ps.uni-saarland.de/extras/cbvlcm2/
• Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic. Yannick Forster and Dominique Larchey-Wendling. LOLA 2018. Subdirectory ILL. https://www.ps.uni-saarland.de/~forster/downloads/LOLA-2018-coq-library-undecidability.pdf
• Verification of PCP-Related Computational Reductions in Coq. Yannick Forster, Edith Heiter, and Gert Smolka. ITP 2018. Subdirectory PCP. https://ps.uni-saarland.de/extras/PCP
• Call-by-Value Lambda Calculus as a Model of Computation in Coq. Yannick Forster and Gert Smolka. Journal of Automated Reasoning (2018) Subdirectory L. https://www.ps.uni-saarland.de/extras/L-computability/

How to contribute

Fork the project on GitHub, add a new subdirectory for your project and your files, then file a pull request. We have guidelines for the directory structure of projects.

Contributors

• Yannick Forster
• Dominique Larchey-Wendling
• Andrej Dudenhefner
• Edith Heiter
• Dominik Kirst
• Fabian Kunze
• Gert Smolka
• Simon Spies
• Dominik Wehr
• Maximilian Wuttke

Parts of the Coq Library of Undecidability Proofs reuse generic code initially developed as a library for the lecture "Introduction to Computational Logics" at Saarland University, which was written by a subset of the above contributors, Sigurd Schneider, and Jan Christian Menz.