%% 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}