Théorie des modèles finis

La théorie des modèles finis est un sous-domaine de la théorie des modèles. Cette dernière est une branche de la logique mathématique qui traite de la relation entre un langage formel (la syntaxe) et ses interprétations (ses sémantiques). La théorie des modèles finis est la restriction de la théorie des modèles aux interprétations de structures finies, donc qui sont définies sur un ensemble (un univers) fini. Ses applications principales sont la théorie des bases de données, la complexité descriptive et la théorie des langages formels.

Propriétés générales

• La théorie des modèles est proche de l'algèbre. En informatique, la théorie des modèles finis est devenue un instrument « unusually effective ». En d'autres termes, et pour citer Immerman : « dans l'histoire de la logique mathématique, l'intérêt s'est porté principalement sur les structures infinies […] Mais les objets que les ordinateurs contiennent et gèrent sont toujours finis. Pour étudier les calculs, nous avons besoin d'une théorie de structures finies ». Les applications principales de la théorie des modèles finis sont : la complexité descriptive, la théorie des bases de données et la théorie des langages formels.
• De nombreux théorèmes de la théorie des modèles cessent d'être vrais si on les restreint aux structures finies. Il en résulte que la théorie des modèles finis n'a plus les mêmes méthodes de démonstration. Parmi les résultats centraux de la théorie des modèles classique qui sont faux pour les structures finies, il y a le théorème de compacité, le théorème de complétude de Gödel et la méthode des ultraproduits pour la logique du premier ordre. Il est donc utile de disposer d'outils spécifiques, dont le premier est le jeu d'Ehrenfeucht-Fraïssé.
• La théorie des modèles traite de définissabilité de structures. La motivation usuelle est la question de savoir si une classe de structures peut être décrite, à un isomorphisme près, dans un langage logique donné : par exemple, est-il possible de définir les graphes cycliques par une formule, de logique du premier ordre par exemple, en trouvant une formule qui est vérifiée par ces graphes seulement ? Ou, autrement dit, est-ce que la propriété « être cyclique » est définissable en logique du premier ordre ?

Problèmes élémentaires

Une structure isolée peut toujours être décrite de manière unique en logique du premier ordre. Certains ensembles finis de structures peuvent également être décrites en logique du premier ordre. Mais cette logique ne suffit pas pour décrire tout ensemble contenant des structures infinies.

Caractérisation d'une structure isolée

La question générale se formule comme suit : Est-ce qu'un langage L est assez expressif pour décrire une structure finie S (à un isomorphisme près) ?

Deux graphes (1) et (1') qui ont des propriétés en commun.

Exemple

Une structure comme figurée par le graphe (1) peut être décrite par des expressions de logique du premier ordre comme :

1. Chaque sommet est relié à un autre sommet : $\forall x\exists yG(x,y)$ ;
2. Aucun sommet n'a d'arête qui le relie à lui-même : $\forall x\neg G(x,x)$ ;
3. Au moins un sommet est relié à tous les autres sommets : $\exists x\forall y(x\neq y\Rightarrow G(x,y))$.

Mais ces propriétés ne suffisent pas à décrire la structure de manière unique (à un isomorphisme près) : la structure (1') vérifie toutes ces propriétés et les deux structures (1) et (1') ne sont pas isomorphes.

La question qui se pose est la suivante : est-il possible d'ajouter assez de propriétés pour que ces propriétés, dans leur ensemble, décrivent (1) exactement, et aucune autre structure (toujours à un isomorphisme près).

Approche

Pour une structure finie isolée, il est toujours possible de décrire sa structure par une seule formule de logique du premier ordre. Le principe est illustré pour une structure avec une relation binaire R et sans constantes :

1. exprimer qu'il y a au moins $n$ éléments : $\varphi _{1}=\bigwedge _{1\leq i<j\leq n}\neg (x_{i}=x_{j})$ ;
2. exprimer qu'il y a au plus $n$ éléments : $\varphi _{2}=\forall y\bigvee _{1\leq i\leq n}(x_{i}=y)$ ;
3. décrire tous les couples dans la relation $R$ : $\varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})$ ;
4. décrire tous les couples qui ne sont pas dans la relation $R$ : $\varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})$

pour le même n-uplet $x_{1},\ldots ,x_{n}$, ce qui donne la formule du premier ordre $\exists {x_{1}}\dots \exists {x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})$.

Extension à un nombre fini de structures

La méthode qui consiste à décrire une structure isolée par une formule du premier ordre peut être facilement étendue à tout nombre fixe fini de structures. Une description unique peut être obtenue par la disjonction des descriptions de chaque structure. Par exemple, pour deux structures cela donnerait :

$\exists {x_{1}}\dots \exists {x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})\lor \exists {x_{1}}\dots \exists {x_{n}}(\varrho _{1}\land \varrho _{2}\land \varrho _{3}\land \varrho _{4}).$

Extension à une structure infinie

Par définition, un ensemble contenant une structure infinie sort du cadre de la théorie des modèles finis. Les structures infinies ne peuvent jamais être définies dans la logique du premier ordre à cause du théorème de compacité de la théorie des modèles classique : pour tout modèle infini, il existe un modèle non isomorphe qui possède exactement les mêmes propriétés du premier ordre.

L'exemple le plus célèbre est probablement le théorème de Skolem qui affirme l'existence d'un modèle dénombrable non standard de l'arithmétique.

Caractérisation d'une classe de structures

La question générale se formule comme suit : Est-ce qu'un langage L est assez expressif pour décrire une des structures finies qui ont en commun une certaine propriété P (à un isomorphisme près) ?

Ensemble de n structures.

Problème

Les descriptions données jusqu'à maintenant spécifient toutes le nombre d'éléments de l'univers. Toutefois, les ensembles de structures les plus intéressantes ne sont pas réduites à une taille donnée, comme les graphes qui sont des arbres, ou qui sont connexes ou sans cycle. La possibilité de discriminer un ensemble fini de structures est donc particulièrement important.

Approche

Plutôt que de formuler un énoncé général, voici une esquisse d'une méthode qui permet de distinguer les structures que l'on peut discriminer des autres.

1.- L'idée centrale est que pour savoir si une propriété P est exprimable en logique du premier ordre, on choisit des structures A et B, où A possède la propriété P et B ne la possède pas. Si les mêmes formules du premier ordre sont valables pour les structures A et B, alors P n'est pas définissable en logique du premier ordre. En bref :

$A\in P,B\notin P$  et  $A\equiv B$

où $A\equiv B$ est une abréviation pour $A\models \alpha \Leftrightarrow B\models \alpha$ pour toute formule du premier ordre $\alpha$, et où $P$ représente la classe des structures ayant la propriété P.

2.- La méthode considère un nombre dénombrable de sous-ensembles du langage dont la réunion compose le langage tout entier. Par exemple, pour la logique du premier ordre, on considère des classes FO[m] pour chaque entier m. Pour chaque m, le test ci-dessus doit être effectué et l'équivalence montrée. En d'autres termes :

$A\in P,B\notin P$ et $A\equiv _{m}B$

avec un couple $A,B$ pour chaque $m$ et $\alpha$ de FO[m]. Il peut être utile de choisir les classes FO[m] de sorte qu'elles forment une partition du langage.

3.- Une façon usuelle de définir FO[m] est par le rang de quantificateurs $q(\alpha )$ qui est le niveau de profondeur de l'imbrication des quantificateurs dans une formule $\alpha$. Pour une formule en forme prénexe, le rang est simplement le nombre de ses quantificateurs. On peut alors définir FO[m] comme l’ensemble des formules du premier ordre $\alpha$ dont le rang de quantificateurs $q(\alpha )$ est au plus m (ou, si l'on cherche une partition, comme celles dont le rang est égal à m).

4.- Tout ceci réduit la preuve de $A\models \alpha \Leftrightarrow B\models \alpha$ aux sous-ensembles FO[m]. L'approche principale employée ici est la caractérisation algébrique fournie par le jeu d'Ehrenfeucht-Fraïssé. De manière informelle, on prend un isomorphisme partiel entre $A$ et $B$ et on l'étend m fois, en vue de prouver ou d'invalider $A\equiv _{m}B$, en fonction du gagnant du jeu.

Jeu d'Ehrenfeucht-Fraissé

Le jeu d'Ehrenfeucht-Fraissé est historiquement l'un des premiers outils de la théorie des modèles finis. Un tel jeu est joué sur deux structures A et B d'un même univers par deux joueurs, appelés le spoiler (littéralement le « gâteur ») et le duplicateur. Le spoiler essaie de montrer que les structures A et B sont différentes, le duplicateur au contraire cherche à prouver qu'elles sont isomorphes. Dans tous les cas, le jeu a un nombre fini de tours, ce qui donne une chance de succès au duplicateur.

Le jeu se joue comme suit. À chaque tour $i$, le spoiler choisit une des deux structures, et un élément dans cette structure ; le duplicateur choisit un élément dans l'autre structure. Ainsi, si le spoiler choisit $A$ et un élément $a_{i}$ dans $A$, le duplicateur répond avec un élément $b_{i}$ de $B$ ; si le spoiler choisit $B$ et un élément $b_{i}$ de $B$, le duplicateur répond par un élément $a_{i}$ de $A$. Après $n$ tours, on possède $n$ points $a_{1},\ldots ,a_{n}$ de $A$ et $b_{1},\ldots ,b_{n}$ de $B$. Le duplicateur gagne le jeu si l'application $a_{i}\to b_{i}$ est un isomorphisme partiel (par exemple, si les structures sont des graphes, alors cela signifie que deux éléments $(a_{i},a_{j})$ sont voisins si et seulement si $(b_{i},b_{j})$ le sont). On dit que le duplicateur a une stratégie gagnante dans un jeu à $n$ tours s'il sait gagner quelle que soit la manière dont joue le spoiler. On écrit alors $A\equiv _{n}B$.

L'importance du jeu est que $A\equiv _{n}B$ si et seulement si $A$ et $B$ satisfont les mêmes formules du premier ordre de rang de quantificateurs au plus $n$. Ceci fournit un outil efficace pour prouver qu'une propriété $P$ n'est pas définissable en logique du premier ordre. Pour cela, on cherche deux familles $A_{n}$ et $B_{n}$ de structures telles que toutes les $A_{n}$ vérifient $P$ et aucune des $B_{n}$ ne la vérifie, et que $A_{n}\equiv _{n}B_{n}$. Si on suppose que $P$ est exprimable par une formule de rang de quantificateurs au plus $n$ et que $A_{n}$ la vérifie, la structure $B_{n}$ ne la vérifie pas, en contradiction avec les faits que $A_{n}\equiv _{n}B_{n}$.

Exemple

Dans cet exemple, on montre que la propriété « La taille d'une structure ordonnée $A=(A,\leq )$ est paire » ne peut être exprimée en logique du premier ordre.

1.- L'idée est de prendre $A$ dans ${\mathcal {P}}$ et $B$ en dehors de ${\mathcal {P}}$, où ${\mathcal {P}}$ désigne la classe des structures de taille paire.

2.- On commence avec deux structures $A_{2}$ et $B_{2}$ avec univers $A_{2}=\{1,2,3,4\}$ et $B_{2}=\{1,2,3,4,5\}$. Évidemment, $A_{2}$ est dans ${\mathcal {P}}$ et $B_{2}$ n'y est pas.

3.- Pour $m=2$, on peut montrer (le détail de l'emploi du jeu d'Ehrenfeucht-Fraïssé est omis ici) qu'en deux mouvements d'un jeu d'Ehrenfeucht-Fraïssé sur $A_{2}$ et $B_{2}$, le duplicateur gagne toujours, et que $A_{2}$ et $B_{2}$ ne peuvent être distingués dans FO[2], c'est-à-dire que $A_{2}\models \alpha \iff B_{2}\models \alpha$ pour toute formule $\alpha$ de FO[2].

4.- On monte maintenant d'échelle en augmentant m. Par exemple, pour m = 3, il faut trouver $A_{3}$ et $B_{3}$ tels que le duplicateur gagne toujours dans un jeu à trois mouvements. On peut montrer que cela est possible avec $A_{3}=\{1,\ldots ,8\}$ et $B_{3}=\{1,\ldots ,9\}$. Plus généralement, on peut prendre $A_{m}=\{1,\ldots ,2^{m}\}$ et $B_{m}=\{1,\ldots ,2^{m}+1\}$; pour tout m, le duplicateur gagne toujours un jeu en m mouvements pour ce couple de structures.

5.- Ceci prouve que la propriété d'avoir un nombre pair d'éléments, pour des structures finies, n'est pas définissable en logique du premier ordre.

Propriétés non définissables au premier ordre

Les propriétés suivantes ne sont pas définissables par des formules du premier ordre ; la preuve est par le jeu d'Ehrenfeur-Fraïssé :

• La propriété « avoir un nombre pair d'éléments » (comme démontré ci-dessus) ;
• La propriété « être connexe » pour un graphe ;
• La propriété « être acyclique » pour un graphe ;
• La propriété « être transitif » pour un graphe.

Loi du zéro-un

On se pose la question, étant donné une formule α, de la probabilité pour qu'une structure A satisfasse α, parmi toutes les structures de même taille n, et on s'intéresse à la limite de cette probabilité quand n tend vers l'infini.

Un exemple est fourni pour les graphes. On note $G_{n}$ l'ensemble des graphes sur l'ensemble des sommets $\{1,\ldots ,n\}$; il y a $2^{\binom {n}{2}}$ éléments dans $G_{n}$. Soit ${\mathcal {P}}$ une propriété des graphes ; on note

$\mu _{n}({\mathcal {P}})={\frac {\operatorname {Card} \{G\in G_{n}\mid G\ {\text{vérifie}}\ {\mathcal {P}}\}}{\operatorname {Card} G_{n}}}$

et

$\mu ({\mathcal {P}})=\lim _{n\to \infty }\mu _{n}({\mathcal {P}})$

pourvu que cette limite existe. Prenons par exemple pour ${\mathcal {P}}$ la propriété « $G$ possède un sommet isolé ». On peut choisir de n façons un sommet isolé et prendre un graphe quelconque sur les sommets restants, donc

$\mu _{n}({\mathcal {P}})\leq {\frac {n\,2^{\binom {n-1}{2}}}{2^{\binom {n}{2}}}}={\frac {n}{2^{n-1}}}\to 0.$

Un calcul un peu plus compliqué montre que pour la propriété « être connexe », la limite est 1. D'autres exemples sont: « un graphe contient un triangle » (probabilité 1), « un graphe est sans cycle », « un graphe est 2-coloriable » (probabilités 0).

Une logique vérifie la loi du zéro-un (à ne pas confondre avec la loi du zéro-un de Borel ou celle de Kolmogorov) si, pour toute formule de cette logique, la probabilité asymptotique que cette formule soit satisfaite est soit 0 soit 1. La probabilité asymptotique est la limite sur n, si elle existe, de la probabilité qu'une structure de taille n choisie au hasard selon la distribution uniforme vérifie la formule. Le résultat important est que la logique du premier ordre vérifie la loi du zéro-un.

Un exemple simple d'application est le test de parité : la probabilité d'être pair alterne entre 0 et 1 avec la taille, donc la probabilité asymptotique n'existe pas.

Applications

Théorie des bases de données

Une partie substantielle du langage SQL, à savoir celui qui correspond à l'algèbre relationnelle, est basée sur la logique du premier ordre, car il peut être traduit en calcul relationnel par le théorème de Codd. Voici un exemple illustratif. Imaginons une table de base de données "GARÇONS" avec deux colonnes "PRÉNOM" et "NOM". Ceci correspond à une relation binaire, disons G(f,l) sur le produit PRÉNOM X NOM. Une requête du premier ordre {l : G('Paul', l)} retourne tous les noms qui correspondent au prénom 'Paul'. En SQL, elle s'écrit comme suit :

select NOM
from GARÇONS
where PRÉNOM = 'Paul'

On suppose ici que les noms de famille n'apparaissent qu'une fois dans la liste. Voici une requête plus complexe. En plus de la table "GARÇONS", on suppose qu'on a une table "FILLES", avec les mêmes deux colonnes. On cherche maintenant les noms des garçons qui ont le même nom de famille qu'une fille. La requête en premier ordre est {(f,l) : ∃h ( G(f, l) ∧ B(h, l) )}, et l'instruction SQL est :

select PRÉNOM, NOM 
from GARÇONS
where NOM IN (select NOM from FILLES);

Pour exprimer le "∧", on a introduit le nouvel élément "IN" avec une instruction de sélection. Ceci rend le langage plus expressif, mais on peut aussi utiliser un opérateur "JOIN", et écrire

select distinct g.PRÉNOM, g.NOM
from GARÇONS g, FILLES b
where g.NOM=b.NOM;

La logique du premier ordre est trop restrictive pour certaines applications en bases de données, par exemple par l'impossibilité d'y exprimer la transitive closure. Ceci a conduit à l'ajout d'opérateurs plus puissants aux langages de requêtes des bases de données, tels que la clause WITH dans la version SQL:1999. Des versions plus expressives de logique, comme la logique du point fixe (en), ont alors été étudiées dans le cadre de la théorie des modèles finis, à cause de leur rapport avec la théorie des bases de données et de ses applications.

Langages formels

Un exemple de la théorie des langages formels. On considère un alphabet binaire $\{a,b\}$. Pour un mot $w=a_{1}\cdots a_{n}$ on crée une structure $M_{w}$ comme suit : l'univers est l'ensemble $\{1,\ldots ,n\}$ correspondant aux positions dans le mot, avec l'ordre usuel. Deux relations unaires $R_{a}$ et $R_{b}$ sont vraies selon la valeur de la lettre : $R_{a}(i)$ est vrai si $a_{i}=a$ et $R_{b}(i)$ est vrai si $a_{i}=b$. Par exemple, $M_{abba}$ a l'univers $\{1,2,3,4\}$, et $R_{a}$ est vrai pour $\{1,4\}$ et $R_{b}$ pour $\{2,3\}$. Un exemple de formule de logique du premier ordre est :

$\lnot (\exists i\exists j((i<j)\land R_{b}(i)\land R_{a}(j))$

Cette formule décrit le fait que les lettres $b$ suivent les lettres $a$ dans le mot, en d'autres termes que le mot appartient au langage rationnel dont une expression régulière est $a^{*}b^{*}$. Le lien entre les langages rationnels et les formules logiques est le suivant :

• Il existe une formule du premier ordre pour décrire un langage si et seulement s'il est un langage sans étoile ;
• Les langages rationnels sont exactement les langages décrits par la logique du second ordre dite monadique, c'est-à-dire avec des quantificateurs du second ordre portant sur des ensembles de positions.

Par exemple, le langage $(aa)^{*}$ formé des mots de longueur paire sur un alphabet unaire n'est pas exprimable par une formule du premier ordre.

Notes et références

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Finite Model Theory » (voir la liste des auteurs).

Notes de cours en ligne

• Arnaud Durand, « Logique, jeux et définissabilité », Notes du cours Théorie des modèles finis du Master Logique Mathématique et Fondements de l'Informatique, Université Paris-7 Diderot.
• Leonid Libkin, « The finite model theory toolbox of a database theoretician », dans PODS 2009: Proceedings of the twenty-eighth ACM SIGACT–SIGMOD symposium on Principles of database systems, 2009 (DOI 10.1145/1559795.1559807, lire en ligne), p. 65–76. Utile comme introduction générale et comme survol.
• Leonid Libkin. Elements of Finite Model Theory, Introduction. Motivation des trois domaines principaux d'application : bases de données, complexité et langages formels.
• Jouko Väänänen, « A Short Course on Finite Model Theory ». Department of Mathematics, University of Helsinki. Basé sur un cours de 1993-1994.
• Anuj Dawar. Infinite and Finite Model Theory, transparents, University of Cambridge, 2002.
• « Algorithmic Model Theory », RWTH Aachen (consulté le 7 novembre 2013). Contient une liste de problèmes ouverts.

Livres de référence

• Heinz-Dieter Ebbinghaus et Jörg Flum, Finite Model Theory, Springer, 1995, 327 p. (ISBN 978-3-540-60149-4)

• Leonid Libkin, Elements of Finite Model Theory, Springer, 2004, 318 p. (ISBN 3-540-21202-7, lire en ligne)

• (en) Serge Abiteboul, Richard Hull et Victor Vianu, Foundations of Databases, Reading, Mass, Addison-Wesley, 1995, 685 p. (ISBN 0-201-53771-0)

• (en) Neil Immerman, Descriptive Complexity, New York, Springer, 1999, 268 p. (ISBN 0-387-98600-6, lire en ligne)

Articles connexes

• Complexité descriptive
• Théorie des bases de données
• Théorie des jeux
• Langage formel
• Calcul des prédicats
• Théorème de Löwenheim-Skolem
• Moshe Vardi
• Ronald Fagin