Présentation syntaxique de ICCΣ

Présentation syntaxique de ICCΣ

ICCΣ est une extension d’une version légèrement modifiée de, du calcul des constructions implicite (ICC) défini par Miquel dans sa thèse [Miq01]. Miquel définit un calcul des constructions ([Coq85, CH88]) avec, comme dans CCω [Coq86]), une hiérarchie d’univers emboîtés et une relation de cumulativité entre ces univers. Le système de Miquel se distingue toutefois nettement de CCω sur deux points : d’une part, sa syntaxe est à la Curry (pas d’annotation de type dans les abstractions), d’autre part il introduit une nouvelle construction primitive, le produit dépendant implicite, noté ∀x : T .U. Contrairement au produit dépendant habituel, le produit dépendant implicite n’a ni constructeur ni éliminateur. Intuitivement, il ressemble à l’opérateur de polymorphisme pour Système F ([Gir72, Rey74]) à la différence près que dans Système F, le polymorphisme n’agit que sur des variables de type, alors que dans ICCΣ, le produit implicite agit sur n’importe quelle variable de terme. Ses règles d’introduction et d’élimination sont semblables à celles du polymorphisme imprédicatif d’une version à la Curry du Système F [Lei83, MS82, Mit88] où l’abstraction de type et l’application de type se font implicitement. Comme le remarquent Barthe et Coquand dans [BC00], le Calcul Implicite de Miquel combine la démarche des Domain-Free Pure Type Systems [BS00] et des Type assignment systems [Bar91].

ICCΣ étend ICC en lui ajoutant les sommes dépendantes. Pour cela, nous allons enrichir le langage de termes , ajouter les règles de réduction liées aux sommes dépendantes et adapter la relation de cumulativité , compléter les règles de typage avec des règles de formation, introduction et élimination des sommes dépendantes et enfin démontrer pour ICCΣ quelques résultats métathéoriques simples déjà prouvés pour ICC .

Syntaxe

Nous introduisons dans cette section les différents termes du langage. Nous expliquerons plus en détail leur signification lors de la présentation des règles de typage .

Sortes et variables. De même que ICC, ICCΣ se base sur une hiérarchie infinie dénombrable de sortes (ou univers dans la terminologie de la théorie des types de Martin-Löf ).

En plus des variables et des sortes, le langage contient, comme dans le calcul des constructions, le produit dépendant Πx : T .U, ainsi que son constructeur, l’abstraction λx .M, et son éliminateur, l’application MN. Notons que dans l’abstraction, la variable abstraite n’a pas d’annotation de type. La nouveauté de ICC est le produit dépendant implicite ∀x : T .U, que nous avons déjà présenté.

La syntaxe de ICCΣ étend celle de ICC en ajoutant les sommes dépendantes Σx : A.B. Elles ont comme constructeurs les paires dépendantes (a , b) et comme éliminateurs les éliminateurs de somme dépendante ElimΣ(x y.f ,c). Dans la continuité de la syntaxe de ICCΣ, qui est à la Curry, les paires n’ont pas d’annotation de type et les variables des éliminateurs ne sont pas non plus annotées. Nous ajoutons deux autres sommes dépendantes le type sous-ensemble {x : A | B} et le type existentiel ∃x : A.B. Le type sous-ensemble n’a ni constructeur ni éliminateur. Le type existentiel a un constructeur (¦, b) et un éliminateur Elim∃(y.f ,c).

CONVENTION. L’abstraction de variables est une opération associative à gauche et l’application de termes est une opération associative à droite. Ainsi λx .λy .M = λx . (λy .M) et MNR = (MN)R. Par ailleurs, l’application de termes a la priorité sur l’abstraction de variable. Ainsi λx .MN = λx . (MN).

La classification suivante des termes de ICCΣ sera utilisée tout au long de ce document.

DÉFINITION (Classification des termes). Soit M un terme de ICCΣ.
• M est un constructeur de type s’il est un produit dépendant, un produit implicite, une somme dépendante, un type existentiel, un sous-ensemble ;
• M est un constructeur s’il est une abstraction, une paire dépendante ou une paire existentielle ;
• M est un éliminateur s’il est une application, un éliminateur de somme dépendante ou un éliminateur d’existentielle.

Typage

Dans cette section, nous allons ajouter à notre langage des règles de typage. Ces règles permettent d’associer à un terme du langage un autre terme, son type. Ces règles sont une restriction du langage : certains termes ne peuvent être associés à aucun type. Mais ne considérer que les termes typables, c’est-à-dire les termes pour lesquels il est possible d’associer un type, présente des avantages. Ainsi, connaître le type d’un terme permet de lui donner une signification. Via l’isomorphisme de Curry-Howard [CF58, How80], nous pouvons associer une proposition mathématique à un type : un terme d’un certain type est alors interprété comme une preuve de la proposition associée à son type. Un deuxième avantage est de pouvoir garantir le comportement calculatoire des termes typables. Ainsi une propriété souhaitable des λ-calculs typés est le fait que tout terme bien typé ne peut se réduire indéfiniment. Cette propriété, appelée normalisation forte, signifie que tout programme (terme) bien typé retournera une valeur lorsqu’il est exécuté (réduit).

Jugements. Nous définissons deux nouvelles structures syntaxiques utilisées dans les règles de typage : les jugements de bonne formation et les jugements de typage. Ces jugements utilisent eux-mêmes une troisième structure : les contextes de typage.

Contextes de typage. Les contextes de typage permettent d’associer des types à un ensemble de variables.

DÉFINITION (Contextes). Un contexte de typage ou, plus brièvement, contexte, est une liste ordonnée, éventuellement vide, de déclarations de type. Une déclaration de type est un couple formé d’une variable x et d’un terme T, noté x : T, qui permet ainsi d’assigner un type à une variable. Plus formellement, nous avons la définition inductive suivante :
Γ ::= •|Γ;x : T

Nous établissons maintenant quelques définitions et notations utiles pour manipuler les contextes.

Le rapport de stage ou le pfe est un document d’analyse, de synthèse et d’évaluation de votre apprentissage, c’est pour cela rapport-gratuit.com propose le téléchargement des modèles complet de projet de fin d’étude, rapport de stage, mémoire, pfe, thèse, pour connaître la méthodologie à avoir et savoir comment construire les parties d’un projet de fin d’étude.

Table des matières

Introduction
Le λ-calcul, ses extensions et ses applications
Problématique de la thèse
Présentation de la thèse
Première partie 1. Syntaxe de ICCΣ
Chapitre 1. Présentation syntaxique de ICCΣ
1. Syntaxe
2. Calcul
3. Typage
Chapitre 2. Préservation du typage par réduction
1. η-réduction et préservation du typage
2. Difficultés à établir la préservation du typage par βι-réduction
3. Substitutions
4. Jugements de structure
5. Inversion des constructeurs de types
6. Inversion des constructeurs
7. Préservation du typage par βι-réduction
Deuxième partie 2. Modèles de ICCΣ
Préambule
Chapitre 3. Modèle abstrait de cohérence
1. Présentation du modèle
2. Propriétés
Chapitre 4. Notions sur les espaces cohérents
1. Espaces cohérents
2. La catégorie des quasi-espaces cohérents
3. La catégorie des µ-espaces cohérents
Chapitre 5. Modèle de cohérence de ICCΣ
1. Interprétation des types
2. Modèle concret du calcul
Perspectives
Troisième partie 3. AICCΣ
Chapitre 6. Présentation syntaxique de AICCΣ
1. Syntaxe
2. Propriétés
Chapitre 7. Relèvement du typage
1. Substitutions et jugements de structure
2. Preuve du relèvement
Quatrième partie 4. Décidabilité du typage
Préambule
Chapitre 8. Inférence de type extrait
1. Sous-algorithmes
2. Algorithme principal
3. Correction
4. Complétude
5. Algorithmes dérivés
Chapitre 9. Inférence de type
1. Règles de réduction
2. Complétude des règles de réduction
3. Correction des règles de réduction
4. Algorithme de réduction
5. Algorithme
Perspectives
Conclusion
Perspectives
Travaux connexes
Annexes