Résumé technique : Réponse aux requêtes orientée but sur les dépendances du premier et du second ordre avec égalité

1. Énoncé du problème

Les dépendances dans les bases de données sont utilisées pour exprimer des contraintes d'intégrité, gérer l'incomplétude des données et spécifier des transformations de schéma. Bien que les dépendances du premier ordre (telles que les dépendances générant des tuples (TGDs) et les dépendances générant des égalités (EGDs)) soient standard, les dépendances du second ordre (SO) sont nécessaires pour exprimer la composition de certaines classes de mappages de schémas. Lorsqu'elles sont étendues par des atomes d'égalité dans les conséquents, les dépendances SO peuvent exprimer des compositions de mappages de schémas hautement expressifs.

L'approche standard pour répondre aux requêtes sur de telles dépendances consiste à calculer un modèle universel en utilisant une variante de l'algorithme de chase. Cependant, cette approche présente des limitations significatives :

1. Inefficacité : Le calcul du modèle universel complet génère souvent un grand nombre d'inférences sans rapport avec une requête spécifique.
2. Passage à l'échelle : Si les données changent fréquemment, le recalcul complet du chase est prohibitivement coûteux.
3. Complexité de l'égalité : Les techniques orientées but existantes (comme les Magic Sets) peinent avec les dépendances contenant des égalités et des variables fonctionnelles. Les approches naïves qui axiomatisent explicitement l'égalité (en utilisant la congruence et les axiomes de réflexivité fonctionnelle) conduisent à un raisonnement inefficace et à des calculs de point fixe non terminants en raison de la prolifération d'inférences redondantes.

L'article aborde le problème ouvert consistant à développer une technique efficace de réponse aux requêtes orientée but pour les dépendances du premier et du second ordre avec égalité, évitant les inférences inutiles tout en garantissant la correction et la terminaison.

2. Méthodologie

Les auteurs proposent une approche basée sur la transformation qui modifie les dépendances d'entrée afin qu'un calcul de chase ultérieur réponde à la requête tout en minimisant les inférences sans rapport. La technique est mise en œuvre sous forme de pipeline (Algorithme 1) composé de sept étapes clés :

2.1 Élimination de la quantification du second ordre

La dépendance SO d'entrée $\Sigma$ est transformée en un ensemble de formules du premier ordre (FO) ($\Sigma_1$) en supprimant les quantificateurs du second ordre et en convertissant les variables fonctionnelles en symboles fonctionnels. Cette transformation préserve les réponses aux requêtes, permettant aux étapes ultérieures d'opérer dans le cadre de la logique du premier ordre, bien qu'avec des symboles fonctionnels.

2.2 Singularisation

Pour gérer l'égalité efficacement sans la surcharge des axiomes de congruence complets, les auteurs appliquent une variante novatrice de la singularisation (étendant le travail de Marnette).

• Mécanisme : La technique modifie les corps des dépendances pour « élaguer » les inférences redondantes. Au lieu d'utiliser des axiomes de congruence pour copier des faits à travers des termes égaux, les dépendances sont réécrites pour joindre explicitement les atomes via l'égalité.
• Correction d'un travail antérieur : Les auteurs identifient une incomplétude dans une formulation précédente de ten Cate et al. concernant la réflexivité fonctionnelle (la propriété selon laquelle si $a \approx b$, alors $f(a) \approx f(b)$). L'ajout simple d'axiomes de réflexivité fonctionnelle complets provoque une non-terminaison.
• Solution : Les auteurs introduisent des axiomes de réflexivité fonctionnelle D-restreints. Ces axiomes dérivent des égalités uniquement pour les termes qui apparaissent dans des faits relationnels (suivis par un prédicat de domaine $D$). Cela garantit que le modèle universel reste fini tout en préservant toutes les réponses aux requêtes pertinentes.

2.3 Skolemisation

Les dépendances FO sont converties en un programme logique ($P_3$) en remplaçant les quantificateurs existentiels par des symboles de fonctions de Skolem. Crucialement, la distinction entre les symboles fonctionnels « vrais » (provenant des dépendances SO originales) et les symboles de Skolem est maintenue. Les axiomes de réflexivité fonctionnelle sont appliqués uniquement aux symboles fonctionnels vrais, empêchant les dérivation infinies pour les termes de Skolem.

2.4 Analyse de pertinence

Une technique de chaînage arrière est utilisée pour éliminer des règles entières qui ne contribuent pas prouvablement aux réponses de la requête.

• Abstraction : L'instance de base est abstraite en une « instance critique » plus petite contenant une constante représentative pour chaque prédicat.
• Analyse : Le point fixe du programme sur cette instance abstraite est calculé. Les règles qui ne peuvent pas s'activer sur l'instance abstraite sont jugées non pertinentes et supprimées.
• Optimisation : L'algorithme exploite le fait que les atomes d'égalité peuvent souvent être dérivés à partir d'atomes relationnels et de règles de domaine, évitant ainsi la nécessité de considérer la règle de réflexivité pour chaque correspondance potentielle.

2.5 Transformation Magic Sets

Une variante de l'algorithme Magic Sets est appliquée aux règles restantes pour élaguer les instances de règles sans rapport (plutôt que de simples règles entières).

• Ornements : Les prédicats sont ornés de marqueurs « liés » (b) ou « libres » (f) pour simuler le passage d'information latéral.
• Gestion de l'égalité : La transformation est optimisée pour l'égalité en traitant le prédicat d'égalité de manière symétrique et en évitant le traitement de la règle de réflexivité, qui déclencherait autrement tous les prédicats.
• Terminaison : Les auteurs prouvent que si le chase original termine, le point fixe du programme transformé termine également, même avec l'introduction de prédicats magiques.

2.6 Suppression des constantes et symboles fonctionnels dans les corps

La transformation Magic Sets peut introduire des termes fonctionnels dans les corps des règles, que la variante standard du chase ne peut pas gérer. Les auteurs appliquent une transformation (defun) qui remplace les constantes et les termes fonctionnels dans les corps par de nouvelles variables et des prédicats auxiliaires ($F_f$), axiomatisant efficacement l'application de fonction sans intégrer de termes dans le corps.

2.7 Désingularisation

Enfin, les égalités introduites lors de la singularisation sont supprimées des corps des règles en substituant les variables par leurs termes égaux. Cela aboutit à un programme logique « sûr » ($P_7$) ne contenant aucune égalité, constante ou symbole fonctionnel dans les corps, prêt pour une évaluation efficace.

2.8 Évaluation finale

Le programme final $P_7$ est évalué en utilisant une variante du chase qui traite l'égalité comme une égalité « vraie » (en utilisant les prédicats $V_f$ pour suivre les applications de fonction) mais n'impose pas la réflexivité fonctionnelle pour les symboles de Skolem. Cela garantit que l'étape finale est efficace et ne souffre pas de la surcharge de l'axiomatisation explicite de l'égalité.

3. Contributions clés

1. Première technique orientée but pour les dépendances SO avec égalité : L'article présente la première technique capable de répondre aux requêtes orientée but pour les dépendances du second ordre généralisées avec égalité.
2. Singularisation révisée : Une technique de singularisation corrigée et étendue qui gère les variables fonctionnelles et garantit l'exhaustivité en traitant la réflexivité fonctionnelle sans provoquer de non-terminaison.
3. Analyse de pertinence pour l'égalité : Une technique d'analyse novatrice qui identifie les dépendances non pertinentes en calculant une abstraction du modèle universel, filtrant efficacement les règles qui ne peuvent pas contribuer aux réponses aux requêtes, même en présence d'égalité.
4. Magic Sets optimisés : Une variante de Magic Sets qui gère l'égalité efficacement en exploitant la symétrie et en évitant le traitement des règles de réflexivité, qui sont généralement une source de surcharge.
5. Génération de benchmarks : Une nouvelle technique pour générer des dépendances du second ordre synthétiques et des ensembles de données qui garantissent d'exhiber des inférences non triviales, comblant le manque de benchmarks existants pour ce domaine.
6. Implémentation et évaluation : La première implémentation d'un chase pour les dépendances du second ordre avec égalité et une évaluation empirique extensive.

4. Résultats expérimentaux

Les auteurs ont implémenté un prototype en Java, utilisant le système RDFox pour le calcul de point fixe. Ils ont évalué l'approche sur :

• Benchmarks du premier ordre : Ensembles de données standards (LUBM, Deep, Ont) de Benedikt et al.
• Benchmarks du second ordre : Nouveaux ensembles de données synthétiques (Gen-26, Gen-27, Gen-28) générés par leur outil.

Constats clés :

• Gains de performance : La réponse aux requêtes orientée but peut être des ordres de grandeur plus rapide que le calcul du modèle universel complet. Dans certains cas (par exemple, le scénario Deep300), le chase complet a échoué à terminer dans le délai imparti, tandis que l'approche orientée but a répondu avec succès à toutes les requêtes.
• Comparaison des techniques :
  • L'analyse de pertinence a été identifiée comme le principal moteur des améliorations de performance, réduisant souvent considérablement le nombre de faits dérivés.
  • Magic Sets a apporté des avantages supplémentaires, en particulier lorsqu'il est combiné à l'analyse de pertinence, bien que dans certains cas (par exemple, Ont-256), la surcharge des règles magiques puisse l'emporter sur les avantages.
  • Surcharge du second ordre : Pour les dépendances du second ordre, la surcharge de génération de faits pour les applications de fonction (via les prédicats $F_f$) était significative. L'analyse de pertinence s'est révélée particulièrement efficace ici car elle a réduit le nombre de termes pour lesquels ces faits devaient être générés.
• Réduction des faits : Les techniques ont considérablement réduit le nombre de faits « utiles » dérivés, souvent de plusieurs ordres de grandeur, par rapport au chase complet.

5. Signification et affirmations

L'article prétend résoudre un goulot d'étranglement critique dans l'intégration de données et la composition de mappages de schémas, où la composition des mappages aboutit souvent à des dépendances complexes du second ordre avec égalité. En démontrant que les techniques orientées but peuvent être adaptées à ce contexte complexe, les auteurs montrent que :

• Il est possible d'éviter la « malédiction de la dimensionnalité » associée au calcul de modèles universels complets.
• La combinaison de la singularisation, de l'analyse de pertinence et des Magic Sets fournit un cadre robuste pour gérer les défis spécifiques de l'égalité et des variables fonctionnelles.
• L'approche est pratique, comme en témoigne la gestion réussie de benchmarks synthétiques à grande échelle où les méthodes traditionnelles échouent.

Les auteurs restent modestes concernant les travaux futurs, notant que l'extension de ces techniques aux scénarios de chase non terminants (par exemple, les dépendances protégées) et la réduction supplémentaire de la surcharge des faits auxiliaires (comme les prédicats $D$ et $F_f$) restent des défis ouverts.