Regular expression containment as a proof search problem - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Regular expression containment as a proof search problem

Résumé

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.
Fichier principal
Vignette du fichier
Komendantsky.pdf (202.68 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00614042 , version 1 (08-08-2011)

Identifiants

  • HAL Id : inria-00614042 , version 1

Citer

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⟩

Collections

PSATTT11
92 Consultations
130 Téléchargements

Partager

Gmail Facebook X LinkedIn More