Start a basic set of slides on higher order logic(s).

1 files changed, 227 insertions, 0 deletions

diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex
new file mode 100644
index 0000000..36485c6
--- /dev/null
+++ b/transp-inf110-03-super.tex
@@ -0,0 +1,227 @@
+%% This is a LaTeX document.  Hey, Emacs, -*- latex -*- , get it?
+\documentclass[mathserif,a4paper,aspectratio=169]{beamer}
+%\documentclass[a4paper]{article}
+%\usepackage[envcountsect,noxcolor]{beamerarticle}
+\usepackage[shorthands=off,french]{babel}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{lmodern}
+\DeclareUnicodeCharacter{00A0}{~}
+\DeclareUnicodeCharacter{2026}{...}
+% Beamer theme:
+\usetheme{Goettingen}
+%\usecolortheme{albatross}
+%\usecolortheme{lily}
+%\setbeamercovered{transparent}
+% A tribute to the worthy AMS:
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{amsthm}
+%
+\usepackage{mathrsfs}
+\usepackage{mathpartir}
+%\usepackage{flagderiv}
+%
+\usepackage{graphicx}
+\usepackage{tikz}
+\usetikzlibrary{arrows,automata,calc}
+%
+\newcommand{\itempoint}{\strut\hbox{\color{beamerstructure}\donotcoloroutermaths$\blacktriangleright$}\nobreak\hskip.5em plus.5em\relax}
+\renewcommand{\thefootnote}{\textdagger}
+\newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
+\newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
+%\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}}
+%\newcommand{\dottedland}{\mathbin{\dot\land}}
+%\newcommand{\dottedlor}{\mathbin{\dot\lor}}
+%\newcommand{\dottedtop}{\mathord{\dot\top}}
+%\newcommand{\dottedbot}{\mathord{\dot\bot}}
+%\newcommand{\dottedneg}{\mathop{\dot\neg}}
+\mathchardef\emdash="07C\relax
+\newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}}
+%\setlength{\derivskip}{4pt}
+%
+%
+%
+\title{Logique(s) et typage(s) d'ordre(s) supérieur(s)}
+\subtitle{INF110 (Logique et Fondements de l'Informatique)}
+\author[David Madore]{David A. Madore\\
+{\footnotesize Télécom Paris}\\
+\texttt{david.madore@enst.fr}}
+\date{2023–2024}
+\mode<presentation>{%
+\beamertemplatenavigationsymbolsempty
+\usenavigationsymbolstemplate{\vbox{\hbox{\footnotesize\hyperlinkslideprev{$\leftarrow$}\insertframenumber/\inserttotalframenumber\hyperlinkslidenext{$\rightarrow$}}}}
+}
+\setbeamercolor{myhighlight}{fg=black,bg=white!90!green}
+\colorlet{mydarkgreen}{green!50!black}
+\begin{document}
+\mode<article>{\maketitle}
+%
+\setlength\abovedisplayskip{2pt plus 2pt minus 2pt}
+\setlength\belowdisplayskip{2pt plus 2pt minus 2pt}
+%
+\begin{frame}
+\titlepage
+{\footnotesize\center{\url{http://perso.enst.fr/madore/inf110/transp-inf110.pdf}}\par}
+{\tiny
+\immediate\write18{sh ./vc > vcline.tex}
+\begin{center}
+Git: \input{vcline.tex}
+\end{center}
+\immediate\write18{echo ' (stale)' >> vcline.tex}
+\par}
+\end{frame}
+%
+\section*{Plan}
+\begin{frame}
+\frametitle{Plan}
+\tableofcontents
+\end{frame}
+%
+\section{Les quantificateurs : discussion informelle}
+\begin{frame}
+\frametitle{Limitations du calcul propositionnel}
+
+\itempoint On a parlé pour l'instant de \textbf{calcul
+  propositionnel}, qui ne connaît que les affirmations logiques et les
+connecteurs propositionnels $\Rightarrow,\land,\lor,\top,\bot$.
+
+\medskip
+
+\itempoint Mais il y a deux notations logiques essentielles en
+mathématiques au-delà de ces connecteurs : les
+\textbf{quantificateurs} $\forall,\exists$, qui :
+\begin{itemize}
+\item prennent une formule $P(x)$ dépendant d'une variable $x$ libre,
+\item lient cette variable pour former une nouvelle formule $\forall
+  x. P(x)$ ou $\exists x. P(x)$.
+\end{itemize}
+
+\medskip
+
+\itempoint Intuitivement, il faut penser à $\forall$ et $\exists$
+comme des « $\land$ et $\lor$ en famille », c'est-à-dire que :
+\begin{itemize}
+\item $\forall x.P(x)$, parfois noté $\bigwedge_x P(x)$ est à $P\land
+  Q$ ce que $\prod_i p_i$ est à $p\times q$,
+\item $\exists x.P(x)$, parfois noté $\bigvee_x P(x)$ est à $P\lor Q$
+  ce que $\sum_i p_i$ est à $p + q$.
+\end{itemize}
+
+\medskip
+
+\itempoint Il existe de \alert{nombreux systèmes logiques} différant
+notamment en \alert{ce qu'on a le droit de quantifier} (qui sont les
+$x$ ici ?).
+
+\smallskip
+
+\textcolor{brown}{Commençons par une discussion informelle de
+  $\forall$ et $\exists$.}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{L'interprétation BHK des quantificateurs}
+
+On a déjà vu l'interprétation informelle des connecteurs, on introduit
+maintenant les quantificateurs :
+
+\begin{itemize}
+\item {\color{darkgray} un témoignage de $P\land Q$, est un témoignage
+  de $P$ et un de $Q$,}
+\item {\color{darkgray} un témoignage de $P\lor Q$, est un témoignage
+  de $P$ ou un de $Q$, et la donnée duquel des deux on a choisi,}
+\item {\color{darkgray} un témoignage de $P\Rightarrow Q$ est un moyen
+  de transformer un témoignage de $P$ en un témoignage de $Q$,}
+\item {\color{darkgray} un témoignage de $\top$ est trivial,} \quad
+  \itempoint {\color{darkgray} un témoignage de $\bot$ n'existe pas,}
+\item un témoignage de $\forall x.P(x)$ est un moyen
+  de transformer un $x$ quelconque en un témoignage de $P(x)$,
+\item un témoignage de $\exists x.P(x)$ est la donnée d'un certain
+  $x_0$ et d'un témoignage de $P(x_0)$.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard pour le $\forall$}
+
+\itempoint On a vu que Curry-Howard fait correspondre
+\alert{conjonction logique} $P\land Q$ {\footnotesize (« un témoignage
+  de $P$ et un de $Q$ »)} avec \alert{type produit} $\sigma\times\tau$
+      {\footnotesize (« une valeur de $\sigma$ et une de $\tau$ »)}.
+
+\medskip
+
+\itempoint De façon analogue, la \alert{quantification universelle}
+$\forall x. P(x)$ {\footnotesize (« une façon de transformer $x$ en un
+  témoignage de $P(x)$ »)}, qui est une sorte de \emph{conjonction en
+famille} $\bigwedge_x P(x)$, correspondra au \alert{type produit en
+  famille} $\prod_x \sigma(x)$ {\footnotesize (« fonction renvoyant
+  une valeur de $\sigma(x)$ pour chaque $x$ »)}.
+
+\medskip
+
+\itempoint Ceci présuppose l'existence de \alert{familles de types} $x
+\mapsto \sigma(x)$ (= types dépendant de quelque chose) dont on puisse
+prendre le produit.
+
+\medskip
+
+\itempoint Une preuve de $\forall x.P(x)$ correspondra à un terme de
+forme $\lambda(x:{?}).\,(\cdots)$, où le type de $(\cdots)$ correspond
+à $P(x)$.
+
+\medskip
+
+\itempoint Remarquer que $\forall x.P$, si $P$ ne dépend pas de $x$,
+« ressemble » à $I \Rightarrow P$ de la même manière que $\prod_{i\in
+  I} X = X^I$.  {\footnotesize (Les détails dépendent de la nature de
+  la quantification.)}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard pour le $\exists$}
+
+\itempoint On a vu que Curry-Howard fait correspondre
+\alert{conjonction logique} $P\lor Q$ {\footnotesize (« un témoignage
+  de $P$ ou un de $Q$, avec la donnée duquel on a choisi »)} avec
+\alert{type somme} $\sigma+\tau$ {\footnotesize (« une valeur de
+  $\sigma$ ou une de $\tau$, avec un sélecteur entre les deux »)}.
+
+\medskip
+
+\itempoint De façon analogue, la \alert{quantification existentielle}
+$\exists x. P(x)$ {\footnotesize (« la donnée d'un $x_0$ et d'un
+  témoignage de $P(x_0)$ »)}, qui est une sorte de \emph{disjonction
+en famille} $\bigvee_x P(x)$, correspondra au \alert{type somme en
+  famille} $\sum_x \sigma(x)$ {\footnotesize (« donnée d'un $x_0$ et
+  d'une valeur de type $\sigma(x_0)$ »)}.
+
+\medskip
+
+\itempoint Une preuve de $\exists x.P(x)$ correspondra à un terme de
+forme $\langle x_0, \cdots\rangle$, où le type de $(\cdots)$
+correspond à $P(x_0)$.  {\footnotesize (De nouveau, il faut des
+  « familles de types ».)}
+
+\medskip
+
+\itempoint Remarquer que $\exists x.P$, si $P$ ne dépend pas de $x$,
+« ressemble » à $I \times P$ de la même manière que $\sum_{i\in I} X =
+I\times X$.  {\footnotesize (Les détails dépendent de la nature de la
+  quantification.)}
+
+\medskip
+
+\itempoint Mais Curry-Howard atteint ses limites : il n'est pas dit
+que d'une preuve de $\exists x.P(x)$ on \alert{puisse extraire} le
+$x_0$ correspondant.  {\footnotesize (Les détails dépendent du système
+  logique précis considéré.)}
+
+\end{frame}
+%
+\end{document}