1 Introduction[modifier le wikicode]
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 le wikicode]
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 le wikicode]
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 le wikicode]
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 le wikicode]
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 le wikicode]
- 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 le wikicode]
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 le wikicode]
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 le wikicode]
8 Références[modifier le wikicode]
Erreur de référence : La balise <ref> définie dans <references> n’a pas d’attribut de nom.