curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

git clone: git://git.pablopie.xyz/curry-howard
Log
Files
Refs
README
LICENSE

Commit: 99d53451a56166373e7d70d11722162dc0ab0354
Parent: d059a165a8966d210fd5c9adf45a5336edf66322
Author: Pablo <pablo-escobar@riseup.net>
Date: Sun, 9 Oct 2022 01:34:35 +0000

Started to rework the section on proposition as types

Diffstat

1 file changed, 22 insertions, 29 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	sections/curry.tex	51	22	29

diff --git a/sections/curry.tex b/sections/curry.tex
@@ -1,21 +1,5 @@
-\section{Provadores de Teoremas}
-
 \begin{frame}[fragile]{Métodos Não-Numéricos?}
   \begin{itemize}
-    \item E se as contas que eu preciso fazer não são \emph{numéricas}?
-      \begin{itemize}
-        \item Indução é conta
-
-          \pause
-
-        \item Continhas em algebra abstrata
-      \end{itemize} \pause
-      \[
-        n! \cdot m! \mid (n + m)!
-      \]
-
-      \pause
-
     \item Antes de tentar provar meu teorema, eu preciso enunciar ele\dots
   \end{itemize}
 
@@ -123,12 +107,17 @@
 \subsection{A Correspondência de Curry-Howard}
 
 \begin{frame}{A Correspondência de Curry-Howard}
-  \begin{itemize}
-    \item Provar que vale \(A\) é o mesmo que mostrar que \(\{\text{provas de}\
-      A\} \ne \emptyset\)
-
-      \pause
+  \begin{center}
+    \begin{tabular}{rcl}
+      Provar que vale \(A\) 
+        & \(\leftrightsquigarrow\) 
+        & Encontrar \(a \in \{ \text{provas de}\ A\}\)
+    \end{tabular}
+  \end{center}
+  
+  \pause
 
+  \begin{itemize}
     \item Proposições como tipos 
       \begin{center}
         \begin{tabular}{rcl}
@@ -149,11 +138,7 @@
 
       \pause
 
-    \item Mas como eu represento isso num computador?
-
-      \pause
-
-    \item Tipos
+    \item Mas como eu represento isso num computador? \pause Tipos!
       \begin{figure}
         \centering
         \inputminted{python}{examples/types.py}
@@ -170,10 +155,18 @@
       \end{figure}
 
     \item Linguagens estaticamente tipadas
-
-    \item Provar que vale \(A\) corresponde a construir um elemento do tipo
-      \(\{\text{provas de}\ A\}\)
   \end{itemize}
+
+  \begin{center}
+    \begin{tabular}{rcl}
+      Provar que vale \(A\) 
+        & \(\leftrightsquigarrow\) 
+        & Construir \(a : \{ \text{provas de}\ A\}\) \\
+      Checar a prova
+        & \(\leftrightsquigarrow\) 
+        & Checar os tipos
+    \end{tabular}
+  \end{center}
 \end{frame}
 
 \begin{frame}{Provadores de Teoremas}