Discipline de type intersection

En logique mathématique , la discipline des types d'intersection est une branche de la théorie des types englobant les systèmes de types qui utilisent le constructeur de types d'intersection pour attribuer plusieurs types à un seul terme. En particulier, si un terme peut être attribué à la fois au type et au type , alors le type d'intersection peut lui être attribué (et vice versa). Par conséquent, le constructeur de types d'intersection peut être utilisé pour exprimer un polymorphisme ad hoc hétérogène fini (par opposition au polymorphisme paramétrique ). Par exemple, le terme λ peut être attribué au type dans la plupart des systèmes de types d'intersection, en supposant pour la variable terme à la fois le type de fonction et le type d'argument correspondant .

Les principaux systèmes de types d'intersection comprennent le système d'attribution de type Coppo–Dezani, le système d'attribution de type Barendregt-Coppo–Dezani, et le système d'attribution de type d'intersection essentiel. termes λ sous β-réduction (et les caractérisent souvent exactement) .

Dans les langages de programmation, tels que TypeScript et Scala, les types d'intersection sont utilisés pour exprimer le polymorphisme ad hoc .

Français La discipline du type d'intersection a été lancée par Mario Coppo, Mariangiola Dezani-Ciancaglini , Patrick Sallé et Garrel Pottinger. La motivation sous-jacente était d'étudier les propriétés sémantiques (telles que la normalisation ) du λ-calcul au moyen de la théorie des types . Alors que les travaux initiaux de Coppo et Dezani ont établi une caractérisation théorique des types de la normalisation forte pour le λI-calcul, Pottinger a étendu cette caractérisation au λK-calcul. De plus, Sallé a contribué à la notion de type universel qui peut être attribué à n'importe quel λ-terme, correspondant ainsi à l'intersection vide. L'utilisation du type universel a permis une analyse fine de la normalisation de la tête, de la normalisation et de la normalisation forte. En collaboration avec Henk Barendregt , un modèle λ de filtre pour un système de types d'intersection a été donné, liant de plus en plus étroitement les types d'intersection à la sémantique du λ-calcul.

En raison de la correspondance avec la normalisation, la typabilité dans les systèmes de types d'intersection importants (à l'exclusion du type universel) est indécidable . De manière complémentaire, l'indécidabilité du problème dual d' habitation de type dans les systèmes de types d'intersection importants a été prouvée par Paweł Urzyczyn. Plus tard, ce résultat a été affiné en montrant la complétude de l'espace exponentiel de l'habitation de type d'intersection de rang 2 et l'indécidabilité de l'habitation de type d'intersection de rang 3. De manière remarquable, l'habitation de type principal est décidable en temps polynomial .

Le système d'attribution de type Coppo-Dezani étend le λ-calcul simplement typé en permettant de supposer plusieurs types pour une variable terme.

Le terme langage de est donné par les termes λ (ou expressions lambda ) :

Le type de langage de est défini inductivement par la grammaire suivante :

Le constructeur de type d'intersection ( ) est pris modulo l'associativité, la commutativité et l'idempotence.

Les règles de frappe , , , et de sont :

La typabilité et la normalisation sont étroitement liées par les propriétés suivantes :

• Réduction du sujet : Siet, alors.
• Normalisation : Si, alorsa une forme β-normale .
• Typabilité des termes λ fortement normalisants : Si est fortement normalisant , alors pour certains et .
• Caractérisation de la λI-normalisation : a une forme normale dans le λI-calcul, si et seulement si pour certains et .

Si le langage de type est étendu pour contenir l'intersection vide, c'est-à-dire , alors il est fermé sous la β-égalité et est solide et complet pour la sémantique d'inférence.

Le système d'attribution de type Barendregt–Coppo–Dezani étend le système d'attribution de type Coppo–Dezani dans les trois aspects suivants :

• constante de type universelle (apparentée à l'intersection vide) qui peut être attribuée à n'importe quel terme λ.
• de sous-typage de type d'intersection sur les types avec une règle de typage correspondante.

Le terme langage de est donné par les termes λ (ou expressions lambda ) :

Le type de langage de est défini inductivement par la grammaire suivante :

Le sous-typage de type d'intersection est défini comme le plus petit préordre ( relation réflexive et transitive ) sur les types d'intersection satisfaisant les propriétés suivantes :

Le sous-typage de type d'intersection est décidable en temps quadratique.

Les règles de frappe , , , , , et de sont :

• Sémantique : est solide et complète par rapport à un modèle λ de filtre, dans lequel l'interprétation d'un terme λ coïncide avec l'ensemble des types qui peuvent lui être assignés.
• Réduction du sujet : Siet, alors.
• Développement du sujet : Si et , alors .
• Caractérisation de la normalisation forte : est fortement normalisante par rapport à la β-réduction, si et seulement si est dérivable sans règle pour certains et .
• Paires principales : Si est fortement normalisant, alors il existe une paire principale telle que pour tout typage la paire peut être obtenue à partir de la paire principale au moyen d'expansions de type, de levages et de substitutions.