curry-howard
Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
main.tex (11632B)
1 \def\hidepauses{yes} 2 \input{preamble} 3 4 \definecolor{hacker}{RGB}{4,165,90} 5 6 \title{Como provar teoremas em um computador?} 7 \author{Pablo \\ \texttt{pablopie.xyz}} 8 \date{Outubro de 2022} 9 10 \begin{document} 11 \begin{frame} 12 \maketitle 13 \end{frame} 14 15 \begin{frame}{Disclaimer} 16 \begin{itemize} 17 \item Hacker\dots 18 \begin{figure} 19 \centering 20 \BVerbatimInput[formatcom=\color{hacker}]{examples/hacker.txt} 21 \end{figure} 22 23 \pause 24 25 \item Dedução natural\dots 26 \[ 27 \begin{array}{cc} 28 \displaystyle{ 29 \frac 30 {\Gamma \vdash_\Sigma h_1 : P \quad \Gamma \vdash_\Sigma h_2 : Q} 31 {\Gamma \vdash_\Sigma \operatorname{intro} h_1 \ h_2 : P \wedge Q} 32 \rightarrow C 33 } & 34 \displaystyle{ 35 \frac{ 36 \Gamma \vdash_\Sigma h : P \quad 37 \Gamma \vdash_\Sigma f : P \supset Q 38 }{\Gamma \vdash_\Sigma f \ h : Q} 39 \rightarrow E 40 } \\ \\ 41 \displaystyle{ 42 \frac{\Gamma \vdash_\Sigma h : P} 43 {\Gamma \vdash_\Sigma \operatorname{inl} h : P \vee Q} 44 \rightarrow D_1 45 } & 46 \displaystyle{ 47 \frac{\Gamma \vdash_\Sigma h : Q} 48 {\Gamma \vdash_\Sigma \operatorname{inr} h : P \vee Q} 49 \rightarrow D_2 50 } 51 \end{array} 52 \] 53 54 \pause 55 56 \item Não precisa entender o código! 57 58 \pause 59 60 \item Me interrompa! 61 \end{itemize} 62 \end{frame} 63 64 \begin{frame}{Como provar teoremas em um computador?} 65 \begin{columns} 66 \begin{column}{.35\linewidth} 67 \begin{figure} 68 \centering 69 \includegraphics[width=\linewidth]{images/kepler.eps} 70 \end{figure} 71 \end{column} 72 \begin{column}{.65\linewidth} 73 \begin{itemize} 74 \item Se eu tenho um número finito de casos\dots\ posso testar todos os 75 casos! 76 \begin{figure} 77 \centering 78 \inputminted{python}{examples/exhaustion.py} 79 \end{figure} 80 \end{itemize} 81 82 \pause 83 84 \begin{theorem}[Conjectura de Kepler] 85 Nenhum arranjo de esferas em três dimensões tem uma densidade média 86 maior do que o arranjo cúbico. 87 \end{theorem} 88 89 \begin{itemize} 90 \item Provado em 1998 por Thomas Hales via exaustão 91 92 \pause 93 94 \item E se o número de casos não for finito??? 95 \end{itemize} 96 \end{column} 97 \end{columns} 98 \end{frame} 99 100 \begin{frame}[fragile]{Como provar teoremas em um computador?} 101 \begin{itemize} 102 \item Antes de tentar provar meu teorema, eu preciso enunciar ele\dots 103 \end{itemize} 104 105 \pause 106 107 \begin{columns} 108 \begin{column}{.5\linewidth} 109 \[ 110 n! = 111 \begin{cases} 112 1 & \text{se}\ n = 0 \\ 113 n \cdot (n - 1)! & \text{se}\ n > 0 114 \end{cases} 115 \] 116 \end{column} 117 \begin{column}{.5\linewidth} 118 \inputminted{python}{examples/factorial.py} 119 \end{column} 120 \end{columns} 121 122 \pause 123 124 \begin{columns} 125 \begin{column}{.5\linewidth} 126 \[ 127 n! \cdot m! \mid (n + m)! 128 \] 129 \end{column} 130 \begin{column}{.5\linewidth} 131 \begin{minted}{python} 132 # ??? 133 \end{minted} 134 \end{column} 135 \end{columns} 136 137 \pause 138 139 \begin{itemize} 140 \item Temos termos, mas não temos formulas! 141 \end{itemize} 142 143 \begin{figure} 144 \centering 145 \begin{tabular}{|l|l|} 146 \hline 147 Termos 148 & Fórmulas \\ 149 \hline 150 Um número \(n\) 151 & ``\(n > m\)'' \\ 152 \hline 153 Um conjunto \(X\) 154 & ``\(x \in X\)'' \\ 155 \hline 156 Pontos, retas, planos, \dots 157 & O quinto postulado de Euclides \\ 158 \hline 159 \end{tabular} 160 \end{figure} 161 \end{frame} 162 163 \begin{frame}[fragile]{Como provar teoremas um computador?} 164 \begin{itemize} 165 \item Objection! 166 \end{itemize} 167 168 \begin{columns} 169 \begin{column}{.3\linewidth} 170 \[ 171 n! \cdot m! \mid (n + m)! 172 \] 173 \end{column} 174 \begin{column}{.5\linewidth} 175 \inputminted{python}{examples/fake-theorem.py} 176 \end{column} 177 \end{columns} 178 179 \pause 180 181 \begin{align*} 182 p : \mathbb{N} \times \mathbb{N} & \to \{0, 1\} \\ 183 (n, m) & \mapsto 184 \begin{cases} 185 1 & \text{se}\ n! \cdot m! \mid (n + m) ! \\ 186 0 & \text{caso contrário} \\ 187 \end{cases} 188 \end{align*} 189 190 \pause 191 192 \begin{itemize} 193 \item Nenhum computador é capaz de checar que \(p(n, m) = 1\) para todos 194 \(n, m\) 195 \begin{figure} 196 \centering 197 \inputminted{python}{examples/exhaustion-naive.py} 198 \end{figure} 199 \end{itemize} 200 \end{frame} 201 202 \begin{frame}{A Correspondência de Curry-Howard} 203 \begin{center} 204 \begin{tabular}{rcl} 205 Provar que vale \(P\) 206 & \(\leftrightsquigarrow\) 207 & Encontrar \(h \in \{ \text{provas de}\ P\}\) 208 \end{tabular} 209 \end{center} 210 211 \pause 212 213 \begin{itemize} 214 \item Proposições como tipos 215 \begin{center} 216 \begin{tabular}{rcl} 217 \(P\) 218 & \(\leftrightsquigarrow\) 219 & \(\{\text{provas de}\ P \}\) \\ 220 \(P\ \text{e}\ Q\) 221 & \(\leftrightsquigarrow\) 222 & \(\{\text{provas de}\ P \} \times \{\text{provas de}\ Q \}\) \\ 223 \(P\ \text{ou}\ Q\) 224 & \(\leftrightsquigarrow\) 225 & \(\{\text{provas de}\ P \} \cup \{\text{provas de}\ Q \}\) \\ 226 \(P \implies Q\) 227 & \(\leftrightsquigarrow\) 228 & \(\{\text{provas de}\ P \} \to \{\text{provas de}\ Q \}\) \\ 229 \end{tabular} 230 \end{center} 231 232 \pause 233 234 \item Mas como eu represento isso num computador? \pause Tipos! 235 \begin{figure} 236 \centering 237 \inputminted{python}{examples/types.py} 238 \end{figure} 239 \end{itemize} 240 \end{frame} 241 242 \begin{frame}[fragile]{A Correspondência de Curry-Howard} 243 \begin{itemize} 244 \item Computadores são muito bons em checar tipos! 245 \begin{figure} 246 \centering 247 \inputminted{c}{examples/typechecking.c} 248 \end{figure} 249 250 \pause 251 252 \item Linguagens estaticamente tipadas 253 \end{itemize} 254 255 \begin{center} 256 \begin{tabular}{rcl} 257 Provar que vale \(P\) 258 & \(\leftrightsquigarrow\) 259 & Construir \(h : \{ \text{provas de}\ P\}\) \\ 260 Checar a prova 261 & \(\leftrightsquigarrow\) 262 & Checar os tipos \\ 263 Inconsistência na prova 264 & \(\leftrightsquigarrow\) 265 & Tipos não batem 266 \end{tabular} 267 \end{center} 268 \end{frame} 269 270 \begin{frame}{A Correspondência de Curry-Howard} 271 \begin{itemize} 272 \item Mas como isso funciona na prática? 273 \begin{figure} 274 \centering 275 \inputminted{python}{examples/types.py} 276 \end{figure} 277 278 \pause 279 280 \begin{figure} 281 \centering 282 \inputminted{lean}{examples/types.lean} 283 \end{figure} 284 285 \item Tipos algébricos! 286 \end{itemize} 287 \end{frame} 288 289 \begin{frame}{A Correspondência de Curry-Howard} 290 \begin{itemize} 291 \item Axiomas! 292 \begin{itemize} 293 \item Dados \(x\) e \(y\), existe o tipo \texttt{x = y} das provas de 294 que \(x = y\) 295 296 \begin{figure} 297 \centering 298 \inputminted{lean}{examples/eq.lean} 299 \end{figure} 300 301 \pause 302 303 \item O tipo \texttt{x = x} tem um único elemento \texttt{rfl} 304 \end{itemize} 305 306 \pause 307 308 \item O tipo \texttt{x = y} varia com \(x\) e \(y\) 309 310 \item Tipos dependentes! 311 312 \pause 313 314 \item Codifico meus objetos como tipos 315 \begin{figure} 316 \centering 317 \inputminted{lean}{examples/nat.lean} 318 \end{figure} 319 \end{itemize} 320 \end{frame} 321 322 \begin{frame}{Proof Checkers} 323 \begin{itemize} 324 \item Coq (\url{https://coq.inria.fr/}) 325 326 \item Agda (\url{https://wiki.portal.chalmers.se/agda/pmwiki.php}) 327 328 \item Lean (\url{https://leanprover.github.io/}) 329 330 \item Idris (\url{https://www.idris-lang.org/}) 331 332 \item Isabelle (\url{https://isabelle.in.tum.de/}) 333 \end{itemize} 334 335 \begin{columns} 336 \begin{column}{.1\linewidth} 337 \begin{figure} 338 \centering 339 \includegraphics[width=\linewidth]{images/coq.png} 340 \end{figure} 341 \end{column} 342 \begin{column}{.45\linewidth} 343 \begin{figure} 344 \centering 345 \includegraphics[width=\linewidth]{images/agda.eps} 346 \end{figure} 347 \end{column} 348 \begin{column}{.25\linewidth} 349 \begin{figure} 350 \centering 351 \includegraphics[width=\linewidth]{images/lean.eps} 352 \end{figure} 353 \end{column} 354 \end{columns} 355 \end{frame} 356 357 \begin{frame}[fragile]{Lean} 358 \begin{columns} 359 \begin{column}{.45\linewidth} 360 \begin{figure}[t] 361 \centering 362 \inputminted{lean}{examples/example.lean} 363 \end{figure} 364 \end{column} \pause 365 \begin{column}{.40\linewidth} 366 \begin{itemize} 367 \item 368 \href{https://leanprover-community.github.io/mathlib-overview.html}{mathlib} 369 \begin{itemize} 370 \item Álgebra abstrata 371 372 \item Topologia 373 374 \item Geometria diferencial 375 376 \item Teoria dos números 377 378 \item Análise funcional 379 380 \item \dots 381 \end{itemize} 382 \end{itemize} 383 \end{column} 384 \end{columns} 385 386 \pause 387 388 \begin{figure} 389 \centering 390 \inputminted{lean}{examples/liquid.lean} 391 \end{figure} 392 \end{frame} 393 394 \begin{frame}{Pra que tudo isso?} 395 \begin{columns} 396 \begin{column}[t]{.65\linewidth} 397 \begin{itemize} 398 \item<2-> Verificação formal de software e hardware \pause 399 \begin{itemize} 400 \item<3-> O bug do Pentium de 1994 401 402 \item<4-> A queda do voo 302 da Ethiopian Airlines em 2019 403 \end{itemize} 404 405 \item<5-> Provas de alta complexidade 406 \begin{itemize} 407 \item<5-> Classificação dos grupos simples finitos 408 409 \item<5-> A prova de Mochizuki da conjetura abc 410 411 \item<6-> A prova de Hales da conjectura de Kepler de 2015! 412 413 \item<6-> 414 A conclusão do 415 \emph{\href{https://leanprover-community.github.io/liquid/}{Liquid 416 Tensor Experiment}} em julho de 2022! 417 \end{itemize} 418 419 \item<7-> \emph{Who watches the Watchmen?} 420 \includegraphics[height=1em]{images/watchmen.eps} 421 \end{itemize} 422 \end{column} 423 \begin{column}[t]{.25\linewidth} 424 \begin{figure}[t] 425 \includegraphics[width=\linewidth]{images/pentium.png} 426 \end{figure} 427 \end{column} 428 \end{columns} 429 \end{frame} 430 431 \begin{frame}{Links} 432 \begin{enumerate} 433 \item 434 \href{https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/} 435 {The Natural Number Game} 436 \item 437 \href{https://leanprover-community.github.io/blog/posts/lte-final/} 438 {Completion of the Liquid Tensor Experiment} 439 440 \item 441 \href{https://www.youtube.com/watch?v=T9ZqbQh-t9E} 442 {Machine-Assisted Proofs} 443 444 \item 445 \href{https://www.nature.com/articles/s41586-021-04086-x} 446 {Advancing mathematics by guiding human intuition with AI} 447 448 \item 449 \href{https://www.youtube.com/watch?v=IOiZatlZtGU} 450 {Propositions as Types} 451 452 \item 453 \href{https://www.hedonisticlearning.com/posts/understanding-typing-judgments.html} 454 {Understanding typing judgments} 455 \end{enumerate} 456 \begin{align*} 457 \frac{\Gamma \vdash_\Sigma h : P} 458 {\Gamma \vdash_\Sigma \operatorname{inl} h : P \vee Q} 459 \rightarrow D_1 460 & & 461 \frac{\Gamma \vdash_\Sigma h : P} 462 {\Gamma \vdash_\Sigma \operatorname{inr} h : P \vee Q} 463 \rightarrow D_2 464 \end{align*} 465 \end{frame} 466 \end{document}