Système U (mathématiques)

En logique mathématique, le Système U et le Système U− sont des systèmes de types purs, c'est-à-dire des formes spéciales d'un calcul lambda typé avec un nombre arbitraire de sortes, d'axiomes et de règles (ou de relations entre les sortes). Ils ont tous deux été prouvés incohérents par Jean-Yves Girard en 1972. Ce résultat conduit alors à ce que la théorie des types de Martin-Löf de 1971 est incohérente car elle permet le même comportement de «type dans le type» que le paradoxe de Girard exploite. Le système U est défini comme un système de type pur avec trois sortes ; deux axiomes ; et cinq règles . Système U− est défini de la même manière à l'exception de la règle . Les sortes et sont classiquement appelés respectivement «Type» et « Genre »; le genre n'a pas de nom spécifique. Les deux axiomes décrivent "l'inclusion" des types dans les genres ( ) et des genres dans ( ). Intuitivement, les sortes décrivent une hiérarchie dans la nature des termes. Toutes les valeurs ont un type, tel qu'un type de base ( par exemple est lu comme « est un booléen») ou un type de fonction (par exemple est lu comme « est une fonction des nombres naturels aux booléens»). est la sorte de tous ces types ( est lu comme « est un type»). De nous pouvons créer plus de termes, tels que qui est le genre d'opérateurs de type niveau unaire (par exemple se lit : « est une fonction allant des types aux types», c'est-à-dire un type polymorphe). Les règles limitent la manière dont nous pouvons former de nouveaux genres. est la sorte de tous ces genres ( est lu comme « est un genre»). De même, nous pouvons construire des termes liés, selon ce que les règles permettent. est la sorte de tous ces termes. Les règles régissent les dépendances entre les sortes : dit que les valeurs peuvent dépendre de valeurs (fonctions), permet aux valeurs de dépendre des types (polymorphisme), permet aux types de dépendre des types (opérateurs de type), etc.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (5)

Concepts associés (4)

Séances de cours associées (1)

Pure type system

NOTOC In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of Barendregt's lambda cube, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts. In fact, Barendregt (1991) framed his cube in this setting.

Parametric polymorphism

In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorphic functions and data types are sometimes called generic functions and generic datatypes, respectively, and they form the basis of generic programming. Parametric polymorphism may be contrasted with ad hoc polymorphism.

Intuitionistic type theory

Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions.

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

, ,

Vibrational properties of molecular crystals are constantly used as structural fingerprints, in order to identify both the chemical nature and the structural arrangement of molecules. The simulation of these properties is typically very costly, especially ...

2019

In this paper, with the example of two different polymorphs of KEu(MoO4)(2), the influence of the ordering of the A-cations on the luminescent properties in scheelite related compounds (A',A '') (B',B '')O-4 is investigated. The polymorphs were synthe ...

American Chemical Society2015

Types dépendants dans les langages de programmation CS-452: Foundations of software

Explore les cartes, les opérateurs de type, l'équivalence, les types de première classe, System Fw, Coq, et les défis de la vérification de type dans les langages de programmation.