
\documentclass[12pt]{article}

\usepackage[cp1252]{inputenc}   % LaTeX, comprends les accents !
\usepackage[T1]{fontenc}      % caractères français
\usepackage{lmodern}
%\addtolength{\hoffset}{-1cm}
%\addtolength{\textwidth}{2cm}  % pour les marges
%\addtolength{\voffset}{-1cm}
%\addtolength{\textheight}{2cm}        
\usepackage[a4paper]{geometry}
\usepackage[frenchb]{babel}
\usepackage{bm,amsmath,amssymb,amsthm,graphicx,MnSymbol}
\usepackage[ruled,vlined]{algorithm2e}


%Pour les Automates%
\usepackage{pgf}
\usepackage{tikz}
\usetikzlibrary{arrows,automata,decorations.text}
%%%% autres options %%%%

%\pagestyle{headings}         % Pour mettre des entêtes avec les titres des sections en haut de page

%\usepackage{pgf,tikz}         % Dessiner des Graphes :
%\usetikzlibrary{automata}     % ...Automates
%\usetikzlibrary{arrows}       % ...Flèches
%\usetikzlibrary{petri}        %

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{L'arithmétique de Presburger est décidable}
   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%% Commandes utiles %%%%

\newcommand{\A}{\mathcal{A}}
\newcommand{\LL}{\mathcal{L}}
\newcommand\N{\mathbb{N}}
\newcommand\C{\mathbb{C}}
\newcommand{\Cb}{\overline{\C}}
\newcommand{\conj}{\mathbf{C}}
\newcommand\R{\mathbb{R}}
\newcommand{\Rb}{\overline{\R}}
\newcommand\D{\mathbb{D}}
\renewcommand\H{\mathbb{H}}
\newcommand{\Hb}{\overline{\H}}
\renewcommand{\S}{\mathbb{S}}
\renewcommand\D{\Delta}
\newcommand{\n}{\bigskip}
\renewcommand{\Im}{\mathrm{Im}}
\renewcommand{\Re}{\mathrm{Re}}
\newcommand{\Hom}{\mathrm{Hom}}
\newcommand{\Mob}{\mathrm{Mob}}
\newcommand{\scal}{<\ ,\ >}
\newcommand{\dd}{\mathrm{d}}
\renewcommand{\frac}{\frac}
%\DeclareMathOperator{\D}{\mathcal{D}}


%%%% Commande \subsubsubsection{} %%%%%%
\setcounter{secnumdepth}{4}
\setcounter{tocdepth}{3}
\makeatletter
\newcounter {subsubsubsection}[subsubsection]
\renewcommand\thesubsubsubsection{\thesubsubsection .\@alph\c@subsubsubsection}
\newcommand\subsubsubsection{\@startsection{subsubsubsection}{4}{\z@}%
                                     {-3.25ex\@plus -1ex \@minus -.2ex}%
                                     {1.5ex \@plus .2ex}%
                                     {\normalfont\normalsize\bfseries}}
\newcommand*\l@subsubsubsection{\@dottedtocline{3}{10.0em}{4.1em}}
\newcommand*{\subsubsubsectionmark}[1]{}
\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%







\usepackage{thmbox}

\theoremstyle{plain}
\newtheorem{thm}{Théorème}
\newtheorem{lem}{Lemme}
\newtheorem{cor}{Corollaire}


\theoremstyle{definition}

\newtheorem{defi}{Définition}
\newtheorem{prop}{Propriété}
\newtheorem{nota}{Notation}

\theoremstyle{remark}
\newtheorem{exe}{Exemple}
\newcommand{\rem}{\bigskip\emph{Remarque : }}
\newcommand{\dem}{\bigskip\emph{Démonstration : }}

\begin{document}
\maketitle

\begin{thm}
	Soit la théorie du premier ordre des entiers munis de l'addition. Sa syntaxe est $$\phi,\phi' := (x=y)|(x+y=z)|\phi\vee\phi'|\neg\phi|\exists x\phi$$
	Alors pour toute formule close (i.e sans variables libres) $\phi$, il est décidable de savoir si $\phi$ est vraie.
\end{thm}

\n \emph{Démonstation :} Soit $\phi$ une formule close.

\begin{itemize}
	\item On admet l'existence de la forme prenexe de $\phi$ : $ \phi=Q_1x_1\cdots Q_nx_n \psi$ avec $\forall i, Q_i\in\{\exists, \neg \exists\}$.
	\item $\forall k\in[|0,n|]$, on pose $\phi_k=Q_{k+1}x_{k+1}\cdots Q_nx_n \psi$ avec $\phi_n=\psi$ et $\phi_0=\phi$.
	\item Pour tout $k$ on pose $\Sigma_k=\{0,1\}^k$. Un mot de longueur $m$ sur cet alphabet sera un $m$-uplet de $k$-uplet de bits. On peut donc pour tout $k$-uplet d'entier $(a_1,\dots,a_k)$ lui associer son écriture binaire sur $\Sigma_k$ : $((b_1^m,b_2^m,\dots,b_k^m),\dots,(b_1^0,b_2^0,\dots,b_k^0))$ où $\forall i\geq k, a_i=\sum_{j=1}^m b_i^j*2^j$. On a donc rajouter des 0 à gauche pour que tous les $a_i$ aient la même longueur en écriture binaire.
	\item Pour $k\in[|0,n|]$, posons $X_k=\{(a_1,\dots,a_k)\in\N^k | [|\phi_k|]_(a_1,\dots,a_k)=1\}$
\end{itemize}

\begin{enumerate}
	\item Construisons $\A_n$ tel que $\LL(\A)=X_n$ :
	\n $\psi$ est s'écrit par induction à partir des formules $(1): x_i=x_j$ et $(2): x_i+x_j=x_r$ et des opérations $\neg$ et $\vee$.
	L'automate $\A_{(1)}$ teste l'égalité bit à bit $x_i=x_j$ : 
	
	\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,semithick,initial text=,initial/.style=initial left, accepting/.style=accepting right]
		\tikzstyle{every state}=[fill=white,draw=black,text=black]
		
		\node[state, initial, accepting] (A)                    {$0$};
		
		\path (A) 			edge [loop above] node {$(0,0)$} (A)
					(A)				edge [loop below] node {$(1,1)$} (A);

	\end{tikzpicture}
	
	où $(a,b)=\{$transitions $(\---,a,\---,b,\---)$, où $a$ est le $i$-ème bit et $b$ le $j$-ème$\}$.
	
	\n L'automate $\A_{(2)}$ teste la somme $x_i+x_j=x_r$ en testant commençant par les bit de plus haut poids : 
	 
	\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=3cm,semithick,initial text=,initial/.style=initial below, accepting/.style=accepting above]
		\tikzstyle{every state}=[fill=white,draw=black,text=black]
		
		\node[state] (A)                    {R};
		\node[state,initial,accepting] (B)	[right of=A]			{S R};
		
		\path (B) 			edge [loop right] node {$(0,0,0), (0,1,1), (1,0,1)$} (B)
		      					edge [bend left]  node {$(0,0,1)$} (A)
		      (A)       edge [bend left]  node {$(1,1,0)$} (B)
		      					edge [loop left] node {$(1,1,1),(1,0,0),(0,1,0)$} (A);
	\end{tikzpicture}
	
	Les transitions $(a,b,c)$ sont définies de manière analogue que $(a,b)$.
	L'état $R$ est l'état dit ``avec retenue'', il est atteint depuis l'état sans retenue $S R$ lorsque le plus grand des trois bit testés est celui de $x_r$.
	
	\n Par exemple, si nous testons la somme $3+5=7$, nous avons $x_1=3,x_2=4, x_3=7$ en écriture binaire, $(x_1,x_2,x_3)$ donne $((0,0,1),(1,1,1),(1,0,1))$. Nous commençons par tester $(0,0,1)$, nous allons dans l'état avec retenue car la somme est juste seulement si le dernier bit est issue d'une retenue. Ensuite nous testons $(1,1,1)$. Cette somme est vraie s'il y a une retenue ($1+1=10$, donc 11 s'il y avait une retenue), nous restons donc dans l'état avec retenue. Enfin, dans l'état avec retenue, nous ne pouvons pas avoir $1+0=1$, la somme formule est donc fausse pour cette valuation.
	
	\n Maitenant que nous avons $\A_{(1)}$ et $\A_{(2)}$ pour tous les $i,j,r$, nous savons construire les négations des formules en prenant l'automate complémentaire et nous savons faire les disjonctions de formules en prenant l'union de deux automates. Par induction nous savons construire $\A_n$.
	
	\n \item Construisons $\A_k$ tel que $\LL(\A_k)=X_k$ à partir de $\A_{k+1}$.
	
	\n $\phi_k=Q_{k+1}x_{k+1} \phi_k$. On peut supposer $\phi_k=\exists \phi_{k+1}$ car sinon $\phi_k=\neq \exists \phi_{k+1}$ et nous savons écrire la négation d'une formule avec les automates.
	
	Nous avons $\A_{k+1}=(Q,\Sigma_{k+1},\delta_{k+1},I_{k+1}, F)$, nous posons alors $\A_k=(Q,\Sigma_k,\delta_k,I_k, F)$ avec $\pi_k : \Sigma_{k+1}\rightarrow\Sigma_k : (b_1,\dots,b_{k+1})\mapsto (b_1,\dots,b_k)$ de la manière suivante :
	$$\forall p,q\in Q, \forall x\in\Sigma_k, si\ \delta_{k+1}(p,a)=q\ alors\ on\ pose\ \delta_k(p,\pi_k(x))=q$$
	$$I_k=I_{k+1} \cup \{ \delta_k(i,(0,\dots,0)), \forall i\in I_{k+1} \}$$
	
	$A_k$ va deviner le $x_{k+1}$ tel que la formule est vraie, puisqu'à chaque fois nous avons le choix entre donner la valeur 0 ou 1 au $(k+1)$-ième bit. La deuxième partie de l'ensemble $I_k$ sert à prendre en compte que l'entier $x_{k+1}$ à deviner pourrait être beaucoup plus grand que les autres entiers $(x_1,\dots,x_k)$ et qu'il va donc falloir rajouter des 0 dans l'écriture binaire de $(x_1,\dots,x_k,x_{k+1})$.
	
	\n Dis autrement, 
	$$\begin{array}{ccc} (a_1,\dots,a_m)\in\LL(\A_k) &\Leftrightarrow &\exists i\stackrel{a_1}{\longrightarrow}p_1\stackrel{a_2}{\longrightarrow}\cdots\stackrel{am}{\longrightarrow}q\in F\ dans\ \A_k\\ \\
																									 &\Leftrightarrow &\exists(b_0,\dots,b_m)\in\{0,1\}^{m+1} et\ \tilde{i}\in I_{k+1},\\
																									 & & \tilde{i}\stackrel{(0,\dots,0,b_0)}{\longrightarrow}i\stackrel{a_1\cdot b_1}{\longrightarrow}\dots\stackrel{a_m\cdot b_m}{\longrightarrow}q \in F\ dans\ \A_{k+1} \\ \\
																									 &\Leftrightarrow &\exists (b_0,\dots,b_m)\in\{0,1\}^{m+1},\\ 
																									 & &((0,\dots,0,b_0),a_1\cdot b_1,\dots,a_m\cdot b_m)\in X_{k=1} \\ \\
																									 &\Leftrightarrow & (a_1,\dots,a_m)\in X_k \end{array}$$
	
	\item Pour finir, nous construirons $\A_0=(Q,\Sigma_0,\delta_0,I_0,F)$. Comme $\Sigma_0=\{0,1\}^0=\emptyset,$ donc $\Sigma_0^*=\{\epsilon\}$. Du coup $\delta$ est défini sur l'ensemble vide, il n'y a donc aucune transition dans $\A_0$. Du coup $\LL(\A_0)=\emptyset$ ou $\{\epsilon\}$, la deuxième solution n'est possible que si $I_0\cap F \neq \emptyset$ et alors $\phi$ est vraie, sinon $\phi$ est fausse.
\end{enumerate}
	
	
\end{document}