Système F

Le système F est un formalisme logique qui permet d'exprimer de façon très riche et très rigoureuse des fonctions et d'y démontrer formellement des propriétés difficiles. Plus précisément, le système F (également connu sous le nom de lambda-calcul polymorphe ou de lambda-calcul du second ordre) est une extension du lambda-calcul simplement typé introduite indépendamment par le logicien Jean-Yves Girard et par l'informaticien John C. Reynolds. Ce système se distingue du lambda-calcul simplement typé par l'existence d'une quantification universelle sur les types qui permet d'exprimer du polymorphisme.

Le système F possède deux propriétés cruciales :

la réduction des termes est fortement normalisante (dit plus crûment : tous les calculs se terminent) ;
il correspond par la correspondance de Curry-Howard à la logique minimale propositionnelle du second ordre. Soit : le calcul propositionnel, sans la négation mais avec les quantificateurs.

Note liminaire : La lecture de cet article suppose la lecture préalable de l'article « lambda-calcul » et son assimilation .

Introduction[modifier | modifier le code]

Ainsi que l'atteste sa double origine, le système F peut être étudié dans deux contextes très différents :

Dans le domaine de la programmation fonctionnelle, où il apparaît comme une extension très expressive du noyau du langage ML. Son expressivité est illustrée par le fait que les types de données courants (booléens, entiers, listes, etc.) sont définissables dans le système F à partir des constructions de base ;
Dans le domaine de la logique, et plus particulièrement de la théorie de la démonstration. À travers la correspondance de Curry-Howard, le système F est en effet isomorphe à la logique minimale du second ordre. En outre, ce système capture très exactement la classe des fonctions numériques dont l'existence est prouvable en arithmétique intuitionniste du second ordre (parfois appelée analyse intuitionniste). C'est d'ailleurs cette propriété remarquable du système F qui a historiquement motivé son introduction par Jean-Yves Girard, dans la mesure où cette propriété permet de résoudre le problème de l'élimination des coupures en arithmétique du second ordre, conjecturé par Takeuti.

Historiquement le système F a joué un rôle essentiel dans les fondations de l'informatique en proposant, dès le début des années 1970, un formalisme de types riche, simple et très expressif de fonctions calculables très générales. Il ouvrait la voie aux langages de programmation typés modernes et aux assistants de preuve comme COQ.

Comme le lambda-calcul simplement typé, le système F admet deux présentations équivalentes :

Une présentation à la Church, dans laquelle chaque terme contient toutes les annotations de type nécessaires à la reconstruction de son type (de manière univoque) ;
Une présentation à la Curry, due à l'informaticien Daniel Leivant, dans laquelle les termes (qui sont ceux du lambda-calcul pur) sont dépourvus de toute annotation de type, et sont ainsi sujets aux problèmes d'ambiguïté typique.

Présentation à la Church[modifier | modifier le code]

Le système F admet deux sortes d'objets: les types et les termes. Les termes peuvent être « réduits » et traduisent des fonctions calculables, tandis que les types annotent les termes et permettent de les catégoriser.

La syntaxe[modifier | modifier le code]

Les types du système F (notés $A$ , $B$ , $C$ , etc.) sont formés à partir d'un ensemble de variables de types (notées $\alpha$ , $\beta$ , $\gamma$ , etc.) à l'aide des trois règles de construction suivantes :

(Variable de type) Si $\alpha$ est une variable de type, alors $\alpha$ est un type ;
(Type flèche) Si $A$ et $B$ sont des types, alors $A\to B$ est un type ;
(Type universel) Si $\alpha$ est une variable de type et $B$ un type, alors $\forall \alpha ~B$ est un type.

En résumé, les types du système F sont donnés par la grammaire BNF :

$A,B~~::=~~\alpha ~~|~~A\to B~~|~~\forall \alpha ~B.$

Comme en lambda-calcul ou en calcul des prédicats, la présence d'un symbole mutificateur $\forall$ nécessite de distinguer les notions de variable libre et de variable liée, et d'introduire les mécanismes usuels de renommage permettant de travailler à $\alpha$ -conversion près. Enfin, l'algèbre de types du système F est munie d'une opération de substitution similaire à celle du lambda-calcul, et l'on note $B\{\alpha :=A\}$ le type obtenu en remplaçant dans le type $B$ toutes les occurrences libres de la variable de type $\alpha$ par le type $A$ .

Les termes (bruts) du système F (notés $M$ , $N$ , etc.) sont formés à partir d'un ensemble de variables de termes (notées $x$ , $y$ , $z$ , etc.) à l'aide des cinq règles de construction suivantes :

(Variable) Si $x$ est une variable de terme, alors $x$ est un terme ;
(Abstraction) Si $x$ est une variable de terme, $A$ un type et $M$ un terme, alors $\lambda x:A.M$ est un terme ;
(Application) Si $M$ et $N$ sont des termes, alors $MN$ est un terme ;
(Abstraction de type) Si $\alpha$ est une variable de type et $M$ un terme, alors $\Lambda \alpha .M$ est un terme ;
(Application de type) Si $M$ est un terme et $A$ un type, alors $MA$ est un terme.

En résumé, les termes (bruts) du système F sont donnés par la grammaire BNF :

$M,N~~::=~~x~~|~~\lambda x\,{:}\,A\,.\,M~~|~~MN~~|~~\Lambda \alpha \,.\,M~~|~~MA.$

Les termes du système F incorporent deux mécanismes de liaison de variable : un mécanisme de liaison de variables de termes (par la construction $\lambda x\,{:}\,A\,.\,M$ ) et un mécanisme de liaison de variables de types (par la construction $\Lambda \alpha \,.\,M$ ), qui sont tous les deux pris en compte au niveau de la relation d' $\alpha$ -conversion. Ce double mécanisme donne naturellement lieu à deux opérations de substitution : une substitution de terme notée $M\{x:=N\}$ , et une substitution de type notée $M\{\alpha :=A\}$ .

La β-réduction[modifier | modifier le code]

La présence d'un double mécanisme d'abstraction et d'application (abstraction/application de terme et abstraction/application de type) donne lieu à deux règles de $\beta$ -réduction, dont l'union engendre par passage au contexte la relation de $\beta$ -réduction en une étape du système F :

$(\lambda x\,{:}\,A\,.\,M)N\longrightarrow M\{x:=N\}$ ;
$(\Lambda \alpha \,.\,M)A\longrightarrow M\{\alpha :=A\}$ .

Comme pour le lambda-calcul pur, la $\beta$ -réduction du système F est confluente (sur les termes bruts) et vérifie la propriété de Church-Rosser :

(Confluence de la $\beta$ -réduction) Si $M\longrightarrow ^{*}M_{1}$ et $M\longrightarrow ^{*}M_{2}$ , alors il existe un terme $M'$ tel que $M_{1}\longrightarrow ^{*}M'$ et $M_{2}\longrightarrow ^{*}M'$ ;
(Propriété de Church-Rosser) Pour que deux termes $M_{1}$ et $M_{2}$ soient $\beta$ -convertibles, il faut et il suffit qu'il existe un terme $M'$ tel que $M_{1}\longrightarrow ^{*}M'$ et $M_{2}\longrightarrow ^{*}M'$ .

Le système de types[modifier | modifier le code]

On appelle contexte de typage (notation : $\Gamma$ , $\Gamma '$ , etc.) toute liste finie de déclarations de la forme $x:A$ (où $x$ est une variable de terme et $A$ un type) dans laquelle une variable de terme est déclarée au plus une fois.

Le système de types du système F est construit autour d'un jugement de typage de la forme $\Gamma \vdash M:A$ (« dans le contexte $\Gamma$ , le terme $M$ a pour type $A$ »), qui est défini à partir des règles d'inférence suivantes :

(Axiome) ${\frac {}{\Gamma \vdash x:A}}$ si $(x:A)\in \Gamma$ ;
( $\to$ -intro) ${\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda x\,{:}\,A\,.\,M:A\to B}}$ ;
( $\to$ -élim) ${\frac {\Gamma \vdash M:A\to B\quad \Gamma \vdash N:A}{\Gamma \vdash MN:B}}$ ;
( $\forall$ -intro) ${\frac {\Gamma \vdash M:B}{\Gamma \vdash \Lambda \alpha \,.\,M:\forall \alpha ~B}}$ si $\alpha$ n'a pas d'occurrence libre dans $\Gamma$ ;
( $\forall$ -élim) ${\frac {\Gamma \vdash M:\forall \alpha ~B}{\Gamma \vdash MA:B\{\alpha :=A\}}}$ .

Les deux propriétés principales de ce système de types sont la propriété de préservation du type par $\beta$ -réduction et la propriété de normalisation forte :

(Préservation du type par réduction) Si $\Gamma \vdash M:A$ et si $M\longrightarrow ^{*}M'$ , alors $\Gamma \vdash M':A$ ;
(Normalisation forte) Si $\Gamma \vdash M:A$ , alors $M$ est fortement normalisable.

La première de ces deux propriétés est une propriété purement combinatoire qui se démontre par une induction directe sur la dérivation de typage. En revanche, la propriété de normalisation forte du système F est une propriété dont la démonstration repose fondamentalement sur des méthodes non combinatoires, basées sur la notion de candidat de réductibilité.

Indécidabilité[modifier | modifier le code]

Sauf indication contraire ou complémentaire, les informations contenues dans cette section proviennent de la traduction de la section Use in programming languages de l'article de la Wikipédia en anglais.

Le système de type présenté dans la section précédente est explicite, ce qui veut dire de les informations sur le type des termes sont données à chaque étape. On dit aussi que c'est un système « à la Church ». Dans un tel système, vérifier qu'un terme est bien typé est très simple.

En 1994, Joe B. Wells a résolu une conjecture ancienne, qui répond à un problème plus général, à savoir que la vérification de type pour un variant « à la Curry » du système F (un système de type où les informations de type ne sont pas données) est indécidable^[1]. Le résultat de Wells signifie que la reconstruction du type pour le système F n'est pas possible. Autrement dit, en système F, on ne peut pas avoir un mécanisme logiciel qui, comme en OCaml ou en Haskell, assigne un type à une fonction que le programmeur a entrée. Cependant dans ces langages, pour aller vers des systèmes de type qui englobent le système F, le programmeur doit fournir, ici ou là, des informations de type pour aider le logiciel à reconstruire le type du terme entier. Dans des langages comme Gallina (de Coq) ou Agda (en) qui contiennent une large extension du système F, la contribution du programmeur au typage est déterminante.

Représentation des types de données[modifier | modifier le code]

Pour pouvoir utiliser le lambda-calcul simplement typé comme un langage de programmation, il est nécessaire de lui adjoindre des types de base (booléens, entiers, etc.) et des règles de réduction supplémentaires qui étendent le pouvoir expressif du formalisme. Un exemple d'une telle extension est le système T de Gödel, qui est obtenu en ajoutant au lambda-calcul simplement typé des entiers naturels primitifs et un mécanisme de récursion similaire à la récursion primitive (mais plus expressif).

Dans le système F, une telle extension n'est pas nécessaire car l'expressivité du formalisme permet de définir les types de base et les constructeurs de types usuels sans qu'il soit nécessaire de modifier ni le système de types ni les règles de réduction.

Booléens et types finis[modifier | modifier le code]

Le type des booléens est défini dans le système F par

${\textbf {Bool}}~\equiv ~\forall \gamma \,(\gamma \to \gamma \to \gamma )$

et les constantes ${\textbf {true}}$ et ${\textbf {false}}$ par :

${\textbf {true}}~\equiv ~\Lambda \gamma \,.\,\lambda x,y\,{:}\,\gamma \,.\,x~:~{\textbf {Bool}}$ ;
${\textbf {false}}~\equiv ~\Lambda \gamma \,.\,\lambda x,y\,{:}\,\gamma \,.\,y~:~{\textbf {Bool}}$ .

On peut démontrer que les deux termes ci-dessus sont les deux seuls termes clos en forme normale de type ${\textbf {Bool}}$ . Ainsi, le type de données ${\textbf {Bool}}$ capture effectivement la notion de booléen.

La construction 'if … then … else …' est définie par

${\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}~\equiv ~MCN_{1}N_{2}$

où $C$ désigne le type d'élimination de la construction 'if ...', c'est-à-dire le type commun aux deux branches de la conditionnelle. Cette définition est correcte du point de vue du typage comme du point de vue calculatoire dans la mesure où :

Dans tout contexte où le terme $M$ a le type ${\textbf {Bool}}$ et où les termes $N_{1}$ et $N_{2}$ ont le type $C$ , la construction ${\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}$ est bien typée et a pour type le type $C$ ;
Si le terme $M\,\!$ se réduit sur ${\textbf {true}}$ , alors la construction ${\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}$ se réduit sur $N_{1}\,\!$ ;
Si le terme $M\,\!$ se réduit sur ${\textbf {false}}$ , alors la construction ${\texttt {if}}_{C}~M~{\texttt {then}}~N_{1}~{\texttt {else}}~N_{2}$ se réduit sur $N_{2}\,\!$ .

Plus généralement, on peut définir un type fini $E_{n}$ à $n$ valeurs $e_{1},\ldots ,e_{n}$ en posant :

$E_{n}~\equiv ~\forall \gamma \,(\underbrace {\gamma \to \cdots \to \gamma } _{n}\to \gamma )$ ;
$e_{i}~\equiv ~\Lambda \gamma \,.\,\lambda x_{1},\ldots ,x_{n}\,{:}\,\gamma \,.\,x_{i}$ (pour tout $1\leq i\leq n$ ).

Là encore, on peut démontrer que les termes $e_{1},\ldots ,e_{n}$ sont les seuls termes clos en forme normale de type $E_{n}$ . L'opération de filtrage correspondant est définie par :

${\texttt {match}}_{C}~M~{\texttt {with}}~e_{1}\mapsto N_{1}|\cdots |e_{n}\mapsto N_{n}~\equiv ~M\,C\,N_{1}\cdots N_{n}$

(où $C$ désigne le type des branches de filtrage).

En particulier :

$E_{2}~\equiv ~\forall \gamma \,(\gamma \to \gamma \to \gamma )~\equiv ~{\textbf {Bool}}$ (type des booléens) ;
$E_{1}~\equiv ~\forall \gamma \,(\gamma \to \gamma )~\equiv ~{\textbf {Unit}}$ (type singleton) ;
$E_{0}~\equiv ~\forall \gamma \,\gamma ~\equiv ~{\textbf {Empty}}$ (type vide).

Le type $E_{0}$ n'est habité par aucun terme clos en forme normale, et, d'après le théorème de normalisation forte, il n'est habité par aucun terme clos.

Produit cartésien et somme directe[modifier | modifier le code]

Soit $A$ et $B$ deux types. Le produit cartésien $A\times B$ est défini dans le système F par

$A\times B~\equiv ~\forall \gamma \,((A\to B\to \gamma )\to \gamma )$

et la construction de couple par

$\langle M;N\rangle ~\equiv ~\Lambda \gamma \,.\,\lambda f\,{:}\,(A\to B\to \gamma )\,.\,f\,M\,N~:~A\times B$ (si $M:A\,\!$ et $N:B\,\!$ )

Comme pour les types énumérés, on peut démontrer que les seuls termes clos en forme normale de type $A\times B$ sont de la forme $\langle M;N\rangle$ , où $M$ et $N$ sont des termes clos en forme normale de type $A$ et $B$ , respectivement. Les fonctions de projection correspondantes sont données par

${\textbf {fst}}~\equiv ~\Lambda \alpha ,\beta \,.\,\lambda p\,{:}\,(\alpha \times \beta )\,.\,p\,\alpha \,(\lambda x\,{:}\,\alpha \,.\,\lambda y\,{:}\,\beta \,.\,x)~:~\forall \alpha ,\beta \,(\alpha \times \beta \to \alpha )$
${\textbf {snd}}~\equiv ~\Lambda \alpha ,\beta \,.\,\lambda p\,{:}\,(\alpha \times \beta )\,.\,p\,\beta \,(\lambda x\,{:}\,\alpha \,.\,\lambda y\,{:}\,\beta \,.\,y)~:~\forall \alpha ,\beta \,(\alpha \times \beta \to \beta )$

Ces fonctions vérifient naturellement les égalités ${\textbf {fst}}\,A\,B\,\langle M;N\rangle =M$ et ${\textbf {snd}}\,A\,B\,\langle M;N\rangle =N$ .

La somme directe $A+B$ est définie par

$A+B~\equiv ~\forall \gamma \,((A\to \gamma )\to (B\to \gamma )\to \gamma )$

Les habitants des types $A$ et $B$ sont plongés dans le type $A+B$ à l'aide des constructions

${\textbf {inl}}(M)~\equiv ~\Lambda \gamma \,.\,\lambda f\,{:}\,(A\to \gamma )\,.\,\lambda g\,{:}\,(B\to \gamma )\,.\,f\,M~:~A+B$ (si $M:A\,\!$ )
${\textbf {inr}}(M)~\equiv ~\Lambda \gamma \,.\,\lambda f\,{:}\,(A\to \gamma )\,.\,\lambda g\,{:}\,(B\to \gamma )\,.\,g\,M~:~A+B$ (si $M:B\,\!$ )

tandis que le filtrage des éléments de type $A+B$ est assuré par la construction

${\texttt {match}}~N~{\texttt {with}}~{\textbf {inl}}(x)\mapsto M_{1}~|~{\textbf {inr}}(y)\mapsto M_{2}~\equiv ~N\,C\,(\lambda x\,{:}\,A\,.\,M_{1})\,(\lambda y\,{:}\,B\,.\,M_{2})$

qui satisfait les égalités définitionnelles attendues.

Contrairement au produit cartésien, l'encodage de la somme directe dans le système F ne capture pas toujours la notion d'union disjointe, dans la mesure où il est possible, dans certains cas, de construire des termes clos en forme normale de type $A+B$ qui ne sont ni de la forme ${\textbf {inl}}(M)$ (avec $M:A$ ) ni de la forme ${\textbf {inr}}(M)$ (avec $M:B$ )^{[réf. nécessaire]}.

Les entiers de Church[modifier | modifier le code]

Le type des entiers de Church est défini dans le système F par

$\mathbf {Nat} ~\equiv ~\forall \gamma \,(\gamma \to (\gamma \to \gamma )\to \gamma )$

Chaque entier naturel $n$ est représenté par le terme

${\bar {n}}~\equiv ~\Lambda \gamma \,\lambda x\,{:}\,\gamma \,.\,\lambda f\,{:}\,(\gamma \to \gamma )\,.\,\underbrace {f(\cdots (f} _{n}\,x)\cdots )~:~\mathbf {Nat}$

Comme pour les booléens, le type $\mathbf {Nat}$ capture la notion d'entier naturel puisque tout terme clos de type $\mathbf {Nat}$ en forme normale est de la forme ${\bar {n}}$ pour un certain entier naturel $n$ .

Présentation à la Curry[modifier | modifier le code]

La fonction d'effacement[modifier | modifier le code]

$|x|=x$
$|\lambda x:A.M|=\lambda x.|M|$
$|MN|=|M||N|$
$|\Lambda \alpha .M|=|M|$
$|MA|=|M|$

Le système de types[modifier | modifier le code]

(Axiome) ${\frac {}{\Gamma \vdash x:A}}$ si $(x:A)\in \Gamma$
( $\to$ -intro) ${\frac {\Gamma ,x:A\vdash M:B}{\Gamma \vdash \lambda x.M:A\to B}}$
( $\to$ -élim) ${\frac {\Gamma \vdash M:A\to B\quad \Gamma \vdash N:A}{\Gamma \vdash MN:B}}$
( $\forall$ -intro) ${\frac {\Gamma \vdash M:B}{\Gamma \vdash M:\forall \alpha ~B}}$ si $\alpha$ n'a pas d'occurrence libre dans $\Gamma$
( $\forall$ -élim) ${\frac {\Gamma \vdash M:\forall \alpha ~B}{\Gamma \vdash M:B\{\alpha :=A\}}}$ .

Équivalence entre les deux systèmes[modifier | modifier le code]

Le théorème de normalisation forte[modifier | modifier le code]

Les termes typables du système F sont fortement normalisables, autrement dit la réduction des termes est une opération qui se termine toujours en produisant une forme normale.

Candidats de réductibilité[modifier | modifier le code]

Sauf indication contraire ou complémentaire, les informations contenues dans cette section proviennent du chapitre 14 de Proofs and Types^[2].

La méthode des candidats de réductibilité a été développée William W. Tait (en)^[3] pour prouver la forte normalisation du système T et étendue ensuite par Jean-Yves Girard pour montrer la forte normalisation du système F, plus particulièrement, sa terminaison. En effet, une simple récurrence sur la taille du type ou du terme n'est pas suffisante, pour deux raisons. Premièrement, si $\lambda x.M$ et $N$ sont fortement normalisables, ce n'est pas nécessairement le cas de $(\lambda x.M)N$ . Deuxièmement, pour montrer que $\Lambda \alpha .M:\forall \alpha .T$ est fortement normalisable, il faut montrer que pour tout type $U$ , $M\{\alpha :=U\}:T\{\alpha :=U\}$ est fortement normalisable, or $T\{\alpha :=U\}$ n'est pas nécessairement un type plus petit que $\forall \alpha .T$ , ce qu'on peut constater en choisissant $T=\alpha \to \alpha$ , $U=\forall \alpha .T$ , on a alors $T\{\alpha :=U\}=(\forall \alpha .T)\to (\forall \alpha .T)$ .

Un candidat de réductibilité $C$ de type $T$ est un ensemble de termes de type $A$ qui vérifie un certain nombre de propriétés :

tous les termes d'un candidat sont fortement normalisables,
un candidat est stable par réduction,
si $t$ est un terme neutre et que tous les réduits de $t$ sont dans $C$ , alors $t\in C$ . Un terme neutre est une variable, appliquée à une liste potentiellement vide de types et de termes en forme normale.

En particulier, l'ensemble $SN_{A}$ des termes fortement normalisables de type $A$ est un candidat de réductibilité de type $A$ .

Soit $A$ un type dont les variables libres sont incluses dans $\alpha _{1},\dots ,\alpha _{n}$ et $R_{1},\dots ,R_{n}$ des candidats de réductibilité de type $\alpha _{1},\dots ,\alpha _{n}$ respectivement. On définit par induction sur $A$ l'ensemble $RED_{A}^{(R_{i})_{i}}$ , qui est un candidat de réductibilité de type $A$ :

Si $A$ est la variable $X_{i}$ , $RED_{A}^{(R_{i})_{i}}=R_{i}$ .
Si $A=T\to U$ , $RED_{A}^{(R_{i})_{i}}=\{M\mid \forall N\in RED_{T}^{(R_{i})_{i}},MN\in RED_{U}^{(R_{i})_{i}}\}$ .
Si $A=\forall \alpha .T$ , $RED_{A}^{(R_{i})_{i}}=\bigcap _{U~{\textrm {type}}}\bigcap _{R'\in {\mathcal {C}}_{U}}RED_{T\{\alpha :=U\}}^{R_{1},\dots ,R_{n},R'}$ , où ${\mathcal {C}}_{U}$ désigne l'ensemble des candidats de réductibilité de type $U$ .

Ensuite, on montre, par induction sur la dérivation, que si $\Gamma \vdash M:A$ , $M\in RED_{A}^{SN_{\alpha _{1}},\dots ,SN_{\alpha _{n}}}$ . On peut en déduire que si $M$ est typable alors $M$ est fortement normalisable.

Les candidats de réductibilité connaissent plusieurs variantes^[4], par exemple les candidats peuvent être non-typés, et cette technique a été largement déclinée pour divers systèmes de types, présentant des caractéristiques variées : intersections de types^[5], types récursifs^[6], types modaux^[7], types dépendants^[8].

Correspondance avec la logique du second ordre[modifier | modifier le code]

À travers la correspondance de Curry-Howard, le système F correspond très exactement à la logique minimale du second ordre, dont les formules sont construites à partir des variables propositionnelles à l'aide de l'implication et de la quantification propositionnelle :

$A,B~~:=~~\alpha ~~|~~A\Rightarrow B~~|~~\forall \alpha \,B$

Rappelons que dans ce cadre, les unités $\top$ (vérité) et $\bot$ (absurdité), les connecteurs $\lnot$ (négation), $\land$ (conjonction) et $\lor$ (disjonction) et la quantification existentielle $\exists \alpha \,B(\alpha )$ sont définissables par

$\top ~\equiv ~\forall \gamma \,(\gamma \Rightarrow \gamma )$
$\bot ~\equiv ~\forall \gamma \,\gamma$
$\lnot A~\equiv ~A\Rightarrow \bot$
$A\land B~\equiv ~\forall \gamma \,((A\Rightarrow B\Rightarrow \gamma )\Rightarrow \gamma )$
$A\lor B~\equiv ~\forall \gamma \,((A\Rightarrow \gamma )\Rightarrow (B\Rightarrow \gamma )\Rightarrow \gamma )$
$\exists \alpha \,B(\alpha )~\equiv ~\forall \gamma \,(\forall \alpha \,(B(\alpha )\Rightarrow \gamma )\Rightarrow \gamma )$

(On notera qu'à travers la correspondance de Curry-Howard, l'absurdité correspond au type vide, la vérité au type singleton, la conjonction au produit cartésien et la disjonction à la somme directe.)

On démontre que dans ce formalisme, une formule est prouvable sans hypothèses si et seulement si le type correspondant dans le système F est habité par un terme clos.

Correspondance avec l'arithmétique du second ordre[modifier | modifier le code]

Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue ! Comment faire ?

Bibliographie[modifier | modifier le code]

Lambda-calcul, types et modèles, Jean-Louis Krivine, chapitre VIII, Masson, 1990, (ISBN 2-225-82091-0)
Proofs and Types, Jean-Yves Girard, Paul Taylor, Yves Lafont, chapitre 11, Cambridge University Press, 1989, (ISBN 0-521-37181-3)

Notes et références[modifier | modifier le code]

↑ J. B. Wells, « Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable », Proceedings of the Ninth Annual Symposium on Logic in Computer Science, Paris, France,‎ 1994, p. 176-185.
↑ (en) Jean Yves-Girard, Paul Taylor et Yves Lafont, chap. 14 « Strong Normalisation for F », dans Proofs and Types, Cambridge University Press, 1989 (ISBN 0-521-37181-3, lire en ligne)
↑ (en) W. W. Tait, « Intensional interpretations of functionals of finite type I », The Journal of Symbolic Logic, vol. 32, n^o 2,‎ août 1967, p. 198–212 (ISSN 0022-4812 et 1943-5886, DOI 10.2307/2271658)
↑ (en) Jean H. Gallier, « On Girard’s “Candidats de réductibilité” », dans Piergiorgio Odifreddi, Logic and Computer Science, Academic Press, coll. « APIC studies in data processing » (n^o 31), 1989, 430 p. (ISBN 978-0-12-524220-2, lire en ligne)
↑ (en) M. Dezani-Ciancaglini, F. Honsell et Y. Motohama, « Compositional Characterizations of λ-Terms Using Intersection Types », Mathematical Foundations of Computer Science 2000, Springer,‎ 2000, p. 304–313 (ISBN 978-3-540-44612-5, DOI 10.1007/3-540-44612-5_26)
↑ Nax Paul Mendler, « Inductive types and type constraints in the second-order lambda calculus », Annals of Pure and Applied Logic, vol. 51, n^os 1-2,‎ mars 1991, p. 159–172 (ISSN 0168-0072, DOI 10.1016/0168-0072(91)90069-x)
↑ (en) G. A. Kavvos, « Dual-context calculi for modal logic », 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), IEEE,‎ juin 2017, p. 1–12 (ISBN 978-1-5090-3018-7, DOI 10.1109/LICS.2017.8005089, arXiv https://arxiv.org/abs/1602.04860)
↑ (en) Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot et Loïc Pujet, « Martin-Löf à la Coq », Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, New York, NY, USA, Association for Computing Machinery,‎ 2024, p. 230–245 (DOI 10.1145/3636501.3636951, arXiv 2310.06376)

[1] J. B. Wells, « Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable », Proceedings of the Ninth Annual Symposium on Logic in Computer Science, Paris, France,‎ 1994, p. 176-185.

[2] (en) Jean Yves-Girard, Paul Taylor et Yves Lafont, chap. 14 « Strong Normalisation for F », dans Proofs and Types, Cambridge University Press, 1989 (ISBN 0-521-37181-3, lire en ligne)

[3] (en) W. W. Tait, « Intensional interpretations of functionals of finite type I », The Journal of Symbolic Logic, vol. 32, n^o 2,‎ août 1967, p. 198–212 (ISSN 0022-4812 et 1943-5886, DOI 10.2307/2271658)

[4] (en) Jean H. Gallier, « On Girard’s “Candidats de réductibilité” », dans Piergiorgio Odifreddi, Logic and Computer Science, Academic Press, coll. « APIC studies in data processing » (n^o 31), 1989, 430 p. (ISBN 978-0-12-524220-2, lire en ligne)

[5] (en) M. Dezani-Ciancaglini, F. Honsell et Y. Motohama, « Compositional Characterizations of λ-Terms Using Intersection Types », Mathematical Foundations of Computer Science 2000, Springer,‎ 2000, p. 304–313 (ISBN 978-3-540-44612-5, DOI 10.1007/3-540-44612-5_26)

[6] Nax Paul Mendler, « Inductive types and type constraints in the second-order lambda calculus », Annals of Pure and Applied Logic, vol. 51, n^os 1-2,‎ mars 1991, p. 159–172 (ISSN 0168-0072, DOI 10.1016/0168-0072(91)90069-x)

[7] (en) G. A. Kavvos, « Dual-context calculi for modal logic », 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), IEEE,‎ juin 2017, p. 1–12 (ISBN 978-1-5090-3018-7, DOI 10.1109/LICS.2017.8005089, arXiv https://arxiv.org/abs/1602.04860)

[8] (en) Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot et Loïc Pujet, « Martin-Löf à la Coq », Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, New York, NY, USA, Association for Computing Machinery,‎ 2024, p. 230–245 (DOI 10.1145/3636501.3636951, arXiv 2310.06376)

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]