M 203 Mie
M 203 Mie
M 203 Mie
Durée : 4 heures
L’utilisation des calculatrices n’est pas autorisée pour cette épreuve
Programmation fonctionnelle,
sémantique et topologie
Notations et définitions
— On note P(E) l’ensemble des parties d’un ensemble E.
— On note E ] F l’union disjointe des ensembles E et F .
— Soit ETun ensemble et F un ensemble de sous-ensemblesSde E, c’est à dire F ⊆ P(E). On
note F l’intersection deTtous les ensemblesS de F et F l’union de tous les ensembles
de F . Quand F est vide, F = E et F = ∅.
— La partie entière inférieure est notée b c. En particulier, si n ∈ N, alors bn/2c est le plus
grand entier m ∈ N tel que 2m ≤ n.
— Un ordre partiel (E, ≤E ) est un ensemble E équipé d’une relation binaire ≤E qui
est réflexive, transitive et antisymétrique. Dans ce contexte, on notera <E l’ordre strict
induit par ≤E , dont on rappelle la définition : x <E y quand x ≤E y et x 6= y.
— Soit (E, ≤E ) un ordre partiel et (xi )i∈N une suite d’éléments de E. On dit que y ∈ E
est un majorant de la suite quand xi ≤E y pour tout i ∈ N. On dit que y est une
borne supérieure de la suite quand y est un majorant de la suite et qu’on a y ≤E z
pour tout majorant z de la suite.
1
Partie I
On définit les types comme les expressions syntaxiques engendrées à partir des types de
base unit, bool et nat au moyen de l’opérateur binaire ( ⇒ ), qui correspond intuitivement
à l’opérateur ( -> ) du langage OCaml. Par exemple, nat et unit ⇒ (bool ⇒ bool) sont des
types. Dans la suite, les types seront représentés par la lettre τ .
L’objectif de cette partie est de définir, pour tout type τ , un certain ensemble partiellement
ordonné (Jτ K, ≤τ ). Dans la partie suivante, les programmes de type τ seront interprétés comme
des éléments de Jτ K.
Étant donné un ordre partiel (A, ≤A ), une suite croissante de A est une suite (ai )i∈N
d’éléments de A telle que, pour tout i ∈ N, ai ≤A ai+1 . On dit que (A, ≤A ) est un ordre
partiel complet quand (A, ≤A ) est un ordre partiel et que toute suite croissante (ai )i∈N
d’éléments de A admet une borne supérieure, notée supA i∈N ai .
Étant donnés deux ordres partiels complets (A, ≤A ) et (B, ≤B ), une application f : A → B
est dite croissante quand, pour tous a1 ∈ A et a2 ∈ A tels que a1 ≤A a2 , on a f (a1 ) ≤B f (a2 ).
L’application f est dite continue quand elle est croissante et que, pour toute suite croissante
(ai )i∈N de A, on a f (supA B
i∈N ai ) = supi∈N f (ai ).
Définissons dans un premier temps (Jτ K, ≤τ ) pour les types de base. À cet effet, on se
donne des constantes distinctes ⊥nat , ⊥bool , ⊥unit , tt, ff et uu. Les trois dernières correspondent
intuitivement aux valeurs OCaml true, false et (). Les constantes ⊥τ serviront à représenter
l’absence de résultat des programmes de type τ dont l’évaluation ne termine pas. On définit :
def def
B = {tt, ff} U = {uu}
def def def
JnatK = N ] {⊥nat } JboolK = B ] {⊥bool } JunitK = U ] {⊥unit }
Pour chaque type de base b ∈ {unit, nat, bool} on définit enfin ≤b comme suit : pour tous
e1 , e2 ∈ JbK, e1 ≤b e2 ssi e1 = e2 ou e1 = ⊥b . Il est clair que cela définit des ordres partiels ;
inutile de le vérifier dans les réponses aux questions. L’ordre partiel ≤nat peut être représenté
graphiquement comme suit :
0 1 2 ···
⊥nat
Question 1.1. On souhaite vérifier que (JnatK, ≤nat ) est un ordre partiel complet :
a. Caractériser les suites croissantes de (JnatK, ≤nat ).
b. En déduire que toute suite croissante de (JnatK, ≤nat ) admet une borne supérieure.
On admet que (JunitK, ≤unit ) et (JboolK, ≤bool ) sont aussi des ordres partiels complets.
Étant donnés deux types τ1 et τ2 pour lesquels on suppose avoir construit les ordres partiels
complets (Jτ1 K, ≤τ1 ) et (Jτ2 K, ≤τ2 ), on définit Jτ1 ⇒ τ2 K comme l’ensemble des applications
continues de Jτ1 K dans Jτ2 K :
def
Jτ1 ⇒ τ2 K = {f : Jτ1 K → Jτ2 K | f est continue}
2
On définit ensuite la relation ≤τ1 ⇒τ2 en posant, pour tous f, g ∈ Jτ1 ⇒ τ2 K :
Enfin, on définit ⊥τ1 ⇒τ2 comme la fonction f : Jτ1 K → Jτ2 K telle que f (e) = ⊥τ2 pour tout
e ∈ Jτ1 K.
On admettra que (Jτ1 ⇒ τ2 K, ≤τ1 ⇒τ2 ) est un ordre partiel, et que ⊥τ1 ⇒τ2 est son plus petit
élément.
Question 1.2. On considère dans cette question le cas particulier où τ1 = nat et τ2 = unit.
a. Montrer que toute application croissante f : JnatK → JunitK est continue.
b. Combien y a-t-il d’éléments f ∈ Jnat ⇒ unitK tels que f (⊥nat ) 6= ⊥unit ?
c. Donner, sans justifier, une suite strictement croissante de Jnat ⇒ unitK, c’est à dire une
suite (fi )i∈N telle que fi <nat⇒unit fi+1 pour tout i ∈ N.
Question 1.3. Soient τ1 et τ2 des types tels que (Jτ1 K, ≤τ1 ) et (Jτ2 K, ≤τ2 ) sont des ordres
partiels complets.
a. Soit (fi )i∈N une suite croissante de (Jτ1 ⇒ τ2 K, ≤τ1 ⇒τ2 ). Pour tout e ∈ Jτ1 K, (fi (e))i∈N
est une suite croissante de (Jτ2 K, ≤τ2 ) par définition de ≤τ1 ⇒τ2 , et admet donc une borne
supérieure.
Montrer que l’application f 0 : Jτ1 K → Jτ2 K définie par f 0 (e) = supi∈N
2
fi (e) est continue.
Jτ K
Tout type étant construit (en un nombre fini d’étapes) à partir des types de base au moyen
de l’opérateur ( ⇒ ), les définitions et résultats précédents nous donnent pour chaque type τ
un ordre partiel complet (Jτ K, ≤τ ).
3
Partie II
Nous introduisons dans cette partie les programmes et leur interprétation. On suppose un
ensemble infini dénombrable de variables, noté X et dont les éléments seront représentés par
les lettres x, y et z dans la suite. Les programmes, qui seront représentés par les lettres p et
q, sont des expressions syntaxiques données par la grammaire suivante, où n dénote un entier
arbitraire :
p ::= uu
| tt | ff | if p0 then p1 else p2 | p1 = p2
| n | p1 + p2 | p1 − p2 | p1 × p2 | p0 /2
| x | (fun x → p0 ) | (p1 p2 ) | (rec p0 )
| (p1 ku p2 )
Cela signifie que l’ensemble des programmes est le plus petit ensemble tel que : les constantes
uu, tt et ff sont des programmes ; tout n ∈ N est un programme ; tout x ∈ X est un programme ;
si p0 , p1 et p2 sont des programmes alors if p0 then p1 else p2 aussi ; etc. Dans la plupart des cas,
les constructions de programmes utilisent les mêmes notations qu’en OCaml, et la signification
intuitive des constructions sera analogue à celle d’OCaml. Certaines autres constructions sont
nouvelles. Dans tous les cas, une signification mathématique précise sera donnée plus loin.
Nous définissons ensuite une notion de typage pour nos programmes. Contrairement au cas
du langage OCaml, un programme de notre langage admettra au plus un type. Afin de fixer
l’unique type de chaque variable, on se donne une application t des variables dans les types.
Nous supposerons que pour tout type τ il existe une infinité de variables x telles que t(x) = τ .
La relation de typage exprimant qu’un programme p est de type τ , notée p : τ , est ensuite
définie par les équivalences suivantes, pour tous programmes p0 , p1 , p2 , pour tout type τ , et
pour tous n ∈ N et x ∈ X :
uu : τ ⇔ τ = unit
tt : τ ⇔ τ = bool
ff : τ ⇔ τ = bool
n:τ ⇔ τ = nat
(if p0 then p1 else p2 ) : τ ⇔ p0 : bool, p1 : τ et p2 : τ
(p1 = p2 ) : τ ⇔ τ = bool et il existe τ 0 ∈ {unit, nat, bool} tel que p1 : τ 0 et p2 : τ 0
p1 + p2 : τ ⇔ τ = nat, p1 : nat et p2 : nat
p1 − p2 : τ ⇔ τ = nat, p1 : nat et p2 : nat
p1 × p2 : τ ⇔ τ = nat, p1 : nat et p2 : nat
p0 /2 : τ ⇔ τ = nat, p0 : nat
x:τ ⇔ t(x) = τ
(fun x → p0 ) : τ ⇔ il existe τ 0 tel que p0 : τ 0 et τ = (t(x) ⇒ τ 0 )
(p1 p2 ) : τ ⇔ il existe τ 0 tel que p1 : (τ 0 ⇒ τ ) et p2 : τ 0
(rec p0 ) : τ ⇔ p0 : (τ ⇒ τ )
(p1 ku p2 ) : τ ⇔ τ = unit, p1 : unit et p2 : unit
On pourra par exemple vérifier que (1 + (fun x → x)) : τ est faux quel que soit τ . Ou encore,
que (fun x → (fun y → (1 + x))) : (nat ⇒ t(y) ⇒ nat) est vrai à condition que t(x) = nat.
4
Question 2.1. Soient x, y et z des variables quelconques, et τ un type. Indiquer, sans justifier,
sous quelles conditions sur τ , t(x), t(y) et t(z) on a (fun x → if x = y then y else z) : τ .
On considère désormais uniquement des programmes p bien typés, c’est à dire pour lesquels
il existe τ tel que p : τ . Quand p est un programme bien typé, on note t(p) son unique type.
5
On s’intéresse maintenant à l’interprétation des programmes de la forme rec p0 , permettant
des définitions récursives de façon analogue au let rec ... d’OCaml. Un programme rec p0 est
de type τ quand p0 : τ ⇒ τ . Puisque Jp0 KE est une application continue de Jτ K dans lui-même,
la suite ((Jp0 KE )i (⊥τ ))i∈N est croissante : on a en effet ⊥τ ≤τ Jp0 KE (⊥τ ) par minimalité de ⊥τ ,
puis Jp0 KE (⊥τ ) ≤τ (Jp0 KE )2 (⊥τ ) par croissance de Jp0 KE , et ainsi de suite. Toute suite croissante
admettant une borne supérieure dans l’ordre partiel complet (Jτ K, ≤τ ), l’interprétation Jrec p0 KE
est bien définie.
Question 2.3. Soient f, n ∈ X des variables telles que t(n) = nat et t(f ) = (nat ⇒ nat). On
pose :
def
p = fun f → fun n → if n = 0 then 1 else n × f (n − 1)
On pourra vérifier que p est bien typé, de type (nat ⇒ nat) ⇒ (nat ⇒ nat).
a. Soit f ∈ Jnat ⇒ natK et e ∈ JnatK. Exprimer JpK(f )(e) en fonction de e et f .
b. Calculer JpKi+1 (⊥nat⇒nat )(e) pour tous i ∈ N et e ∈ JnatK.
c. En déduire que Jrec pK(k) = k! pour tout k ∈ N, et donner la valeur de Jrec pK(⊥nat ).
On vérifie aisément que DIVτ : τ et JDIVτ K = ⊥τ . Intuitivement, DIVτ est défini récursivement
comme un objet x égal à lui même. L’évaluation de DIVτ déroule à l’infini cette définition, et
ne termine donc pas.
Il existe donc des programmes p : τ1 ⇒ τ2 tels que JpK(e) = ⊥τ2 pour tout e ∈ Jτ1 K. Si τ2 est
un type de base, l’évaluation de (p q) ne termine donc pas, quel que soit q : τ1 . Réciproquement,
il existe des programmes p : τ1 ⇒ τ2 tels que (p q) termine toujours, même quand JqK = ⊥τ1 .
Par exemple, si x est une variable de type nat, le programme (fun x → 42) : nat ⇒ nat a pour
interprétation l’application qui envoie tout élément de JnatK sur l’entier 42. Intuitivement, ce
programme peut terminer même si l’évaluation de son argument ne termine pas, puisque cet
argument n’est pas utilisé. Par contre, on pourra vérifier que fun x → if x = x then 42 else 13
a pour interprétation une application f telle que f (⊥nat ) = ⊥nat — on notera aussi que cette
application ne prend jamais la valeur 13, car Jx = xKE ∈ {tt, ⊥bool } pour tout E.
Soit τ un type. On dit qu’un élément e ∈ Jτ K est calculable quand il existe un programme
p : τ tel que JpK = e. Par extension, on dira qu’une application f : Jτ1 K → Jτ2 K est calculable
quand il existe p : τ1 ⇒ τ2 tel que JpK = f .
6
Question 2.5.
a. Montrer que tous les éléments de Junit ⇒ unitK sont calculables.
b. On admet que l’ensemble des programmes est dénombrable. Montrer qu’il existe des
éléments non calculables dans Jnat ⇒ unitK.
Question 2.6. Donner un programme unit and : unit ⇒ unit ⇒ unit tel que, pour tout
environnement E et pour tous p : unit et q : unit,
Question 2.7.
a. Soit x une variable telle que t(x) = (bool ⇒ unit). On pose :
def
p = fun x → (x tt) ku (x ff)
7
Partie III
Question 3.1. Soit τ un type. Montrer que Jτ K est à la fois un ouvert calculatoire et un
fermé calculatoire de Jτ K.
Question 3.5. On souhaite montrer qu’une union infinie calculable d’ouverts calculatoires
est encore un ouvert calculatoire, dans le sens suivant. Soient (Ui )i∈N une suite de parties de
Jτ K et p : nat ⇒ τ ⇒ unit un programme tels que, pour tout i ∈ N, Jp iK est la fonction
caractéristique de Ui . Montrer que ∪i∈N Ui est un ouvert calculatoire de Jτ K. Indication : on
pourra construire un programme intermédiaire rec q : nat ⇒ τ ⇒ unit dont on montrera qu’il
satisfait, pour tous k ∈ N et e ∈ Jτ K, Jrec qK(k)(e) = uu ssi e ∈ ∪i≥k Ui .
8
Un sous-ensemble U ⊆ Jτ K est calculatoirement compact dans Jτ K s’il existe un pro-
gramme ∀U : (τ ⇒ unit) ⇒ unit tel que, pour tout programme p : τ ⇒ unit,
Par exemple, l’ensemble E = {40, 12} est calculatoirement compact dans JnatK, comme en
témoigne le programme ∀E = fun f → (f 40) &u (f 12), où f est une variable quelconque de
type nat ⇒ unit.
Question 3.7. Soit U ⊆ N. Montrer que U est calculatoirement compact dans JnatK ssi U
est fini. Indication : on pourra écrire un certain programme p : nat ⇒ unit comme la borne
supérieure d’une suite croissante.
9
Partie IV
Étant donnée une suite de booléens s = (si )i∈N ∈ BN on définit fs ∈ Jnat ⇒ boolK par
fs (⊥nat ) = ⊥bool et fs (i) = si pour tout i ∈ N. On définit l’espace de Cantor C comme
l’ensemble de ces applications :
def
C = {fs | s ∈ BN }
L’objectif de cette partie est de montrer que C est calculatoirement compact dans Jnat ⇒ boolK.
On remarquera que C contient des éléments non calculables. Réciproquement, il existe des
éléments calculables de Jnat ⇒ boolK qui ne sont pas dans C.
Dans la suite de l’énoncé, les programmes de type nat ⇒ bool seront représentés par la
lettre q. Les programmes de type (nat ⇒ bool) ⇒ unit seront représentés par la lettre p.
Pour b ∈ B et s ∈ BN on note b::s la suite s0 ∈ BN telle que s00 = b et s0n+1 = sn pour
tout n ∈ N. Pour tout programme q : nat ⇒ bool on définit l’opération analogue avec la même
notation, où x est une variable de type nat :
def
b::q = fun x → if x = 0 then b else q (x − 1)
Enfin, pour p : (nat ⇒ bool) ⇒ unit on définit, en prenant une variable y de type nat ⇒ bool :
def
p/b = fun y → p (b::y)
Pour s ∈ BN et k ∈ N on note fs<k l’application f 0 ∈ Jnat ⇒ boolK telle que f 0 (i) = si pour
tout i tel que 0 ≤ i < k, et f 0 (e) = ⊥bool sinon.
Question 4.1. Soient un programme p : (nat ⇒ bool) ⇒ unit et s ∈ BN tels que JpK(fs ) = uu.
Montrer qu’il existe un entier k tel que JpK(fs<k ) = uu. Dans la suite du sujet, on notera k(s, p)
le plus petit entier satisfaisant cette propriété.
Question 4.3. Soit p : (nat ⇒ bool) ⇒ unit tel que, pour tout f ∈ C, JpK(f ) = uu. On
définit :
def
K(p) = {k(s, p) | s ∈ BN }
a. Soit s ∈ BN . On pose i = k(s, p). Montrer que
b. Montrer que, si K(p) est non borné, alors il existe b ∈ B tel que K(p/b) est encore non
borné.
c. En déduire que K(p) est borné.
La borne supérieure de K(p) sera notée |p| et appelée module d’uniforme continuité de p.
10
Question 4.4. Soit p : (nat ⇒ bool) ⇒ unit tel que, pour tout f ∈ C, JpK(f ) = uu.
a. Soient b ∈ B et s ∈ BN tels que k(b::s, p) > 0. Montrer que k(s, p/b) < k(b::s, p).
b. Montrer que, si |p| > 0, on a |p/b| < |p| pour tout b ∈ B.
Question 4.5. Montrer que C est calculatoirement compact dans Jnat ⇒ boolK.
11
12
def
JcKE = c pour tout c ∈ N ∪ B ∪ {uu}
def
JxKE = E(x)
⊥bool si Jp1 KE = ⊥ ou Jp2 KE = ⊥
def
Jp1 = p2 KE = tt si Jp1 KE 6= ⊥, Jp2 KE 6= ⊥ et Jp1 KE = Jp2 KE
ff si Jp1 KE 6= ⊥, Jp2 KE 6= ⊥ et Jp1 KE 6= Jp2 KE
Jp1 KE si Jp0 KE = tt
def
Jif p0 then p1 else p2 KE = Jp2 KE si Jp0 KE = ff
⊥τ si Jp0 KE = ⊥, où τ = t(p1 ) = t(p2 )
si Jp1 KE = ⊥ ou Jp2 KE = ⊥
def ⊥nat
Jp1 + p2 KE =
Jp1 KE + Jp2 KE si Jp1 KE ∈ N et Jp2 KE ∈ N
si Jp1 KE = ⊥ ou Jp2 KE = ⊥
def ⊥nat
Jp1 × p2 KE =
Jp1 KE × Jp2 KE si Jp1 KE ∈ N et Jp2 KE ∈ N
si Jp1 KE = ⊥ ou Jp2 KE = ⊥
def ⊥nat
Jp1 − p2 KE =
max(0, Jp1 K − Jp2 K ) si Jp1 KE ∈ N et Jp2 KE ∈ N
E E
si Jp0 KE = ⊥
def ⊥nat
Jp0 /2KE =
bJp0 K /2c si Jp0 KE ∈ N
E
def
Jp1 p2 KE = Jp1 KE (Jp2 KE )
Jfun x → p0 KE est l’application f : Jt(x)K → Jt(p0 )K telle que f (e) = Jp0 KE[x7→e] pour tout e ∈ Jt(x)K
def
Jrec p0 KE supi∈N (Jp0 KE )i (⊥τ )
= où τ = t(rec p0 )
Jτ K
13