VENDREDI 24 AVRIL 2020-14h00-18h00
FILIERE MP
ÉPREUVE INFO-MATHS (ULCR)
Durée : 4 heures
L'utilisation des calculatrices n'est pas autorisée pour cette épreuve
Programmation fonctionnelle, sémantique et topologie
Le sujet comporte 13 pages, numérotées de 1 à 13 .Pour le traitement des trois dernières parties du sujet, il est recommandé de détacher la page 13 afin que son contenu soit facilement consultable.
Dans ce sujet, on considère un langage de programmation fonctionnelle minimaliste, proche mais différent d'OCaml. On définit rigoureusement la sémantique (signification) des programmes au moyen d'objets mathématiques usuels (e.g. entiers, fonctions, ordres partiels) et on l'utilise pour concevoir et prouver des programmes.
La première partie introduit un système de types simples, ainsi que la notion d'ordre partiel complet. On y construit, pour chaque type, un certain ordre partiel complet.
La deuxième partie introduit le langage de programmation, et définit l'interprétation des programmes.
La troisième partie étudie des notions d'inspiration topologique issues de notre langage de programmation : on y parlera d'ouverts, de fermés et de compacts calculatoires.
La quatrième partie porte sur la preuve de compacité de l'espace de Cantor : on y démontrera qu'il existe un programme p qui permet de déterminer, pour tout programme q, si q termine sur toute suite de bits.
Notations et définitions
On note 𝒫(E) l'ensemble des parties d'un ensemble E.
On note E⊎F l'union disjointe des ensembles E et F.
Soit E un ensemble et F un ensemble de sous-ensembles de E, c'est à dire F ⊆ 𝒫(E). On note ⋂F l'intersection de tous les ensembles 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 ⌊_⌋. En particulier, si n ∈ ℕ, alors ⌊n/2⌋ est le plus grand entier m ∈ ℕ 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 ≠ y.
Soit (E, ≤ _E) un ordre partiel et (x_i)_(i ∈ ℕ) une suite d'éléments de E. On dit que y ∈ E est un majorant de la suite quand x_i ≤ _E y pour tout i ∈ ℕ. 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.
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é ( [ [τ] ], ≤ _τ ). Dans la partie suivante, les programmes de type τ seront interprétés comme des éléments de [ [τ] ].
Étant donné un ordre partiel (A, ≤ _A), une suite croissante de A est une suite (a_i)_(i ∈ ℕ) d'éléments de A telle que, pour tout i ∈ ℕ, a_i ≤ _A a_(i + 1). On dit que ( A, ≤ _A ) est un ordre partiel complet quand (A, ≤ _A) est un ordre partiel et que toute suite croissante (a_i)_(i ∈ ℕ) d'éléments de A admet une borne supérieure, notée sup_(i ∈ ℕ)^A a_i.
Étant donnés deux ordres partiels complets (A, ≤ _A) et (B, ≤ _B), une application f : A → B est dite croissante quand, pour tous a_1 ∈ A et a_2 ∈ A tels que a_1 ≤ _A a_2, on a f(a_1) ≤ _B f(a_2). L'application f est dite continue quand elle est croissante et que, pour toute suite croissante (a_i)_(i ∈ ℕ) de A, on a f(sup_(i ∈ ℕ)^A a_i) = sup_(i ∈ ℕ)^B f(a_i).
Définissons dans un premier temps ( [ [τ] ], ≤ _τ ) 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 :
Pour chaque type de base b ∈ { unit, nat, bool } on définit enfin ≤ _b comme suit : pour tous e_1, e_2 ∈ [ [b] ], e_1 ≤ _b e_2 ssi e_1 = e_2 ou e_1 = ⊥ _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 :
Question 1.1. On souhaite vérifier que ( [ [nat] ], ≤ _(nat) ) est un ordre partiel complet :
a. Caractériser les suites croissantes de ( [ [ nat ] ], ≤ _(nat) ).
b. En déduire que toute suite croissante de ( [ [nat] ], ≤ _(nat) ) admet une borne supérieure.
On admet que ( [ [ unit ] ], ≤ _(unit) ) et ( [ [ bool ] ], ≤ _(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 ( [ [τ_1] ], ≤ _(τ_1) ) et ( [ [τ_2] ], ≤ _(τ_2) ), on définit [ [τ_1 ⇒ τ_2] ] comme l'ensemble des applications continues de [ [τ_1] ] dans [ [τ_2] ] :
On définit ensuite la relation ≤ _(τ_1 ⇒ τ_2) en posant, pour tous f, g ∈ [ [τ_1 ⇒ τ_2] ] :
f ≤ τ_(τ_1 ⇒ τ_2)g ssi f(e) ≤ τ_(τ_2)g(e) pour tout e ∈ [ [τ_1] ]
Enfin, on définit ⊥ _(τ_1 ⇒ τ_2) comme la fonction f : [ [τ_1] ] → [ [τ_2] ] telle que f(e) = ⊥ _(τ_2) pour tout e ∈ [ [τ_1] ].
On admettra que ( [ [τ_1 ⇒ τ_2] ], ≤ τ_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 : [ [ nat ] ] → [ [ unit ] ] est continue.
b. Combien y a-t-il d'éléments f ∈ [ [ nat ⇒ unit ] ] tels que f(⊥ _(nat)) ≠ ⊥ _(unit) ?
c. Donner, sans justifier, une suite strictement croissante de [nat ⇒ unit], c'est à dire une suite (f_i)_(i ∈ ℕ) telle que f_i < _(nat ⇒ unit)f_(i + 1) pour tout i ∈ ℕ.
Question 1.3. Soient τ_1 et τ_2 des types tels que ( [ [τ_1] ], ≤ τ_(τ_1) ) et ( [ [τ_2] ], ≤ τ_2 ) sont des ordres partiels complets.
a. Soit (f_i)_(i ∈ ℕ) une suite croissante de ([ [τ_1 ⇒ τ_2] ], ≤ _(τ_1 ⇒ τ_2)). Pour tout e ∈ [ [τ_1] ], (f_i(e))_(i ∈ ℕ) est une suite croissante de ( [ [τ_2] ], ≤ _(τ_2) ) par définition de ≤ _(τ_1 ⇒ τ_2), et admet donc une borne supérieure.
Montrer que l'application f^′ : [ [τ_1] ] → [ [τ_2] ] définie par f^′(e) = sup_(i ∈ ℕ)^([ [τ_2] ])f_i(e) est continue.
b. Montrer que ( [ [τ_1 ⇒ τ_2] ], ≤ _(τ_1 ⇒ τ_2) ) est un ordre partiel complet.
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 ( [ [τ] ], ≤ _τ ).
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 :
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 ∈ ℕ est un programme ; tout x ∈ X est un programme; si p_0, p_1 et p_2 sont des programmes alors if p_0 then p_1 else p_2 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 p_0, p_1, p_2, pour tout type τ, et pour tous n ∈ ℕ et x ∈ X :
uu : τ, ⇔ τ = unit; tt : τ, ⇔ τ = bool; ff : τ, ⇔ τ = bool; n : τ, ⇔ τ = nat; (if p_0 then p_1 else p_2) : τ, ⇔ p_0 : bool, p_1 : τ et p_2 : τ; (p_1 = p_2) : τ, ⇔ τ = bool et il existe τ^′ ∈ { unit, nat, bool } tel que p_1 : τ^′ et p_2 : τ^′; p_1 + p_2 : τ, ⇔ τ = nat, p_1 : nat et p_2 : nat; p_1 − p_2 : τ, ⇔ τ = nat, p_1 : nat et p_2 : nat; p_1 × p_2 : τ, ⇔ τ = nat, p_1 : nat et p_2 : nat; p_0/2 : τ, ⇔ τ = nat, p_0 : nat; x : τ, ⇔ t(x) = τ; (fun x → p_0) : τ, ⇔ il existe τ^′ tel que p_0 : τ^′ et τ = (t(x) ⇒ τ^′); (p_1 p_2) : τ, ⇔ il existe τ^′ tel que p_1 : (τ^′ ⇒ τ) et p_2 : τ^′; (rec p_0) : τ, ⇔ p_0 : (τ ⇒ τ); (p_1‖_u p_2) : τ, ⇔ τ = unit, p_1 : unit et p_2 : 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.
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.
Pour donner un sens aux variables présentes dans un programme, on introduit la notion suivante : un environnement est une application E : X → ⋃_τ[ [τ] ] telle qu'on a E(x) ∈ [ [t(x)] ] pour tout x ∈ X. Si E est un environnement et e ∈ [ [t(x)] ], E[x ↦ e] est l'environnement E^′ tel que E^′(x) = e et E^′(y) = E(y) pour tout y ≠ x.
L'interprétation d'un programme p dans un environnement E, notée [ [p] ]^E, est définie par les clauses de la figure 1, page 13, qu'il n'est pas nécessaire de consulter immédiatement. Dans ces clauses, on écrit simplement [ [p] ]^E=⊥ pour [ [p] ]^E = ⊥ _(t(p)). On admettra que, pour tout programme (bien typé) p et pour tout environnement E, l'interprétation de p dans E est bien définie et appartient à [ [t(p)] ] :
[ [p] ]^E ∈ [ [t(p)] ]
La figure 1 comporte de nombreux cas, dont certains sont assez techniques, et les intuitions (parfois trompeuses) issues de la pratique d'OCaml ne seront pas suffisantes pour en comprendre l'ensemble : le candidat est encouragé à ne pas s'y attarder trop, mais à en approfondir les différents cas au fil de l'énoncé. Pour cela, il est conseillé de séparer la page de la figure du reste de l'énoncé pour la garder à portée de main.
Intuitivement, l'interprétation d'un programme représente le résultat de son évaluation. Pour les types de base, une évaluation n'a jamais pour résultat ⊥, mais cet élément spécial représente au contraire le résultat indéfini d'une évaluation qui ne termine pas.
Considérons par exemple le programme fun x → x + y, de type nat ⇒ nat si x, y ∈ X et t(x) = t(y) = nat. Par définition de l'interprétation, [ [ fun x → x + y] ]^E est l'application définie par [ [ fun x → x + y] ]^E(e) = [ [x + y] ]^(E[x ↦ e]) pour tout e ∈ [ [ nat ] ]. Si e = ⊥ _(nat) ou E(y) = ⊥ _(nat), on vérifie [ [ fun x → x + y] ]^E(e) = ⊥ _(nat). Sinon, e ∈ ℕ et E(y) ∈ ℕ, et l'on a [ [ fun x → x + y] ]^E(e) = e + E(y).
On remarque dans cet exemple que la valeur de E sur les variables autres que y n'entre pas en jeu dans l'interprétation du programme. Cela correspond intuitivement au fait que seule la variable y fait référence à un objet extérieur au programme - on dit que cette variable est libre. À l'inverse, la variable x utilisée dans le sous-programme x + y est une référence interne au programme, correspondant à l'argument de la fonction définie - l'occurrence de x dans x + y est dite liée par la construction fun x → … englobante.
On dit que l'interprétation d'un programme q est indépendante de l'environnement quand [ [q] ]^E = [ [q] ]^(E^′) quels que soient E et E^′. On notera simplement [ [q] ] l'interprétation d'un tel programme dans un environnement arbitraire. Dans la suite du sujet, si on demande au candidat un programme q tel que [ [q] ] satisfasse une certaine propriété, on attend un programme dont l'interprétation soit indépendante de l'environnement - ce qui est garanti si le programme est sans variable libre.
Question 2.2. Soit une variable x telle que t(x) = nat.
a. On considère le programme p_e = ( fun x → ((2 × (x/2)) = x)), de type nat ⇒ bool. Caractériser {n ∈ ℕ|[ [p_e] ](n) = tt} en justifiant par le calcul de [ [p_e] ].
b. On définit l'application f_c : ℕ → ℕ par f_c(n) = n/2 si n est pair, f_c(n) = 3n + 1 sinon. Donner un programme p_c : nat ⇒ nat tel que [ [p_c] ] coïncide avec f_c sur ℕ. On utilisera directement p_e plutôt que de recopier sa définition.
On s'intéresse maintenant à l'interprétation des programmes de la forme rec p_0, permettant des définitions récursives de façon analogue au let rec . . . d'OCaml. Un programme rec p_0 est de type τ quand p_0 : τ ⇒ τ. Puisque [ [p_0] ]^E est une application continue de [ [τ] ] dans lui-même, la suite (([ [p_0] ]^E)^i(⊥ _τ))_(i ∈ ℕ) est croissante : on a en effet ⊥ _τ ≤ _τ[ [p_0] ]^E(⊥ _τ) par minimalité de ⊥ _τ, puis [ [p_0] ]^E(⊥ _τ) ≤ _τ([ [p_0] ]^E)^2(⊥ _τ) par croissance de [ [p_0] ]^E, et ainsi de suite. Toute suite croissante admettant une borne supérieure dans l'ordre partiel complet ( [ [τ] ], ≤ _τ ), l'interprétation [ [ rec p_0] ]^E 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 :
p = ^(def) 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 ∈ [ [ nat ⇒ nat ] ] et e ∈ [ [ nat ] ]. Exprimer [ [p] ](f)(e) en fonction de e et f.
b. Calculer [ [p] ]^(i + 1)(⊥ _(nat ⇒ nat))(e) pour tous i ∈ ℕ et e ∈ [ [ nat ] ].
c. En déduire que [ [recp] ](k) = k! pour tout k ∈ ℕ, et donner la valeur de [ [recp] ](⊥ _(nat)).
Question 2.4. On reprend la définition de f_c de la question 2.2. La conjecture de Collatz énonce que, pour tout n ∈ ℕ^∗, il existe i ∈ ℕ tel que f_c^i(n) = 1. Autrement dit, la suite des itérées de f_c finirait toujours par atteindre 1, quelle que soit la valeur de départ non nulle.
a. Donner un programme q : (nat ⇒ unit) ⇒ (nat ⇒ unit) tel que, pour tous i ∈ ℕ et n ∈ ℕ^∗, [ [q] ]^(i + 1)(⊥ _(nat ⇒ unit))(n) = uu ssi il existe k ≤ i tel que f_c^k(n) = 1. On utilisera directement le programme p_c de la question 2.2 sans en recopier la définition.
b. Donner un programme p : nat ⇒ unit tel que, pour tout n ∈ ℕ^∗, [ [p] ](n) = uu ssi il existe k ∈ ℕ tel que f_c^k(n) = 1. Justifier.
Soient τ un type et x une variable de type τ. On définit :
DIV_τ = ^(def)rec(fun x → x)
On vérifie aisément que DIV _τ : τ et [ [ DIV _τ] ] = ⊥ _τ. 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 [ [p] ](e) = ⊥ _(τ_2) pour tout e ∈ [ [τ_1] ]. Si τ_2 est un type de base, l'évaluation de ( pq ) ne termine donc pas, quel que soit q : τ_1. Réciproquement, il existe des programmes p : τ_1 ⇒ τ_2 tels que ( pq ) termine toujours, même quand [ [q] ] = ⊥ _(τ_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 [nat] 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 [ [x = x] ]^E ∈ {tt, ⊥ _(bool)} pour tout E.
Soit τ un type. On dit qu'un élément e ∈ [ [τ] ] est calculable quand il existe un programme p : τ tel que [ [p] ] = e. Par extension, on dira qu'une application f : [ [τ_1] ] → [ [τ_2] ] est calculable quand il existe p : τ_1 ⇒ τ_2 tel que [ [p] ] = f.
Question 2.5.
a. Montrer que tous les éléments de 【unit ⇒ unit】 sont calculables.
b. On admet que l'ensemble des programmes est dénombrable. Montrer qu'il existe des éléments non calculables dans [ [ nat ⇒ unit ] ].
Dans la suite du sujet, nous chercherons à reconnaître certains éléments de [ [τ] ] au moyen de programmes de type τ ⇒ unit : ces programmes devront renvoyer uu quand un élément est reconnu, et ne pas terminer sinon. Dans ce cadre, des notions de conjonction et de disjonction sur le type unit seront utiles.
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,
Par la suite, on écrira simplement p&_u q au lieu de unit_and pq.
On considère enfin l'opérateur (- ‖_u-) de disjonction sur unit. La définition de [ [p_1‖_u p_2] ]^E en figure 1 indique que ce programme peut terminer (renvoyer uu) dès que l'un de ses deux sous-programmes termine. Intuitivement, on peut penser que les deux sous-programmes sont évalués en parallèle, et que uu est renvoyé dès que l'une de ces deux évaluations termine.
Question 2.7.
a. Soit x une variable telle que t(x) = (bool ⇒ unit). On pose:
p = ^(def) fun x → ((xtt)‖_u(xff))
Caractériser {f ∈ [ [ bool ⇒ unit ] ]|[ [p] ](f) = uu}.
b. Soient x, p^′, et n des variables telles que t(x) = t(p^′) = (nat ⇒ unit) et t(n) = nat. On pose :
p = ^(def) fun x → ((rec(fun p^′ → fun n → xn‖_u p^′(n + 1)))0)
Il existe de nombreux liens entre topologie et sémantique des langages de programmation. Nous nous proposons ici de dériver des notions topologiques à partir de notre langage de programmation.
On dit que l'application f : [ [τ] ] → [ [ unit ] ] est la fonction caractéristique de U ⊆ [ [τ] ] quand, pour tout e ∈ [ [τ] ], f(e) = uu ssi e ∈ U. Un ensemble U ⊆ [ [τ] ] est un ouvert calculatoire de [ [τ] ] quand la fonction caractéristique de U est calculable. Un ensemble U ⊆ [ [τ] ] est un fermé calculatoire de [ [τ] ] quand son complémentaire dans [ [τ] ] est un ouvert calculatoire de [ [τ] ].
Par exemple, [ [ nat ] ]∖{ ⊥ _(nat), 13} est un ouvert calculatoire de [ [ nat ] ]. En effet, sa fonction caractéristique est l'interprétation du programme fun x → if x = 13 then DIV _(unit) else uu.
Question 3.1. Soit τ un type. Montrer que [ [τ] ] est à la fois un ouvert calculatoire et un fermé calculatoire de [ [τ] ].
Question 3.2. Quels sont les ouverts calculatoires de 【unit】?
Question 3.3. Soient τ et τ^′ des types, U un ouvert calculatoire de [ [τ^′] ], et f : [ [τ] ] → [ [τ^′] ] une application calculable. Montrer que la pré-image f^(− 1)(U) de U par f est un ouvert calculatoire de [ [τ] ].
Question 3.4. On considère un type τ quelconque. Utiliser les opérateurs (- ‖_(u_−)) et ( &_(u_−)) pour montrer les propriétés suivantes.
a. L'union de deux ouverts calculatoires de [ [τ] ] est encore un ouvert calculatoire de [ [τ] ].
b. L'intersection de deux ouverts calculatoires de [ [τ] ] est encore un ouvert calculatoire de [ [τ] ].
Pour la prochaine question on pourra utiliser le résultat suivant sans le justifier :
Propriété A. Soient τ_1 et τ_2 des types quelconques. On pose τ = (τ_1 ⇒ τ_2 ⇒ unit ). Pour tous p : τ ⇒ τ, e_1 ∈ [ [τ_1] ] et e_2 ∈ [ [τ_2] ], on a
Question 3.5. On souhaite montrer qu'une union infinie calculable d'ouverts calculatoires est encore un ouvert calculatoire, dans le sens suivant. Soient (U_i)_(i ∈ ℕ) une suite de parties de [ [τ] ] et p : nat ⇒ τ ⇒ unit un programme tels que, pour tout i ∈ ℕ, [ [pi] ] est la fonction caractéristique de U_i. Montrer que ∪ _(i ∈ ℕ)U_i est un ouvert calculatoire de [ [τ] ]. Indication : on pourra construire un programme intermédiaire rec q : nat ⇒ τ ⇒ unit dont on montrera qu'il satisfait, pour tous k ∈ ℕ et e ∈ [ [τ] ], [ [recq] ](k)(e) = uu ssi e ∈ ∪ _(i ≥ k)U_i.
Un sous-ensemble U ⊆ [ [τ] ] est calculatoirement compact dans [ [τ] ] s'il existe un programme ∀_U : (τ ⇒ unit ) ⇒ unit tel que, pour tout programme p : τ ⇒ unit,
[ [∀_U p] ] = uu ssi [ [p] ](e) = uu pour tout e ∈ U.
Par exemple, l'ensemble E = {40, 12} est calculatoirement compact dans [ [ nat ] ], comme en témoigne le programme ∀_E = fun f → (f40)&_u(f12), où f est une variable quelconque de type nat ⇒ unit.
Question 3.6. Soit τ un type.
a. Montrer que ∅ est calculatoirement compact dans [ [τ] ].
b. Soit E ⊆ [ [τ] ] tel que ⊥ _τ ∈ E. Montrer que E est calculatoirement compact dans [ [τ] ].
c. En déduire que tout fermé calculatoire de [ [τ] ] est calculatoirement compact dans [ [τ] ].
Question 3.7. Soit U ⊆ ℕ. Montrer que U est calculatoirement compact dans [ [ nat ] ] ssi U est fini. Indication : on pourra écrire un certain programme p : nat ⇒ unit comme la borne supérieure d'une suite croissante.
Partie IV
Étant donnée une suite de booléens s = (s_i)_(i ∈ ℕ) ∈ 𝔹^ℕ on définit f_s ∈ [ [ nat ⇒ bool ] ] par f_s(⊥ _(nat)) = ⊥ _(bool) et f_s(i) = s_i pour tout i ∈ ℕ. On définit l'espace de Cantor ℂ comme l'ensemble de ces applications :
ℂ = ^(def) {f_s|s ∈ 𝔹^ℕ}
L'objectif de cette partie est de montrer que ℂ est calculatoirement compact dans [ [ nat ⇒ bool ] ]. On remarquera que ℂ contient des éléments non calculables. Réciproquement, il existe des éléments calculables de [ [ nat ⇒ bool ] ] qui ne sont pas dans ℂ.
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 ∈ 𝔹 et s ∈ 𝔹^ℕ on note b : s la suite s^′ ∈ 𝔹^ℕ telle que s_0^′ = b et s_(n + 1)^′ = s_n pour tout 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 :
b : q = ^(def) 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 :
p/b = ^(def) fun y → p(b : y)
Pour s ∈ 𝔹^ℕ et k ∈ ℕ on note f_(s < k) l'application f^′ ∈ [ [ nat ⇒ bool ] ] telle que f^′(i) = s_i pour tout i tel que 0 ≤ i < k, et f^′(e) = ⊥ _(bool) sinon.
Question 4.1. Soient un programme p : (nat ⇒ bool) ⇒ unit et s ∈ 𝔹^ℕ tels que [ [p] ](f_s) = uu. Montrer qu'il existe un entier k tel que [ [p] ](f_(s < k)) = uu. Dans la suite du sujet, on notera k(s, p) le plus petit entier satisfaisant cette propriété.
Question 4.2. Soient un programme p : (nat ⇒ bool) ⇒ unit, b ∈ 𝔹 et s ∈ 𝔹^ℕ tels que [ [p] ](f_(b : s)) = uu. Montrer, pour tout k ∈ ℕ, que [ [p/b] ](f_(s < k)) = [ [p] ](f_(b : s < 1 + k)).
Question 4.3. Soit p : ( nat ⇒ bool ) ⇒ unit tel que, pour tout f ∈ ℂ, [ [p] ](f) = uu. On définit :
K(p) = ^(def) {k(s, p)|s ∈ 𝔹^ℕ}
a. Soit s ∈ 𝔹^ℕ. On pose i = k(s, p). Montrer que
K(((p/s_0)/s_1)…/s_(i − 1)) = {0}
b. Montrer que, si K(p) est non borné, alors il existe 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.
Question 4.4. Soit p : ( nat ⇒ bool ) ⇒ unit tel que, pour tout f ∈ ℂ, [ [p] ](f) = uu.
a. Soient b ∈ 𝔹 et s ∈ 𝔹^ℕ 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 ∈ 𝔹.
Question 4.5. Montrer que ℂ est calculatoirement compact dans [ [ nat ⇒ bool ] ].
[ [c] ]^E = ^(def)c pour tout c ∈ ℕ ∪ 𝔹 ∪ { uu }; [ [x] ]^E = ^(def)E(x); [ [p_1 = p_2] ]^E = ^(def){⊥ _(bool), si [ [p_1] ]^E=⊥ ou [ [p_2] ]^E=⊥; tt, si [ [p_1] ]^E≠⊥, [ [p_2] ]^E≠⊥ et [ [p_1] ]^E = [ [p_2] ]^E; ff, si [ [p_1] ]^E≠⊥, [ [p_2] ]^E≠⊥ et [ [p_1] ]^E ≠ [ [p_2] ]^E; [ [ if p_0 then p_1 else p_2] ]^E = ^(def){[ [p_1] ]^E, si [ [p_0] ]^E = tt; [ [p_2] ]^E, si [ [p_0] ]^E = ff; ⊥ _τ, si [ [p_0] ]^E=⊥, où τ = t(p_1) = t(p_2); [ [p_1 + p_2] ]^E = ^(def){⊥ _(nat), si [ [p_1] ]^E=⊥ ou [ [p_2] ]^E=⊥; [ [p_1] ]^E + [ [p_2] ]^E, si [ [p_1] ]^E ∈ ℕ et [ [p_2] ]^E ∈ ℕ; [ [p_1 × p_2] ]^E = ^(def){⊥ _(nat), si [ [p_1] ]^E=⊥ ou [ [p_2] ]^E=⊥; [ [p_1] ]^E × [ [p_2] ]^E, si [ [p_1] ]^E ∈ ℕ et [ [p_2] ]^E ∈ ℕ; [ [p_1 − p_2] ]^E = ^(def){⊥ _(nat), si [ [p_1] ]^E=⊥ ou [ [p_2] ]^E=⊥; max (0, [ [p_1] ]^E − [ [p_2] ]^E, si [ [p_1] ]^E ∈ ℕ et [ [p_2] ]^E ∈ ℕ; [ [p_0/2] ]^E = ^(def){⊥ _(nat), si [ [p_0] ]^E=⊥; ⌊[ [p_0] ]^E/2⌋, si [ [p_0] ]^E ∈ ℕ; [ [p_1 p_2] ]^E = ^(def)[[ [p_1] ]^E([ [p_2] ]^E); [ [ fun x → p_0] ]^E est l'application f : [ [t(x)] ] → [ [t(p_0)] ] telle que f(e) = [ [p_0] ]^(E[x ↦ e]) pour tout e ∈ [ [t(x)] ]
Figure 1 - Définition de l'interprétation des programmes.
