Tata Institute of Fundamental Research
Building Certificates of Regular Expressions Equivalence
Seminar
Speaker:
Benoit Razet
Tata Institute of Fundamental Research
School of Technology and Computer Science
Homi Bhabha Road
Date:
Wednesday, 16 Mar 2011 (all day)
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Regular expressions are mostly known as pattern matching expressions in scripting languages (Perl, sed, awk, etc.). They are also theoretically studied for their strong relationship with Automata Theory. A regular expression denote a language (set of words) and two regular expressions are equivalent when they denote the same language. The equivalence problem is decidable and furthermore, any equivalence can be proved axiomatically. Various such axiomatisations have flourished during the last fifty years, we will survey the most important ones.
Every axiomatisation come together with a proof of completeness of the following form: if two regular expressions are equivalent then there exists proof within the axiomatic system. In principle, when this completeness proof is constructive one can extract from it an algorithm that produces a certificate of the equivalence. We have filled the gap developping a program (written in OCaml) that computes certificates. For this purpose we have designed a domain specific proof system with a language of commands for composing a certificate checkable within this system (this is a joint work with Bodhayan Roy).
| Speaker: | Benoit Razet Tata Institute of Fundamental Research School of Technology and Computer Science Homi Bhabha Road |
| Date: | Wednesday, 16 Mar 2011 (all day) |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
Regular expressions are mostly known as pattern matching expressions in scripting languages (Perl, sed, awk, etc.). They are also theoretically studied for their strong relationship with Automata Theory. A regular expression denote a language (set of words) and two regular expressions are equivalent when they denote the same language. The equivalence problem is decidable and furthermore, any equivalence can be proved axiomatically. Various such axiomatisations have flourished during the last fifty years, we will survey the most important ones.
Every axiomatisation come together with a proof of completeness of the following form: if two regular expressions are equivalent then there exists proof within the axiomatic system. In principle, when this completeness proof is constructive one can extract from it an algorithm that produces a certificate of the equivalence. We have filled the gap developping a program (written in OCaml) that computes certificates. For this purpose we have designed a domain specific proof system with a language of commands for composing a certificate checkable within this system (this is a joint work with Bodhayan Roy).
Every axiomatisation come together with a proof of completeness of the following form: if two regular expressions are equivalent then there exists proof within the axiomatic system. In principle, when this completeness proof is constructive one can extract from it an algorithm that produces a certificate of the equivalence. We have filled the gap developping a program (written in OCaml) that computes certificates. For this purpose we have designed a domain specific proof system with a language of commands for composing a certificate checkable within this system (this is a joint work with Bodhayan Roy).