1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
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}
|
