1 Introduction[modifier]
Programming Computable Functions (abrégé en PCF) est un langage de programmation fonctionnel minimaliste conçu pour étudier les fondements mathématiques de la calculabilité et de la sémantique des langages de programmation. Il joue un rôle central en théorie de la computation, en particulier dans l'analyse formelle des programmes et la preuve de propriétés comme la complétude en extensionnelle.
2 Historique[modifier]
PCF a été introduit dans les années 1970 par Gordon Plotkin dans son article fondamental [LCF considered as a programming language » (1977)] afin d’explorer un modèle théorique des fonctions calculables à l’aide de langages fonctionnels avec types. PCF est devenu un outil de référence en sémantique dénotationnelle et en théorie des types.
3 Définition formelle[modifier]
PCF est une extension calculable du λ-calcul typé, enrichi avec :
- des types de base, typiquement le type naturel ;
- des constantes pour zéro et successeur ;
- des opérateurs conditionnels, notamment if zero then else ;
- une opération de récursion générale permettant de définir des fonctions récursives.
3.1 Syntaxe[modifier]
La syntaxe de PCF est minimaliste et se compose principalement de :
- variables,
- abstraction (λx:T. M),
- application (M N),
- constantes (0, 1, 2, ...),
- opérateurs conditionnels,
- opérateur récursif (fixpoint).
3.2 Sémantique[modifier]
La sémantique de PCF est souvent donnée par des modèles dénotationnels utilisant les domaines commutatifs, notamment dans la sémantique domaine-théorique de Scott, permettant de traiter la récursion et la non-termination.
4 Caractéristiques[modifier]
- Langage typé statiquement, garantissant la sécurité de type.
- Supporte la récursion et donc la définition de fonctions calculables totales et partielles.
- Modèle pour comprendre la calculabilité fonctionnelle dans un cadre formel.
- Point de départ pour de nombreuses extensions vers des langages plus puissants.
5 Importance en informatique théorique[modifier]
PCF est un langage pivot dans :
- la preuve de la complétude universelle des fonctions calculables dans les langages λ-typés ;
- l'étude des propriétés de normalisation et de terminaison ;
- la construction de compilateurs optimisés à partir de raisonnements formels ;
- la recherche en sémantique opérationnelle et dénotationnelle.
6 Exemples[modifier]
Un exemple simple dans PCF permet de définir une fonction récursive pour calculer la factorielle :
fix = μ f. λ n. if n = 0 then 1 else n * f (n - 1)
Cela illustre la définition fonctionnelle classique avec l’opérateur de point fixe μ et la récursion.
7 Voir aussi[modifier]
8 Références[modifier]
Erreur de référence : La balise <ref> définie dans <references> n’a pas d’attribut de nom.