Localité et théorèmes de préservation

Résumé en Français d’un article
Posté le 16-11-2023 par Aliaume Lopez – lecture en 11 minutes (≈ 2648 mots)
Partie 3/3 d'une série de posts sur les résumés de mes articles
Table des matières

Ce document est le résumé en français de l’article de Lopez (2022) présenté à la conférence LICS 2022, dont le pdf, les slides de présentations, ainsi que le fichier bibtex associé sont disponibles sur ma page web.

Résumé

Cet article s’intéresse au pouvoir expressif d’un fragment de la logique du premier ordre dérivé de la forme normale de Gaifman, nommément, les combinaisons positives de formules closes basiques locales. Nous montrons que ces dernières ont le même pouvoir expressif que les formules closes existentielles locales, c’est-à-dire les formules obtenues en considérant la clôture existentielle d’une formule locale. De plus, dans le cadre des structures arbitraires, les formules existentielles locales ont le même pouvoir expressif que les formules préservées par les plongements élémentaires locaux, ce qui correspond à une généralisation du théorème de Łoś-Tarski. En effet, ce dernier considère les formules existentielles, qui sont précisément les formules existentielles \(0\)-locales. Comme il est d’usage, ce théorème de préservation ne relativise pas à la classe des structures finies, et nous démontrons de plus que les problèmes associés à cet échec (décider si une formule est préservée, décider si une formule est équivalente à une combinaison positive de formules closes basiques locales, etc.) sont indécidables.

Nous montrons cependant que la compréhension des formules existentielles locales permet d’obtenir une caractérisation des classes de structures finies, héréditaires et closes sous union disjointe, pour lesquelles le théorème de Łoś-Tarski relativise, en montrant que ce sont exactement celles où le théorème de Łoś-Tarski relativise localement, c’est-à-dire, relativise aux voisinages des structures de la classe. Cette caractérisation permet de déduire simplement des résultats préexistants, et de construire de nouvelles classes de structures où le théorème de Łoś-Tarski relativise.

Contextualisation

Le théorème de Łoś-Tarski est un résultat classique de la théorie des modèles, dans la lignée des théorèmes de préservation (voir par exemple Chang and Keisler 1990, vol. 73, sec. 5.2). En toute généralité, un théorème de préservation sert de pont entre deux classes de formules au premier ordre, l’une définie syntaxiquement, l’autre définie de manière sémantique.

Théorème (Łoś 1955; Tarski 1954). Soit \(\sigma\) une signature relationnelle finie, et \(\varphi\) une formule dans \(\mathsf{FO}[\sigma]\). Les deux propriétés suivantes sont équivalentes :

1.

On utilise la notation \(A \subseteq_iB\) pour désigner l’existence d’une fonction \(h \colon A \to B\) telle que pour tout tuple \(\vec{a} \in A\), et toute relation \(R \in \sigma\), si \(\vec{a} \in R^A\), alors \(h(\vec{a}) \in R^B\). Une telle fonction est un morphisme qui témoigne que \(A\) est une sous-structure induite de \(B\), ou bien, de manière équivalente que \(B\) est une extension de \(A\).

  1. Il existe une formule existentielle \(\psi\) équivalente à \(\varphi\),
  2. Pour toute paire \(A \subseteq_iB\) de structures, si \(A \models \varphi\), alors \(B \models \varphi\).11
2.

Comprendre, il existe une structure \(A\) telle que pour tout \(\varphi \in T\), \(A \models \varphi\). On dit aussi que l’ensemble \(T\) est satisfiable.

Comme de nombreux résultats de la théorie des modèles, les théorèmes de préservation reposent en général sur l’utilisation du théorème de compacité de la logique au premier ordre. Ce dernier certifie qu’un ensemble \(T\) de formules possède un modèle22 si et seulement si toute partie finie de \(T\) possède un modèle. Ce théorème fondamental de la théorie des modèles ne relativise pas à l’ensemble des structures finies. En effet, il existe un ensemble de formules qui ne possède aucun modèle fini, mais dont toute partie finie possède un modèle fini. Il suffit par exemple de considérer les formules \(\varphi_n\) disant “il existe au moins \(n\) éléments distincts”. Une structure \(A\) qui satisfait \(\varphi_n\) pour tout \(n\) ne peut pas être finie, mais tout sous ensemble fini des formules \(\varphi_n\) est satisfait par une structure finie \(A\) “assez grande”.

Cependant, ce n’est pas parce que la preuve des théorèmes de préservation utilise un résultat qui ne relativise pas aux structures finies que les théorèmes eux-mêmes ne relativisent pas au cas fini. On peut imaginer d’autres preuves, plus combinatoires, qui permettraient d’obtenir ces correspondances entre syntaxe et sémantique dans ce cadre plus restreint. Notons que la relativisation du théorème de Łoś-Tarski au cas fini n’est pas triviale : plus de formules sont équivalentes lorsque l’on restreint notre attention aux modèles finis, mais simultanément, plus de formules sont préservées par extensions lorsque l’on restreint notre attention aux structures finies.

Pour une majorité de théorèmes de préservation, il a été rapidement démontré qu’ils ne relativisent pas au cas fini (voir par exemple Tait 1959; Stolboushkin 1995; Gurevich 1984; Ajtai and Gurevich 1994; ou plus récemment Kuperberg 2021), avec une exception notable : le théorème de préservation par homomorphisme. La question du théorème de préservation par homomorphisme est restée ouverte jusqu’à ce que sa relativisation au cas fini soit démontrée par Rossman (2008), environ 49 ans après le premier contre exemple fourni par Tait.

En parallèle des résultats négatifs obtenus sur la classe des structures finies, les relativisations des théorèmes de préservations à des classes encore plus restreintes de structures (avec degré borné, héréditaires, etc.) ont été étudiées (pour citer quelques exemples, on peut s’intéresser aux résultats de Atserias, Dawar, and Kolaitis 2006; Atserias, Dawar, and Grohe 2008; Dawar and Sankaran 2021; Harwath, Heimberg, and Schweikardt 2015). Concrètement, le théorème de Łoś-Tarski relativise à une classe \(\mathcal{C}\) de structures lorsque les deux propositions suivantes sont équivalentes pour toute formule \(\varphi \in \mathsf{FO}[\sigma]\) :

  1. Il existe une formule existentielle \(\psi\) équivalente à \(\varphi\) sur la classe \(\mathcal{C}\), i.e., pour toute structure \(A \in \mathcal{C}\), \(A \models \varphi\) si et seulement si \(A \models \psi\).
  2. La formule \(\varphi\) est préservée par extensions sur \(\mathcal{C}\), i.e., pour toute paire \(A,B\) de structures dans \(\mathcal{C}\), telles que \(A \subseteq_iB\), si \(A \models \varphi\), alors \(B \models \varphi\).

Dans le cas particulier où \(\mathcal{C}\) est la classe de toutes les structures, on obtient le théorème de Łoś-Tarski. Lorsqu’on relativise le théorème aux structures finies (\(\mathcal{C}\) est la classe de toutes les structures finies), la relativisation est fausse (Tait 1959). Le théorème de Łoś-Tarski relativise cependant à n’importe quelle classe \(\mathcal{C}\) de structures finies contenant un nombre fini de structures, ainsi qu’aux classes \(\mathcal{C}\) de structures finies héréditaires, de degré borné et closes par union disjointe (Atserias, Dawar, and Grohe 2008). La preuve de ce dernier résultat de relativisation repose sur les techniques de théorie des modèles finis, comme la localité de la logique du premier ordre.

En effet, le théorème de Gaifman permet de réécrire n’importe quelle formule \(\varphi \in \mathsf{FO}[\sigma]\) en une combinaison Booléenne de formules basiques locales (Gaifman 1982). Une conséquence de ce résultat est que la valeur de vérité d’une formule \(\varphi\) pour une structure \(A\) ne dépend que des comportements locaux observables dans la structure \(A\). Dans les preuves de relativisation, le théorème de localité sert de substitut au théorème de compacité de la logique au premier ordre, en permettant de réduire le théorème au comportement local de la classe de structure étudiée.

Contributions

La première contribution de cet article est l’introduction et la caractérisation de la classe des formules existentielles locales. Les formules existentielles locales sont obtenues comme la clôture existentielle des formules locales. En comparaison, les formules basiques locales apparaissant dans la forme normale de Gaifman sont obtenues en quantifiant existentiellement sur un ensemble \(r\)-indépendant de témoins d’une formule locale avec une unique variable libre. Nous montrons dans un premier théorème que les formules existentielles locales ont la même expressivité que les combinaisons Booléennes positives de formules basiques locales. Ce résultat ne dépend pas de la classe de structure \(\mathcal{C}\) considérée. Sur la classe de toutes les structures, les formules existentielles locales ont la même expressivité que les formules préservées par les plongements élémentaires locaux, ce qui correspond à un nouveau théorème de préservation associé à ce fragment.

Le théorème de préservation par plongements élémentaires locaux, comme la vaste majorité des théorèmes de préservation, ne relativise pas aux structures finies. C’est la seconde contribution de cet article. En plus de fournir un exemple de formule préservée par plongements élémentaires locaux sur les structures finies qui n’est équivalente à aucune formule existentielle locale, nous prouvons les résultats suivants :

  1. On ne peut pas décider si une formule \(\varphi\) est préservée par plongements élémentaires locaux sur la classe des structures finies.
  2. On ne peut pas décider si une formule \(\varphi\) est équivalente à une formule existentielle locale sur la classe des structures finies.
  3. Il n’existe pas d’algorithme qui, étant donné une formule \(\varphi\) et une garantie que celle-ci est équivalente à une formule existentielle locale, calcule une formule existentielle locale équivalente à \(\varphi\).

Ces théorèmes d’impossibilités sont obtenus sur une signature \(\sigma\) contenant trois relations binaires et de multiples relations unaires. Il est certainement possible de limiter l’utilisation de ces prédicats, mais le résultat ainsi formulé est plus simple et possède l’avantage de se prêter à une analyse plus fine.

En effet, les formules existentielles locales peuvent se paramétrer en fonction du rayon \(r\) de localité de la formule existentiellement quantifiée. Ce paramètre \(r\) peut servir de curseur pour passer des formules existentielles \(0\)-locales, qui sont précisément les formules existentielles, aux formules \(\infty\)-locales, qui capturent toutes les formules au premier ordre (sur les structures finies). Les plongements élémentaires locaux peuvent, de la même manière, être paramétrés ce rayon \(r\) de localité. Ainsi, une formule préservée par plongements élémentaires \(0\)-locaux est précisément préservée par extensions, alors qu’une formule préservée par plongements élémentaires \(\infty\)-locaux est (sur les structures finies) précisément préservée par union disjointe : si \(A \models \varphi\), alors \(A \uplus B \models \varphi\), pour toute paire \(A,B\) de structures finies.

Il existe deux autres paramètres naturels sur les formules existentielles locales : le rang de quantification \(q\) de la formule locale sous-jacente et le nombre \(k\) de variables libres quantifiées existentiellement. En faisant varier les paramètres \(r\), \(q\) et \(k\) sur les formules existentielles locales, et sur les plongements élémentaires locaux, on obtient une relaxation de la propriété de préservation formulée comme suit : toute formule \(\varphi\) préservée par plongements élémentaires \((r,q,k)\)-locaux sur les structures finies est équivalente à une formule existentielle locale sur les structures finies. Cette propriété de préservation est fausse quand \(r = q = k = \infty\), mais devient vraie pour certains choix de paramètres. L’article fournit une caractérisation complète des paramètres \(r,q,k\) tels que la propriété est vraie, et montre en particulier qu’elle est vraie pour \(r = 0\) et \(q,k = \infty\). Ce dernier résultat, troisième contribution de l’article, se traduit comme suit :

Une formule \(\varphi\) préservée par extensions sur les structures finies est équivalente à une formule existentielle locale.

Plus généralement, pour n’importe quelle classe \(\mathcal{C}\) de structures finies, héréditaire et close par union disjointe, une formule \(\varphi\) préservée par extensions sur la classe \(\mathcal{C}\) est équivalente (sur cette même classe) à une formule existentielle locale. Ce théorème combinatoire (non trivial) peut se traduire en termes de forme normale de Gaifman, grâce aux résultats précédents. Il implique que toute formule \(\varphi\) préservée par extensions sur les structures finies (ou autre classe satisfaisant les hypothèses du théorème) possède une forme normale de Gaifman sans négations. Cela extrait l’essence des preuves de relativisation du théorème de Łoś-Tarski basées sur la forme normale de Gaifman, dans un cadre beaucoup plus général.

En utilisant l’existence d’une formule équivalente existentielle locale donnée par le théorème ci-dessus, prouver que le théorème de Łoś-Tarski relativise à une classe \(\mathcal{C}\) de structures héréditaire et close par union disjointe se réduit à l’étude des formules existentielles locales préservées par extensions. Il est alors aisé de déduire le théorème suivant, dit local-à-global, qui est la quatrième et principale contribution de l’article : les deux propriétés suivantes sont équivalentes pour toute classe héréditaire \(\mathcal{C}\) de structures finies close par union disjointe

  1. Le théorème de Łoś-Tarski relativise à la classe \(\mathcal{C}\),
  2. Pour tout \(r,k \in \mathbb{N}\), le théorème de Łoś-Tarski relativise à la classe des voisinages de rayon \(r\) centrés en \(k\) points des structures de \(\mathcal{C}\).

De ce théorème, on déduit immédiatement le résultat prouvé par Atserias, Dawar, and Grohe (2008). De plus, on peut construire une hiérarchie stricte de propriétés, strictement plus faibles que celles introduites par Atserias, Dawar et Grohe, impliquant la relativisation du théorème de Łoś-Tarski.

Conclusion

Cet article introduit une variante positive du théorème de localité de Gaifman, caractérisée par les formules existentielles locales et la préservation par plongements élémentaires locaux. Dans certaines classes de structures finies, les formules préservées par extensions possèdent systématiquement une forme normale de Gaifman positive, ce qui permet de réduire la relativisation du théorème de Łoś-Tarski à sa version localisée. Cette technique de preuve s’avère particulièrement efficace, puisqu’elle généralise strictement les résultats précédemment obtenus.

La notion de localité positive semble particulièrement pertinente pour étudier les théorèmes de préservation, mais pourrait aussi servir d’outil, au même titre que le théorème de localité, dans la théorie des modèles finis. En particulier, cette notion semble généraliser la forme normale de Gaifman existentielle proposée par Grohe and Wöhrle (2004).

Une des limitations de l’article, inhérente aux approches par localité, est que certaines classes de structures sont aussi complexes localement que globalement. C’est par exemple le cas des cliques, dont les voisinages de rayon \(1\) contiennent toute la structure. Notons que, dans le cas des cliques, la classe obtenue en inversant la relation d’arête (les ensembles indépendants de sommets) est particulièrement bien adaptée aux techniques de localité (les voisinages sont réduits à un unique point). Il manque ainsi une théorie de la localité modulo renversements (flips en anglais).

Références

Ajtai, Miklós, and Yuri Gurevich. 1994. “Datalog Vs First-Order Logic.” J. Comput. Syst. Sci. 49 (3): 562–88. https://doi.org/10.1016/S0022-0000(05)80071-6.
Atserias, Albert, Anuj Dawar, and Martin Grohe. 2008. “Preservation Under Extensions on Well-Behaved Finite Structures.” SIAM J. Comput. 38 (4): 1364–81. https://doi.org/10.1137/060658709.
Atserias, Albert, Anuj Dawar, and Phokion G. Kolaitis. 2006. “On Preservation Under Homomorphisms and Unions of Conjunctive Queries.” J. ACM 53 (2): 208–37. https://doi.org/10.1145/1131342.1131344.
Chang, Chen Chung, and H. Jerome Keisler. 1990. Model Theory. Vol. 73. Studies in Logic and the Foundations of Mathematics. Elsevier.
Dawar, Anuj, and Abhisekh Sankaran. 2021. “Extension Preservation in the Finite and Prefix Classes of First Order Logic.” In Proc. CSL’21, 183:18:1–13. LIPIcs. LZI. https://doi.org/10.4230/LIPIcs.CSL.2021.18.
Gaifman, Haim. 1982. “On Local and Non-Local Properties.” In Proc. Herbrand Symposium, 107:105–35. Studies in Logic and the Foundations of Mathematics. Elsevier. https://doi.org/10.1016/S0049-237X(08)71879-2.
Grohe, Martin, and Stefan Wöhrle. 2004. “An Existential Locality Theorem.” Ann. Pure Appl. Logic 129 (1–3): 131–48. https://doi.org/10.1016/j.apal.2004.01.005.
Gurevich, Yuri. 1984. “Toward Logic Tailored for Computational Complexity.” In Computation and Proof Theory, Proceedings of LC’84, 1104:175–216. Lecture Notes in Mathematics. Springer. https://doi.org/10.1007/BFb0099486.
Harwath, Frederik, Lucas Heimberg, and Nicole Schweikardt. 2015. “Preservation and decomposition theorems for bounded degree structures.” Log. Meth. Comput. Sci. 11 (4). https://doi.org/10.2168/LMCS-11(4:17)2015.
Kuperberg, Denis. 2021. “Positive First-Order Logic on Words.” In Proc. LICS’21, 1–13. IEEE. https://doi.org/10.1109/LICS52264.2021.9470602.
Lopez, Aliaume. 2022. “When Locality Meets Preservation.” Conf. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, 1–14. LICS ’22. New York, NY, USA: Association for Computing Machinery. https://doi.org/10.1145/3531130.3532498.
Łoś, Jerzy. 1955. “On the Extending of Models (I).” Fund. Math. 42 (1): 38–54. https://doi.org/10.4064/fm-42-1-38-54.
Rossman, Benjamin. 2008. “Homomorphism Preservation Theorems.” J. ACM 55 (3): 15:1–53. https://doi.org/10.1145/1379759.1379763.
Stolboushkin, Alexei P. 1995. “Finitely Monotone Properties.” In Proc. LICS’95, 324–30. https://doi.org/10.1109/LICS.1995.523267.
Tait, William W. 1959. “A Counterexample to a Conjecture of Scott and Suppes.” J. Symb. Logic 24 (1): 15–16. https://doi.org/10.2307/2964569.
Tarski, Alfred. 1954. “Contributions to the Theory of Models. I.” Indag. Math. (Proc.) 57: 572–81. https://doi.org/10.1016/S1385-7258(54)50074-0.

  1. On utilise la notation \(A \subseteq_iB\) pour désigner l’existence d’une fonction \(h \colon A \to B\) telle que pour tout tuple \(\vec{a} \in A\), et toute relation \(R \in \sigma\), si \(\vec{a} \in R^A\), alors \(h(\vec{a}) \in R^B\). Une telle fonction est un morphisme qui témoigne que \(A\) est une sous-structure induite de \(B\), ou bien, de manière équivalente que \(B\) est une extension de \(A\).↩︎

  2. Comprendre, il existe une structure \(A\) telle que pour tout \(\varphi \in T\), \(A \models \varphi\). On dit aussi que l’ensemble \(T\) est satisfiable.↩︎