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.
Type de document :
Communication dans un congrès
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00614042
Contributeur : Assia Mahboubi <>
Soumis le : lundi 8 août 2011 - 21:49:31
Dernière modification le : mercredi 10 août 2011 - 12:48:03
Document(s) archivé(s) le : mercredi 9 novembre 2011 - 02:26:10

Fichier

Komendantsky.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00614042, version 1

Collections

Citation

Vladimir Komendantsky. Regular expression containment as a proof search problem. PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011. 〈inria-00614042〉

Partager

Métriques

Consultations de la notice

113

Téléchargements de fichiers

70