En informatique théorique, Programming Computable Functions ou PCF est un langage de programmation théorique apparu pour la première fois dans une publication 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, , et un type représentant les entiers, . Les types sont donc , , ou avec et des types déjà formés. Ce type représente le type des fonctions de vers . La notation doit être lue comme .

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 ; si est un terme de type et un terme de type , est un terme de type qui représente l'évaluation de la fonction en ; et si est un terme de type dans un contexte où la variable est de type , est de type et représente la fonction . Si est un terme de type , on notera . 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 , on ajoute une constante . De plus, il y a une constante pour chaque booléen, et . Pour chaque type de base , c'est-à-dire et , on a une constante représentant une instruction conditionnelle : l'idée étant que si vaut , l'expression vaut , si vaut , elle s'évalue en . De plus, il y a deux fonctions pour manipuler les entiers, la fonction successeur et la fonction prédécesseur , qui correspondent à ajouter ou soustraire à leur argument. Enfin, il y a une fonction qui renvoie si son argument vaut l'entier , sinon.

Enfin, le principal ingrédient de PCF est sa construction de point fixe : pour chaque type , on dispose d'une constante 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 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 .

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

: pour évaluer l'application de la fonction en , on remplace par dans ; : cela exprime que est un point fixe de ;

Les règles contextuelles sont les suivantes : si alors , , , et . Elles donnent à PCF une sémantique d'appel par nom.

Cette sémantique est déterministe, c'est-à-dire que si et , alors . De plus, elle préserve le typage : si et est de type , alors 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 avec et qui n'est pas une lambda-abstraction ou ou ou ). Dans ce cas, la réduction obtenue préserve encore le typage et est confluente. De plus, si avec cette réduction, et si est en forme normale, alors 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 :

Si on note la fonction à l'intérieur de , la somme de deux et trois est calculée par la suite de réductions suivante : Ainsi, se réduit bien en la valeur .

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 intéressant de traduire un terme comme en une fonction au sens mathématique du terme. C'est le rôle de la sémantique dénotationnelle.

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 filtrantes ont une borne supérieure, et qui possède un plus petit élément. L'intérêt des cpo réside dans ce que chaque fonction continue, possède un plus petit point fixe. Une fonction est continue au sens des cpo si elle préserve les bornes supérieures de partie filtrantes. La catégorie des cpo est cartésienne fermée.

La sémantique dénotationnelle va traduire chaque terme par un objet appartenant à un certain modèle, fixé à l'avance. La propriété de correction énoncera ensuite que si , alors .

Modèle continu Le modèle continu est l'interprétation usuelle de PCF. On va définir pour chaque type, chaque contexte et chaque terme une traduction telle que l'interprétation d'un contexte ou d'un type soit un cpo, et si dans PCF, alors est une fonction continue de l'interprétation du contexte vers l'interprétation du type de .

Les types de base sont interprétés comme des domaines plats : on a et , où est l'ensemble des entiers naturels, l'ensemble des booléens et pour tout ensemble , est le cpo défini sur l'ensemble auquel on adjoint un élément , avec l'ordre défini par pour tout , et les éléments de sont incomparables entre eux. Intuitivement, désigne un programme qui ne termine pas. Le type est interprété comme l'ensemble des fonctions continues de vers . L'idée intuitive derrière cet ordre étant que pour deux fonctions et de même type, représentant des fonctions partiellement définies, signifie que est une approximation de , ou que est définie en plus de points que . Un contexte est interprété par . On remarque que chaque type est un cpo, donc a un plus petit élément .

Considérons maintenant un terme typé et son contexte , avec .

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

. . .

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

est la fonction qui à chaque associe son plus petit point fixe. Il est défini comme , c'est-à-dire comme le supremum de la suite croissante . Puisque intuitivement, , et que le plus petit point fixe de la fonction identité est , s'il est présent, .

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

si et . si et , et .

, si et , et . , et .

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-sets sont des cpo pour tous objets et ; la composition, le pairage et la currification sont continues ; l'évaluation et la composition sont strictes : pour tous objets , et et tout morphisme , si l'on désigne par le plus petit élément d'un cpo , on a : et si l'on désigne par l'objet des fonctions de vers dans la catégorie cartésienne fermée, par l'opération de pairage et par le morphisme d'évaluation, on a :

la catégorie possède deux objets et tels que soit isomorphe à et soit isomorphe à en tant que cpo, où l'objet terminal de la catégorie . Dans la catégorie des cpo, 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 et et en interprétant les constructions sur les types primitifs de la même façon que dans le modèle continu en posant et , ce qui est rendu possible par les isomorphismes et , on obtient la sémantique désirée.

Vocabulaire des modèles standards On peut distinguer certains types de modèles de PCF. Les définitions présentées ici sont celles de Amadio et Curien, et ne sont pas standard ; Milner désigne par le vocable « extensionnel » ce qu'Amadio et Curien désignent par « extensionnellement ordonné » :

Un modèle standard est extensionnel si pour tous , si et seulement si , où l'objet terminal de . Cela signifie que peut être vu comme un ensemble de fonctions de vers . Cela correspond à la notion de catégorie bien pointée. Un modèle standard est extensionnellement ordonné s'il est extensionnel et que pour tous , si et seulement si . Cela signifie que si on regarde et comme des fonctions, l'ordre entre et est l'ordre point à point.

Adéquation Le théorème d'adéquation () énonce que dans tout modèle standard, un programme calculant un entier est interprété par l'entier qu'il calcule.

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 ou par Amadio et Curien utilisent la méthode des , 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.

Équivalences entre termes Étant donné deux termes et , on peut se demander à quelle condition ces deux termes sont « les mêmes ».

Équivalence observationnelle Une première notion d'équivalence entre termes est l'équivalence observationnelle : 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 et , qui calculent toutes deux l'identité, mais sont en forme normale pour . 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 et , 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 pour et des booléens et . Sans perte de généralité, les résultats qui suivront ne mentionneront que les entiers.