A Coq Library of Undecidability Proofs

This library contains undecidable problems and mechanised reductions between them. Feel free to contribute or start using the problems!

Existing undecidable problems

• Post correspondence problem (PCP in Problems/PCP.v), good seed
• Halting problems for single-tape and multi-tape Turing machines (Halt in Problems/TM.v)
• Halting problem for Minsky machines (MM_HALTING in Problems/MM.v)
• Halting problem for two counters Minsky machines (MM2_HALTING in Problems/MM2.v) with self-contained explanations, good seed
• Halting problem for Binary Stack Machines (BSM_HALTING in Problems/BSM.v)
• Halting problem for the call-by-value lambda-calculus (eva in Problems/L.v)
• String rewriting (SR in Problems/SR.v)
• Entailment in Elementary Intuitionistic Linear Logic (EILL_PROVABILITY in Problems/ILL.v)
• Entailment in Intuitionistic Linear Logic (ILL_PROVABILITY in Problems/ILL.v)
• Provability in Minimal (Intuitionistic, Classical) First-Order Logic (prv in Problems/FOL.v)
• Validity in Minimal (Intuitionistic, Classical) First-Order Logic (valid in Problems/FOL.v, kvalid in Problems/FOL.v)
• Satisfiability in Intuitionistic (Classical) First-Order Logic (satis in Problems/FOL.v, ksatis in Problems/FOL.v)
• Halting problem for FRACTRAN programs (FRACTRAN_REG_HALTING in Problems/FRACTRAN.v), good seed
• Satisfiability for elementary diophantine constraints (DIO_ELEM_SAT in Problems/DIOPHANTINE.v)
• Hilbert's 10th problem, i.e. solvability of a single diophantine equation (H10 in in Problems/DIOPHANTINE.v)
• Satisfiability of elementary Diophantine constraints of the form x=1, x=y+z or x=y.z without parameters (H10C_SAT in Problems/H10C.v), good seed

How to build

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.

Required packages

You need Coq 8.8.1, 8.8.2 or 8.9.1 built on OCAML > 4.02.3, the Equations package and the MetaCoq package for Coq. If you're 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

Build external libraries

The Undecidability libraries depends on several external libraries. Initialise and build them once as follows:

git submodule update --init --recursive
make deps

Building the undecidability library

• make all builds the library
• 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
• make realclean also removes all build files in the external directory. You have to run make deps again after this.

Published work and technical reports

• 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
• Undecidability of Higher-Order Unification Formalised in Coq. Simon Spies and Yannick Forster. CPP '20. 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. CPP '20. Subdirectory TM. https://github.com/uds-psl/tm-verification-framework/
• Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory. Yannick Forster, Dominik Kirst, Dominik Wehr. LFCS '20. Subdirectory FOLP. https://www.ps.uni-saarland.de/extras/fol-completeness/
• 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 LAM. 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.
• Create a new subdirectory for your project and add your files.
• Add a license for your project.
• Edit the "Existing undecidable problems" and the "Contributors" section in this file
• File a pull request.

Contributors

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