Soutenance mémoire
Le système UT Tr
Ce système est une extension de la version du calcul UT T considérée dans [Gog94], par l’ajout d’une règle de jugement d’égalité (voir section 2.4). Le calcul UT Tr est formulé dans le « Logical Framework » LF [Luo94b], un système formel qui a pour vocation d’être utilisé comme un cadre pour définir des théories de types. LF est une théorie simple possédant des types fonctionnels, des types dépendants, et dans laquelle on définit de nouvelles théories par ajout de constantes et de règles d’égalité. UT Tr comprend un univers imprédicatif des propositions qui est distinct de la collection des types. On inclut le type des propositions et les types des preuves de chaque proposition dans cet univers. Nous retrouvons également un univers prédicatif des types. Cet univers inclut les types inductifs (qui sont importants pour la programmation et les mathématiques), comme les entiers naturels, le type produit, les listes etc. UT Tr fournit un excellent environnement pour étudier les spécifications et la vérification de programmes. Luo discute cette approche dans [Luo93a, Luo94b].
« Logical Framework » LF
Les termes de LF sont de la forme suivante : Type, El(A), (x : K)K′ , [x : K]k′ , f(k), où les occurrences libres de la variable x sont liées par les opérateurs (x : K) et [x : K] respectivement.
Il y a cinq formes de jugement dans LF :
• Γ ⊢ valid, signifie Γ est un contexte valide ;
• Γ ⊢ Kkind, signifie que K est une sorte,
• Γ ⊢ k : K signifie que k est un objet de sorte K,
• Γ ⊢ k = k′ : K signifie que k et k′ sont des objets égaux de sorte K,
• Γ ⊢ K = K′ signifie que K et K′ sont deux sortes égales.
Schéma pour les types inductifs
Le système UT Tr contient des types inductifs dont l’introduction repose sur la notion de schéma inductif. Nous allons considérer ici les opérateurs et constantes de LF permettant d’introduire de manière générale des types inductifs.
Définition 2.3 (Petite sorte). On dit qu’une sorte A est une petite sorte (small kind) si
• A ≡ El(M) ou
• A ≡ (x : A1)A2, où A1 et A2 sont des petites sortes.
Définition 2.4 (Famille de schémas). Soit Γ un contexte valide et X une variable.
• Une sorte Φ est un opérateur strictement positif dans Γ par rapport à X, notation P OSΓ;X(Φ), si Γ, X : Type ⊢ Φkind et
– Φ ≡ El(X) ou
– (x : A)Φ0, où A est une petite sorte et P OSΓ;X(Φ0).
• Une sorte Θ est un schéma inductif par rapport à X, notation SCHΓ;X(Θ), si
– Θ ≡ El(X),
– (x : A)Θ0, où A est une petite sorte et SCHΓ;X(Θ0), ou
– (Φ)Θ0, où P OSΓ;X(Φ) et SCHΓ;X(Θ0).
• Une séquence finie de sortes hΘ1, . . . , Θni, notée Θ¯ , est une famille de schémas dans Γ par rapport à X, notation SCHΓ;X(Θ1, . . . , Θn), si SCHΓ;X(Θi) pour 1 ≤ i ≤ n .
Notation
• Par la suite, nous prendrons l’habitude d’omettre l’opérateur El lorsque nous considérerons les opérateurs et constantes relatifs aux types inductifs ainsi que certaines constantes déclarées.
• Nous notons Φ(M) pour [M/X]Φ si P OSΓ;X(Φ), pareillement pour Θ telle que SCHΓ;X(Θ).
• Si Θ est un schéma inductif par rapport à X alors nous notons ARIT YX(Θ) la séquence Φ1, . . . , Φm des opérateurs strictement positifs de Θ dans Γ par rapport à X.
• Nous utilisons la notation F[x1, . . . , xn] =df M pour présenter des définitions avec des variables x1, . . . , xn. La notation F[N1, . . . , Nn] représente donc le terme ou la sorte [N1, . . . , Nn/x1, . . . , xn]M.
Propriétés du système UT Tr
Notre objectif est de montrer que certaines propriétés, comme la consistance, la terminaison des calculs, sont vérifiées pour le système UT Tr . Or, nous rappelons que UT Tr est le système UT T enrichi d’une nouvelle règle d’égalité concernant les types finis, à savoir la règle (ϑ-eq). Healdene Goguen a démontré lors de sa thèse [Gog94], sous la direction Rod Burstall et Zhaohui Luo, que le calcul UT T possède certaines propriétés dont la normalisation forte, la préservation du type et la confluence. Goguen, afin de réaliser sa preuve, a développé une sémantique opérationnelle typée pour UT T qu’il nomme UT T S . Pour construire notre preuve, nous allons donc adapter la technique employée pour prouver les propriétés de normalisation forte, de confluence et de préservation du type du système UT T. Les réductions non typées fournissent une sémantique opérationnelle naturelle, c’est-à dire une description de l’aspect calculatoire pour les théories des types. Les lemmes de normalisation forte nous apprennent qu’une telle sémantique est correcte. Cependant, ces réductions ne prennent pas en compte les informations sur les types et ne nous donnent pas d’informations sur les formes canoniques des termes. Goguen introduit donc la sémantique opérationnelle typée qui définit une réduction vers la forme normale pour les termes qui sont bien typés dans la théorie. Une fois la sémantique opérationnelle typée UT T S définie, Goguen prouve que ce système vérifie certaines propriétés comme la normalisation forte, la préservation du type et la confluence puis il transfère ces propriétés au calcul UT T en démontrant que UT T est correcte par rapport à UT T S . Nous suivrons dans notre démonstration la même démarche.
la sémantique opérationnelle : le système UT TrS
Nous introduisons ici le système UT TrS qui représente une sémantique opérationnelle typée pour le calcul UT Tr .
Définitions pour la métathéorie
Dans un premier temps, nous présentons plusieurs notions métathéoriques qui seront importantes pour la présentation de UT TrS ainsi que pour exposer les propriétés de UT Tr.
Définition 3.1 (Sous-dérivation). Soient deux dérivations J1 et J2. J1 est une sousdérivation de J2 si J1 apparaît comme un sous-arbre de J2.
Définition 3.2 (Equivalence syntaxique). Deux termes sont équivalents syntaxiquement, M ≡ N, s’ils sont identiques au renommage des variables liées près.
Définition 3.3 (Famille de Pré-schémas). Soit X une variable.
• Une sorte Φ est un opérateur pré-positif par rapport à X, notation P P OSX(Φ), si :
– Φ ≡ El(X) ou
– (x : A)Φ0, où A est une petite sorte et P P OSX(Φ0).
• Une sorte Θ est un pré-schéma inductif par rapport à X, notation P SCHX(Θ), si :
– Θ ≡ El(X),
– (x : A)Θ0, où A est une petite sorte et P SCHX(Θ0), ou
– (Φ)Θ0, où P P OSX(Φ) et P SCHX(Θ0).
• Une séquence finie de sortes hΘ1, . . . , Θni, notée Θ¯ , est une famille de préschémas par rapport à X, notation P SCHX(Θ1, . . . , Θn), si P SCHX(Θi) pour 1 ≤ i ≤ n.
|
Table des matières
Introduction
1 Contexte
1.1 Les modèles
1.1.1 Le modèle ensembliste
1.1.2 Le modèle catégorique
1.1.3 Les modèles de Kripke
1.1.4 λ-modèles
1.2 Notion de sous-typage
2 Le système UT Tr
2.1 « Logical Framework » LF
2.1.1 Spécifier une théorie de types dans LF
2.1.2 Schéma pour les types inductifs
2.2 Un univers imprédicatif des propositions
2.3 Univers prédicatif
2.4 La ϑ-réduction
3 Propriétés du système UT Tr
3.1 Plan de la partie technique
3.2 la sémantique opérationnelle : le système UT TrS
3.2.1 Définitions pour la métathéorie
3.2.2 Jugements et dérivations
3.2.3 Propriétés de UT TrS
3.2.4 Construction d’un modèle ensembliste classique pour UT Tr
3.2.5 UT Tr est correcte par rapport à UT TrS
3.2.5.1 Objets sémantiques
3.2.5.2 Interprétation
3.2.5.3 Correction
4 Sous-typage coercitif
4.1 Présentation : Le système formel
4.1.1 Formes de jugements
4.1.2 Sous-typage
4.1.3 Condition de cohérence
4.1.4 Sous-sortes
4.1.5 Règles coercitives
4.2 Preuve de conservativité
4.2.1 Principaux problèmes, méthode et résultats
4.2.1.1 Completion des coercions
4.2.1.2 Le problème de conservativité
4.2.1.3 Propriétés méta-théoriques de UT Tr [R] et ses sous-systèmes
4.2.2 Plan de la preuve
4.2.3 Propriétés méta-théoriques
4.2.3.1 Sous-systèmes
4.2.3.2 Propriétés basiques
4.2.3.3 Eliminations et jugements présupposés
4.2.3.4 Elimination de la transitivité pour les sous-sortes
4.2.4 Complétion des coercions
4.2.4.1 Définition de la transformation Ψ
4.2.4.2 Ψ et les dérivations
4.2.4.3 Ψ est totale
4.2.5 Conservativité
Conclusion
