Skip to Main content Skip to Navigation
Conference papers

Regular expression containment as a proof search problem

Abstract : Regular expression containment has recently enjoyed a re- newed interest as a type-theoretic problem. By viewing regular expres- sions as types, it is possible to view containments as functions that coerce one regular expression into another. Containment of a given regular ex- pression in another one is therefore a coercion inference problem. It is not straightforward how to apply here generic proof-theoretic approaches such as those based on the MALL with the least fixpoint. We propose an alternative approach, still a purely syntactic one, to decide contain- ment in reasonable time. We employ the partial derivative construction that, for a regular expression E, yields a syntactic NFA recognising the language of E; and, for a containment E ≤ F , it yields a simulation of E by F , with the empty simulation representing the absence of coercion. We are currently working on a proof of completeness of this optimised coercion search algorithm.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Monday, August 8, 2011 - 9:49:31 PM
Last modification on : Tuesday, October 20, 2020 - 1:04:02 PM
Long-term archiving on: : Wednesday, November 9, 2011 - 2:26:10 AM


Files produced by the author(s)


  • HAL Id : inria-00614042, version 1



Vladimir Komendantsky. Regular expression containment as a proof search problem. PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland. ⟨inria-00614042⟩



Record views


Files downloads