Prove that building a DFA using derivatives terminates #139
Description
Prove that building a DFA using derivatives terminates
In Brozozowski's original paper (also easier to read in Owens' paper), it is mentioned that building a DFA using derivatives terminates, if we incorporate the following simplification rules:
- r | r = r (idempotent)
- r | s = s | r (commutative)
- (r | s) | t = r | (s | t) (associative)
This issue is created for the task of proving that building a DFA with derivatives does in fact terminate.
It is probably worth reading the paper "Stop when you are almost-full: Adventures in constructive termination", which has examples of termination proofs in Coq, to get ideas for a strategy on how to implement this proof.
References
- Owens, Scott, John Reppy, and Aaron Turon. "Regular-expression derivatives re-examined." Journal of Functional Programming 19.2 (2009): 173-190.
- Brzozowski, Janusz A. "Derivatives of regular expressions." Journal of the ACM (JACM) 11.4 (1964): 481-494.
- Vytiniotis, Dimitrios, Thierry Coquand, and David Wahlstedt. "Stop when you are almost-full: Adventures in constructive termination." Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings 3. Springer Berlin Heidelberg, 2012.