search

uds-psl / coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.
Mozilla Public License 2.0
111 stars 30 forks source link
coq

readme

Coq Library of Undecidability Proofs

CI

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. A problem P is considered undecidable if its decidability in Coq implies the enumerability of the complement of halting problem for Turing machines (SBTM_HALT in TM/SBTM.v). Since the Turing machine halting is enumerable (SBTM_HALT_enum in TM/SBTM_enum.v), enumerability of its complement would classically imply its decidability.

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. Some advanced problems are proven decidable to contrast negative 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

Advanced Problems

Halting Problems for Traditional Models of Computation

An equivalence proof that most of the mentioned models of computation compute the same n-ary functional relations over natural numbers is available in Models_Equivalent.v.

Problems from Logic

Other Problems

Decidable Problems

Target Problems

Manual Installation Instructions

If you can use opam 2 on your system, you can follow the instructions here.

Install from git via opam

You can use opam to install the current state of this branch as follows.

We recommend creating a fresh opam switch:

opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
eval $(opam env)

Then the following commands install the library:

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam pin add coq-library-undecidability.dev+8.20 "https://github.com/uds-psl/coq-library-undecidability.git#coq-8.20"

Manual installation

You need Coq 8.20 built on OCAML >= 4.09.1 (but we recommend and test OCaml version 4.14.1+flambda) and the Template-Coq part of 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 --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install . --deps-only

Building the undecidability library

Compiled interfaces

The library is compatible with Coq's compiled interfaces (vos) for quick infrastructural access.

Troubleshooting

Coq version

Be careful that this branch only compiles under Coq 8.20. 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

Computability in Constructive Type Theory. Yannick Forster. PhD thesis. https://dx.doi.org/10.22028/D291-35758

Papers and abstracts on problems and proofs included in the library

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

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.

[^1]: Minsky, Marvin Lee. Computation. Englewood Cliffs: Prentice-Hall, 1967.