From aa60558447744c8cca494641fe3d5cc5aa7895c0 Mon Sep 17 00:00:00 2001 From: Florian Hatat Date: Wed, 29 Apr 2026 09:50:48 +0200 Subject: [PATCH] =?UTF-8?q?Apr=C3=A8s=20relecture?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- 2026-ccmp-mp-option.tex | 85 +++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 42 deletions(-) diff --git a/2026-ccmp-mp-option.tex b/2026-ccmp-mp-option.tex index af9370e..044131e 100644 --- a/2026-ccmp-mp-option.tex +++ b/2026-ccmp-mp-option.tex @@ -77,7 +77,7 @@ Dans tout le sujet, pour tout entier $n$ positif, on notera $\Sigma_n$ l'alphabe \Sigma_2=\left\{\binom{0}{0},\binom{1}{0},\binom{0}{1},\binom{1}{1}\right\} \] -Pour tout entier $i$ dans $\llbracket 1, n \rrbracket$, et pour tout mot $m$ sur $\Sigma_n$, on note $\pi_i(m)$ la projection de $m$ sur la composante $i$, c'est-à-dire, le mot sur $\{0,1\}$ composé du terme à la $i$-ème ligne sur chaque lettre de $m$. +Pour tout entier $i$ dans $\llbracket 1, n \rrbracket$, et pour tout mot $m$ sur $\Sigma_n$, on note $\pi_i(m)$ la projection de $m$ sur la composante $i$, c'est-à-dire, le mot sur $\{0,1\}$ composé du terme à la $i$\ieme{} ligne sur chaque lettre de $m$. Par abus de notation, on s'autorise à confondre la lettre $0$ et $1$ de l'alphabet $\{0,1\}$ avec les entiers $0$ et $1$. Pour tout mot $u$ de taille $|u|=k$ sur $\{0,1\}$ tel que $u=u_0 \ldots u_{k-1}$, on va noter $v(u)$ la valeur suivante : @@ -87,7 +87,7 @@ v(u)=\sum_{j=0}^{k-1} 2^{j} u_j Autrement dit, $v(u)$ est l'entier dont $u$ en est une de ses représentations en binaire telles que le bit de poids faible soit à gauche, donc à l'inverse du sens habituel. -Pour un mot $m$ sur $\Sigma_n$ et un entier $i$ entre 1 et $n$, on note $v_i(m)=v\left(\pi_(m)\right)$. +Pour un mot $m$ sur $\Sigma_n$ et un entier $i$ entre 1 et $n$, on note $v_i(m)=v(\pi_i(m))$. Considérons par exemple le mot $m$ suivant : @@ -148,9 +148,9 @@ On représente en OCaml les lettres de $\Sigma_n$ à l'aide du type \mintinline{ \section{\label{sec:automates-finis}Automates finis sur $\sum_n$} -Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ suivants : +Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ dont les représentations sont données sur les figures \ref{fig:automate-a1} et \ref{fig:automate-a2}. -\begin{figure}[h] +\begin{figure}[ht] \begin{center} \begin{tikzpicture}[initial text = {}] \node[state, initial] (q0) {$q_0$}; @@ -165,10 +165,11 @@ Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ suivants : ; \end{tikzpicture} \caption{Représentation de l'automate $\mathcal{A}_1$} + \label{fig:automate-a1} \end{center} \end{figure} -\begin{figure}[h] +\begin{figure}[ht] \begin{center} \begin{tikzpicture}[initial text = {}] \node[state, initial] (q0) {$q_0$}; @@ -181,31 +182,32 @@ Considérons les automates $\mathcal{A}_1$ et $\mathcal{A}_2$ suivants : ; \end{tikzpicture} \caption{Représentation de l'automate $\mathcal{A}_2$} + \label{fig:automate-a2} \end{center} \end{figure} Soit $E$ l'ensemble des mots $m$ sur $\Sigma_2$ tels que $v_2(m)$ est la plus grande puissance de 2 qui divise $v_1(m)$. \begin{question} - Démontrer que $\mathcal{L}\left(\mathcal{A}_1\right)=E$. + Démontrer que $\mathcal{L}(\mathcal{A}_1)=E$. \end{question} \begin{question} - Montrer que pour tout $m \in \mathcal{L}\left(\mathcal{A}_1\right), v_1(m) \equiv v_2(m)\left[2 \times v_2(m)\right]$. + Montrer que pour tout $m \in \mathcal{L}(\mathcal{A}_1), v_1(m) \equiv v_2(m) \quad [2 \times v_2(m)]$. \end{question} \begin{question} - Décrire sans justifier le langage $\mathcal{L}\left(\mathcal{A}_2\right)$ en donnant une condition nécessaire et suffisante pour qu'un mot $m$ sur $\Sigma_2$ soit dans le langage qui fait intervenir $v_1(m)$ et $v_2(m)$. + Décrire sans justifier le langage $\mathcal{L}(\mathcal{A}_2)$ en donnant une condition nécessaire et suffisante pour qu'un mot $m$ sur $\Sigma_2$ soit dans le langage qui fait intervenir $v_1(m)$ et $v_2(m)$. \end{question} \begin{question} Proposer sans justifier un automate à 3 états qui reconnaît le langage $L$ défini par : \[ - L=\left\{m \in \Sigma_3^{*} \mid v_1(m)=v_3(m) \text { ou } v_2(m)=v_3(m)\right\} + L=\{m \in \Sigma_3^{*} \mid v_1(m)=v_3(m) \text { ou } v_2(m)=v_3(m)\} \] \end{question} -Pour implémenter les automates, on utilise le type automate suivant en OCaml. Un automate sur $\Sigma_n$ à $k$ états est représenté en utilisant un entier différent dans $\llbracket 0, k-1 \rrbracket$ pour chaque état. L'état initial est toujours l'état $0$. +Pour implémenter les automates, on utilise le type \mintinline{ocaml}{automate} suivant en OCaml. Un automate sur $\Sigma_n$ à $k$ états est représenté en utilisant un entier différent dans $\llbracket 0, k-1 \rrbracket$ pour chaque état. L'état initial est toujours l'état $0$. \begin{minted}{ocaml} type automate = { @@ -301,7 +303,7 @@ Dans la formule $\exists x . \forall y .(z=t+y \wedge z=x) \vee(\exists w . z=t+ Pour $\bar{x}$ un vecteur de variables, on notera souvent $\varphi(\bar{x})$ pour signifier que $\bar{x}$ est l'ensemble des variables libres de $\varphi$. Une assignation est une fonction des variables libres de $\varphi$ vers $\mathbb{N}$. Pour $\varphi$ une formule de Presburger et $a$ une assignation de ses variables libres, on note $\llbracket \varphi \rrbracket_a$ la valeur de vérité de $\varphi$ dans l'assignation $a$. -Par exemple, considérons la formule $\varphi_{\leqslant}(x, y):=\exists z . y=x+z$, où : $=$ est un opérateur de définition. Ici, $z$ est une variable liée, et $y$ et $x$ sont des variables libres. Pour un $x$ et un $y$ donnés, cette formule est vraie si et seulement s'il existe un entier $z$ dans $\mathbb{N}$ tel que $y=x+z$, donc si et seulement si $x \leqslant y$. +Par exemple, considérons la formule $\varphi_{\leqslant}(x, y):=\exists z . y=x+z$, où $:=$ est un opérateur de définition. Ici, $z$ est une variable liée, et $y$ et $x$ sont des variables libres. Pour un $x$ et un $y$ donnés, cette formule est vraie si et seulement s'il existe un entier $z$ dans $\mathbb{N}$ tel que $y=x+z$, donc si et seulement si $x \leqslant y$. Pour deux formules $\varphi$ et $\varphi^{\prime}$ ayant le même ensemble de variables libres, on dit qu'elles sont équivalentes, si pour toute assignation de ces variables libres, elles ont la même valeur de vérité. @@ -317,7 +319,7 @@ Pour deux formules $\varphi$ et $\varphi^{\prime}$ ayant le même ensemble de va On dit qu'une formule est sous forme simple si elle vérifie les propriétés suivantes : \begin{enumerate}[(i)] - \item elle ne contient pas les opérateurs $\vee$ et $→$ ; + \item elle ne contient pas les opérateurs $\vee$ et $\rightarrow$ ; \item elle ne contient pas le quantificateur $\forall$ ; \item pour toute sous-formule de la forme $t_1=t_2$, $t_1$ est une variable dans $\mathcal{V}$ et \begin{itemize} @@ -339,7 +341,7 @@ On veut à présent montrer que certaines formules sont des tautologies à l'aid Pour $\varphi$ une formule, $x$ une variable, et $t$ un terme, on note $\varphi[t / x]$ la formule $\varphi$ où toutes les occurrences libres de $x$ ont été remplacées par le terme $t$. Pour pouvoir effectuer des preuves sur des formules plus complexes, on introduit les règles suivantes sur l'égalité pour $x$ une variable, $\varphi$ une formule et $t$ un terme : \begin{mathpar} - \inferrule{}{\Gamma \vdash t=t} \quad {\operatorname{ax}_{=}} + \inferrule{ }{\Gamma \vdash t=t} \quad {\operatorname{ax}_{=}} \and \inferrule{\Gamma, x=t \vdash \varphi[t / x]}{\Gamma, x=t \vdash \varphi} \quad {\operatorname{sub}_{=}} \end{mathpar} @@ -353,7 +355,7 @@ De plus, on sait que l'addition est associative et pour simplifier les preuves, \section{\label{sec:retour-automates}Retour sur les automates} \begin{question} - Écrire une fonction \mintinline{ocaml}{sans_zero : automate -> automate} qui prend en entrée un automate et qui renvoie une copie de cet automate ayant pour états finaux tout état permettant d'accéder à un état final par une suite de transitions étiquetées par la lettre $\begin{pmatrix}0 \\ \ldots \\ 0\end{pmatrix}$ dans l'automate initial. + Écrire une fonction \mintinline{ocaml}{sans_zero : automate -> automate} qui prend en entrée un automate et qui renvoie une copie de cet automate ayant pour états finaux tout état permettant d'accéder à un état final par une suite de transitions étiquetées par la lettre $\begin{pmatrix}0 \\ \vdots \\ 0\end{pmatrix}$ dans l'automate initial. \end{question} Avant de faire le lien entre automate et formules, on doit d'abord s'intéresser au problème des différentes représentations des entiers dues aux zéros non significatifs. @@ -375,13 +377,13 @@ Autrement dit, il s'agit de l'ensemble des mots égaux à un mot de $L$ sauf pos Soit $n$ un entier supérieur ou égal à $3$. Soit, $i$, $j$ et $k$ des entiers de $\llbracket 1, n \rrbracket$. -On note $L_{i, j, k}$ le langage $\{m \in \Sigma_n^{*} \mid v_(m)+v_(m)=v_k(m)\}$. On suppose disposer d'une fonction \mintinline{ocaml}{automate_somme : int -> int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_somme n i j k} renvoie un automate reconnaissant $L_{i, j, k}$. +On note $L_{i, j, k}$ le langage $\{m \in \Sigma_n^{*} \mid v_i(m)+v_j(m)=v_k(m)\}$. On suppose disposer d'une fonction \mintinline{ocaml}{automate_somme : int -> int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_somme n i j k} renvoie un automate reconnaissant $L_{i, j, k}$. -On note $L_{=i, j}$ le langage $\{m \in \Sigma_n^{*} \mid v_(m)=v_(m)\}$. On suppose disposer d'une fonction \mintinline{ocaml}{automate_egalite : int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_egalite n i j} renvoie un automate reconnaissant $L_{=i, j}$. +On note $L_{=i, j}$ le langage $\{m \in \Sigma_n^{*} \mid v_i(m)=v_j(m)\}$. On suppose disposer d'une fonction\\ \mintinline{ocaml}{automate_egalite : int -> int -> int -> automate} telle que \mintinline{ocaml}{automate_egalite n i j} renvoie un automate reconnaissant $L_{=i, j}$. Considérons une formule sous forme simple $\varphi$ utilisant $n$ variables qu'on note $\{x_1, \ldots, x_n\}$. Soit $k$ le nombre de variables libres de $\varphi$. Soit une fonction $f$ strictement croissante de $\llbracket 1, k \rrbracket$ dans $\llbracket 1, n \rrbracket$ telle que les $\{x_{f(1)}, \ldots, x_{f(k)}\}$ est l'ensemble des variables libres de $\varphi$. Pour tout mot $m$ de $\Sigma_n$, on note $a^{m}$ l'assignation des variables libres de $\varphi$ définie pour $i$ dans $\llbracket 1, k \rrbracket$ par $a^{m}(x_{f(i)})=v_{f(i)}(m)$. On note $L_{\varphi}$ le langage \[ -L_{\varphi}=\{m \in \Sigma_n^{*} \mid \llbracket \varphi \rrbracket_{a^{m}} \text { est vrai }\} +L_{\varphi}=\{m \in \Sigma_n^{*} \mid \llbracket \varphi \rrbracket_{a^{m}} \text { est vrai}\} \] Intéressons nous à l'implémentation des formules de Presburger sous forme simple. On représente les variables par des entiers. On utilise les types OCaml suivants : @@ -424,49 +426,48 @@ On présente les règles de la déduction naturelle suivantes. Les arbres de preuves doivent être effectués à partir de l'ensemble de règles fourni ci-dessous. \begin{mathpar} - \inferrule{\Gamma \vdash}{\Gamma, A \vdash A} \quad \text{ax} + \inferrule{ }{\Gamma, A \vdash A} \quad \text{ax} \and \inferrule{\Gamma \vdash B}{\Gamma, A \vdash B} \quad \text{aff} \and - \inferrule{\Gamma \vdash \bot}{\Gamma \vdash A} \quad \bot + \inferrule{\Gamma \vdash \bot}{\Gamma \vdash A} \quad \bot \\ - \inferrule{}{\Gamma \vdash A \vee \neg A} \quad \text {t.e.} + \inferrule{ }{\Gamma \vdash A \vee \neg A} \quad \text {t.e.} \and \inferrule{\Gamma, \neg A \vdash \bot}{\Gamma \vdash A} \quad \text{RAA} \\ \inferrule{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \quad \rightarrow_i - \quad - \inferrule{\Gamma \vdash A \rightarrow B \\ \Gamma \vdash A}{\Gamma \vdash B} \rightarrow_e - \\ - \inferrule{\Gamma \vdash A \\ \Gamma \vdash B}{\Gamma \vdash A \wedge B} \wedge_i \and - \inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash A} \wedge_e^{g} - \and - \inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash B} \wedge_e^{d} + \inferrule{\Gamma \vdash A \rightarrow B \\ \Gamma \vdash A}{\Gamma \vdash B} \quad \rightarrow_e \\ - \inferrule{\Gamma \vdash A}{\Gamma \vdash A \vee B} \vee_i^{g} + \inferrule{\Gamma \vdash A \\ \Gamma \vdash B}{\Gamma \vdash A \wedge B} \quad \wedge_i \and - \inferrule{\Gamma \vdash B}{\Gamma \vdash A \vee B} \vee_i^{d} + \inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash A} \quad \wedge_e^{g} \and - \inferrule{\Gamma \vdash A \vee B \\ \Gamma, A \vdash C \\ \Gamma, B \vdash C}{\Gamma \vdash C} \vee_e + \inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash B} \quad \wedge_e^{d} \\ - \inferrule{\Gamma, A \vdash \perp}{\Gamma \vdash \neg A} \neg_i + \inferrule{\Gamma \vdash A}{\Gamma \vdash A \vee B} \quad \vee_i^{g} \and - \inferrule{\Gamma \vdash \neg A \\ \Gamma \vdash A}{\Gamma \vdash \bot} \neg_e - \\ - \inferrule{\Gamma, A, B \vdash C}{\Gamma, A \wedge B \vdash C} \text{cut} - \\ - \inferrule{\Gamma \vdash A \\ x \not\in \operatorname{FV}(\Gamma)}{\Gamma \vdash \forall x. A} \forall_i + \inferrule{\Gamma \vdash B}{\Gamma \vdash A \vee B} \quad \vee_i^{d} \and - \inferrule{\Gamma \vdash \forall x. A}{\Gamma \vdash A[t/x]} \forall_e + \inferrule{\Gamma \vdash A \vee B \\ \Gamma, A \vdash C \\ \Gamma, B \vdash C}{\Gamma \vdash C} \quad \vee_e \\ - \inferrule{\Gamma \vdash A[t/x]}{\Gamma \vdash \exists x. A} \exists_i + \inferrule{\Gamma, A \vdash \perp}{\Gamma \vdash \neg A} \quad \neg_i \and - \inferrule{\Gamma \vdash \exists x. A \\ \Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma \vdash B} \exists_e + \inferrule{\Gamma \vdash \neg A \\ \Gamma \vdash A}{\Gamma \vdash \bot} \quad \neg_e \\ - \inferrule{\Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma, \exists x. A \vdash B} \exists'_e + \inferrule{\Gamma, A, B \vdash C}{\Gamma, A \wedge B \vdash C} \quad \text{cut} + \\ + \inferrule{\Gamma \vdash A \\ x \not\in \operatorname{FV}(\Gamma)}{\Gamma \vdash \forall x. A} \quad \forall_i + \and + \inferrule{\Gamma \vdash \forall x. A}{\Gamma \vdash A[t/x]} \quad \forall_e + \\ + \inferrule{\Gamma \vdash A[t/x]}{\Gamma \vdash \exists x. A} \quad \exists_i + \and + \inferrule{\Gamma \vdash \exists x. A \\ \Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma \vdash B} \quad \exists_e + \\ + \inferrule{\Gamma, A \vdash B \\ x \not\in \operatorname{FV}(\Gamma) \cup \operatorname{FV}(B)}{\Gamma, \exists x. A \vdash B} \quad \exists'_e \end{mathpar} - -Où $\operatorname{FV}(A)$ désigne l'ensemble des variables libres dans une formule $A$ et $\operatorname{FV}(\Gamma)$ l'ensemble des variables libres dans un ensemble de formules $\Gamma$. De plus, $A[t / x]$ correspond à la formule $A$ où les occurrences d'une variable libre $x$ ont été remplacées par $t$. +où $\operatorname{FV}(A)$ désigne l'ensemble des variables libres dans une formule $A$ et $\operatorname{FV}(\Gamma)$ l'ensemble des variables libres dans un ensemble de formules $\Gamma$. De plus, $A[t / x]$ correspond à la formule $A$ où les occurrences d'une variable libre $x$ ont été remplacées par $t$. \end{document}