Corrigé Mines-Ponts 2026 Informatique option MP — Partie 5 (Q23 à Q30) : Des formules de Presburger aux automates : décidabilité

Sujet officiel du concours Mines-Ponts, session 2026, épreuve Informatique option MP. Corrigé rédigé par Ibrahim Alame.

Énoncé

On reprend le type automate et les fonctions des parties 1 et 2 (pow2, decompose, union, determinise, complementaire, intersection). On note $0$ la lettre de $Σ_{n}$ dont toutes les lignes valent $0$ . Pour $L \subseteq Σ_{n}^{*}$ et $i \in [[1, n]]$ ,

$L_{\exists i} = {m \in Σ_{n}^{*} ∣ \exists w \in L, \forall k \in [[1, n]] ∖ {i}, π_{k} (m) = π_{k} (w)}$

(les mots de $L$ dont on a oublié la ligne $i$ ). On dispose de automate_somme n i j k, qui reconnaît $L_{i, j, k} = {m \in Σ_{n}^{*} ∣ v_{i} (m) + v_{j} (m) = v_{k} (m)}$ (pour $n ⩾ 3$ ), et de automate_egalite n i j, qui reconnaît $L_{= i, j} = {m ∣ v_{i} (m) = v_{j} (m)}$ . Pour une formule sous forme simple $φ$ sur les variables $x_{1}, \dots, x_{n}$ , $a^{m}$ est l'assignation qui donne à chaque variable libre $x_{i}$ la valeur $v_{i} (m)$ , et $L_{φ} = {m \in Σ_{n}^{*} ∣ [[φ]]_{a^{m}} est vrai}$ . Types du sujet (les variables sont des entiers) :


type terme = V of int | Plus of int*int

type formule =
    |Existe of int * formule
    |Et of formule * formule
    |Non of formule
    |Egale of terme * terme

Q23. Écrire sans_zero : automate -> automate : même automate, dont les états finaux sont les états permettant d'atteindre un état final par une suite de transitions étiquetées $0$ .
Q24. Pour $L = {ε, (011), (000) (111)}$ , donner $L_{\exists2}$ .
Q25. Écrire automate_existe : automate -> int -> automate reconnaissant $L (A)_{\exists i}$ .
Q26. Expliquer le principe d'un algorithme qui, pour $φ$ sous forme simple et l'indice $n$ de sa plus grande variable, renvoie un automate reconnaissant $L_{φ}$ .
Q27. Le faire tourner à la main, automates intermédiaires compris, sur $φ (x_{2}) := \neg\exists x_{1} .\neg (x_{1} = x_{2})$ .
Q28. Écrire automate_formule : formule -> int -> automate.
Q29. Démontrer la correction de cet algorithme.
Q30. En déduire est_vraie : formule -> int -> bool qui décide si une formule sous forme simple sans variable libre est vraie.

Corrigé

Q23. Un état $q$ doit devenir final s'il existe un chemin $q 0 \dots 0 f$ (de longueur éventuellement nulle) vers un état final $f$ . On construit le graphe des transitions par $0$ renversé, puis on le parcourt en profondeur depuis les états finaux :


let sans_zero a =
  let zero = Array.make a.n 0 in
  (* pred.(q') : les états q tels que q --0--> q' *)
  let pred = Array.make a.k [] in
  for q = 0 to a.k - 1 do
    List.iter (fun q' -> pred.(q') <- q :: pred.(q')) (a.delta q zero)
  done;
  let finaux = Array.copy a.finaux in
  let rec remonte q' =
    List.iter (fun q -> if not finaux.(q) then begin
                          finaux.(q) <- true; remonte q end) pred.(q')
  in
  for q = 0 to a.k - 1 do
    if a.finaux.(q) then remonte q
  done;
  { a with finaux = finaux }

Correction. Un état marqué l'est parce qu'il est final ou parce qu'il a une transition par $0$ vers un état marqué : par récurrence sur l'ordre de marquage, il atteint un état final par des $0$ . Réciproquement, si $q = q_{0}^{'} 0 q_{1}^{'} \to \dots \to q_{r}^{'}$ avec $q_{r}^{'}$ final, on montre par récurrence descendante sur $j$ que $q_{j}^{'}$ est marqué : $q_{r}^{'}$ l'est au départ, et quand $q_{j + 1}^{'}$ est marqué, remonte est appelée sur lui (au départ s'il est final, au moment de son marquage sinon) et marque $q_{j}^{'} \in$ pred.($q_{j+1}'$). Terminaison et coût : remonte n'est appelée qu'une fois par état (un état n'est marqué qu'une fois), d'où un coût $O (k + T_{0})$ , où $T_{0}$ est le nombre de transitions par $0$ , plus $k$ appels à delta. L'automate d'entrée n'est pas modifié (copie de finaux).

Conséquence, utilisée plus loin : $L (sans_zero A) = {m ∣ \exists p \in N, m 0^{p} \in L (A)}$ , car un calcul sur $m$ finit dans un état désormais final si et seulement s'il se prolonge par $0^{p}$ jusqu'à un état final de $A$ . (Exécutée : sur l'automate à quatre états $0010203$ , $3$ final, les quatre états deviennent finaux ; sur un automate de $Σ_{1}$ (lettres écrites comme des bits) reconnaissant le seul mot $0100$ , les mots acceptés de longueur $⩽ 5$ deviennent $01$ , $010$ et $0100$ .)

Q24. On garde les lignes 1 et 3 de chaque mot de $L$ et l'on laisse la ligne 2 libre, avec la même longueur. Le mot vide donne $ε$ ; la lettre $(011)$ donne deux mots ; le mot de longueur $2$ en donne $2 \times 2 = 4$ :

$L_{\exists2} = {ε, (001), (011), (000) (101), (000) (111), (010) (101), (010) (111)} .$

Soit $7$ mots. (Confirmé en appliquant automate_existe de Q25 à un automate reconnaissant $L$ et en énumérant les mots acceptés de longueur $⩽ 3$ .) Ce que le correcteur attend : l'énumération des mots, pas une paraphrase de la définition (rapport du jury MPI sur le sujet jumeau).

100 % gratuit

La suite du corrigé est sur Adloun

Le corrigé rédigé en entier, question par question, et le tuteur pour poser des questions sur ce sujet.

Voir le corrigé complet, gratuitement

Inscription gratuite en 30 secondes (e-mail, nom d'utilisateur, mot de passe, classe ou profil), sans carte bancaire : arrivée directe sur le corrigé.

Toutes les parties de l'épreuve

Corrigé complet gratuit →