Expressive Logical Combinators for Free - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2013

Expressive Logical Combinators for Free

Pierre Genevès
Nabil Layaïda

Résumé

A popular technique in the static analysis for query languages relies on the construction of compilers that effectively translate queries into logical formulas. These formulas are then solved for satisfiability using an off-the-shelf satisfiability solver. A critical aspect in this approach is the size of the obtained logical formula, since it constitutes a factor that affects the combined complexity of the global approach. We show that a whole class of logical combinators (or ''macros'') can be used as an intermediate language between the query language and the logical language. Those logical combinators provide an exponential gain in succinctness over the corresponding explicit logical representation, yet preserving the typical exponential time complexity of the subsequent logical decision procedure. This opens the way for solving a wide range of problems such as satisfiability and containment for expressive query languages in exponential-time even though their direct formulation into the underlying logic results in an exponential blowup of the formula size, yielding an incorrectly presumed two-exponential time complexity. We illustrate this from a very practical point of view on a few examples such as numerical occurrence constraints and tree frontier properties which are concrete problems found in the XML world.

Domaines

Web
Fichier principal
Vignette du fichier
cc.pdf (353.21 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00868724 , version 1 (01-10-2013)
hal-00868724 , version 2 (08-10-2013)
hal-00868724 , version 3 (11-10-2013)
hal-00868724 , version 4 (06-05-2015)

Identifiants

  • HAL Id : hal-00868724 , version 3

Citer

Pierre Genevès, Nabil Layaïda, Alan Schmitt. Expressive Logical Combinators for Free. 2013. ⟨hal-00868724v3⟩
814 Consultations
305 Téléchargements

Partager

Gmail Facebook X LinkedIn More