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, mais qui est basé sur des notes de Dana S. Scott de 1969 qui n'ont été publiées qu'en 1993. 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.

Syntaxe et typage

PCF reprend les types du lambda-calcul simplement typé en y adjoignant un type représentant comme types de base les booléens, $o$, et un type représentant les entiers, $\iota$Modèle:,. Les types sont donc $o$, $\iota$, ou $\alpha \to \beta$ avec $\alpha$ et $\beta$ des types déjà formés. Ce type représente le type des fonctions de $\alpha$ vers $\beta$. La notation $\alpha \to \beta \to \gamma$ doit être lue comme $\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 $x,y,z,\dots$  ; si $M$ est un terme de type $\alpha \to \beta$ et $N$ un terme de type $\alpha$, $MN$ est un terme de type $\beta$ qui représente l'évaluation de la fonction $M$ en $N$ ; et si $M$ est un terme de type $\beta$ dans un contexte où la variable $x$ est de type $\alpha$, $\lambda x^{\alpha }.M$ est de type $\alpha \to \beta$ et représente la fonction $x\mapsto M$. Si $M$ est un terme de type $\alpha$, on notera $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 $n\in \mathbb{N}$, on ajoute une constante $\underset{\_}{n}:\iota$. De plus, il y a une constante pour chaque booléen, $\mathrm{true}:o$ et $\mathrm{false}:o$. Pour chaque type de base $\sigma$, c'est-à-dire $\iota$ et $o$, on a une constante $\mathrm{if}\mathrm{then}\mathrm{else}:o\to \sigma \to \sigma \to \sigma$ représentant une instruction conditionnelle : l'idée étant que si $b$ vaut $\mathrm{true}$, l'expression $\mathrm{if}b\mathrm{then}M\mathrm{else}N$vaut $M$, si $b$ vaut $\mathrm{false}$, elle s'évalue en $N$. De plus, il y a deux fonctions pour manipuler les entiers, la fonction successeur $\mathrm{succ}:\iota \to \iota$ et la fonction prédécesseur $\mathrm{pred}:\iota \to \iota$, qui correspondent à ajouter ou soustraire $1$ à leur argument. Enfin, il y a une fonction $\mathrm{zero}?:\iota \to o$ qui renvoie $\mathrm{true}$ si son argument vaut l'entier $\underset{\_}{0}$, $\mathrm{false}$ sinon.

Enfin, le principal ingrédient de PCF est sa construction de point fixe : pour chaque type $\alpha$, on dispose d'une constante $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 rajoutent à chaque type une constante $\mathrm{\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, mais peut y être définie comme $Y(\lambda x^{\alpha }.x)$.

Sémantique opérationnelle

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

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

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

De plus, 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 $NM\to N{M}^{\prime }$ avec $M\to M^{\prime }$ et $N$ qui n'est pas une lambda-abstraction ou $\mathrm{succ}$ ou $\mathrm{pred}$ ou $\mathrm{zero}?$). Dans ce cas, la réduction obtenue préserve encore le typage et est confluente. De plus, si $M{\to }^{*}N$ avec cette réduction, et si $N$ est en forme normale, alors $M{\to }^{*}N$ avec la version restreinte. En clair, la sémantique opérationnelle définie ici est standardisante.

Exemple

PCF permet par exemple de définir des programmes effectuant l'addition de deux entiers. En voici un : Modèle:Center Si on note $ad{d}^{\prime }$ la fonction à l'intérieur de $Y$, la somme de deux et trois est calculée par la suite de réductions suivante : Modèle:CenterAinsi, $\mathrm{add}\underset{\_}{2}\underset{\_}{3}$ se réduit bien en la valeur $\underset{\_}{5}$.

Sémantique dénotationnelle

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 interéssant de traduire un terme comme $\lambda x^{\alpha }.M$ en une fonction au sens mathématique du terme. C'est le rôle de la sémantique dénotationnelle. Mais contrairement au lambda-calcul simplement typé, on ne peut pas interpréter PCF directement dans les fonctions et les ensembles, 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. 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.

Modèle continu

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

Les types de base sont interprétés comme des domaines plats : on a $[[\iota ]]={\mathbb{N}}_{\mathrm{\perp }}$ et $[[o]]={𝔹}_{\mathrm{\perp }}$, où $\mathbb{N}$ est l'ensemble des entiers naturels, $𝔹$ l'ensemble des booléens et pour tout ensemble $X$, $X_{\mathrm{\perp }}$ est le cpo défini sur l'ensemble $X$ auquel on adjoint un élément $\mathrm{\perp }$, avec l'ordre défini par $\mathrm{\perp }\le x$ pour tout $x$, et les éléments de $X$ sont incomparables entre eux. Le type $\alpha \to \beta$ est interprété comme l'ensemble des fonctions continues de $[[\alpha ]]$ vers $[[\beta ]]$. Un contexte $x_1:{\alpha }_1,\dots ,x_n:{\alpha }_n$ est interprété par $[[{\alpha }_1]]\times \dots \times [[{\alpha }_n]]$. On remarque que chaque type est un cpo, donc a un plus petit élément $\mathrm{\perp }$.

Considérons maintenant un terme typé et son contexte $\mathrm{\Gamma }⊢M:\alpha$, avec $\mathrm{\Gamma }=x_1:{\alpha }_1,\dots ,x_n:{\alpha }_n$.

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

• $[[x_i]]=(x_1,\dots ,x_n)\mapsto x_i$.
• $[[\lambda x^{\alpha }.M]]=(x_1,\dots ,x_n)\mapsto (x\mapsto [[M]](x_1,\dots ,x_n,x))$.
• $[[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 :

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

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

• $[[\mathrm{succ}]](n)=n+1$ si $n\in \mathbb{N}$ et $[[\mathrm{succ}]](\mathrm{\perp })=\mathrm{\perp }$.
• $[[\mathrm{pred}]](n)=n-1$ si $n\in \mathbb{N}$ et $n\ne 0$, $[[\mathrm{pred}]](0)=\mathrm{\perp }$ et $[[\mathrm{pred}]](\mathrm{\perp })=\mathrm{\perp }$.

• $[[zero?]](0)=\mathrm{true}$, $[[zero?]](n)=\mathrm{false}$ si $n\in \mathbb{N}$ et $n\ne 0$, et $[[zero?]](\mathrm{\perp })=\mathrm{\perp }$.
• $[[\mathrm{if}\mathrm{then}\mathrm{else}]](\mathrm{true})(x)(y)=x$, $[[\mathrm{if}\mathrm{then}\mathrm{else}]](\mathrm{false})(x)(y)=y$ et $[[\mathrm{if}\mathrm{then}\mathrm{else}]](\mathrm{\perp })(x)(y)=y$.

Modèles standards

Plus généralement, on peut interpréter PCF dans des catégories cartésiennes fermées enrichies dans les cpo. 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 $𝒞$ telle que :

• les hom-set $𝒞(A,B)$ sont des cpo pour tous objets $A$ et $B$ ;
• la composition, le pairage et la currification sont continues ;
• l'évaluation et la composition sont strictes : pour tous objets $A$, $B$ et $C$ et tout morphisme $f:A\to B$, si l'on désigne par ${\mathrm{\perp }}_D$ le plus petit élément d'un cpo $D$, on a :Modèle:Center et si l'on désigne par $B\to C$ l'objet des fonctions de $B$ vers $C$ dans la catégorie cartésienne fermée, par $⟨\cdot ,\cdot ⟩$ l'opération de pairage et par $e{v}_{B,C}:(B\to C)\times B\to C$ le morphisme d'évaluation, on a :

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

Dans ce cas, en interprétant dans $𝒞$ les constructions issues du lambda-calcul simplement typé de la façon uselle, en définissant $[[\mathrm{\Omega }]]=\mathrm{\perp }$ et $[[Y]]=\underset{n\in \mathbb{N}}{\bigvee }[[\lambda f.f^n\mathrm{\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 $[[\iota ]]=D^{\iota }$ et $[[o]]=D^o$, ce qui est rendu possible par les isomorphismes $𝒞(1,D^{\iota })\simeq {\mathbb{N}}_{\mathrm{\perp }}$ et $𝒞(1,D^o)\simeq {𝔹}_{\mathrm{\perp }}$, on obtient la sémantique désirée.

Expressivité

Turing-complétude

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

Réciproquement, étant donnée une fonction calculable $f:{\mathbb{N}}^k\to \mathbb{N}$, on peut se demander si elle est représentée par un terme $t:\stackrel{k}{\overbrace{\iota \to \iota \to \dots }}\to \iota$ de PCF tel que pour tous entiers $n_1,\dots ,n_k$ et $m$, Modèle:Center 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. Modèle:Démonstration

Bibliographie

• Modèle:Ouvrage