Les algorithmes séquentiels

Les algorithmes séquentiels

 Logique du premier ordre

Bien que nous aurions pu l’éviter, dans un soucis de cohérence de notation et de simplification de la présentation, notre formalisation de la logique du premier ordre ne sera pas classique 1 . En effet : 1. Nous suivrons la présentation de Yuri Gurevich d’une part concernant le symbole undef pour les fonctions partielles, et d’autre part concernant les relations. Ainsi, les symboles de relation seront vus comme des symboles de fonction comme les autres, mais ayant leur valeur dans les booléens 2 . En particulier les formules seront vues comme des termes comme les autres. 2. Nous n’utiliserons pas la notion de variable logique dans les termes et formules. En particulier tous les termes et formules seront clos, et nous n’utiliserons pas les quantificateurs. Ce que nous appelerons « variables » seront les symboles dynamiques d’arité 0, dont l’interprétation pourra évoluer au fur et à mesure d’une exécution. Ces précautions par rapport à la littérature habituelle étant prises, nous allons pouvoir présenter le plus succintement possible les structures du premier ordre, qui nous serviront dans la section suivante à formaliser (d’après le second postulat) les états d’une exécution :

Structures du premier ordre Un langage (du premier ordre)

L est un ensemble de symboles de fonction. Un langage sera dit fini si son cardinal est fini. Comme nous ne nous intéresserons qu’à des langages permettant d’écrire des programmes, nous supposerons que tous nos langages seront finis. L’arité d’un symbole de fonction f est le nombre d’arguments de f. Par exemple la factorielle est unaire alors que l’addition est binaire. Notation. Soient α(f) l’arité de f, ou tout simplement α en l’absence d’ambiguïté, et Fα(L) l’ensemble des symboles de fonction d’arité α de L. Pour homogénéiser les écritures, nous considèrerons que les symboles de constante c seront des symboles de fonction d’arité 0.

Définition 1.1.1.

(Interprétation dans une structure) Une structure (du premier ordre) X de langage L, aussi appelée L-structure, est la donnée : 1. d’un ensemble U(X) non vide appelé l’univers de X 2. pour chaque symbole s ∈ L d’une interprétation s X telle que : a. si c ∈ F0(L) alors c X est un élément de U(X) b. si f ∈ Fα(L) avec α > 0 alors f X est une application : U(X) α → U(X) Notation. Soit L(X) le langage de la structure X. Les fonctions d’un langage L sont interprétées dans une structure X comme étant totales. Pour simuler les fonctions partielles dans X nous suivrons la présentation de Gurevich [Gur00] en ajoutant un symbole undef :

Exemple 1.1.2.

(Les fonctions partielles) Nous supposerons que le symbole undef sera présent dans tous nos langages, et comme U(X) est non vide il contient au moins un élément, qui nous servira comme interprétation de undef . Nous dirons que f n’est pas définie en (a1, . . . , aα) si f X (a1, . . . , aα) = undef X , et nous noterons : 1. Dom(f, X) =def {(a1, . . . , aα) ∈ U(X) α | f X (a1, . . . , aα) 6= undef X } 2. Im(f, X) =def f X (Dom(f, X)) Les fonctions partielles permettent notamment de définir des constructeurs et des opérations sur des sous-ensembles de l’univers. Je les utilise en particulier à la section B.1 pour introduire une notion de typage dans cette présentation. Cela n’est pas nécessaire pour prouver notre caractérisation impérative des classes algorithmiques, toutefois j’ai inclus cette section dans le chapitre des Compléments pour : 1. Obtenir une définition naturelle de la taille d’un élément dans une structure, en prenant le nombre de symboles utilisés pour représenter cet élément dans la structure. En effet, nous utilisons la notion de taille pour définir les classes en temps p.33, et les classes en espace p.74, et nous trouvions insatisfaisant de la supposer simplement donnée. 

Termes d’un langage

Les termes permettent de représenter syntaxiquement les éléments de l’univers considéré. Cette notion sera centrale pour énoncer le troisième postulat de Gurevich p.27, mais pas seulement. En particulier, en utilisant notre formalisation des booléens, les formules seront des termes comme les autres. Cela simplifiera nos notations par la suite, en particulier la traduction p.88. Rappel. Nous n’utilisons pas la notion de variable logique, le mot « variable » étant réservé aux symboles dynamiques d’arité 0. En particulier les termes seront clos, et nous n’utiliserons pas les quantificateurs dans les formules.

Cela ne sera cependant pas un problème car la preuve de proposition 2.1.9 p.40 montre qu’avec le troisième postulat nous n’avons en fait besoin que de formules de la forme ( ∧ 1≤i,j≤n Eij ) où Eij est ti = tj ou ti 6= tj , et ti , tj sont des termes. Définition 1.1.4. (Termes d’un langage) T erm(L), l’ensemble des termes (clos) du langage L, est défini par induction : 1. F0(L) ⊆ T erm(L) 2. Si f ∈ Fα(L) avec α > 0 et t1, . . . , tα ∈ T erm(L) alors f t1 . . . tα ∈ T erm(L) Soit T un ensemble de termes. Nous dirons que T est stable par sous-termes s’il vérifie que pour tout f t1 . . . tα ∈ T alors t1, . . . , tα ∈ T. Nous définissons plus rigoureusement cette notation p.115 en introduisant Sub(T), la clôture par sous-termes de T. Cela nous sera utile pour faire des preuves par induction sur les termes, notamment l’isomorphisme par remplacement p.21. Nous pouvons maintenant étendre l’interprétation des symboles dans une structure à l’interprétation des termes :

Définition 1.1.5. (Interprétation d’un terme) L’interprétation t X d’un terme t ∈ T erm(L) dans une L-structure X est définie par induction sur t : 1. Si t = c ∈ F0(L) Alors t X =def c X 2. Si t = f t1 . . . tα où f ∈ Fα(L) avec α > 0 et t1, . . . , tα ∈ T erm(L) Alors t X =def f X (t1 X , . . . ,tα X ) Illustrons cette définition en introduisant la représentation unaire des entiers, les autres bases étant esquissées p.144. Exemple 1.1.6. (Les entiers unaires N1) L’univers est étendu avec une copie de N. Les constructeurs sont {∅, S}, interprétés par : 1. ∅ X = 0 2. S X : x 7→ x + 1 Où le successeur S est supposé indéfini ailleurs que sur N1. Notez que les termes formés uniquement de constructeurs sont de la forme S n∅, et ils sont interprétés par Sn∅ X = n. Nous dirons que S n∅ est la représentation de n. Par défaut nous utiliserons dans notre manuscrit la représentation unaire pour les entiers. Ainsi, quand il n’y aura pas d’ambiguïté, nous confondrons la valeur et la représentation. Par exemple dans un programme 4 désignera le terme SSSS∅, et t+ 1 sera une notation pour le terme St.

Enfin, nous introduisons p.142 une définition de la taille d’un élément comme étant le nombre de symboles utilisés dans sa représentation. Dans ce formalisme la taille de n ∈ N1 est de n + 1. Remarque. Tous les termes ne sont pas des représentations. Par exemple 4 + 3, qu’il faudrait écrire rigoureusement +S 4∅S 3∅ (notation polonaise), vaut 7 mais n’est pas la représentation S 7∅ de 7. Ainsi, dans notre formalisme la taille de 4 + 3X est donc 8 (le nombre de symboles formant S 7∅), et non 10 (le nombre de symboles formant +S 4∅S 3∅). Maintenant que nous avons introduit les booléens et les entiers unaires, il est possible de construire des termes en mélangeant les constructeurs ou les opérations disponibles. Par exemple, que vaut le terme Strue ? Comme le successeur S est défini uniquement sur N1 et que trueX n’est pas un entier, nécessairement nous avons que StrueX = undef X . Nous dirons par la suite qu’un terme t est bien typé sur X si t X 6= undef X .