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 qui permet de déterminer, pour tout programme , si termine sur toute suite de bits.
Notations et définitions
On note l'ensemble des parties d'un ensemble .
On note l'union disjointe des ensembles et .
Soit un ensemble et un ensemble de sous-ensembles de , c'est à dire . On note l'intersection de tous les ensembles de et l'union de tous les ensembles de . Quand est vide, et .
La partie entière inférieure est notée . En particulier, si , alors est le plus grand entier tel que .
Un ordre partiel ( ) est un ensemble équipé d'une relation binaire qui est réflexive, transitive et antisymétrique. Dans ce contexte, on notera l'ordre strict induit par , dont on rappelle la définition : quand et .
Soit un ordre partiel et une suite d'éléments de . On dit que est un majorant de la suite quand pour tout . On dit que est une borne supérieure de la suite quand est un majorant de la suite et qu'on a pour tout majorant 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 , une suite croissante de est une suite d'éléments de telle que, pour tout . On dit que ( ) est un ordre partiel complet quand est un ordre partiel et que toute suite croissante d'éléments de admet une borne supérieure, notée .
Étant donnés deux ordres partiels complets et , une application est dite croissante quand, pour tous et tels que , on a . L'application est dite continue quand elle est croissante et que, pour toute suite croissante de , on a .
Définissons dans un premier temps ( ) pour les types de base. À cet effet, on se donne des constantes distinctes , 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 unit, nat, bool on définit enfin comme suit : pour tous ssi ou . Il est clair que cela définit des ordres partiels; inutile de le vérifier dans les réponses aux questions. L'ordre partiel peut être représenté graphiquement comme suit :
Question 1.1. On souhaite vérifier que ( ) est un ordre partiel complet :
a. Caractériser les suites croissantes de ( nat ).
b. En déduire que toute suite croissante de ( ) admet une borne supérieure.
On admet que ( unit ) et ( bool ) sont aussi des ordres partiels complets.
Étant donnés deux types et pour lesquels on suppose avoir construit les ordres partiels complets ( ) et ( ), on définit comme l'ensemble des applications continues de dans :
On définit ensuite la relation en posant, pour tous :
Enfin, on définit comme la fonction telle que pour tout .
On admettra que ( ) est un ordre partiel, et que est son plus petit élément.
Question 1.2. On considère dans cette question le cas particulier où nat et unit.
a. Montrer que toute application croissante nat unit est continue.
b. Combien y a-t-il d'éléments nat unit tels que ?
c. Donner, sans justifier, une suite strictement croissante de [nat unit], c'est à dire une suite telle que pour tout .
Question 1.3. Soient et des types tels que ( ) et ( ) sont des ordres partiels complets.
a. Soit une suite croissante de . Pour tout est une suite croissante de ( ) par définition de , et admet donc une borne supérieure.
Montrer que l'application définie par est continue.
b. Montrer que ( , ) 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é et dont les éléments seront représentés par les lettres et dans la suite. Les programmes, qui seront représentés par les lettres et , sont des expressions syntaxiques données par la grammaire suivante, où 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 est un programme ; tout est un programme; si et sont des programmes alors if then else 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 des variables dans les types. Nous supposerons que pour tout type il existe une infinité de variables telles que . La relation de typage exprimant qu'un programme est de type , notée , est ensuite définie par les équivalences suivantes, pour tous programmes , pour tout type , et pour tous et :
On pourra par exemple vérifier que fun est faux quel que soit . Ou encore, que (fun fun nat nat est vrai à condition que nat.
Question 2.1. Soient et des variables quelconques, et un type. Indiquer, sans justifier, sous quelles conditions sur et on a (fun if then else ) : .
On considère désormais uniquement des programmes bien typés, c'est à dire pour lesquels il existe tel que . Quand est un programme bien typé, on note son unique type.
Pour donner un sens aux variables présentes dans un programme, on introduit la notion suivante : un environnement est une application telle qu'on a pour tout . Si est un environnement et est l'environnement tel que et pour tout .
L'interprétation d'un programme dans un environnement , noté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 pour . On admettra que, pour tout programme (bien typé) et pour tout environnement , l'interprétation de dans est bien définie et appartient à :
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 , de type nat nat si et nat. Par définition de l'interprétation, fun est l'application définie par fun pour tout nat . Si ou , on vérifie fun . Sinon, et , et l'on a fun .
On remarque dans cet exemple que la valeur de sur les variables autres que n'entre pas en jeu dans l'interprétation du programme. Cela correspond intuitivement au fait que seule la variable fait référence à un objet extérieur au programme - on dit que cette variable est libre. À l'inverse, la variable utilisée dans le sous-programme est une référence interne au programme, correspondant à l'argument de la fonction définie - l'occurrence de dans est dite liée par la construction fun englobante.
On dit que l'interprétation d'un programme est indépendante de l'environnement quand quels que soient et . On notera simplement l'interprétation d'un tel programme dans un environnement arbitraire. Dans la suite du sujet, si on demande au candidat un programme tel que 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 telle que nat.
a. On considère le programme fun , de type nat bool. Caractériser en justifiant par le calcul de .
b. On définit l'application par si est pair, sinon. Donner un programme : nat nat tel que coïncide avec sur . On utilisera directement plutôt que de recopier sa définition.
On s'intéresse maintenant à l'interprétation des programmes de la forme rec , permettant des définitions récursives de façon analogue au let rec . . . d'OCaml. Un programme rec est de type quand . Puisque est une application continue de dans lui-même, la suite est croissante : on a en effet par minimalité de , puis par croissance de , et ainsi de suite. Toute suite croissante admettant une borne supérieure dans l'ordre partiel complet ( ), l'interprétation rec est bien définie.
Question 2.3. Soient des variables telles que nat et (nat nat). On pose :
On pourra vérifier que est bien typé, de type (nat nat (nat nat) .
a. Soit nat nat et nat . Exprimer en fonction de et .
b. Calculer pour tous et nat .
c. En déduire que pour tout , et donner la valeur de .
Question 2.4. On reprend la définition de de la question 2.2. La conjecture de Collatz énonce que, pour tout , il existe tel que . Autrement dit, la suite des itérées de finirait toujours par atteindre 1, quelle que soit la valeur de départ non nulle.
a. Donner un programme (nat unit) (nat unit) tel que, pour tous et uu ssi il existe tel que . On utilisera directement le programme de la question 2.2 sans en recopier la définition.
b. Donner un programme : nat unit tel que, pour tout uu ssi il existe tel que . Justifier.
Soient un type et une variable de type . On définit :
On vérifie aisément que DIV et DIV . Intuitivement, DIV est défini récursivement comme un objet é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 tels que pour tout . Si est un type de base, l'évaluation de ( ) ne termine donc pas, quel que soit . Réciproquement, il existe des programmes tels que ( ) termine toujours, même quand . Par exemple, si est une variable de type nat, le programme (fun ) : 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 if then 42 else 13 a pour interprétation une application telle que - on notera aussi que cette application ne prend jamais la valeur 13, car pour tout .
Soit un type. On dit qu'un élément est calculable quand il existe un programme tel que . Par extension, on dira qu'une application est calculable quand il existe tel que .
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 et pour tous : unit et : unit,
Par la suite, on écrira simplement au lieu de unit_and .
On considère enfin l'opérateur (- -) de disjonction sur unit. La définition de 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 une variable telle que (bool unit). On pose:
Caractériser bool unit .
b. Soient , et des variables telles que (nat unit) et nat. On pose :
Caractériser, sans justifier, .
Partie III
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 unit est la fonction caractéristique de quand, pour tout uu ssi . Un ensemble est un ouvert calculatoire de quand la fonction caractéristique de est calculable. Un ensemble est un fermé calculatoire de quand son complémentaire dans est un ouvert calculatoire de .
Par exemple, nat est un ouvert calculatoire de nat . En effet, sa fonction caractéristique est l'interprétation du programme fun if then DIV 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, un ouvert calculatoire de , et une application calculable. Montrer que la pré-image de par est un ouvert calculatoire de .
Question 3.4. On considère un type quelconque. Utiliser les opérateurs (- ) et ( ) 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 et des types quelconques. On pose unit . Pour tous et , 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 une suite de parties de et nat unit un programme tels que, pour tout est la fonction caractéristique de . Montrer que est un ouvert calculatoire de . Indication : on pourra construire un programme intermédiaire rec : nat unit dont on montrera qu'il satisfait, pour tous et , uu ssi .
Un sous-ensemble est calculatoirement compact dans s'il existe un programme unit unit tel que, pour tout programme unit,
Par exemple, l'ensemble est calculatoirement compact dans nat , comme en témoigne le programme fun , où est une variable quelconque de type nat unit.
Question 3.6. Soit un type.
a. Montrer que est calculatoirement compact dans .
b. Soit tel que . Montrer que est calculatoirement compact dans .
c. En déduire que tout fermé calculatoire de est calculatoirement compact dans .
Question 3.7. Soit . Montrer que est calculatoirement compact dans nat ssi est fini. Indication : on pourra écrire un certain programme : nat unit comme la borne supérieure d'une suite croissante.
Partie IV
Étant donnée une suite de booléens on définit nat bool par et pour tout . On définit l'espace de Cantor comme l'ensemble de ces applications :
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 . Les programmes de type (nat bool) unit seront représentés par la lettre .
Pour et on note la suite telle que et pour tout . Pour tout programme : nat bool on définit l'opération analogue avec la même notation, où est une variable de type nat :
Enfin, pour nat bool unit on définit, en prenant une variable de type nat bool :
Pour et on note l'application nat bool telle que pour tout tel que , et sinon.
Question 4.1. Soient un programme (nat bool) unit et tels que uu. Montrer qu'il existe un entier tel que uu. Dans la suite du sujet, on notera le plus petit entier satisfaisant cette propriété.
Question 4.2. Soient un programme (nat bool) unit, et tels que uu. Montrer, pour tout , que .
Question 4.3. Soit nat bool unit tel que, pour tout uu. On définit :
a. Soit . On pose . Montrer que
b. Montrer que, si est non borné, alors il existe tel que est encore non borné.
c. En déduire que est borné.
La borne supérieure de sera notée et appelée module d'uniforme continuité de .
Question 4.4. Soit nat bool unit tel que, pour tout uu.
a. Soient et tels que . Montrer que .
b. Montrer que, si , on a pour tout .
Question 4.5. Montrer que est calculatoirement compact dans nat bool .
Figure 1 - Définition de l'interprétation des programmes.
ENS Informatique Fondamentale (Maths Info) MP 2020 - Version Web LaTeX | WikiPrépa | WikiPrépa
