Skip to content

Latest commit

 

History

History
99 lines (78 loc) · 4.13 KB

README.md

File metadata and controls

99 lines (78 loc) · 4.13 KB

Regular Language Representations in Coq

Docker CI Contributing Code of Conduct Zulip coqdoc DOI

This library provides definitions and verified translations between different representations of regular languages: various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. It also contains various decidability results and closure properties of regular languages.

Meta

Building and installation instructions

The easiest way to install the latest released version of Regular Language Representations in Coq is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-reglang

To instead build and install manually, do:

git clone https://github.com/coq-community/reglang.git
cd reglang
make   # or make -j <number-of-cores-on-your-machine> 
make install

HTML Documentation

To generate HTML documentation, run make coqdoc and point your browser at docs/coqdoc/toc.html.

See also the pregenerated HTML documentation for the latest release.

File Contents

  • misc.v, setoid_leq.v: basic infrastructure independent of regular languages
  • languages.v: languages and decidable languages
  • dfa.v:
    • results on deterministic one-way automata
    • definition of regularity
    • criteria for nonregularity
  • nfa.v: Results on nondeterministic one-way automata
  • regexp.v: Regular expressions and Kleene Theorem
  • minimization.v: minimization and uniqueness of minimal DFAs
  • myhill_nerode.v: classifiers and the constructive Myhill-Nerode theorem
  • two_way.v: deterministic and nondeterministic two-way automata
  • vardi.v: translation from 2NFAs to NFAs for the complement language
  • shepherdson.v: translation from 2NFAs and 2DFAs to DFAs (via classifiers)
  • wmso.v:
    • decidability of WS1S
    • WS1S as representation of regular languages