Planche : 1


Le langage PCF


Planche : 2


A
Quelques particularités
B
Un peu de rigueur

Planche : 3


Un langage fonctionnel


Planche : 4


Les constructions pragmatiques

L’arithmétique: syntaxe

Nous avons défini un certain ensemble de termes.


Planche : 5


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:

n1 op n2—→n1 op n2

Au passage: la soustraction est limitée aux entiers naturels. xy = 0 quand xy.

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

Pour la conditionnelle, on précise:

Ifz 0 Then t1 Else t2—→t1
Ifz n Then t1 Else t2—→t2  (n constante entière différente de 0)

Planche : 6


Et si les entiers n’existent pas ?

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

Mais bon, on va supposer que les entiers existent.


Planche : 7


Une fonction ?

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

Parfois écrit f: ℕ → ℕ, nn × 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:

1


0
 x2 dx
1


0
 u2 du

Planche : 8


Que faire avec une fonction ?

L’appliquer (à un argument) notation t1 t2.

(Fun x -> x*x) 2

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



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



Note 2 L’application « associe à gauche », c’est à dire que t1 t2 t3 est à comprendre comme (t1 t2) t3. Soit:


Planche : 9


Sémantique de l’application

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

(Fun x -> t1t2—→[t2\x]t1

Où la notation [t2\x]t1 veut dire: « t1x est remplacé par t2 » (on y reviendra).

Par exemple:

(Fun x -> x*x) 2

Devient

2*2

Qui, comme chacun sait, vaut 4.


Planche : 10


Fonctions de première classe

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


Planche : 11


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*mx)

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

Fun x ->  2*x+1

Ce qui correspond bien à la composition.


Planche : 12


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 = t1 In t2 ∼ (Fun x -> t2t1

Soit comme règle sémantique :

Let x = t1 In t2—→[t1\x]t2

Planche : 13


La récursion

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

 
 
x × x × ⋯ × x


n fois

Planche : 14


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)

Planche : 15


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.


Planche : 16


Un peu de rigueur: syntaxe

Les termes de PCF sont définis, par


Planche : 17


Syntaxe abstraite de PCF

type var = string

type
 op = Add | Sub | Mul | Div

type
 t =
  | Num of int
  | Var of var
  | Op  of op * t * t
  | Ifz of t * t * t
  | Let of var * t * t
  | App of t * t
  | Fun of var * t
  | Fix of var * t

Planche : 18


Un peu de rigueur: sémantique

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

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

(Fun x -> t1t2—→[t2\x]t1
Let x = t1 In t2—→[t1\x]t2
Fix x -> t—→[(Fix x -> t)\x]t
Ifz 0 Then t1 Else t2—→t1
Ifz n Then t1 Else t2—→t2 (n ≠ 0)
n1 op n2—→n1 op n2

Planche : 19


Sémantique « à petits pas »


Planche : 20


Sémantique à petits pas

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


Planche : 21


Exemples

Valeur de :


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,


Planche : 25


Retour sur la substitution

On a dit : [t1\x]t2 = remplacer x par t1 dans t2.

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(t1 op t2) = F(t1) ⋃ F(t2)
F(t1 t2) = F(t1) ⋃ F(t2)
F(Fun x -> t) = F(t) ∖ {  x  }
F(Fix x -> t) = F(t) ∖ {  x  }
F(Let x = t1 In t2) = F(t1) ⋃ (F(t2) ∖ {  x  })

Planche : 26


Remplacer x par t1

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

[t\x]x = t
[t\x]y = y
[t\x](t1 op t2) = ([t\x]t1op ([t\x]t2)
[t\x](t1 t2) = ([t\x]t1) ([t\x]t2)
[t\x](Ifz t1 Then t2 Else t3) = Ifz [t\x]t1 Then [t\x]t2 Else [t\x]t3

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 -> t1) = Fun x -> t1
[t\x](Fun y -> t1) = Fun y -> [t\x]t1
etc.
Let y = t In Fun x -> x + y

En substituant…


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 -> 

Or

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 -> t2) = Fun z -> [t\x]([z\y]t2)
[t\x](Fix y -> t2) = Fix z -> [t\x]([z\y]t2)
[t\x](Let y = t1 In t2) = Let z = [t\x]t1 In [t\x]([z\y]t2)

z est tel que zF(t) (éviter capture vue) et zF(t2) (é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.


Planche : 31


Programmes et réduction faible

  1. Dans un programme, il n’y a pas d’inconnu : on ne réduit que des termes clos.
  2. 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 :


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 ).

t1—→nt1
t1 t2—→nt1 t2
t1—→nt1
t1 op t2—→nt1 op t2
t2—→nt2
v1 op t2—→nv1 op t2
t1—→nt1
Ifz t1 Then t2 Else t3—→nIfz t1 Then t2 Else t3

Planche : 33


Autre présentation

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

Rn(t) = t, si t radical
Rn(t1 t2) = Rn(t1)
Rn(Ifz t1 Then t2 Else t3) = Rn(t1)
Rn(v op t) = Rn(t)
Rn(t1 op t2) = Rn(t1)

Planche : 34


Présentation directe de l’appel par nom

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

t1nFun x -> t3           [t2\x]t3nv
t1 t2nv
Fun x -> tnFun x -> t
[t1\x]t2nv
Let x = t1 In t2nv
[(Fix x -> t)\x]tnv
Fix x -> tnv
t1n0           t2nv
Ifz t1 Then t2 Else t3nv
t1nn (n ≠ 0)           t3nv
Ifz t1 Then t2 Else t3nv
t1nn1         t2nn2
t1 op t2nn1 op n2
nnn

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)


Planche : 36


Une autre stratégie : l’appel par valeur

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

t1nFun x -> t3           [t2\x]t3nv
t1 t2nv
[t1\x]t2nv
Let x = t1 In t2nv

Deviennent

t1vFun x -> t3           t2vv2           [v2\x]t3vv
t1 t2vv
t1vv1           [v1\x]t2vv
Let x = t1 In t2vv

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.

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

Planche : 39


Comparaison des stratégies

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

On démontre :

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


Planche : 40



Ce document a été traduit de LATEX par HEVEA