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 : . 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) ?

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

 Chaque sommet est relié à un autre sommet :  ;
 Aucun sommet n'a d'arête qui le relie à lui-même :  ;
 Au moins un sommet est relié à tous les autres sommets : .

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 : 
 exprimer qu'il y a au moins  éléments :  ;
 exprimer qu'il y a au plus  éléments :  ;
 décrire tous les couples dans la relation  :  ;
 décrire tous les couples qui ne sont pas dans la relation  : 
pour le même n-uplet , ce qui donne la formule du premier ordre .

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 :

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) ?

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 :

  et  

où  est une abréviation pour  pour toute formule du premier ordre , et où  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 : 

 et 

avec un couple  pour chaque  et  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  qui est le niveau de profondeur de l'imbrication des quantificateurs dans une formule . 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  dont le rang de quantificateurs  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  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  et  et on l'étend m fois, en vue de prouver ou d'invalider , 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  (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 , 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  et un élément  dans , le duplicateur répond avec un élément  de  ; si le spoiler choisit  et un élément  de , le duplicateur répond par un élément  de . Après  tours, on possède  points  de  et  de . Le duplicateur gagne le jeu si l'application  est un isomorphisme partiel (par exemple, si les structures sont des graphes, alors cela signifie que deux éléments  sont voisins si et seulement si  le sont). On dit que le duplicateur a une stratégie gagnante dans un jeu à  tours s'il sait gagner quelle que soit la manière dont joue le spoiler. On écrit alors .

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

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

1.- L'idée est de prendre  dans  et  en dehors de , où  désigne la classe des structures de taille paire.

2.- On commence avec deux structures  et  avec univers  et . Évidemment,  est dans  et  n'y est pas.

3.- Pour , 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  et , le duplicateur gagne toujours, et que  et  ne peuvent être distingués dans FO[2], c'est-à-dire que  pour toute formule  de FO[2].

4.- On monte maintenant d'échelle en augmentant m. Par exemple, pour m = 3, il faut trouver  et  tels que le duplicateur gagne toujours dans un jeu à trois mouvements. On peut montrer que cela est possible avec  et . Plus généralement, on peut prendre  et ; 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  l'ensemble des graphes sur l'ensemble des sommets ; il y a  éléments dans . Soit  une propriété des graphes ; on note

et

pourvu que cette limite existe.
Prenons par exemple pour  la propriété «  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

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 que 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 , 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 . Pour un mot  on crée une structure  comme suit : l'univers est l'ensemble  correspondant aux positions dans le mot, avec l'ordre usuel. Deux relations unaires  et  sont vraies selon la valeur de la lettre :  est vrai si  et  est vrai si . Par exemple,  a l'univers , et  est vrai pour  et  pour . Un exemple de formule de logique du premier ordre est :

Cette formule décrit le fait que les lettres  suivent les lettres  dans le mot, en d'autres termes que le mot appartient au langage rationnel dont une expression régulière est . 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  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

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.
 . 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.
 . 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.
 . Contient une liste de problèmes ouverts.

Livres de référence

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

Théorie des modèles