Florian Hatat
474 lignes
27 KiB
TeX
474 lignes
27 KiB
TeX
\documentclass[10pt,a4paper]{article}
|
||
\usepackage[french]{babel}
|
||
\usepackage[utf8]{inputenc}
|
||
\usepackage{amsmath}
|
||
\usepackage{amsfonts}
|
||
\usepackage{amsthm}
|
||
\usepackage{amssymb}
|
||
\usepackage{stmaryrd}
|
||
\usepackage{tikz}
|
||
\usetikzlibrary{automata}
|
||
\usepackage{algorithm}
|
||
\usepackage{algpseudocode}
|
||
\usepackage{minted}
|
||
\usepackage{fullpage}
|
||
\usepackage{enumerate}
|
||
\usepackage{mathpartir}
|
||
|
||
\theoremstyle{definition}
|
||
\newtheorem{question}{Question}
|
||
\newtheorem{definition}{Définition}
|
||
\newtheorem{theorem}{Théorème}
|
||
|
||
% Algorithmes
|
||
\renewcommand{\listalgorithmname}{Liste des algorithmes}
|
||
\floatname{algorithm}{Algorithme}
|
||
\renewcommand{\algorithmicreturn}{\textbf{renvoyer}}
|
||
\renewcommand{\algorithmicprocedure}{\textbf{procédure}}
|
||
\renewcommand{\algorithmicfunction}{\textbf{fonction}}
|
||
\renewcommand{\algorithmicrequire}{\textbf{Entrée~:}}
|
||
\renewcommand{\algorithmicensure}{\textbf{Sortie~:}}
|
||
\renewcommand{\algorithmiccomment}[1]{\hfill\texttt{// #1}}
|
||
\renewcommand{\algorithmicend}{\textbf{fin}}
|
||
\renewcommand{\algorithmicif}{\textbf{si}}
|
||
\renewcommand{\algorithmicthen}{\textbf{alors}}
|
||
\renewcommand{\algorithmicelse}{\textbf{sinon}}
|
||
\renewcommand{\algorithmicfor}{\textbf{pour}}
|
||
\renewcommand{\algorithmicforall}{\textbf{pour tout}}
|
||
\renewcommand{\algorithmicdo}{\textbf{faire}}
|
||
\renewcommand{\algorithmicwhile}{\textbf{tant que}}
|
||
\newcommand{\algorithmicelsif}{\algorithmicelse\ \algorithmicif}
|
||
\newcommand{\algorithmicendif}{\algorithmicend\ \algorithmicif}
|
||
\newcommand{\algorithmicendfor}{\algorithmicend\ \algorithmicfor}
|
||
|
||
\title{Épreuve d'option informatique MP}
|
||
\author{Concours Mines Ponts}
|
||
\date{2026-04-27}
|
||
|
||
\begin{document}
|
||
|
||
\maketitle
|
||
|
||
\section*{Préliminaires}
|
||
|
||
L'épreuve est composée d'un problème unique, comportant \ref{q:derniere-question} questions. Le problème est divisé en cinq sections. Dans la première section (page \pageref{sec:fonctions-utiles}), nous implémentons plusieurs fonctions mathématiques. Dans la deuxième section (page \pageref{sec:automates-finis}), nous étudions des automates sur un alphabet particulier et nous nous intéressons à une implémentation. Dans la troisième section (page \pageref{sec:operations-arithmetiques}), nous nous intéressons à la reconnaissabilité de certains langages sous cet alphabet. Dans la quatrième section (page \pageref{sec:presburger}), nous nous intéressons à l'arithmétique de Presburger et ses formules logiques. Enfin, dans la cinquième et dernière section (page \pageref{sec:retour-automates}), nous cherchons à décider de la satisfiabilité de ces formules à l'aide des automates précédemment étudiés.
|
||
|
||
Dans tout l'énoncé, un même identificateur écrit dans deux polices de caractères différentes désigne la même entité, mais du point de vue mathématique pour la police en italique (par exemple $n$) et du point de vue informatique pour celle en romain avec espacement fixe (par exemple \mintinline{ocaml}{n}).
|
||
|
||
Des rappels portant sur les règles de la déduction naturelle sont fournis en annexe.
|
||
|
||
\section*{Travail attendu}
|
||
|
||
Pour répondre à une question, il est permis de réutiliser le résultat d'une question antérieure, même sans avoir réussi à établir ce résultat.
|
||
|
||
Il faudra coder des fonctions à l'aide du langage de programmation OCaml exclusivement. Les fonctions des modules \mintinline{ocaml}{List} et \mintinline{ocaml}{Array} peuvent être utilisées sans explication. Il est cependant recommandé de s'en tenir aux fonctions les plus courantes afin de rester compréhensible.
|
||
|
||
Le barème tient compte de la clarté et de la concision des programmes. Nous recommandons de choisir des noms de variables intelligibles ou encore de structurer de longs codes par des blocs ou par des fonctions auxiliaires dont on décrit le rôle.
|
||
|
||
\section*{Introduction}
|
||
|
||
On note $\mathbb{N}$ l'ensemble des entiers naturels. Pour tout couple d'entiers $a, b$ tel que $a \leqslant b$, on note $\llbracket a, b \rrbracket$ l'ensemble des entiers de $a$ à $b$ compris. Pour tout ensemble $E$, on note $\mathcal{P}(E)$ l'ensemble des parties de $E$, c'est-à-dire l'ensemble des sous-ensembles de $E$. Pour tout ensemble fini $E$, on note $|E|$ son cardinal.
|
||
|
||
Pour tout mot $m$, on note $|m|$ la taille de $m$, qui correspond à son nombre de lettres.
|
||
|
||
Dans tout le sujet, pour tout entier $n$ positif, on notera $\Sigma_n$ l'alphabet composé des vecteurs colonnes de taille $n$ à valeurs dans $\{0,1\}$. Par exemple,
|
||
|
||
\[
|
||
\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$\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 :
|
||
|
||
\[
|
||
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(\pi_i(m))$.
|
||
|
||
Considérons par exemple le mot $m$ suivant :
|
||
|
||
\[
|
||
m =
|
||
\begin{pmatrix} 0 \\ 1 \\ 1 \end{pmatrix}
|
||
\begin{pmatrix} 1 \\ 0 \\ 1 \end{pmatrix}
|
||
\begin{pmatrix} 1 \\ 0 \\ 0 \end{pmatrix}
|
||
\begin{pmatrix} 0 \\ 0 \\ 0 \end{pmatrix}
|
||
\begin{pmatrix} 1 \\ 1 \\ 1 \end{pmatrix}
|
||
\begin{pmatrix} 0 \\ 1 \\ 1 \end{pmatrix}
|
||
\begin{pmatrix} 1 \\ 0 \\ 1 \end{pmatrix}
|
||
\begin{pmatrix} 1 \\ 0 \\ 0 \end{pmatrix}
|
||
\]
|
||
|
||
On a $\pi_2(m)=10001100$, $v_1(m)=2+4+16+64+128=214$, $v_2(m)=49$ et $v_3(m)=115$.
|
||
|
||
Dans ce sujet, un automate fini non déterministe à un seul état initial, qu'on s'autorise à appeler simplement automate, est défini comme un tuple $\mathcal{A}=(\Sigma, Q, q_i, F, \delta)$ où :
|
||
\begin{itemize}
|
||
\item $\Sigma$ est un alphabet fini ;
|
||
\item $Q$ est un ensemble fini d'états ;
|
||
\item $q_i$ est un état de $Q$ appelé état initial ;
|
||
\item $F$ est un sous-ensemble de $Q$ appelé ensemble des états finaux ;
|
||
\item $\delta$ est une fonction de $Q \times \Sigma$ dans $\mathcal{P}(Q)$ appelée fonction de transition.
|
||
\end{itemize}
|
||
|
||
On dit qu'un automate $\mathcal{A}=(\Sigma, Q, q_i, \delta, F)$ est déterministe complet lorsque pour chaque sommet $q \in Q$, et chaque lettre $a \in \Sigma$, on a $|\delta(q, a)|=1$.
|
||
|
||
Pour deux états $p$ et $q$ de $Q$, et pour toute lettre $a$ de $\Sigma$, on note $p \xrightarrow{a} q$ si $q \in \delta(p, a)$. On dit qu'il existe une transition de $p$ à $q$ étiquetée par $a$. On prend comme convention graphique d'indiquer l'état initial par une flèche entrante et les états finaux en les entourant.
|
||
|
||
Pour un automate $\mathcal{A}$ on note $\mathcal{L}(\mathcal{A})$ le langage reconnu par $\mathcal{A}$.
|
||
|
||
Dans tout le sujet, on fera l'hypothèse simplificatrice qu'en OCaml, on dispose d'une mémoire infinie et que les variables peuvent stocker des valeurs aussi grandes que l'on souhaite.
|
||
|
||
\section{\label{sec:fonctions-utiles}Implémentation de quelques fonctions utiles}
|
||
|
||
Commençons par implémenter plusieurs fonctions mathématiques qui nous seront utiles dans la suite.
|
||
|
||
\begin{question}
|
||
Écrire une fonction \mintinline{ocaml}{pow2 : int -> int} qui prend en entrée un entier $n$ et renvoie $2^n$. On attend une fonction récursive de complexité temporelle en $O(\log(n))$ qui n'utilise pas les opérateurs de décalage \mintinline{ocaml}{lsr} et \mintinline{ocaml}{lsl}.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Démontrer que la complexité de votre algorithme est bien en $O(\log (n))$.
|
||
\end{question}
|
||
|
||
On représente en OCaml les lettres de $\Sigma_n$ à l'aide du type \mintinline{ocaml}{int array} en utilisant des tableaux de dimension $n$ dont les éléments sont à valeurs dans $\{0,1\}$.
|
||
|
||
\begin{question}
|
||
Exhiber une bijection entre $\llbracket 0,2^{n}-1 \rrbracket$ et $\Sigma_n$.
|
||
\end{question}
|
||
|
||
À présent, on souhaite implémenter notre bijection.
|
||
|
||
\begin{question}
|
||
Écrire une fonction \mintinline{ocaml}{decompose : int -> int -> int array} qui prend en entrée \mintinline{ocaml}{x} et \mintinline{ocaml}{n} tels que $x \in \llbracket 0,2^{n}-1 \rrbracket$ et qui renvoie l'élément de $\Sigma_n$ associée par la bijection précédemment définie. On vérifiera que l'entrée est valide à l'aide d'une assertion.
|
||
\end{question}
|
||
|
||
\section{\label{sec:automates-finis}Automates finis sur $\sum_n$}
|
||
|
||
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}[ht]
|
||
\begin{center}
|
||
\begin{tikzpicture}[initial text = {}]
|
||
\node[state, initial] (q0) {$q_0$};
|
||
\node[state, right of=q0,xshift=3cm,accepting] (q1) {$q_1$};
|
||
\node[state, right of=q1,xshift=3cm] (q2) {$q_2$};
|
||
\draw [line width=.75pt,->]
|
||
(q0) edge[loop above] node{$\binom{0}{0}$} (q0)
|
||
(q1) edge[loop above] node{$\binom{0}{0},\binom{1}{0}$} (q1)
|
||
(q0) edge[bend left, above] node{$\binom{1}{1}$} (q1)
|
||
(q1) edge[bend left,above] node{$\binom{0}{1},\binom{1}{1}$} (q2)
|
||
(q0) edge[bend right,below] node{$\binom{1}{0},\binom{0}{1}$} (q2)
|
||
;
|
||
\end{tikzpicture}
|
||
\caption{Représentation de l'automate $\mathcal{A}_1$}
|
||
\label{fig:automate-a1}
|
||
\end{center}
|
||
\end{figure}
|
||
|
||
\begin{figure}[ht]
|
||
\begin{center}
|
||
\begin{tikzpicture}[initial text = {}]
|
||
\node[state, initial] (q0) {$q_0$};
|
||
\node[state, right of=q0,xshift=3cm,accepting] (q1) {$q_1$};
|
||
\draw [line width=.75pt,->]
|
||
(q0) edge[loop above] node{$\binom{0}{0},\binom{0}{1}, \binom{1}{1}$} (q0)
|
||
(q1) edge[loop above] node{$\binom{0}{0},\binom{1}{0},\binom{1}{1}$} (q1)
|
||
(q0) edge[bend left, above] node{$\binom{1}{0}$} (q1)
|
||
(q1) edge[bend left,below] node{$\binom{0}{1}$} (q0)
|
||
;
|
||
\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}(\mathcal{A}_1)=E$.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
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}(\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=\{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 \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 = {
|
||
k : int;
|
||
n : int;
|
||
finaux : bool array;
|
||
delta : int -> int array -> int list;
|
||
}
|
||
\end{minted}
|
||
|
||
Ici, \mintinline{ocaml}{k} correspond donc au nombre d'états de l'automate, \mintinline{ocaml}{n} correspond à $n$, \mintinline{ocaml}{finaux} est un tableau de booléens de taille $k$ qui indique si un état est final, et \mintinline{ocaml}{delta} est la fonction de transition prenant en paramètre un état $q$ et une lettre $a$, représentée par un tableau d'entiers de taille $n$, et renvoie la liste des états de $\delta(q, a)$.
|
||
|
||
\begin{question}
|
||
Écrire une fonction \mintinline{ocaml}{est_deterministe_complet : automate -> bool} qui vérifie si un automate $\mathcal{A}=(\Sigma_n, Q, q_i, \delta, F)$ est déterministe complet. On attend une complexité temporelle en $O(n \times|Q| \times |\Sigma_n|)$. Justifier la complexité obtenue.
|
||
\end{question}
|
||
|
||
On se propose maintenant d'implémenter l'algorithme de déterminisation des automates.
|
||
|
||
\begin{question}
|
||
Soit $\mathcal{A}=(\Sigma, Q, q_i, \delta, F)$ un automate fini non déterministe. Donner la construction formelle d'un automate déterministe reconnaissant $\mathcal{L}(\mathcal{A})$.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Écrire une fonction \mintinline{ocaml}{union : int array -> automate -> int array -> int array} qui prend en entrée les paramètres \mintinline{ocaml}{etats}, \mintinline{ocaml}{a} et \mintinline{ocaml}{lettre}, tels que :
|
||
\begin{itemize}
|
||
\item \mintinline{ocaml}{a} soit un automate à $k$ états ;
|
||
\item \mintinline{ocaml}{etats} soit un tableau d'entiers de taille $k$ à valeur dans $\{0,1\}$ ;
|
||
\item \mintinline{ocaml}{lettre} soit une lettre représentée par un tableau d'entiers.
|
||
\end{itemize}
|
||
Cette fonction doit renvoyer un tableau \mintinline{ocaml}{t} de taille $k$, tel que \mintinline{ocaml}{t.(i)=1} s'il existe un $q$ tel que \mintinline{ocaml}{etats.(q)=1} et $q \xrightarrow{\texttt{ lettre }} i$ est une transition de \mintinline{ocaml}{a}, et \mintinline{ocaml}{t.(i)=0} sinon.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
En déduire une fonction \mintinline{ocaml}{determinise : automate -> automate} qui prend en entrée un automate et renvoie un automate déterministe complet reconnaissant le même langage.
|
||
|
||
Indication : on pourra utiliser la fonction \mintinline{ocaml}{decompose} plusieurs fois.
|
||
\end{question}
|
||
|
||
On appelle complémentaire d'un langage $L$ sur un alphabet $\Sigma$ le langage $\bar{L}$ des mots sur $\Sigma$ n'appartenant pas à $L$.
|
||
|
||
\begin{question}
|
||
Écrire une fonction \mintinline{ocaml}{complementaire : automate -> automate} qui prend en entrée un automate et renvoie un automate reconnaissant son langage complémentaire.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Considérons deux automates $\mathcal{A}_1=(\Sigma_n, Q_1, q_1, \delta_1, F_1)$ et $\mathcal{A}_2=(\Sigma_n, Q_2, q_2, \delta_2, F_2)$. Donner la construction formelle d'un automate ayant pour ensemble d'états $Q_1 \times Q_2$ et reconnaissant $\mathcal{L}(\mathcal{A}_1) \cap \mathcal{L}(\mathcal{A}_2)$. Ici $Q_1 \times Q_2$ est le produit cartésien de $Q_1$ et $Q_2$.
|
||
\end{question}
|
||
|
||
On suppose dans la suite disposer d'une fonction OCaml \mintinline{ocaml}{intersection : automate -> automate -> automate} qui prend en entrée deux automates et renvoie un automate reconnaissant l'intersection de leurs langages.
|
||
|
||
\section{\label{sec:operations-arithmetiques}Opérations arithmétiques}
|
||
On s'intéresse à présent aux opérations arithmétiques en binaire et à la possibilité de les représenter à l'aide d'automates sur $\Sigma_3$.
|
||
|
||
\begin{question}
|
||
Donner, dans un premier temps sans justifier, un automate à deux états reconnaissant le langage $L_+=\{m \in \Sigma_3^{*} \mid v_1(m)+v_2(m)=v_3(m)\}$.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Démontrer que l'automate proposé dans la question précédente reconnaît bien $L_+$.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Le langage $L_{\times}=\{m \in \Sigma_3^{*} \mid v_1(m) \times v_2(m)=v_3(m)\}$ est-il reconnaissable ? Justifier.
|
||
\end{question}
|
||
|
||
\section{\label{sec:presburger}Arithmétique de Presburger}
|
||
|
||
L'arithmétique de Presburger est l'arithmétique usuelle des entiers et de l'addition, mais sans la multiplication.
|
||
|
||
Soit $\mathcal{V}$ un ensemble infini de variables.
|
||
|
||
L'ensemble des termes est défini inductivement de la façon suivante :
|
||
|
||
\begin{itemize}
|
||
\item pour tout $x \in \mathcal{V}, x$ est un terme ;
|
||
\item pour deux termes $t_1$ et $t_2, t_1+t_2$ est un terme.
|
||
\end{itemize}
|
||
|
||
L'ensemble des formules de Presburger, qu'on s'autorise à appeler formules, est ensuite défini inductivement de la façon suivante :
|
||
|
||
\begin{itemize}
|
||
\item pour $t_1$ et $t_2$ deux termes, $t_1=t_2$ est une formule ;
|
||
\item pour $\varphi$ une formule, $\neg \varphi$ est une formule ;
|
||
\item pour $\varphi_1$ et $\varphi_2$ deux formules $\varphi_1 \rightarrow \varphi_2, \varphi_1 \wedge \varphi_2$ et $\varphi_1 \vee \varphi_2$ sont des formules ;
|
||
\item pour $\varphi$ une formule et $x$ une variable qui n'apparaît pas juste après un quantificateur dans $\varphi$, alors $\exists x . \varphi$ et $\forall x . \varphi$ sont des formules.
|
||
\end{itemize}
|
||
|
||
L'évaluation des formules suit le sens habituel de l'opérateur d'égalité $=$, et des opérateurs logiques. Les quantificateurs ont leur sens usuel avec des variables prises à valeurs dans l'ensemble $\mathbb{N}$. On utilise des parenthèses pour repérer les sous-formules lorsqu'il y a ambiguïté et pour indiquer les priorités d'ordre des opérations usuelles.
|
||
|
||
Pour toute formule $\varphi$, et toute sous-formule $\forall x . \psi$ ou $\exists x . \psi$ de $\varphi$, on dit que toutes les occurrences de $x$ dans $\psi$ sont liées. Les occurrences non liées de $x$ dans $\varphi$ sont dites libres. Si $\varphi$ possède des occurrences libres de $x$, on dit que $x$ est une variable libre de $\varphi$.
|
||
|
||
Dans la formule $\exists x . \forall y .(z=t+y \wedge z=x) \vee(\exists w . z=t+w)$, les variables $x, y$ et $w$ sont liées, et les variables libres sont $z$ et $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$.
|
||
|
||
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é.
|
||
|
||
\begin{question}
|
||
Donner une formule de Presburger $\operatorname{div}_2(x)$ qui est vraie si et seulement si $x$ est divisible par 2.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Pour tout entier $n \in \mathbb{N}$, donner une formule de Presburger $f_n(x)$ qui est vraie si et seulement si $x=n$.
|
||
|
||
Attention, $n$ n'est pas un terme et ne peut donc pas apparaître dans votre formule sous cette forme.
|
||
\end{question}
|
||
|
||
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 $\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}
|
||
\item soit $t_2$ est une variable dans $\mathcal{V}$,
|
||
\item soit $t_2=x+y$ avec $x$ et $y$ deux variables de $\mathcal{V}$.
|
||
\end{itemize}
|
||
\end{enumerate}
|
||
|
||
\begin{question}
|
||
Montrer que toute formule de Presburger $\varphi$ est équivalente à une formule sous forme simple.
|
||
\end{question}
|
||
|
||
On veut à présent montrer que certaines formules sont des tautologies à l'aide de la déduction naturelle.
|
||
|
||
\begin{question}
|
||
Prouver à l'aide de la déduction naturelle le séquent suivant où $\varphi(x)$ désigne une formule faisant apparaître la variable libre $x$ et $\psi(y)$ désigne une formule faisant apparaître la variable libre $y$.
|
||
\[\vdash(\varphi(x) \vee \psi(y)) \rightarrow(\neg \varphi(x) \rightarrow \psi(y))\]
|
||
\end{question}
|
||
|
||
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}_{=}}
|
||
\and
|
||
\inferrule{\Gamma, x=t \vdash \varphi[t / x]}{\Gamma, x=t \vdash \varphi} \quad {\operatorname{sub}_{=}}
|
||
\end{mathpar}
|
||
|
||
De plus, on sait que l'addition est associative et pour simplifier les preuves, on s'autorise à utiliser cette propriété dans nos arbres. Par exemple, pour $t_1$, $t_2$ et $t_3$ des termes, on peut considérer que $t_1+(t_2+t_3)$ est le même terme que $(t_1+t_2)+t_3$ ainsi que $t_1+t_2+t_3$.
|
||
|
||
\begin{question}
|
||
Donner une formule de Presburger $\varphi(x, y, z)$ avec 3 variables libres exprimant le fait que l'égalité est transitive sur les variables et la prouver à l'aide de la déduction naturelle.
|
||
\end{question}
|
||
|
||
\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 \\ \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.
|
||
|
||
Soit $n$ un entier naturel non nul et $i$ dans $\llbracket 1, n \rrbracket$. Soit $L$ un langage sur $\Sigma_n$. On note $L_{\exists i}$ le langage défini par :
|
||
\[
|
||
L_{\exists i}=\{m \in \Sigma_n^{*} \mid \exists w \in L, \forall k \in \llbracket 1, n \rrbracket, k \neq i, \pi_k(m)=\pi_k(w)\}
|
||
\]
|
||
|
||
Autrement dit, il s'agit de l'ensemble des mots égaux à un mot de $L$ sauf possiblement à la ligne $i$.
|
||
|
||
\begin{question}
|
||
Soit $L=\left\{\varepsilon,\begin{pmatrix}0 \\ 1 \\ 1\end{pmatrix},\begin{pmatrix}0 \\ 0 \\ 0\end{pmatrix}\begin{pmatrix}1 \\ 1 \\ 1\end{pmatrix}\right\}$, donner $L_{\exists 2}$.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Écrire une fonction \mintinline{ocaml}{automate_existe : automate -> int -> automate} qui prend en entrée un automate $\mathcal{A}$ et un entier $i$ et qui renvoie un automate reconnaissant $\mathcal{L}(\mathcal{A})_{\exists i}$.
|
||
\end{question}
|
||
|
||
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_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_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}\}
|
||
\]
|
||
|
||
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 :
|
||
|
||
\begin{minted}{ocaml}
|
||
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
|
||
\end{minted}
|
||
|
||
\begin{question}
|
||
Expliquer en langage courant le principe d'un algorithme qui prend en entrée une formule $\varphi$ sous forme simple, l'indice de la plus grande variable apparaissant dans $\varphi$, et qui renvoie un automate reconnaissant $L_{\varphi}$.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Faites tourner à la main votre algorithme en détaillant bien les étapes et automates intermédiaires sur la formule $\varphi(x_2):=\neg \exists x_1 . \neg(x_1=x_2)$ pour renvoyer l'automate correspondant.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Écrire une fonction \mintinline{ocaml}{automate_formule : formule -> int -> automate} qui prend en entrée une formule $\varphi$ sous forme simple et l'indice de la plus grande variable apparaissant dans $\varphi$, et qui renvoie un automate reconnaissant $L_{\varphi}$.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
Démontrer la correction de votre algorithme.
|
||
\end{question}
|
||
|
||
\begin{question}
|
||
\label{q:derniere-question}
|
||
En déduire une fonction \mintinline{ocaml}{est_vraie : formule -> int -> bool} qui détermine pour une formule sous forme simple supposée sans variable libre et le plus grand indice de ses variables si elle est vraie.
|
||
\end{question}
|
||
|
||
\appendix
|
||
\section{Annexe : Règles de la déduction naturelle}
|
||
|
||
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, 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 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
|
||
\and
|
||
\inferrule{\Gamma \vdash A \rightarrow B \\ \Gamma \vdash A}{\Gamma \vdash B} \quad \rightarrow_e
|
||
\\
|
||
\inferrule{\Gamma \vdash A \\ \Gamma \vdash B}{\Gamma \vdash A \wedge B} \quad \wedge_i
|
||
\and
|
||
\inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash A} \quad \wedge_e^{g}
|
||
\and
|
||
\inferrule{\Gamma \vdash A \wedge B}{\Gamma \vdash B} \quad \wedge_e^{d}
|
||
\\
|
||
\inferrule{\Gamma \vdash A}{\Gamma \vdash A \vee B} \quad \vee_i^{g}
|
||
\and
|
||
\inferrule{\Gamma \vdash B}{\Gamma \vdash A \vee B} \quad \vee_i^{d}
|
||
\and
|
||
\inferrule{\Gamma \vdash A \vee B \\ \Gamma, A \vdash C \\ \Gamma, B \vdash C}{\Gamma \vdash C} \quad \vee_e
|
||
\\
|
||
\inferrule{\Gamma, A \vdash \perp}{\Gamma \vdash \neg A} \quad \neg_i
|
||
\and
|
||
\inferrule{\Gamma \vdash \neg A \\ \Gamma \vdash A}{\Gamma \vdash \bot} \quad \neg_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$.
|
||
|
||
\end{document}
|