Programming Computable Functions

En informatique théorique, Programming Computable Functions ou PCF est un langage de programmation théorique apparu pour la première fois en 1977 dans un article de Gordon Plotkin^[1], mais qui est basé sur des notes de Dana S. Scott de 1969 qui n'ont été publiées qu'en 1993^[2]. Ce langage consiste en une extension du lambda-calcul simplement typé avec des combinateurs de points fixes et des entiers naturels, ce qui permet de récupérer la complétude au sens de Turing, c'est-à-dire la possibilité d'exprimer n'importe quelle fonction calculable. En effet, l'ajout d'une discipline de types au lambda-calcul, donnant le lambda-calcul simplement typé, limite l'expressivité du langage et les fonctions qui y sont définissables ; l'ajout de combinateurs de point fixe et d'entiers résout ce problème.

PCF reprend les types du lambda-calcul simplement typé en y adjoignant un type représentant comme types de base les booléens, ${\displaystyle o}$, et un type représentant les entiers, ${\displaystyle \iota }$^[1],[3]. Les types sont donc ${\displaystyle o}$, ${\displaystyle \iota }$, ou ${\displaystyle \alpha \to \beta }$ avec ${\displaystyle \alpha }$ et ${\displaystyle \beta }$ des types déjà formés. Ce type représente le type des fonctions de ${\displaystyle \alpha }$ vers ${\displaystyle \beta }$. La notation ${\displaystyle \alpha \to \beta \to \gamma }$ doit être lue comme ${\displaystyle \alpha \to (\beta \to \gamma )}$.

De plus, la syntaxe de PCF comprend la syntaxe du lambda-calcul simplement typé, et les constructions de base y sont les mêmes : il y a des variables, notées ${\displaystyle x,y,z,\dots }$  ; si ${\displaystyle M}$ est un terme de type ${\displaystyle \alpha \to \beta }$ et ${\displaystyle N}$ un terme de type ${\displaystyle \alpha }$, ${\displaystyle MN}$ est un terme de type ${\displaystyle \beta }$ qui représente l'évaluation de la fonction ${\displaystyle M}$ en ${\displaystyle N}$ ; et si ${\displaystyle M}$ est un terme de type ${\displaystyle \beta }$ dans un contexte où la variable ${\displaystyle x}$ est de type ${\displaystyle \alpha }$, ${\displaystyle \lambda x^{\alpha }.M}$ est de type ${\displaystyle \alpha \to \beta }$ et représente la fonction ${\displaystyle x\mapsto M}$. Si ${\displaystyle M}$ est un terme de type ${\displaystyle \alpha }$, on notera ${\displaystyle M:\alpha }$. Pour plus de détails, consulter les sections Syntaxe et Règles de typage de l'article sur le lambda-calcul simplement typé.

À cela se rajoutent les constantes propres permettant de manipuler les types de base. Pour chaque entier naturel ${\displaystyle n\in \mathbb {N} }$, on ajoute une constante ${\displaystyle {\underline {n}}:\iota }$. De plus, il y a une constante pour chaque booléen, ${\displaystyle \operatorname {true} :o}$ et ${\displaystyle \operatorname {false} :o}$. Pour chaque type de base ${\displaystyle \sigma }$, c'est-à-dire ${\displaystyle \iota }$ et ${\displaystyle o}$, on a une constante ${\displaystyle \operatorname {if} \ \operatorname {then} \ \operatorname {else} :o\to \sigma \to \sigma \to \sigma }$ représentant une instruction conditionnelle : l'idée étant que si ${\displaystyle b}$ vaut ${\displaystyle \operatorname {true} }$, l'expression ${\displaystyle \operatorname {if} b\operatorname {then} M\operatorname {else} N}$vaut ${\displaystyle M}$, si ${\displaystyle b}$ vaut ${\displaystyle \operatorname {false} }$, elle s'évalue en ${\displaystyle N}$. De plus, il y a deux fonctions pour manipuler les entiers, la fonction successeur ${\displaystyle \operatorname {succ} :\iota \to \iota }$ et la fonction prédécesseur ${\displaystyle \operatorname {pred} :\iota \to \iota }$, qui correspondent à ajouter ou soustraire ${\displaystyle 1}$ à leur argument. Enfin, il y a une fonction ${\displaystyle \operatorname {zero} ?:\iota \to o}$ qui renvoie ${\displaystyle \operatorname {true} }$ si son argument vaut l'entier ${\displaystyle {\underline {0}}}$, ${\displaystyle \operatorname {false} }$ sinon.

Enfin, le principal ingrédient de PCF est sa construction de point fixe : pour chaque type ${\displaystyle \alpha }$, on dispose d'une constante ${\displaystyle Y:(\alpha \to \alpha )\to \alpha }$ dont l'interprétation est qu'il renvoie le plus petit point fixe de la fonction qu'on lui passe en argument. Certains auteurs^[4] rajoutent à chaque type une constante ${\displaystyle \Omega :\alpha }$ qui répresente un programme qui ne termine pas. Cette construction n'est pas incluse dans la présentation originelle de Gordon Plotkin^[1], mais peut y être définie comme ${\displaystyle Y(\lambda x^{\alpha }.x)}$.

PCF peut être muni d'une sémantique opérationnelle ${\displaystyle \to }$^[5]. Si ${\displaystyle M}$ et ${\displaystyle N}$ sont des termes, on a ${\displaystyle M\to N}$ si ${\displaystyle M}$ se transforme en ${\displaystyle N}$ après une étape élémentaire de calcul. On note ${\displaystyle M\to ^{*}N}$ pour dire que ${\displaystyle M}$ se transforme en ${\displaystyle N}$ en zéro ou plusieurs étapes. La relation ${\displaystyle \to }$ est définie comme suit :

• ${\displaystyle (\lambda x^{\alpha }.M)N\to M[x:=N]}$ : pour évaluer l'application de la fonction ${\displaystyle x\mapsto M}$ en ${\displaystyle N}$, on remplace ${\displaystyle x}$ par ${\displaystyle N}$ dans ${\displaystyle M}$ ;
• ${\displaystyle YM\to M(YM)}$ : cela exprime que ${\displaystyle YM}$ est un point fixe de ${\displaystyle M}$ ;
• ${\displaystyle \operatorname {succ} ({\underline {n}})\to {\underline {n+1}}}$;
• ${\displaystyle \operatorname {pred} ({\underline {n+1}})\to {\underline {n}}}$ ;
• ${\displaystyle \operatorname {zero} ?({\underline {0}})\to \operatorname {true} }$ ;
• ${\displaystyle \operatorname {zero} ?({\underline {n+1}})\to \operatorname {false} }$ ;
• ${\displaystyle \operatorname {if} \operatorname {true} \operatorname {then} M\operatorname {else} N\to M}$ ;
• ${\displaystyle \operatorname {if} \operatorname {false} \operatorname {then} M\operatorname {else} N\to N}$ ;
• Les règles contextuelles sont les suivantes : si ${\displaystyle M\to M'}$ alors ${\displaystyle MN\to M'N}$, ${\displaystyle \operatorname {succ} M\to \operatorname {succ} M'}$, ${\displaystyle \operatorname {pred} M\to \operatorname {pred} M'}$, ${\displaystyle \operatorname {zero} ?(M)\to \operatorname {zero} ?(M')}$ et ${\displaystyle \operatorname {if} M\operatorname {then} N\operatorname {else} P\to \operatorname {if} M'\operatorname {then} N\operatorname {else} P}$. Elles donnent à PCF une sémantique d'appel par nom.

Cette sémantique est déterministe, c'est-à-dire que si ${\displaystyle M\to N}$ et ${\displaystyle M\to N'}$, alors ${\displaystyle N=N'}$. De plus, elle préserve le typage : si ${\displaystyle M\to N}$ et que ${\displaystyle M}$ est de type ${\displaystyle \alpha }$, alors ${\displaystyle N}$ aussi.

On pourrait autoriser la réduction dans tous les contextes, plutôt qu'uniquement dans ceux précisés dans la dernière règle (qui interdit, par exemple, la réduction ${\displaystyle NM\to NM'}$ avec ${\displaystyle M\to M'}$ et ${\displaystyle N}$ qui n'est pas une lambda-abstraction ou ${\displaystyle \operatorname {succ} }$ ou ${\displaystyle \operatorname {pred} }$ ou ${\displaystyle \operatorname {zero} ?}$). Dans ce cas, la réduction obtenue préserve encore le typage et est confluente. De plus, si ${\displaystyle M\to ^{*}N}$ avec cette réduction, et si ${\displaystyle N}$ est en forme normale, alors ${\displaystyle M\to ^{*}N}$ avec la version restreinte. En clair, la sémantique opérationnelle définie ici est standardisante^[6].

PCF permet par exemple de définir des programmes effectuant l'addition de deux entiers. En voici un^[6] :

${\displaystyle add:=Y(\lambda f^{\iota \to \iota \to \iota }.\lambda x^{\iota }.\lambda y^{\iota }.\operatorname {if} \operatorname {zero} ?(x)\operatorname {then} y\operatorname {else} \operatorname {succ} (f(\operatorname {pred} x)y))}$.

Si on note ${\displaystyle add'}$ la fonction à l'intérieur de ${\displaystyle Y}$, la somme de deux et trois est calculée par la suite de réductions suivante :

${\displaystyle add~{\underline {2}}~{\underline {3}}\to add'~add~{\underline {2}}~{\underline {3}}\to ^{*}\operatorname {if} \operatorname {zero} ?({\underline {0}})\operatorname {then} {\underline {3}}\operatorname {else} \operatorname {succ} (add(\operatorname {pred} {\underline {2}}){\underline {3}})\to ^{*}\operatorname {succ} (add~{\underline {1}}~{\underline {3}})\to ^{*}}$

${\displaystyle \operatorname {succ} (\operatorname {if} \operatorname {zero} ?({\underline {1}})\operatorname {then} {\underline {3}}\operatorname {else} \operatorname {succ} (add(\operatorname {pred} {\underline {1}}){\underline {3}}))\to ^{*}\operatorname {succ} (\operatorname {succ} (add~{\underline {0}}~{\underline {3}}))\to ^{*}}$

${\displaystyle \operatorname {succ} (\operatorname {succ} (\operatorname {if} \operatorname {zero} ?({\underline {0}})\operatorname {then} {\underline {3}}\operatorname {else} \operatorname {succ} (add(\operatorname {pred} {\underline {0}}){\underline {3}})))\to ^{*}\operatorname {succ} (\operatorname {succ} ({\underline {3}})))\to ^{*}{\underline {5}}}$.

Ainsi, ${\displaystyle \operatorname {add} ~{\underline {2}}~{\underline {3}}}$ se réduit bien en la valeur ${\displaystyle {\underline {5}}}$.

La sémantique opérationnelle présentée plus haut permet de déterminer comment exécuter un terme de PCF comme un programme. Mais pour étudier PCF, il peut être intéressant de traduire un terme comme ${\displaystyle \lambda x^{\alpha }.M}$ en une fonction au sens mathématique du terme. C'est le rôle de la sémantique dénotationnelle^[7].

Contrairement au lambda-calcul simplement typé, on ne peut pas interpréter PCF directement dans les ensembles et les fonctions, puisqu'il existe des fonctions qui n'ont pas de point fixe. On va donc interpréter les termes de PCF comme des fonctions continues entre cpo. Un cpo est un ensemble ordonné dans lequel toutes les parties dirigées ont une borne supérieure, et qui possède un plus petit élément^[8]. L'intérêt des cpo réside dans ce cas chaque fonction continue possède un plus petit point fixe. La catégorie des cpo est cartésienne fermée^[9].

La sémantique dénotationnelle va traduire chaque terme ${\displaystyle t}$ par un objet ${\displaystyle [\![t]\!]}$ appartenant à un certain modèle, fixé à l'avance. La propriété de correction énoncera ensuite que si ${\displaystyle t\to u}$, alors ${\displaystyle [\![t]\!]=[\![u]\!]}$.

Le modèle continu est l'interprétation usuelle de PCF^[10],[11]. On va définir pour chaque type, chaque contexte et chaque terme une traduction ${\displaystyle [\![\cdot ]\!]}$ telle que l'interprétation d'un contexte ou d'un type soit un cpo, et si ${\displaystyle \Gamma \vdash M:\alpha }$ dans PCF, alors ${\displaystyle [\![M]\!]:[\![\Gamma ]\!]\to [\![\alpha ]\!]}$ est une fonction continue de l'interprétation du contexte vers l'interprétation du type de ${\displaystyle M}$.

Les types de base sont interprétés comme des domaines plats : on a ${\displaystyle [\![\iota ]\!]=\mathbb {N} _{\bot }}$ et ${\displaystyle [\![o]\!]=\mathbb {B} _{\bot }}$, où ${\displaystyle \mathbb {N} }$ est l'ensemble des entiers naturels, ${\displaystyle \mathbb {B} }$ l'ensemble des booléens et pour tout ensemble ${\displaystyle X}$, ${\displaystyle X_{\bot }}$ est le cpo défini sur l'ensemble ${\displaystyle X}$ auquel on adjoint un élément ${\displaystyle \bot }$, avec l'ordre défini par ${\displaystyle \bot \leq x}$ pour tout ${\displaystyle x}$, et les éléments de ${\displaystyle X}$ sont incomparables entre eux. Le type ${\displaystyle \alpha \to \beta }$ est interprété comme l'ensemble des fonctions continues de ${\displaystyle [\![\alpha ]\!]}$ vers ${\displaystyle [\![\beta ]\!]}$. L'idée intuitive derrière cet ordre étant que pour deux fonctions ${\displaystyle f}$ et ${\displaystyle g}$ de même type, représentant des fonctions partiellement définies, ${\displaystyle f\leq g}$ signifie que ${\displaystyle f}$ est une approximation de ${\displaystyle g}$, ou que ${\displaystyle g}$ est définie en plus de points que ${\displaystyle f}$. Un contexte ${\displaystyle x_{1}:\alpha _{1},\dots ,x_{n}:\alpha _{n}}$ est interprété par ${\displaystyle [\![\alpha _{1}]\!]\times \dots \times [\![\alpha _{n}]\!]}$. On remarque que chaque type est un cpo, donc a un plus petit élément ${\displaystyle \bot }$.

Considérons maintenant un terme typé et son contexte ${\displaystyle \Gamma \vdash M:\alpha }$, avec ${\displaystyle \Gamma =x_{1}:\alpha _{1},\dots ,x_{n}:\alpha _{n}}$.

L'interprétation des constructions issues du lambda-calcul est la suivante :

• ${\displaystyle [\![x_{i}]\!]=(x_{1},\dots ,x_{n})\mapsto x_{i}}$.
• ${\displaystyle [\![\lambda x^{\alpha }.M]\!]=(x_{1},\dots ,x_{n})\mapsto (x\mapsto [\![M]\!](x_{1},\dots ,x_{n},x))}$.
• ${\displaystyle [\![MN]\!]=(x_{1},\dots ,x_{n})\mapsto [\![M]\!](x_{1},\dots ,x_{n})([\![N]\!](x_{1},\dots ,x_{n}))}$.

L'opérateur de point fixe est définie comme suit :

• ${\displaystyle [\![Y]\!]}$ est la fonction ${\displaystyle ([\![T]\!]\to [\![T]\!])\to [\![T]\!]}$ qui à chaque ${\displaystyle f:[\![T]\!]\to [\![T]\!]}$ associe son plus petit point fixe. Il est défini comme ${\displaystyle \bigvee _{n\in \mathbb {N} }f^{n}(\bot )}$, c'est-à-dire comme le supremum de la suite croissante ${\displaystyle \bot ,f(\bot ),f(f(\bot )),\dots }$.
• Puisque intuitivement, ${\displaystyle \Omega =Y(\lambda x.x)}$, et que le plus petit point fixe de la fonction identité est ${\displaystyle \bot }$, ${\displaystyle [\![\Omega ]\!]=\bot }$.

Les primitives sur les entiers et les booléens sont interprétées comme suit, l'idée étant que ${\displaystyle \bot }$ représente une valeur non déterminée, par exemple un programme qui ne termine pas :

• ${\displaystyle [\![\operatorname {succ} ]\!]({\underline {n}})={\underline {n+1}}}$ si ${\displaystyle n\in \mathbb {N} }$ et ${\displaystyle [\![\operatorname {succ} ]\!](\bot )=\bot }$.
• ${\displaystyle [\![\operatorname {pred} ]\!]({\underline {n}})={\underline {n-1}}}$ si ${\displaystyle n\in \mathbb {N} }$ et ${\displaystyle n\neq 0}$, ${\displaystyle [\![\operatorname {pred} ]\!]({\underline {0}})=\bot }$ et ${\displaystyle [\![\operatorname {pred} ]\!](\bot )=\bot }$.

• ${\displaystyle [\![\operatorname {zero} ?]\!]({\underline {0}})=\operatorname {true} }$, ${\displaystyle [\![\operatorname {zero} ?]\!]({\underline {n}})=\operatorname {false} }$ si ${\displaystyle n\in \mathbb {N} }$ et ${\displaystyle n\neq 0}$, et ${\displaystyle [\![\operatorname {zero} ?]\!](\bot )=\bot }$.
• ${\displaystyle [\![\operatorname {if} \ \operatorname {then} \ \operatorname {else} ]\!](\operatorname {true} )(x)(y)=x}$, ${\displaystyle [\![\operatorname {if} \ \operatorname {then} \ \operatorname {else} ]\!](\operatorname {false} )(x)(y)=y}$ et ${\displaystyle [\![\operatorname {if} \ \operatorname {then} \ \operatorname {else} ]\!](\bot )(x)(y)=y}$.

Plus généralement, on peut interpréter PCF dans des catégories cartésiennes fermées enrichies dans les cpo^[10],[11]. Un tel modèle est appelé modèle standard de PCF. Une catégorie cartésienne fermée enrichie dans les cpo est une catégorie cartésienne fermée ${\displaystyle {\mathcal {C}}}$ telle que :

• les hom-sets ${\displaystyle {\mathcal {C}}(A,B)}$ sont des cpo pour tous objets ${\displaystyle A}$ et ${\displaystyle B}$ ;
• la composition, le pairage et la currification sont continues ;
• l'évaluation et la composition sont strictes : pour tous objets ${\displaystyle A}$, ${\displaystyle B}$ et ${\displaystyle C}$ et tout morphisme ${\displaystyle f:A\to B}$, si l'on désigne par ${\displaystyle \bot _{D}}$ le plus petit élément d'un cpo ${\displaystyle D}$, on a :
  ${\displaystyle \bot _{{\mathcal {C}}(B,C)}\circ f=\bot _{{\mathcal {C}}(A,C)}}$,
  et si l'on désigne par ${\displaystyle B\to C}$ l'objet des fonctions de ${\displaystyle B}$ vers ${\displaystyle C}$ dans la catégorie cartésienne fermée, par ${\displaystyle \langle \cdot ,\cdot \rangle }$ l'opération de pairage et par ${\displaystyle ev_{B,C}:(B\to C)\times B\to C}$ le morphisme d'évaluation, on a :

${\displaystyle ev_{A,B}\circ \langle \bot _{{\mathcal {C}}(A,B\to C)},f\rangle =\bot _{{\mathcal {C}}(A,C)}}$.

• la catégorie possède deux objets ${\displaystyle D^{\iota }}$ et ${\displaystyle D^{o}}$ tels que ${\displaystyle {\mathcal {C}}(1,D^{\iota })}$ soit isomorphe à ${\displaystyle \mathbb {N} _{\bot }}$ et ${\displaystyle {\mathcal {C}}(1,D^{o})}$ soit isomorphe à ${\displaystyle \mathbb {B} _{\bot }}$ en tant que cpo, où ${\displaystyle 1}$ l'objet terminal de la catégorie ${\displaystyle {\mathcal {C}}}$. Dans la catégorie des cpo, ${\displaystyle 1}$ est l'ensemble à un élément muni de l'égalité comme relation d'ordre.

Dans ce cas, en interprétant dans ${\displaystyle {\mathcal {C}}}$ les constructions issues du lambda-calcul simplement typé de la façon uselle, en définissant ${\displaystyle [\![\Omega ]\!]=\bot }$ et ${\displaystyle [\![Y]\!]=\bigvee _{n\in \mathbb {N} }[\![\lambda f.f^{n}\Omega ]\!]}$ et en interprétant les constructions sur les types primitifs de la même façon que dans le modèle continu en posant ${\displaystyle [\![\iota ]\!]=D^{\iota }}$ et ${\displaystyle [\![o]\!]=D^{o}}$, ce qui est rendu possible par les isomorphismes ${\displaystyle {\mathcal {C}}(1,D^{\iota })\simeq \mathbb {N} _{\bot }}$ et ${\displaystyle {\mathcal {C}}(1,D^{o})\simeq \mathbb {B} _{\bot }}$, on obtient la sémantique désirée.

On peut distinguer certains types de modèles de PCF :

• Un modèle ${\displaystyle {\mathcal {C}}}$ est extensionnel^[12] si pour tous ${\displaystyle f,g\in {\mathcal {C}}(A,B)}$, ${\displaystyle f=g}$ si et seulement si ${\displaystyle \forall h\in {\mathcal {C}}(1,A),f\circ h=g\circ h}$, où ${\displaystyle 1}$ l'objet terminal de ${\displaystyle {\mathcal {C}}}$. Cela signifie que ${\displaystyle {\mathcal {C}}(A,B)}$ peut être vu comme un ensemble de fonctions de ${\displaystyle {\mathcal {C}}(1,A)}$ vers ${\displaystyle {\mathcal {C}}(1,B)}$. Cela correspond à la notion de catégorie bien pointée.
• Un modèle ${\displaystyle {\mathcal {C}}}$ est extensionnellement ordonné^[13] s'il est extensionnel et que pour tous ${\displaystyle f,g\in {\mathcal {C}}(A,B)}$, ${\displaystyle f\leq g}$ si et seulement si ${\displaystyle \forall h\in {\mathcal {C}}(1,A),f\circ h\leq g\circ h}$. Cela signifie que si on regarde ${\displaystyle f}$ et ${\displaystyle g}$ comme des fonctions, l'ordre entre ${\displaystyle f}$ et ${\displaystyle g}$ est l'ordre point à point.

Le théorème d'adéquation (en anglais : adequacy) énonce que dans tout modèle standard, un programme calculant un entier est interprété par l'entier qu'il calcule^[14].

On en déduit le corollaire suivant :

Ce théorème permet de relier la sémantique dénotationnelle et la sémantique opérationnelle de PCF, et de montrer en particulier que la sémantique de PCF ne distingue pas les termes égaux.

Le sens direct de ce résultat est immédiat, c'est la propriété de correction d'un modèle. Le sens réciproque est plus difficile à démontrer ; les démonstrations données par Plotkin^[15] ou par Amadio et Curien^[14] utilisent la méthode des relations logiques (en), qui consiste grossièrement à séparer cette preuve en deux propriétés, puis à montrer une première propriété par induction sur les types, et une deuxième sur les termes.

Étant donné deux termes ${\displaystyle \Gamma \vdash t:A}$ et ${\displaystyle \Gamma \vdash u:A}$, on peut se demander à quelle condition ces deux termes sont « les mêmes ».

Une première notion d'équivalence entre termes est l'équivalence observationnelle^[16],[17] : intuitivement, deux termes sont observationnellement équivalents si on peut remplacer l'un par l'autre dans n'importe quel programme en obtenant le même résultat.

Une première question soulevée par cette définition vient de la notion même de « résultat ». En effet, on ne peut pas distinguer deux fonctions directement : d'une part, le code d'une fonction n'est pas accessible dans PCF, d'autre part, certaines fonctions sont clairement équivalentes, comme ${\displaystyle \lambda x^{A}.x^{A}}$ et ${\displaystyle \lambda x^{A}.(\lambda y^{A}.y^{A})~x^{A}}$, qui calculent toutes deux l'identité, mais sont en forme normale pour ${\displaystyle \to }$. Le seul moyen de distinguer deux fonctions est d'appliquer chacune à un même argument, et observer que leurs résultats diffèrent.

En revanche, étant donné les booléens ${\displaystyle \operatorname {true} }$ et ${\displaystyle \operatorname {false} }$, il est évident qu'ils sont différents. On définit donc les termes observables comme ceux qu'on peut intuitivement séparer : il s'agit des entiers ${\displaystyle {\underline {n}}}$ pour ${\displaystyle n\in \mathbb {N} }$ et des booléens ${\displaystyle \operatorname {true} }$ et ${\displaystyle \operatorname {false} }$. Sans perte de généralité, les résultats qui suivront ne mentionneront que les entiers.

Si ${\displaystyle t}$ et ${\displaystyle u}$ sont des termes clos d'un type de base, ils sont observationnellement équivalents s'ils se réduisent tous deux vers le même observable, ou si tous les deux ne terminent pas. Dans le cas plus général, si ${\displaystyle A}$ n'est pas un type de base, il n'y a pas d'observable de type ${\displaystyle A}$, et si ${\displaystyle t}$ et ${\displaystyle u}$ ne sont pas clos, alors ils pourraient se réduire vers des variables, qu'on ne sait pas distinguer intuitivement non plus. On définit donc la notion de contexte (différente de ${\displaystyle \Gamma }$ dans ${\displaystyle \Gamma \vdash t:A}$, qu'on appelle aussi contexte) : un contexte ${\displaystyle C[\_]}$ est un terme avec exactement un « trou », c'est-à-dire qu'exactement un sous-terme est remplacé par ${\displaystyle \square }$. Un contexte peut-être typé, et une opération naturelle consiste à remplacer le trou par un terme du même type : on note cela ${\displaystyle C[t]}$. Un contexte clos d'un type de base permet ainsi de représenter un programme, dont on sait qu'il va s'évaluer vers un observable, et dans lequel on peut mettre soit ${\displaystyle t}$, soit ${\displaystyle u}$.

Par exemple, on peut distinguer les deux fonctions ${\displaystyle \lambda x^{\mathbb {N} }.{\underline {0}}}$ et ${\displaystyle \lambda x^{\mathbb {N} }.{\underline {1}}}$ de type ${\displaystyle \mathbb {N} \to \mathbb {N} }$, dans le contexte ${\displaystyle C[\_]=\square ~{\underline {0}}}$, puisque dans ce contexte, la première fonction se réduit vers ${\displaystyle {\underline {0}}}$ tandis que la deuxième se réduit vers ${\displaystyle {\underline {1}}}$.

Plus généralement, on peut définir un préordre entre termes d'un même type pour lequel ${\displaystyle t}$ est plus petit que ${\displaystyle u}$ si ${\displaystyle u}$ représente un programme qui étend ${\displaystyle t}$, dans le sens où quand ${\displaystyle t}$ renvoie un résultat, ${\displaystyle u}$ renvoie le même, ${\displaystyle u}$ peut être défini sur plus d'arguments que ${\displaystyle t}$.

Par exemple, si ${\displaystyle t}$ et ${\displaystyle u}$ sont des fonctions de ${\displaystyle \mathbb {N} \to \mathbb {N} }$ telle que ${\displaystyle t}$ renvoie toujours ${\displaystyle \bot }$, sauf en ${\displaystyle {\underline {0}}}$, où ${\displaystyle t}$ renvoie ${\displaystyle {\underline {0}}}$, alors ${\displaystyle t\leq _{op}u}$ si et seulement si ${\displaystyle u~{\underline {0}}\to ^{*}{\underline {0}}}$.

Tout modèle standard induit également une notion d'équivalence entre deux termes^[18], à savoir le fait qu'ils aient la même dénotation. De même, un modèle induit également une relation d'ordre entre termes, où ${\displaystyle t}$ est plus petit que ${\displaystyle u}$ lorsque ${\displaystyle [\![t]\!]\leq [\![u]\!]}$. Cette relation capture l'idée que dans le modèle, ${\displaystyle u}$ est plus défini que ${\displaystyle t}$. Ces relations dépendent du modèle choisi.

On peut se demander dans quelle mesure ces deux notions d'équivalence sont comparables^[18]. De manière générale, le théorème d'adéquation peut se reformuler comme le fait que pour termes ${\displaystyle t}$ et ${\displaystyle u}$, ${\displaystyle t\leq _{obs}u}$ si et seulement si pour tout contexte ${\displaystyle C[\_]}$ clos et de type entier, ${\displaystyle [\![C[t]]\!]\leq [\![C[u]]\!]}$^[19].

Ce théorème a deux conséquences intéressantes : La première est que pour tous termes clos ${\displaystyle t}$ et ${\displaystyle u}$ de type entier, ${\displaystyle t=_{obs}u\iff [\![t]\!]=[\![u]\!]}$, donc qu'équivalence dénotationnelle et observationnelle coïncident au niveau des types de base^[17]. La seconde est que pour tous termes ${\displaystyle \Gamma \vdash t:A}$ et ${\displaystyle \Gamma \vdash u:A}$, ${\displaystyle [\![t]\!]\leq [\![u]\!]\implies t\leq _{obs}u}$ (donc en particulier que ${\displaystyle [\![t]\!]=[\![u]\!]\implies t=_{obs}u}$)^[20],[21].

Plotkin a montré que cette propriété n'est pas vérifiée par le modèle continu de PCF^[22]. On peut en effet définir dans ce modèle la fonction « ou parallèle » ${\displaystyle por:\mathbb {B} _{\bot }\times \mathbb {B} _{\bot }\to \mathbb {B} _{\bot }}$ (en anglais : parallel or) dans ce modèle, qui est définie par :

$${\displaystyle por(x,y)={\begin{cases}\operatorname {true} &{\text{si }}x=\operatorname {true} {\text{ ou }}y=\operatorname {true} \\\operatorname {false} &{\text{si }}x=\operatorname {false} {\text{ et }}y=\operatorname {false} \\\bot &{\text{sinon}}\end{cases}}}$$

En revanche, cette fonction n'est pas définissable dans PCF : aucun terme ${\displaystyle t}$ n'est tel que ${\displaystyle [\![t]\!]=por}$. Intuitivement, un tel terme lancerait en parallèle les deux programmes qu'on lui passe en argument, renvoyant vrai dès que l'un d'eux retourne vrai, ou faux si les deux retournent faux. Au contraire, PCF est un langage séquentiel^[23],[20], qui ne supporte pas l'exécution entrelacée.

On peut montrer que si on définit, pour chaque booléen ${\displaystyle b}$, le terme ${\displaystyle t_{b}}$ suivant :

$${\displaystyle \lambda g^{\mathbb {B} \times \mathbb {B} \to \mathbb {B} }.\operatorname {if} ~g~(\operatorname {true} ,\bot )~\operatorname {then} ~(\operatorname {if} ~g(\bot ,\operatorname {true} )~\operatorname {then} ~(\operatorname {if} ~g~(\operatorname {false} ,\operatorname {false} )~\operatorname {then} ~\bot ~\operatorname {else} ~b)~\operatorname {else} ~\bot )~\operatorname {else} ~\bot }$$

Alors ${\displaystyle t_{\operatorname {true} }=_{obs}t_{\operatorname {false} }}$, mais ${\displaystyle [\![t_{\operatorname {true} }]\!](por)\neq [\![t_{\operatorname {true} }]\!](por)}$ car pour tout booléen ${\displaystyle b}$, ${\displaystyle [\![t_{b}]\!](por)=b}$, donc le modèle standard de PCF n'est pas complètement abstrait^[20]. En revanche, ce modèle est complètement abstrait pour une version de PCF à laquelle on a rajouté une primitive représentant ${\displaystyle por}$^[24].

Milner a fourni en premier en 1977 un modèle complètement adéquat de PCF en quotiantant la syntaxe de PCF pour identifier les termes observationnellement équivalents. Il a de plus donné, sous certaines conditions, une caractérisation des modèles complètement adéquats de PCF^[25] :

De plus, il a montré que sous ces conditions, tous ces modèles sont isomorphes^[25]:

Néanmoins le modèle proposé par Milner n'a pas été jugé satisfaisant par la communauté scientifique, qui désirait trouver un modèle plus sémantique^[26]. La communauté scientifique a donc essayé de trouver une description plus sémantique de cet unique modèle complètement adéquat^[17]. Un compte rendu détaillé de cette recherche est décrit au début de l'article d'Hyland et Ong^[27], ainsi que dans l'article de Curien^[17]. Gérard Berry a proposé ensuite en 1978 le modèle stable de PCF^[28],[29], qui est extensionnel mais pas extensionnellement ordonné, puis Berry et Curien ont proposé en 1982 le modèle des algorithmes séquentiels^[30],[31], qui n'est pas extensionnel. Dans ces deux modèles, il y a des éléments compacts non définissables^[17]. Cela à ouvert la voie à d'autres travaux qui tentaient de définir la séquentialité pour les fonctions d'ordre supérieur, notamment par Antonio Bucciarelli et Thomas Ehrhard^[32],[33].

En 2000, Martin Hyland et Luke Ong et Samson Abramsky, Radha Jagadeesan et Pasquale Malacaria ont indépendamment proposé chacun un modèle basé sur la sémantique des jeux, le modèle des jeux OH^[27] et le modèle des jeux AJM^[34] (nommés d'après les initiales respectives de leurs auteurs). Ces modèles présentent la propriété que tous les éléments compacts sont définissables, mais ils ne sont pas extensionnels, et correspondent à des descriptions purement sémantiques de la catégorie des arbres de Böhm de PCF^[17]. Il est possible, via une construction catégorique, de rendre ces modèles extensionnellement ordonnés, et donc d'obtenir à partir de ces modèles une description du modèle complètement adéquat de PCF^[35],[17].

Ceci conclut la quête de la solution au problème de la complète adéquation, puisqu'en 2001 Ralph Loader a montré que la relation d'équivalence observationnelle dans PCF finitaire, c'est-à-dire PCF sans les entiers, avec uniquement les booléens comme type de base, était indécidable^[36], et donc qu'un modèle de PCF vérifiant les critères de Achim Jung and Allen Stoughton^[37], qui précisent que les objets interprétants les types finis doivent être effectivement décrits, est impossible.

Si ${\displaystyle t:\overbrace {\iota \to \iota \to \dots } ^{k}\to \iota }$ est un programme dans PCF qui prend ${\displaystyle k}$ entiers en entrée et renvoie un entier, on peut montrer que ${\displaystyle t}$ détermine une fonction calculable ${\displaystyle f:\mathbb {N} ^{k}\to \mathbb {N} }$ par ${\displaystyle f(n_{1},\dots ,n_{k})=m}$ si ${\displaystyle f~{\underline {n}}_{1}\dots {\underline {n}}_{k}\to ^{*}{\underline {m}}}$ et ${\displaystyle f(n_{1},\dots ,n_{k})}$ n'est pas définie sinon.

Réciproquement, étant donnée une fonction calculable ${\displaystyle f:\mathbb {N} ^{k}\to \mathbb {N} }$, on peut se demander si elle est représentée par un terme ${\displaystyle t:\overbrace {\iota \to \iota \to \dots } ^{k}\to \iota }$ de PCF tel que pour tous entiers ${\displaystyle n_{1},\dots ,n_{k}}$ et ${\displaystyle m}$,

${\displaystyle t~{\underline {n}}_{1}\dots {\underline {n}}_{k}\to ^{*}{\underline {m}}\iff f(n_{1},\dots ,n_{k})=m}$.

Ce problème correspond à la notion de complétude au sens de Turing. La réponse est positive, donc PCF peut représenter toutes les fonctions calculables entre les entiers^[38].

• (en) Roberto M. Amadio et Pierre-Louis Curien, Domains and Lambda-Calculi, Cambridge University Press, coll. « Cambridge Tracts in Theoretical Computer Science », 1998, 534 p. (ISBN 978-0-521-62277-6, lire en ligne). 

• Portail de l'informatique théorique