Notions mathématiques

Alphabets, mots, langages

Soit Σ un ensemble de symboles. Nous considérons le monoïde libre (noté Σ ∗ ) formé à partir de la base Σ par l’opération « . », qui est donc associative et dotée d’un élément neutre noté ε. L’ensemble Σ est appelé alphabet, et ses éléments lettres ; les éléments de Σ ∗ sont appelés mots, l’opération « . » concaténation et son élément neutre le mot vide. Un ensemble (fini ou non) de mots sur Σ ∗ est appelé langage. L’ensemble Σ ∗ est appelé langage universel. Enfin, un ensemble de langages est appelé une classe de langages. Pour tout mot w de Σ ∗ et tout entier naturel n, w n dénote le mot formé en concaténant n fois le mot w ; par convention, w 0 = ε. Pour toute lettre l de Σ et tout mot w, |w| l dénote le nombre d’occurrences de l dans w ; et la longueur d’un mot est notée |w| = P l∈Σ |w| l . Enfin, l’image de Parikh est une fonction (notée ψ) qui associe à tout mot w construit sur un alphabet Σ un vecteur v de N~ Σ, tel que v.l = |w| l pour tout l ∈ Σ. Par extension, l’image de Parikh d’un langage L est définie comme l’ensemble des images de Parikh de ses mots : ψ(L) = {ψ(w) | w ∈ L}. 

Alphabets gradués, termes, contextes 

Un alphabet gradué est un ensemble de symboles, accompagné d’une fonction nommée arité (notée ρ) qui associe à tout élément de l’ensemble un entier naturel. Dans ce contexte, nous écrirons parfois sk pour introduire un nouveau symbole s d’arité ρ(s) = k. Si S est un alphabet gradué, l’ensemble des termes sur S est défini inductivement de la manière suivante : étant donné n termes t1 . . . tn sur S et un symbole s de S tel que ρ(s) = n, s(t1, . . . , tn) est un terme sur S. Si s est d’arité zéro, nous écrirons parfois s au lieu de s(). Une position dans un terme est un mot de (N) ∗ . Étant donné un terme t, une position p est dite valide dans t si et seulement si p = ε ou si p = ip0 , t = s(t1 . . . tn) et i ∈ [n] et que p 0 est une position valide dans ti . L’ensemble des positions valides d’un terme t est appelé le domaine de t (noté Dom(t)). Le plus petit ancêtre commun de deux positions p et p 0 dans un terme désigne la position construite comme le plus long préfixe commun à p et p 0 . Étant donné une position p valide dans un terme t, le sous-terme de t à la position p (noté t|p) est défini inductivement comme : t|p = t si p = ε ; et t|p = ti |p 0 si t = s(t1 . . . tn) et p = ip0 ; la définition des termes et de la validité d’une position garantit l’existence d’un tel sous-terme. Par analogie avec les arbres, une position valide désignant un sous-terme d’arité nulle est appelée une feuille, et la position ε la racine. Considérons maintenant un ensemble dénombrable de variables X (notées x, y, z, . . .) : un contexte sur S est un terme construit sur l’alphabet gradué S ∪ X où tous les éléments de X sont d’arité nulle. Tout sous-terme x() dans un contexte C est appelé une occurrence de x dans C. Un contexte est dit linéaire s’il contient au plus une occurrence de x pour tout x ∈ X . Étant donné un contexte C, son arité ρ(C) dénote le nombre de variables distinctes ayant des occurrences dans C ; un contexte d’arité k est également dit k-aire. Par suite, si X = {x1 . . . xn} est l’ensemble ordonné des variables d’un contexte n-aire C, C[t1, . . . , tn] = C[xi ← ti ] dénote le résultat de la substitution simultanée de chacune des variables xi par ti dans C, pour i ∈ [n]. Celle-ci est distincte de la séquence de substitutions C[x1 ← t1] . . .[xn ← tn], en particulier si l’un des termes ti contient une variable xj avec j > i : aucune substitution n’est alors effectuée dans le terme substitué ti . Enfin, si C est un contexte unaire et n ∈ N, l’exponentiation C n = C[x ← C] . . .[x ← C] dénote le contexte obtenu en substituant n − 1 fois C à x (séquentiellement) ; ainsi, C 1 = C et, par abus de notation, C 0 = x est le contexte trivial. 

Ensembles semilinéaires

Étant donné un ensemble E et un tuple de vecteurs T = (v0, . . . , vn) appartenant chacun à N~ E, l’ensemble linéaire défini par T est l’ensemble de vecteurs :    v0 + X i∈[n] kivi | ∀i ∈ [n], ki ∈ N    En outre, un ensemble de vecteurs est dit semilinéaire s’il peut être décrit comme une union finie d’ensembles linéaires de vecteurs. L’appartenance d’un vecteur v à un ensemble semilinéaire est décidable avec une complexité en espace logarithmique par rapport à la norme supremum kvk de v (en choisissant le bon ensemble linéaire et en soustrayant itérativement un vi judicieusement choisi jusqu’à aboutir à v0)

Logique formelle 

La logique formelle permet de formuler et d’évaluer la vérité de propositions portant sur une classe particulière d’objets. Un langage logique permet d’écrire des formules, lesquelles s’appuient sur un ensemble de prédicats et de relations en lien avec la classe d’objets étudiée. Différents types de logiques offrent divers degrés d’expressivité, ce qui revêt une importance particulière lorsqu’on considère, en théorie des modèles, les ensembles d’objets satisfaisant une formule en particulier. Nous définissons ici deux types de logiques, la logique du premier ordre et la logique du second ordre monadique, sur une signature quelconque, en rappelant la syntaxe et la sémantique usuelle des formules qu’elles construisent.

Signatures, formules 

Soit X1 et X2 deux ensembles dénombrables de variables, respectivement dites du premier ordre et du second ordre, et notées x, y, z, . . . et X, Y, Z, . . . . Une signature est un ensemble de symboles nommés prédicats ou relations (notés P, Q, R, . . .), munis de deux arités ρ1 et ρ2 . Ces arités correspondent respectivement aux nombres de variables du premier et du second ordre dont dépend un prédicat. Nous emploierons souvent dans la suite le terme de prédicat par défaut, en réservant le terme de relation pour des prédicats dont l’arité est supérieure ou égale à deux. Dans le cas général, une signature peut également contenir des termes, interprétés comme des constantes, ainsi que des fonctions s’appliquant à des séries de termes ou de variables, et munies d’une interprétation fonctionnelle de façon similaire à la sémantique donnée plus loin pour les prédicats. N’en ayant pas l’usage dans la suite, nous excluons ces derniers éléments de cette présentation. En outre, toute fonction dans une signature peut être remplacée de façon équivalente par un prédicat d’arité supérieure dénotant une relation fonctionnelle. Si une signature ne contient que des symboles du premier ordre, c’est-à-dire que ρ2 (P) = 0 pour tout P, la logique du premier ordre sur cette signature décrit l’ensemble de formules suivant : — Si P est un prédicat, alors les expressions P(x1, . . . , xρ1 (P)) et x = y (égalité) sont des formules dites atomiques. — Si φ, ψ sont des formules, alors les expressions ¬φ (négation), φ ∧ ψ (conjonction), φ ∨ ψ (disjonction), φ ⇒ ψ (implication), φ ⇔ ψ (équivalence), ∃x.φ (quantification existentielle) et ∀x.φ (quantification universelle) sont des formules dites composites. L’ensemble des formules de la logique monadique du second ordre est composé de la même façon, en y ajoutant d’éventuels prédicats portant sur des variables du second ordre, ainsi que les constructions suivantes pour les formules : — Les expressions x ∈ X (appartenance) et X ⊆ Y (inclusion) sont des formules atomiques. — Si φ est une formule, les expressions ∃ 2X.φ et ∀ 2X.φ sont des formules composites. Le qualificatif de « monadique » dénote le fait que les variables du second ordre peuvent être vues comme des prédicats unaires sur les variables du premier ordre. Ainsi, une formule atomique d’appartenance x ∈ X dénote simplement l’application X(x) du prédicat dénoté par X à la variable x. Plusieurs autres formules atomiques données ici peuvent être définies à partir d’un ensemble plus réduit de primitives, comme l’illustre la sémantique donnée plus bas ; cependant, nous les définissons comme des primitives par simplicité. Comme pour les termes, une sous-formule est formule apparaissant dans une formule composite. Si une formule φ est une quantification, la variable qui lui est rattachée est dite liée dans toute sous-formule de φ. Toute variable apparaissant dans une formule sans être liée par un quantificateur est dite libre dans cette formule ; et une formule close est une formule ne contenant pas de variables libres.

 Sémantique, modèles 

Toute formule logique construite sur une signature dénote une affirmation portant sur une classe d’objets, dont le sens dépend de l’interprétation associée aux prédicats de la signature et aux variables libres de la formule. L’approche de la théorie des modèles confronte les formules logiques aux objets dont elles traitent (les modèles), en associant à toute formule une valeur de vérité dépendant d’un modèle et de la valuation des éventuelles variables libres de la formule dans un domaine fixé. Plus précisément, pour une signature donnée, un modèle M = (D, [[]]) est formé par un domaine D et une interprétation [[]] qui associe à tout prédicat P de la signature une fonction [[P]] de Dρ1 (P)×P(D) ρ2 (P) dans B = {Vrai, Faux}. Enfin, une valuation est une fonction partielle de X1 dans D et de X2 dans P(D).