/cs420-library

Primary LanguageCoqMIT LicenseMIT

Introduction to the Theory of Computation

The Turing project aims to offer the foundations of the Theory of Computation formalized in Coq. This includes results on

  • Formal languages: common operators and language equality results
  • Regular languages: regular expressions, pumping lemma
  • Turing machines: acceptance, equality, map-reducibility, decidability.

This project is led by Tiago Cogumbreiro to support teaching an undergraduate course on Theory of Computing, CS 420, at UMass Boston. See Tiago's archives of Fall'20 to access the teaching material.

Installation

Windows

  • Step 1. Install scoop
  • Step 2. Open powershell and run:
> scoop install https://gitlab.com/cogumbreiro/turing/-/raw/master/scoop/turing.json

Unix-based OS

To install the Turing library in your system run these commands:

$ git clone https://gitlab.com/cogumbreiro/turing
$ cd turing
$ ./configure.sh
$ make
$ make install

Updating

Make sure you have already installed Turing in your system.

Windows

  • Step 1. Open a powershell prompt and run
> scoop update turing

Unix-based OS

Then, run the following commands:

$ cd /path/where/you/installed/turing
$ git pull
$ make
$ make install

Coverage

In this project, we are formalizing some content of the textbook Introduction to the Theory of Computation, by Michael Sipser, 3rd edition.

Chapter 1: Regular.v

  • Theorem 1.70: Pumping lemma for regular languages
  • Example 1.73: $\{ 0^n 1^n \mid n \ge 0 \}$ is not regular

Chapter 4: LangDec.v

  • Theorem 4.11: $A_{\mathsf{TM}}$ is undecidable.
  • Corollary 4.18: Some languages are not recognizable.
  • Theorem 4.22: $L$ is decidable iff $L$ is recognizable and co-recognizable
  • Theorem 4.23: $\overline{A}_{\mathsf{TM}}$ is not recognizable.

Chapter 5: LangRed.v

  • Theorem 5.1: $HALT_{\mathsf{TM}}$ is undecidable.
  • Theorem 5.2: $E_{\mathsf{TM}}$ is undecidable.
  • Theorem 5.4: $EQ_{\mathsf{TM}}$ is undedicable.
  • Theorem 5.22: If $A \le_{\mathrm{m}} B$ and $A$ decidable, then $B$ decidable.
  • Theorem 5.28: If $A \le_{\mathrm{m}} B$ and $A$ recognizable, then $B$ recognizable.
  • Corollary 5.29: If $A \le_{\mathrm{m}} B$ and $B$ is undecidable, then $A$ is undecidable.
  • Corollary 5.30: $EQ_{\mathsf{TM}}$ unrecognizable and co-unrecognizable.