diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 142 |
1 files changed, 142 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 9b95039..06473c2 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1711,6 +1711,148 @@ $ \end{frame} % +\begin{frame} +\frametitle{Un peu d'histoire des maths : Brouwer et l'intuitionnisme} + +\itempoint L'\textbf{intuitionnisme} est à l'origine une philosophie +des mathématiques développée (à partir de 1912) par L. E. J. Brouwer +(1881–1966) en réaction/opposition au \textbf{formalisme} promu par +D. Hilbert (1862–1943). + +\medskip + +Quelques principes de l'intuitionnisme \emph{à l'origine} : + +\begin{itemize} +\item rejet de la loi du tiers exclu (« principe d'omniscience ») pour + demander des preuves \alert{constructives} (pour Brouwer, montrer + que $x$ ne peut pas ne pas exister n'est pas la même chose que + montrer que $x$ existe), +\item refus de la logique formelle (pour Brouwer, les maths sont + « créatives »), +\item principes de continuité (notamment : toute fonction $\mathbb{R} + \to \mathbb{R}$ est continue). +\end{itemize} + +\medskip + +\itempoint Idées rejetées par Hilbert (et la plupart des +mathématiciens). + +$\rightarrow$ « controverse Hilbert-Brouwer » {\footnotesize + (rapidement devenue querelle personnelle)} + +\medskip + +Hilbert : « Retirer au mathématicien le principe du tiers exclu +serait comme empêcher à un boxeur d'utiliser ses poings. » + +\end{frame} +% +\begin{frame} +\frametitle{Les maths constructives après Brouwer} + +\itempoint L'intuitionnisme a été ensuite reformulé et modifié par les +élèves de Brouwer et leurs propres élèves (notamment A. Heyting, +A. Troelstra) et d'autres écoles (analyse constructive d'E. Bishop, +constructivisme russe de A. Markov fils) : + +\begin{itemize} +\item dans le cadre de la logique formelle (ou compatible avec elle), +\item sans impliquer de principe \emph{contredisant} les maths + classiques, +\item mais toujours \alert{sans la loi du tiers exclu}. +\end{itemize} + +\bigskip + +\itempoint Les termes de « \textbf{mathématiques constructives} » et +« intuitionnisme » sont devenus plus ou moins interchangeables pour +« maths sans le tiers exclu ». + +\bigskip + +\itempoint Dans \emph{certains} tels systèmes, prouver $P\lor Q$ +resp. $\exists x.P(x)$ passe forcément par la preuve de $P$ ou de $Q$, +resp. par la construction d'un $x$ vérifiant $P(x)$. + +\end{frame} +% +\begin{frame} +\frametitle{Pourquoi vouloir « boxer sans ses poings » ?} + +{\footnotesize Évidence : l'\alert{écrasante majorité des maths} + se fait en logique classique (loi du tiers exclu admise) !\par} + +\medskip + +Une preuve « constructive » (sans tiers exclu) est plus restrictive +qu'une preuve classique, donc \alert{apporte plus} : + +\begin{itemize} +\item principe de parcimonie ; \quad \itempoint curiosité purement théorique ; +\item intérêt philosophique (pas de « principe d'omniscience ») ; +\item validité dans un cadre mathématique plus large + ($\rightarrow$ « topos ») ; +\item lien avec les systèmes de typage (via Curry-Howard) ; +\item extraction d'algorithme (p.ex., d'une preuve de $\forall + m. \exists n. P(m,n)$ dans certains systèmes on peut extraire un + algo qui \alert{calcule} $n$ à partir de $m$) ; +\item compatibilité avec des axiomes qui contredisent les maths + classiques (p.ex. « toute fonction $\mathbb{R}\to\mathbb{R}$ est + continue », « toute fonction $\mathbb{N}\to\mathbb{N}$ est + calculable » [$\leftarrow$ « calculabilité synthétique »]) qu'on + peut vouloir étudier. +\end{itemize} + +\end{frame} +% +\begin{frame} +\frametitle{Preuves classiques pas toujours satisfaisantes} + +Que penser de la preuve suivante ? + +\medskip + +\textbf{Affirmation :} Il existe un algo qui donné $k \in +\mathbb{N}$ \alert{termine en temps fini} et renvoie +\begin{itemize} +\item soit le rang de la première occurrence de $k$ chiffres $7$ dans + l'écriture décimale de $\pi$, +\item soit « $\infty$ » si une telle occurrence n'existe pas. +\end{itemize} + +\medskip + +{\footnotesize + +\underline{Preuve} (classique !) : soit $f\colon \mathbb{N} \to +\mathbb{N} \cup \{\infty\}$ la fonction qui à $k$ associe le rang +recherché. + +\alert{De deux choses l'une :} +\begin{itemize} +\item soit il existe $k_0$ tel que $f(k) = \infty$ pour $k\geq k_0$ : + alors $f$ est calculable car $f$ est déterminée par $k_0$ et un + nombre \emph{fini} de valeurs $(f(0),\ldots,f(k_0-1))$ ; +\item soit $f(k)$ est fini pour tout $k \in \mathbb{N}$ : alors $f$ + est calculable par l'algorithme qui, donné $k$, calcule indéfiniment + des décimales de $\pi$ jusqu'à en trouver $k$ consécutives + valant $7$, et renvoie le rang (cet algorithme termine toujours par + hypothèse). +\end{itemize} + +Dans tous les cas $f$ est calculable.\qed +\par} + +\medskip + +\textcolor{blue}{Objection :} cette preuve (correcte en maths +classiques) ne nous donne pas du tout d'algorithme ! Elle montre +juste qu'il « existe » classiquement. + +\end{frame} +% % TODO: % - substitution des variables propositionnelles par des formules % - substitution d'équivalences |