Finite Automata Theory in Coq
A constructive proof of Kleene's theorem
Abstract:
We describe here a development in the Coq proof assistant of a piece of
Finite Automata Theory. The main result is the Kleene's theorem,
expressing that regular expressions and finite automata define the same
languages. From a constructive proof of this result, we automatically
obtain a functional program that compiles any regular expression into
a finite automata, which constitutes the main part of the
implementation of grep-like programs. This functional program is
obtained by the automatic method of extraction which removes the
logical parts of the proof to keep only its informative contents.
Starting with an idea of what we would have written in ML,
we write the specification and do the proofs in such a way that we obtain
the expected program, which is therefore efficient.
A research report is available.
Get it.
BibTeX.
Source of the development
The whole Coq development will be soon available from this page.
Computational meaning of the proof
From the constructive proof of this theorem, we automatically obtain
a certified Caml program (which realizes the specification).
To get more details about the process of extraction in the Coq system,
you may have a look at the documentation (available by FTP with the
system) : Execution of extracted programs in Caml and Gofer.
Here is the program we obtain :
The Caml program extracted from the proof
Test of the extracted program
In order to test the extracted program, we first define some pretty-printers
for various types, to make the results easier to read
(file test.ml).
Here are the results for the following regular expressions:
Jean-Christophe Filliâtre
(formatted with yamlpp).