Calcul lambda simplement typé - Simply typed lambda calculus

Le calcul lambda simplement typé ( ), une forme de théorie des types , est une interprétation typée du calcul lambda avec un seul constructeur de type ( ) qui construit des types de fonction . C'est l'exemple canonique et le plus simple d'un calcul lambda typé. Le calcul lambda simplement typé a été introduit à l'origine par Alonzo Church en 1940 pour tenter d'éviter les utilisations paradoxales du calcul lambda non typé , et il présente de nombreuses propriétés souhaitables et intéressantes. ${\displaystyle \lambda ^{\to }}$${\style d'affichage \to }$

Le terme type simple est également utilisé pour désigner des extensions du calcul lambda simplement typé telles que des produits , des coproduits ou des nombres naturels ( Système T ) ou même une récursivité complète (comme PCF ). En revanche, les systèmes qui introduisent des types polymorphes (comme le système F ) ou des types dépendants (comme le cadre logique ) ne sont pas considérés comme simplement typés . Les premiers, à l'exception de la récursivité complète, sont toujours considérés comme simples car les codages Church de telles structures peuvent être effectués en utilisant uniquement des variables de type appropriées, alors que le polymorphisme et la dépendance ne le peuvent pas. ${\style d'affichage \to }$

Syntaxe

Dans cet article, nous utilisons et pour varier les types. De manière informelle, le type de fonction fait référence au type de fonctions qui, étant donné une entrée de type , produisent une sortie de type . Par convention, associés à droite: nous lisons que . ${\style d'affichage \sigma }$${\style d'affichage \tau }$ ${\displaystyle \sigma \to \tau }$${\style d'affichage \sigma }$${\style d'affichage \tau }$${\style d'affichage \to }$${\displaystyle \sigma \to \tau \to \rho }$${\displaystyle \sigma \to (\tau \to \rho )}$

Pour définir les types, on commence par fixer un ensemble de types de base , . Celles-ci sont parfois appelées types atomiques ou constantes de type . Avec ce corrigé, la syntaxe des types est : ${\style d'affichage B}$

${\displaystyle \tau ::=\tau \to \tau \mid T\quad \mathrm {where} \quad T\in B}$.

Par exemple, , génère un ensemble infini de types commençant par${\style d'affichage B=\{a,b\}}$${\style d'affichage a,b,}$${\displaystyle a\to a,}$${\displaystyle a\à b,b\à b,}$${\displaystyle b\to a,}$${\displaystyle a\to (a\to a),\ldots ,}$${\displaystyle (b\to a)\to (a\to b),\ldots }$

Nous fixons également un ensemble de constantes de terme pour les types de base. Par exemple, nous pourrions supposer un type de base nat , et le terme constantes pourrait être les nombres naturels. Dans la présentation originale, Church n'utilisait que deux types de base : pour « le type de propositions » et pour « le type d'individus ». Le type n'a pas de constante de terme, alors qu'il a une constante de terme. Fréquemment, le calcul avec un seul type de base, généralement , est considéré. ${\style d'affichage o}$${\style d'affichage \iota }$${\style d'affichage o}$${\style d'affichage \iota }$${\style d'affichage o}$

La syntaxe du lambda calcul simplement typé est essentiellement celle du lambda calcul lui-même. Nous écrivons pour indiquer que la variable est de type . Le terme syntaxe, en BNF, est alors : ${\displaystyle x{\mathbin {:}}\tau }$${\style d'affichage x}$${\style d'affichage \tau }$

${\displaystyle e::=x\mid \lambda x{\mathbin {:}}\tau .e\mid e\,e\mid c}$

où est un terme constant. ${\style d'affichage c}$

C'est-à-dire référence de variable , abstractions , application et constante . Une référence de variable est liée si elle se trouve à l'intérieur d'une liaison d'abstraction . Un terme est fermé s'il n'y a pas de variables non liées. ${\style d'affichage x}$${\style d'affichage x}$

Comparez cela à la syntaxe du calcul lambda non typé :

${\displaystyle e::=x\mid \lambda xe\mid e\,e}$

On voit que dans le lambda calcul typé chaque fonction ( abstraction ) doit spécifier le type de son argument.

Règles de saisie

Pour définir l'ensemble des termes lambda bien typés d'un type donné, nous allons définir une relation de typage entre termes et types. Tout d'abord, nous introduisons des contextes de typage ou des environnements de typage , qui sont des ensembles d'hypothèses de typage. Une hypothèse de typage a la forme , le sens a le type . ${\displaystyle \Gamma ,\Delta ,\dots }$${\displaystyle x{\mathbin {:}}\sigma }$${\style d'affichage x}$${\style d'affichage \sigma }$

La relation de typage indique qu'il s'agit d'un terme de type en contexte . Dans ce cas est dit bien typé (ayant le type ). Les instances de la relation de typage sont appelées jugements de typage . La validité d'un jugement de typage est montrée en fournissant une dérivation de typage , construite à l'aide de règles de typage (dans lesquelles les prémisses au-dessus de la ligne nous permettent de dériver la conclusion en dessous de la ligne). Le calcul lambda simplement typé utilise ces règles : ${\displaystyle \Gamma \vdash e{\mathbin {:}}\sigma }$${\style d'affichage e}$${\style d'affichage \sigma }$${\style d'affichage \Gamma }$${\style d'affichage e}$${\style d'affichage \sigma }$

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x{\mathbin {:}}\sigma }}}$ (1)	${\displaystyle {\frac {c{\text{ est une constante de type }}T}{\Gamma \vdash c{\mathbin {:}}T}}}$ (2)
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e{\mathbin {:}}\tau }{\Gamma \vdash (\lambda x{\mathbin {:}}\ sigma .~e){\mathbin {:}}(\sigma \to \tau )}}}$ (3)	${\displaystyle {\frac {\Gamma \vdash e_{1}{\mathbin {:}}\sigma \to \tau \quad \Gamma \vdash e_{2}{\mathbin {:}}\sigma }{\ Gamma \vdash e_{1}~e_{2}{\mathbin {:}}\tau }}}$ (4)

Dans les mots,

1. Si a type dans le contexte, nous savons que a type .${\style d'affichage x}$${\style d'affichage \sigma }$${\style d'affichage x}$${\style d'affichage \sigma }$
2. Les constantes de terme ont les types de base appropriés.
3. Si, dans un certain contexte avec type , a type , alors, dans le même contexte sans , a type .${\style d'affichage x}$${\style d'affichage \sigma }$${\style d'affichage e}$${\style d'affichage \tau }$${\style d'affichage x}$${\displaystyle \lambda x{\mathbin {:}}\sigma .~e}$${\displaystyle \sigma \to \tau }$
4. Si, dans un certain contexte, a type , et a type , alors a type .${\style d'affichage e_{1}}$${\displaystyle \sigma \to \tau }$${\style d'affichage e_{2}}$${\style d'affichage \sigma }$${\displaystyle e_{1}~e_{2}}$${\style d'affichage \tau }$

Des exemples de termes fermés, c'est -à- dire des termes typables dans le contexte vide, sont :

• Pour chaque type , un terme (fonction d'identité/I-combinateur),${\style d'affichage \tau }$${\displaystyle \lambda x{\mathbin {:}}\tau .x{\mathbin {:}}\tau \to \tau }$
• Pour les types , un terme (le K-combinateur) et${\displaystyle \sigma ,\tau }$${\displaystyle \lambda x{\mathbin {:}}\sigma .\lambda y{\mathbin {:}}\tau .x{\mathbin {:}}\sigma \to \tau \to \sigma }$
• Pour les types , un terme (le S-combinateur).${\displaystyle \tau ,\tau ',\tau ''}$${\displaystyle \lambda x{\mathbin {:}}\tau \to \tau '\to \tau ''.\lambda y{\mathbin {:}}\tau \to \tau '.\lambda z{\ mathbin {:}}\tau .xz(yz):(\tau \to \tau '\to \tau '')\to (\tau \to \tau ')\to \tau \to \tau ''}$

Ce sont les représentations typées lambda calcul des combinateurs de base de la logique combinatoire .

A chaque type est attribué un ordre, un numéro . Pour les types de base, ; pour les types de fonctions, . C'est-à-dire que l'ordre d'un type mesure la profondeur de la flèche la plus à gauche. D'où: ${\style d'affichage \tau }$${\style d'affichage o(\tau )}$${\style d'affichage o(T)=0}$${\displaystyle o(\sigma \to \tau )={\mbox{max}}(o(\sigma )+1,o(\tau ))}$

${\displaystyle o(\iota \to \iota \to \iota )=1}$

${\displaystyle o((\iota \to \iota )\to \iota )=2}$

Sémantique

Interprétations intrinsèques ou extrinsèques

D'une manière générale, il existe deux manières différentes d'attribuer un sens au calcul lambda simplement typé, en ce qui concerne les langages typés plus généralement, parfois appelés intrinsèques contre extrinsèques , ou de style Church contre style Curry . Une sémantique intrinsèque/de style Église n'attribue de sens qu'aux termes bien typés, ou plus précisément, attribue un sens directement aux dérivations de typage. Cela a pour effet que les termes ne différant que par les annotations de type peuvent néanmoins se voir attribuer des significations différentes. Par exemple, le terme d'identité sur les entiers et le terme d'identité sur les booléens peuvent signifier des choses différentes. (Les interprétations classiques prévues sont la fonction d'identité sur les entiers et la fonction d'identité sur les valeurs booléennes.) En revanche, une sémantique extrinsèque/de style Curry attribue un sens aux termes indépendamment du typage, comme ils seraient interprétés dans un langage non typé. De ce point de vue, et signifient la même chose ( c'est -à- dire la même chose que ). ${\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}$${\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}$${\displaystyle \lambda x{\mathbin {:}}{\mathtt {int}}.~x}$${\displaystyle \lambda x{\mathbin {:}}{\mathtt {bool}}.~x}$${\style d'affichage \lambda x.~x}$

La distinction entre sémantique intrinsèque et extrinsèque est parfois associée à la présence ou à l'absence d'annotations sur les abstractions lambda, mais à proprement parler cet usage est imprécis. Il est possible de définir une sémantique de style Curry sur les termes annotés en ignorant simplement les types ( c. -à , par l' effacement de type ), car il est possible de donner une sémantique de style Église sur les termes annotés lorsque les types peuvent être déduites à partir du contexte ( c. -à- , par inférence de type ). La différence essentielle entre les approches intrinsèques et extrinsèques est simplement de savoir si les règles de typage sont considérées comme définissant le langage ou comme un formalisme permettant de vérifier les propriétés d'un langage sous-jacent plus primitif. La plupart des différentes interprétations sémantiques discutées ci-dessous peuvent être vues à travers une perspective d'Église ou de Curry.

Théorie des équations

Le lambda calcul simplement typé a la même théorie équationnelle de la -équivalence que le lambda calcul non typé , mais soumis à des restrictions de type. L'équation de la réduction bêta

${\displaystyle (\lambda x{\mathbin {:}}\sigma .~t)\,u=_{\beta }t[x:=u]}$

tient dans le contexte à chaque fois que et , tandis que l'équation pour la réduction eta${\style d'affichage \Gamma }$${\displaystyle \Gamma ,x{\mathbin {:}}\sigma \vdash t{\mathbin {:}}\tau }$${\displaystyle \Gamma \vdash u{\mathbin {:}}\sigma }$

${\displaystyle \lambda x{\mathbin {:}}\sigma .~t\,x=_{\eta }t}$

tient à chaque fois et n'apparaît pas libre dans . ${\displaystyle \Gamma \vdash t\!:\sigma \to \tau }$${\style d'affichage x}$${\style d'affichage t}$

Sémantique opérationnelle

De même, la sémantique opérationnelle du lambda calcul simplement typé peut être fixée comme pour le lambda calcul non typé, en utilisant call by name , call by value , ou d'autres stratégies d'évaluation . Comme pour tout langage typé, la sécurité de type est une propriété fondamentale de toutes ces stratégies d'évaluation. De plus, la propriété de normalisation forte décrite ci-dessous implique que toute stratégie d'évaluation se terminera sur tous les termes simplement typés.

Sémantique catégorielle

Le lambda calcul simplement typé (avec -équivalence) est le langage interne des catégories fermées cartésiennes (CCC), comme cela a été observé pour la première fois par Lambek . Compte tenu de tout CCC spécifique, les types de base du lambda calcul correspondant ne sont que les objets , et les termes sont les morphismes . Inversement, tout lambda calcul simplement typé donne un CCC dont les objets sont les types, et les morphismes sont des classes d'équivalence de termes. ${\displaystyle \beta \eta }$

Pour clarifier la correspondance, un constructeur de type pour le produit cartésien est généralement ajouté à ce qui précède. Pour conserver la catégorisation du produit cartésien , on ajoute des règles de type pour l' appariement , la projection , et un terme unitaire . Étant donné deux termes et , le terme a le type . De même, si on a un terme , alors il y a des termes et où les correspondent aux projections du produit cartésien. Le terme unitaire , de type 1, s'écrit as et vocalisé 'nil', est l' objet final . La théorie équationnelle est étendue de la même manière, de sorte que l'on a ${\displaystyle s{\mathbin {:}}\sigma }$${\displaystyle t{\mathbin {:}}\tau }$${\style d'affichage (s,t)}$${\displaystyle \sigma \times \tau }$${\displaystyle u{\mathbin {:}}\tau _{1}\times \tau _{2}}$${\displaystyle \pi _{1}(u){\mathbin {:}}\tau _{1}}$${\displaystyle \pi _{2}(u){\mathbin {:}}\tau _{2}}$${\style d'affichage \pi _{i}}$${\style d'affichage ()}$

${\displaystyle \pi _{1}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=s{\mathbin {:}}\sigma }$

${\displaystyle \pi _{2}(s{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )=t{\mathbin {:}}\tau }$

${\displaystyle (\pi _{1}(u{\mathbin {:}}\sigma \times \tau ),\pi _{2}(u{\mathbin {:}}\sigma \times \tau )) =u{\mathbin {:}}\sigma \times \tau }$

${\displaystyle t{\mathbin {:}}1=()}$

Ce dernier se lit comme « si t est de type 1, alors il se réduit à nil ».

Ce qui précède peut alors être transformé en une catégorie en prenant les types comme objets . Les morphismes sont des classes d'équivalence de paires où x est une variable (de type ) et t est un terme (de type ), ne contenant aucune variable libre, à l'exception (éventuellement) de x . La fermeture est obtenue par curry et application , comme d'habitude. ${\displaystyle \sigma \to \tau }$${\displaystyle (x{\mathbin {:}}\sigma ,t{\mathbin {:}}\tau )}$${\style d'affichage \sigma }$${\style d'affichage \tau }$

Plus précisément, il existe des foncteurs entre la catégorie des catégories fermées cartésiennes, et la catégorie des théories lambda simplement typées.

Il est courant d'étendre ce cas aux catégories monoïdales symétriques fermées en utilisant un système de type linéaire . La raison en est que le CCC est un cas particulier de la catégorie monoïdale symétrique fermée, qui est généralement considérée comme la catégorie des ensembles . C'est bien pour jeter les bases de la théorie des ensembles , mais le topos plus général semble fournir une base supérieure.

Sémantique de la preuve théorique

Le lambda calcul simplement typé est étroitement lié au fragment implicationnel de la logique intuitionniste propositionnelle , c'est-à-dire la logique minimale , via l' isomorphisme de Curry-Howard : les termes correspondent précisément à des preuves en déduction naturelle , et les types habités sont exactement les tautologies de la logique minimale.

Syntaxes alternatives

La présentation donnée ci-dessus n'est pas la seule façon de définir la syntaxe du lambda calcul simplement typé. Une alternative consiste à supprimer complètement les annotations de type (afin que la syntaxe soit identique au calcul lambda non typé), tout en s'assurant que les termes sont bien typés via l' inférence de type Hindley-Milner . L'algorithme d'inférence est final, solide et complet : chaque fois qu'un terme est typable, l'algorithme calcule son type. Plus précisément, il calcule le type principal du terme , car souvent un terme non annoté (comme ) peut avoir plus d'un type ( , , etc., qui sont tous des instances du type principal ). ${\style d'affichage \lambda x.~x}$${\displaystyle {\mathtt {int}}\to {\mathtt {int}}}$${\displaystyle {\mathtt {bool}}\to {\mathtt {bool}}}$${\displaystyle \alpha \to \alpha }$

Une autre présentation alternative du calcul lambda simplement typé est basée sur la vérification de type bidirectionnelle , qui nécessite plus d'annotations de type que l'inférence Hindley-Milner mais est plus facile à décrire. Le système de typage est divisé en deux jugements, représentant à la fois la vérification et la synthèse , respectivement écrit et . Opérationnellement, les trois composants , , et sont tous des entrées du jugement de vérification , alors que le jugement de synthèse ne prend que et comme entrées, produisant le type comme sortie. Ces jugements découlent des règles suivantes : ${\displaystyle \Gamma \vdash e\Leftarrow \tau }$${\displaystyle \Gamma \vdash e\Rightarrow \tau }$${\style d'affichage \Gamma }$${\style d'affichage e}$${\style d'affichage \tau }$${\displaystyle \Gamma \vdash e\Leftarrow \tau }$${\displaystyle \Gamma \vdash e\Rightarrow \tau }$${\style d'affichage \Gamma }$${\style d'affichage e}$${\style d'affichage \tau }$

${\displaystyle {\frac {x{\mathbin {:}}\sigma \in \Gamma }{\Gamma \vdash x\Rightarrow \sigma }}}$ [1]	${\displaystyle {\frac {c{\text{ est une constante de type }}T}{\Gamma \vdash c\Rightarrow T}}}$ [2]
${\displaystyle {\frac {\Gamma ,x{\mathbin {:}}\sigma \vdash e\Leftarrow \tau }{\Gamma \vdash \lambda x.~e\Leftarrow \sigma \to \tau }}}$ [3]	${\displaystyle {\frac {\Gamma \vdash e_{1}\Rightarrow \sigma \to \tau \quad \Gamma \vdash e_{2}\Leftarrow \sigma }{\Gamma \vdash e_{1}~e_{ 2}\Rightarrow \tau }}}$ [4]
${\displaystyle {\frac {\Gamma \vdash e\Rightarrow \tau }{\Gamma \vdash e\Leftarrow \tau }}}$ [5]	${\displaystyle {\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e{\mathbin {:}}\tau )\Rightarrow \tau }}}$ [6]

Observez que les règles [1]–[4] sont presque identiques aux règles (1)–(4) ci-dessus, à l'exception du choix judicieux des jugements de vérification ou de synthèse. Ces choix peuvent s'expliquer ainsi :

1. Si est dans le contexte, nous pouvons synthétiser le type pour .${\displaystyle x{\mathbin {:}}\sigma }$${\style d'affichage \sigma }$${\style d'affichage x}$
2. Les types de constantes de terme sont fixes et peuvent être synthétisés.
3. Pour vérifier que a le type dans un certain contexte, nous étendons le contexte avec et vérifions qui a le type .${\displaystyle \lambda x.~e}$${\displaystyle \sigma \to \tau }$${\displaystyle x{\mathbin {:}}\sigma }$${\style d'affichage e}$${\style d'affichage \tau }$
4. If synthétise le type (dans un certain contexte) et vérifie par rapport au type (dans le même contexte), puis synthétise le type .${\style d'affichage e_{1}}$${\displaystyle \sigma \to \tau }$${\style d'affichage e_{2}}$${\style d'affichage \sigma }$${\displaystyle e_{1}~e_{2}}$${\style d'affichage \tau }$

Observez que les règles de synthèse sont lues de haut en bas, alors que les règles de vérification sont lues de bas en haut. Note en particulier que nous ne pas besoin d' une annotation sur l'abstraction lambda en règle [3], parce que le type de la variable liée peut être déduite à partir du type auquel nous vérifions la fonction. Enfin, nous expliquons les règles [5] et [6] comme suit :

5. Pour vérifier qu'il a du type , il suffit de synthétiser le type .${\style d'affichage e}$${\style d'affichage \tau }$${\style d'affichage \tau }$
6. Si vérifie par rapport au type , alors le terme explicitement annoté est synthétisé . ${\style d'affichage e}$${\style d'affichage \tau }$${\displaystyle (e{\mathbin {:}}\tau )}$${\style d'affichage \tau }$

En raison de ces deux dernières règles contraignantes entre la synthèse et la vérification, il est facile de voir que tout terme bien typé mais non annoté peut être vérifié dans le système bidirectionnel, à condition d'insérer "suffisamment" d'annotations de type. Et en fait, les annotations ne sont nécessaires qu'aux -redexes.

Observations générales

Compte tenu de la sémantique standard, le lambda calcul simplement typé est fortement normalisant : c'est-à-dire que les termes bien typés se réduisent toujours à une valeur, c'est-à-dire une abstraction. En effet, la récursivité n'est pas autorisée par les règles de typage : il est impossible de trouver des types pour les combinateurs à virgule fixe et le terme de bouclage . La récursivité peut être ajoutée au langage en ayant un opérateur spécial de type ou en ajoutant des types récursifs généraux , bien que les deux éliminent la normalisation forte. ${\style d'affichage \lambda }$${\displaystyle \Omega =(\lambda x.~x~x)(\lambda x.~x~x)}$${\displaystyle {\mathtt {fix}}_{\alpha }}$${\displaystyle (\alpha \to \alpha )\to \alpha }$

Comme il est fortement normalisant, il est décidable si oui ou non un programme de haltes de calcul lambda simplement typé: en fait, il toujours arrête. On peut donc conclure que le langage de Turing n'est pas complet .

Résultats importants

• Tait a montré en 1967 que la réduction est fortement normalisante . En corollaire, l' équivalence est décidable . Statman a montré en 1977 que le problème de normalisation n'est pas récursif élémentaire , preuve qui a été simplifiée plus tard par Mairson (1992). Le problème est connu pour être dans l'ensemble de la hiérarchie de Grzegorczyk . Une preuve de normalisation purement sémantique (voir normalisation par évaluation ) a été donnée par Berger et Schwichtenberg en 1991.${\displaystyle \beta }$${\displaystyle \beta \eta }$${\displaystyle {\mathcal {E}}^{4}}$
• Le problème d' unification pour l' équivalence est indécidable. Huet a montré en 1973 que l'unification du 3ème ordre est indécidable et ceci a été amélioré par Baxter en 1978 puis par Goldfarb en 1981 en montrant que l'unification du 2ème ordre est déjà indécidable. Une preuve que l'appariement d'ordre supérieur (unification où un seul terme contient des variables existentielles) est décidable a été annoncée par Colin Stirling en 2006, et une preuve complète a été publiée en 2009.${\displaystyle \beta \eta }$
• On peut coder les nombres naturels par des termes du type ( chiffres d'église ). Schwichtenberg a montré en 1976 que dans exactement les polynômes étendus sont représentables comme des fonctions sur des chiffres d'Église ; ce sont à peu près les polynômes fermés sous un opérateur conditionnel.${\displaystyle (o\to o)\to (o\to o)}$${\displaystyle \lambda ^{\to }}$
• Un modèle complet de est donné en interprétant les types de base comme des ensembles et des types de fonction par l' espace des fonctions de la théorie des ensembles . Friedman a montré en 1975 que cette interprétation est complète pour -équivalence, si les types de base sont interprétés par des ensembles infinis. Statman a montré en 1983 que -equivalence est l'équivalence maximale qui est typiquement ambiguë , c'est-à-dire fermée par substitutions de types ( Statman's Typique Ambiguity Theorem ). Un corollaire de ceci est que la propriété du modèle fini est vraie, c'est-à-dire que les ensembles finis sont suffisants pour distinguer les termes qui ne sont pas identifiés par -équivalence.${\displaystyle \lambda ^{\to }}$${\displaystyle \beta \eta }$${\displaystyle \beta \eta }$${\displaystyle \beta \eta }$
• Plotkin a introduit des relations logiques en 1973 pour caractériser les éléments d'un modèle définissables par des termes lambda. En 1993, Jung et Tiuryn ​​ont montré qu'une forme générale de relation logique (relations logiques de Kripke avec une arité variable) caractérise exactement la définissabilité lambda. Plotkin et Statman ont conjecturé qu'il est possible de décider si un élément donné d'un modèle généré à partir d'ensembles finis est définissable par un terme lambda ( conjecture de Plotkin-Statman ). La conjecture s'est avérée fausse par Loader en 1993.

Remarques

Les références

• A. Église : une formulation de la théorie simple des types , JSL 5, 1940
• WWTait : Interprétations intentionnelles des fonctionnelles de type fini I, JSL 32(2), 1967
• GD Plotkin : Lambda-définissabilité et relations logiques, Rapport technique, 1973
• GP Huet : L'indécidabilité de l'unification dans l' information et le contrôle de la logique de troisième ordre 22(3) : 257-267 (1973)
• H. Friedman : Égalité entre fonctionnels . LogicColl. '73, pages 22-37, LNM 453, 1975.
• H. Schwichtenberg : Fonctions définissables dans le calcul lambda simplement typé, Arch. Math Logik 17 (1976) 113-114.
• R. Statman : Le calcul lambda typé n'est pas récursif élémentaire FOCS 1977 : 90-94
• WD Goldfarb : L'indécidabilité du problème d'unification du 2ème ordre, TCS (1981), no. 13, 225-230.
• R. Statman. -fonctions définissables et conversion. Cambre. Math. Logik, 23:21-26, 1983.${\style d'affichage \lambda }$${\displaystyle \beta \eta }$
• J. Lambek : Catégories fermées cartésiennes et Lambda-calculs typés . Combinateurs et langages de programmation fonctionnels 1985 : 136-175
• U. Berger, H. Schwichtenberg: An Inverse of the Evaluation Functional for typed lambda-calculus LICS 1991: 203-211
• H. Mairson : Une preuve simple d'un théorème de Statman , TCS 103(2):387-394, 1992.
• Jung, A.,Tiuryn, J.: Une nouvelle caractérisation de la définiabilité Lambda , TLCA 1993
• R. Loader: The Undecidability of λ-definability , paru dans le Church Festschrift, 2001
• H. Barendregt, Lambda Calculi with Types , Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1993. ISBN  0-19-853761-1 .
• L. Baxter : L'indécidabilité du problème d'unification dyadique du troisième ordre , Information and Control 38(2), 170-178 (1978)

Liens externes

• Loader, Ralph (février 1998). "Notes sur le calcul lambda simplement typé" .
• Entrée « Théorie des types de l'Église » dans l'Encyclopédie de philosophie de Stanford