Le langage PCF

Planche : 2

A

Quelques particularités

Les fonctions.
La récursion.

B

Un peu de rigueur

Syntaxe.
Sémantique à petits pas.
Sémantique à grands pas.

Un langage fonctionnel

PCF est un modèle de langage de programmation.
- Dans un modèle, on simplifie, au profit d’un traitement rigoureux et complet de la sémantique.
- PCF dit ce que les langages fonctionnels (ML, Lisp, Haskell) ont en commun (leur noyau).
PCF est d’abord un calcul des fonctions.
Plus quelques constructions « pragmatiques » (genre: l’arithmétique et ses quatre opérations).

Les constructions pragmatiques

L’arithmétique: syntaxe

Une infinité de constantes: 0, 1 etc.
Quatre symboles binaires pour quatre opérations +, -, *, /.
Une conditionnelle, symbole ternaire Ifz t₁ Then t₂ Else t₃.

Nous avons défini un certain ensemble de termes.

L’arithmétique: sémantique

On définit une infinité d’axiomes qui donnent le sens des quatre opérations:

0+0—→0

1+0—→1

1+1—→2

…

Résumé en:

n₁ op n₂—→n₁ op n₂

Au passage: la soustraction est limitée aux entiers naturels. x−y = 0 quand x ≤ y.

Cela revient à supposer que les entiers existent, ce qui est raisonable

Pour la conditionnelle, on précise:

Ifz 0 Then t₁ Else t₂—→t₁

Ifz n Then t₁ Else t₂—→t₂ (n constante entière différente de 0)

Et si les entiers n’existent pas ?

Les définir selon l’arithmétique de Peano:

Une constante 0 et un symbole unaire S (successeur) Deux se note alors S (S 0).
Des axiomes en nombre fini du genre:

0+t—→t

S(t₁)+t₂—→S(t₁+t₂)

… Ifz 0 Then t₁ Else t₂—→t₁

Ifz S(t) Then t₁ Else t₂—→t₂

Mais bon, on va supposer que les entiers existent.

Une fonction ?

En maths : soit f définie de ℕ dans ℕ, qui à n associe n × n.

Parfois écrit f: ℕ → ℕ, n ↦ n × n.

En PCF:

Fun n -> n * n

La différence: la liaison de la variable n est explicite.

Ces variables sont muettes, on aurait pu écrire:

Fun x -> x * x

La variable « muette » est déjà connue:

∫

x² dx

∫

u² du

…

Que faire avec une fonction ?

L’appliquer (à un argument) notation t₁ t₂.

(Fun x -> x*x) 2

L’exécution du terme/programme ci dessus, doit bien renvoyer 4.

Note 1 La notation t₁ t₂ cache l’existence d’un symbole binaire “@” parfois explicité: @(t₁,t₂).

Note 2 L’application « associe à gauche », c’est à dire que t₁ t₂ t₃ est à comprendre comme (t₁ t₂) t₃. Soit:

Sémantique de l’application

Ou plutôt du passage d’argument ou β réduction

(Fun x -> t₁) t₂—→[t₂\x]t₁

Où la notation [t₂\x]t₁ veut dire: « t₁ où x est remplacé par t₂ » (on y reviendra).

Par exemple:

(Fun x -> x*x) 2

Devient

2*2

Qui, comme chacun sait, vaut 4.

Fonctions de première classe

L’argument d’une fonction peut être une fonction.
Fun f -> f 0
Appliquée à Fun x -> 1+x la fonction ci-dessus renvoie: 1.
Le résultat d’une fonction peut être une fonction.
Fun n -> Fun m -> n + m
Appliquée à 1, la fonction ci-dessus renvoie: Fun m -> 1+m, une fonction qui ajoute 1 à son argument.

Remarque : Avec les fonctions qui renvoient des fonctions, on a aussi les fonctions à plusieurs arguments (curryfication).

Exemple classique de fonctions de première classe

La composition.

Fun f -> Fun g -> Fun x -> f (g x)

Ainsi:

(Fun f -> Fun g -> Fun x -> f (g x))
(Fun n -> n+1)
(Fun m -> 2*m)

Doit valoir (deux β-réductions, sur f puis g)

Fun x -> (Fun n -> n+1) ((Fun m -> 2*m) x)

Et donc (deux autres β-réductions, sur m puis n)

Fun x -> 2*x+1

Ce qui correspond bien à la composition.

La définition locale

Il est plus clair d’écrire:

Let comp = Fun f -> Fun g -> Fun x -> f (g x)) In
Let inc = Fun n -> n+1 In
Let twice = Fun m -> 2*m In
comp inc twice

En gros, l’idée c’est:

Let x = t₁ In t₂ ∼ (Fun x -> t₂) t₁

Soit comme règle sémantique :

Let x = t₁ In t₂—→[t₁\x]t₂

La récursion

Comment définir la fonction puissance (ℕ² → ℕ), qui à x et n entiers associe:


x × x × ⋯ × x
◥	▼	◤

n fois

En mathématiques (si on évite le ⋯ vite ambigu): récurrence.
Dans les langages de programmation:
- Boucle (Java):
  int r = 1 ;
  for (int k = 1 ; k <= n ; k++) r := r * x ;
- Définition récursive (Caml):
  let rec pow x n =
  if n = 0 then 1 else x * pow x (n-1)

Définition « par point fixe »

En PCF on définit la fonction pow comme égale à

Fun x -> Fun n -> Ifz n Then 1 Else x * pow x (n-1)

Mais pow ne peut pas être utilisée dans sa propre définition.

On écrit plutôt p = Φ p avec:

Let Φ =
Fun pow ->
Fun x -> Fun n -> Ifz n Then 1 Else x * pow x (n-1)

À comprendre comme: la fonction p est point fixe de Φ.

On laisse de côté pour le moment la question de l’existence/unicité de ce point fixe et on note :

Fix pow ->
Fun x -> Fun n -> Ifz n Then 1 Else x * pow x (n-1)

Réduction du Fix

Un moyen de contourner l’existence/unicité : définir l’effet du Fix.

Fix x -> t—→[Fix x -> t\x]t

L’idée est en fait très simple:

(Fix fact -> Fun n -> Ifz n Then 1 Else n*fact (n-1)) 3

Règle du Fix, remplacer fact par Fix fact -> ….

(Fun n -> Ifz n Then 1 Else n * (Fix fact -> …) (n-1)) 3

β-règle (remplacer n par 3).

Ifz 3 Then 1 Else 3 * (Fix fact -> …) (3-1)

Comme 3 n’est pas nul, et que 3-1 vaut 2:

3 * (Fix fact -> …) 2

Soit en gros 3 * fact 2 c’est gagné. Au final 3 * 2 * 1 * 1.

Un peu de rigueur: syntaxe

Les termes de PCF sont définis, par

Une infinité de constantes 0, 1, etc.
Quatre symboles d’opération +, -, *, / (binaires, notés de façon infixe dans les termes t₁ + t₂).
Un symbole ternaire (Ifz, notation des termes Ifz t₁ Then t₂ Else t₃).
Un ensemble de variables.
Le symbole binaire de fonction, termes notés Fun x -> t (le premier argument est une variable, liée dans t).
Le symbole binaire du point fixe, termes notés Fix x -> t.
La définition, ternaire, termes notés Let x = t₁ In t₂.

Syntaxe abstraite de PCF

Planche : 18

Un peu de rigueur: sémantique

Le but est de définir une relation t↪v entre les programmes (termes de PCF) et leur valeurs.

Base de départ, six axiomes de réduction élémentaires:

(Fun x -> t₁) t₂—→[t₂\x]t₁

Let x = t₁ In t₂—→[t₁\x]t₂

Fix x -> t—→[(Fix x -> t)\x]t

Ifz 0 Then t₁ Else t₂—→t₁

Ifz n Then t₁ Else t₂—→t₂ (n ≠ 0)

n₁ op n₂—→n₁ op n₂

Planche : 19

Sémantique « à petits pas »

Les termes réductibles ou radicaux. Ex. 1 + 1, (Fun x -> x + x) y.
Contracter un radical (règle t₁—→t₂) c’est remplacer t₁ par t₂. Ex. 2, y + y.
Plus « Passage au contexte »: contracter les radicaux dans les termes.

t₁—→t′₁

t₁ t₂—→t′₁ t₂

t₂—→t′₂

t₁ t₂—→t₁ t′₂

t—→t′

Fun x -> t—→Fun x -> t′

…

Planche : 20

Sémantique à petits pas

Rappel ? La fermeture réflexive-transitive R^* d’une relation R.

t R t

t₁ R t₂

t₁ R^* t₂

t₁ R^* t₂ t₂ R^* t₃

t₁ R^* t₃
Les valeurs v sont définies comme les termes irréductibles (ou formes normales)
v ∈ NF ⇔∄w, v—→w
Définition de la sémantique t↪v ssi:
t—→^*v et v ∈ NF

Autrement dit: réduire les radicaux de t, jusqu’à plus soif.

Planche : 21

Exemples

Valeur de :

Fix x -> x ? Pas de valeur car t—→t et pas le choix.
(Fun y -> 3) 2 ? 3 en une β-réduction.
(Fun y -> 3) (Fix x -> x) ? 3 en une β-réduction, si on est malin,
Fix n -> 1+n ? Pas de valeur, réduction de t sur 1+t, 1+(1+t), 1+(1+(1+t)), etc.

Planche : 22

Exemple plus sérieux

Let pow2 = Fix p -> Fun n -> Ifz n Then 1 Else 2 * p (n-1) In
pow2 2

Réduire liaison:

(Fix p -> Fun n -> Ifz n Then 1 Else 2 * p (n-1)) 2

Notons P = Fix p -> ⋯. Réduire point fixe:

(Fun n -> Ifz n Then 1 Else 2 * P (n-1)) 2

β-réduction.

Ifz 2 Then 1 Else 2 * P (2-1)

2 * P (2-1)

2 * (Fun n -> Ifz n Then 1 Else 2 * P (n-1)) (2-1)

2 * (Ifz 2-1 Then 1 Else 2 * P ((2-1)-1))

2 * (Ifz 1 Then 1 Else 2 * P ((2-1)-1))

2 * (2 * P ((2-1)-1))

2 * (2 * ((Fun n -> Ifz n Then 1 Else 2 * P (n-1)) ((2-1)-1)))

2 * (2 * (Ifz ((2-1)-1) Then 1 Else 2 * P (((2-1)-1)-1))

2 * (2 * (Ifz (1-1) Then 1 Else 2 * P (((2-1)-1)-1))

2 * (2 * (Ifz 0 Then 1 Else 2 * P (((2-1)-1)-1))

2 * (2 * 1)

Deux multiplications, ouf 4.

Planche : 23

Le déterminisme

Dans un terme, il peut y avoir plusieurs radicaux. La réduction opère donc un choix.

Ce choix a-t-il un impact ? Les valeurs (formes normales) sont elles uniques ?)

Planche : 24

Confluence

L’unicité des formes normales découle du résultat plus fort de confluence (Théorème, admis).

Qui dit en gros,

Deux calculs divergents (t₂ ou t₃).
Ne le sont jamais définitivement (il existe t₄).

Planche : 25

Retour sur la substitution

On a dit : [t₁\x]t₂ = remplacer x par t₁ dans t₂.

La substitution donne le sens des variables.

Elle permet aussi de donner un sens aux expressions qui possèdent des variables libres (ou non-closes).

Par ex. x+1. possède un sens clair dès que l’on donne une valeur à x.

Rappel ? définition des variables libres

F(n) = ∅

F(x) = { x }

F(t₁ op t₂) = F(t₁) ⋃ F(t₂)

F(t₁ t₂) = F(t₁) ⋃ F(t₂)

F(Fun x -> t) = F(t) ∖ { x }

F(Fix x -> t) = F(t) ∖ { x }

F(Let x = t₁ In t₂) = F(t₁) ⋃ (F(t₂) ∖ { x })

Planche : 26

Remplacer x par t₁

Est-ce si simple ? En l’absence de lieurs, oui.

[t\x]x = t

[t\x]y = y

[t\x](t₁ op t₂) = ([t\x]t₁) op ([t\x]t₂)

[t\x](t₁ t₂) = ([t\x]t₁) ([t\x]t₂)

[t\x](Ifz t₁ Then t₂ Else t₃) = Ifz [t\x]t₁ Then [t\x]t₂ Else [t\x]t₃

Soit par exemple,

[t\x](x + y) = t + y

Planche : 27

En présence de lieurs

La substitution donne la valeur des variables libres. On propose donc:

[t\x](Fun x -> t₁) = Fun x -> t₁

[t\x](Fun y -> t₁) = Fun y -> [t\x]t₁

etc.

Let y = t In Fun x -> x + y

En substituant…

Si t est 4 on a Fun x -> x + 4.
Si t est z on a Fun x -> x + z.
Si t est x a-t-on Fun x -> x + x ?
Il ne vaut mieux pas ! Considérer la confluence de:
Let x = 1 in Let y = x in Fun x -> x + y

Planche : 28

Alpha-équivalence

Dans l’exemple [x\y](Fun x -> x + y), nous sommes victimes de la capture de la variable libre x, qui devient liée en traversant la liaison Fun x -> …

Si l’argument de la fonction est nommé z on peut substituer :
[x\y](Fun z -> z + y) = Fun z -> z + x.
Les fonctions Fun x -> x + y et Fun z -> z + y sont les mêmes (changement de la variable muette).

L’alpha-équivalence est l’égalité modulo le changement des variables muettes.

On considère les termes « modulo alpha-équivalence ».

Planche : 29

Une définition de la substitution

Choisir un bon représentant des classes d’alpha-équivalence.

[t\x](Fun y -> t₂) = Fun z -> [t\x]([z\y]t₂)

[t\x](Fix y -> t₂) = Fix z -> [t\x]([z\y]t₂)

[t\x](Let y = t₁ In t₂) = Let z = [t\x]t₁ In [t\x]([z\y]t₂)

Où z est tel que z ∉F(t) (éviter capture vue) et z ∉F(t₂) (éviter autre capture).

Plus les définitions pour les symboles sans lieurs.

Planche : 30

Sémantique et exécution de programme

Dans un terme, il peut y avoir un choix de radicaux.

On veut modéliser le calcul d’un ordinateur déterministe.
Or, certains choix de radicaux de réduction calculent la forme normale, d’autres non.
Let loop = Fix f -> Fun x -> f x In
Let k = Fun x -> Fun y -> y In
k (loop 0) 1
La sémantique doit répondre à : vaut 1 ou ne termine pas ?
En outre, peu d’intérêt à distinguer:
Fun x -> x + 11

Fun x -> x + (7+4)
En outre, toutes les variables d’un programme ont une définition.

Planche : 31

Programmes et réduction faible

Dans un programme, il n’y a pas d’inconnu : on ne réduit que des termes clos.
Les fonctions sont des fonction et point.

On réduit des termes clos et on utilise jamais la règle :

t—→t′

Fun x -> t—→Fun x -> t′

Tout cela revient à définir les valeurs v ainsi :

Une constante entière n.
Ou bien une fonction Fun x -> t (t terme quelconque, avec F(t) ⊆ { x }).

Planche : 32

Une stratégie

C’est une sous-relation (⇒, ⊆) déterministe de la relation de réduction (→).

Définissons « l’appel par nom », dont la principale caractéristique est de ne pas réduire les arguments des fonctions.

Les axiomes ne changent pas (voir slide ).

t₁—→_nt′₁

t₁ t₂—→_nt′₁ t₂

t₁—→_nt′₁

t₁ op t₂—→_nt′₁ op t₂

t₂—→_nt′₂

v₁ op t₂—→_nv₁ op t′₂

t₁—→_nt′₁

Ifz t₁ Then t₂ Else t₃—→_nIfz t′₁ Then t₂ Else t₃

Planche : 33

Autre présentation

Le radical réduit est le plus extérieur (et le plus à gauche).

R_n(t) = t, si t radical

R_n(t₁ t₂) = R_n(t₁)

R_n(Ifz t₁ Then t₂ Else t₃) = R_n(t₁)

R_n(v op t) = R_n(t)

R_n(t₁ op t₂) = R_n(t₁)

Une étape: contracter R_n(t).
Itérer (—→_n^*) jusqu’à trouver une valeur.

Planche : 34

Présentation directe de l’appel par nom

En sémantique dite à grands pas, ou naturelle.

t₁↪_nFun x -> t₃ [t₂\x]t₃↪_nv

t₁ t₂↪_nv

Fun x -> t↪_nFun x -> t

[t₁\x]t₂↪_nv

Let x = t₁ In t₂↪_nv

[(Fix x -> t)\x]t↪_nv

Fix x -> t↪_nv

t₁↪_n0 t₂↪_nv

Ifz t₁ Then t₂ Else t₃↪_nv

t₁↪_nn (n ≠ 0) t₃↪_nv

Ifz t₁ Then t₂ Else t₃↪_nv

t₁↪_nn₁ t₂↪_nn₂

t₁ op t₂↪_nn₁ op n₂

n↪_nn

Planche : 35

Quelle présentation choisir ?

On préfère souvent la sémantique naturelle plus concise, en particulier pour programmer un évaluateur (TP).

Mais, ne dit rien des termes qui ne terminent pas, ne dit rien des termes « bloqués » (ex. 1 appliqué à 2).

Les résultats théoriques sont donc plus précis en sémantique par petit pas.

Équivalences (admises)

Si t↪_nv, alors t—→_n^*v.
Si t—→_n^*v (v valeur), alors t↪_nv.

Planche : 36

Une autre stratégie : l’appel par valeur

Par rapport à l’appel par nom, deux règles changent :

t₁↪_nFun x -> t₃ [t₂\x]t₃↪_nv

t₁ t₂↪_nv

[t₁\x]t₂↪_nv

Let x = t₁ In t₂↪_nv

Deviennent

t₁↪_vFun x -> t₃ t₂↪_vv₂ [v₂\x]t₃↪_vv

t₁ t₂↪_vv

t₁↪_vv₁ [v₁\x]t₂↪_vv

Let x = t₁ In t₂↪_vv

Note : Les arguments sont réduits avant la substitution.

Planche : 37

Appel par valeur

Parfois caractérisé comme « contracter le radical le plus profond » (et le plus à gauche). Ce n’est pas tout à fait exact.

Le Ifz ne change pas. Autrement dit on ne remplace pas

t₁↪_n0 t₂↪_nv₂

Ifz t₁ Then t₂ Else t₃↪_nv₂

par

t₁↪_v0 t₂↪_vv₂ t₃↪_vv₃

Ifz t₁ Then t₂ Else t₃↪_vv₂
Autrement dit, il reste un peu d’appel par nom.

Idem pour Fix x -> t. Le termes t n’est pas réduit, même si il contient un radical « plus profond ».

Planche : 38

Manque d’expressivité de l’appel par valeur

On définit (Let) la function fi.

Fun x -> Fun y -> Fun z -> Ifz x Then z Else y

En appel par nom, on a l’équivalence :
fi t₁ t₂ t₃↪_nv ⇔Ifz t₁ Then t₃ Else t₂↪_nv
Mais pas en appel par valeur. Considérer :
Ifz 0 Then 1 Else (Fix x -> x)
Et
fi 0 (Fix x -> x) 1
Noter :
Fix x -> x → Fix x -> x → Fix x -> x → ⋯

Planche : 39

Comparaison des stratégies

Appel par nom : Algol 60, Haskell. Appel par valeur : tout les autres langages (ML).

On démontre :

Que l’appel par nom est sûr.
(t—→^*v) ⇒ (t↪_nv)

Exemple simple :
(Fun x -> Fun y -> y) (Fix x -> x) 1
Que l’appel par nom autorise les transformations de programme arbitraires.
t—→^*t′ ⇒ (t↪_nv ⇔t′↪_nv′)

Avec v = v′ pour les entiers, v ←→^* v′ en gal.

On constate que l’appel par valeur est plus facile à comprendre.

Planche : 40

TP, divers évaluateurs.
La prochaine fois, interprétation.

Ce document a été traduit de L^AT_EX par H^EV^EA

Planche : 1

Planche : 2

Planche : 3

Un langage fonctionnel

Planche : 4

Les constructions pragmatiques

Planche : 5

L’arithmétique: sémantique

Planche : 6

Et si les entiers n’existent pas ?

Planche : 7

Une fonction ?

Planche : 8

Que faire avec une fonction ?

Planche : 9

Sémantique de l’application

Planche : 10

Fonctions de première classe

Planche : 11

Exemple classique de fonctions de première classe

Planche : 12

La définition locale

Planche : 13

La récursion

Planche : 14

Définition « par point fixe »

Planche : 15

Réduction du Fix

Planche : 16

Un peu de rigueur: syntaxe

Planche : 17

Syntaxe abstraite de PCF

Planche : 18

Un peu de rigueur: sémantique

Planche : 19

Sémantique « à petits pas »

Planche : 20

Sémantique à petits pas

Planche : 21

Exemples

Planche : 22

Exemple plus sérieux

Planche : 23

Le déterminisme

Planche : 24

Confluence

Planche : 25

Retour sur la substitution

Planche : 26

Remplacer x par t1

Planche : 27

En présence de lieurs

Planche : 28

Alpha-équivalence

Planche : 29

Une définition de la substitution

Planche : 30

Sémantique et exécution de programme

Planche : 31

Programmes et réduction faible

Planche : 32

Une stratégie

Planche : 33

Autre présentation

Planche : 34

Présentation directe de l’appel par nom

Planche : 35

Quelle présentation choisir ?

Équivalences (admises)

Planche : 36

Une autre stratégie : l’appel par valeur

Planche : 37

Appel par valeur

Planche : 38

Manque d’expressivité de l’appel par valeur

Planche : 39

Comparaison des stratégies

Planche : 40

Remplacer x par t₁