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: cbc4358fe1b152aac415886933cdcdb6a8f16c4b
Parent: f8e84114c03abad5a851e93458687d8583cae978
Author: Pablo <pablo-escobar@riseup.net>
Date: Thu, 13 Oct 2022 21:53:02 +0000

Changed the notation for propositions

Also added a link to a talk on the idea of propositions as types

Also added decorative formulas to the last slide

Diffstat

4 files changed, 43 insertions, 27 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	examples/example.lean	4	2	2
Modified	examples/types.lean	12	6	6
Modified	examples/types.py	10	5	5
Modified	main.tex	44	30	14

diff --git a/examples/example.lean b/examples/example.lean
@@ -3,5 +3,5 @@ lemma ex : or p q → or q p := by
   match h with
   | inl h1 =>
     exact inr h1
-  | inr h1 =>
-    exact inl h1
+  | inr h2 =>
+    exact inl h2

diff --git a/examples/types.lean b/examples/types.lean
@@ -1,7 +1,7 @@
--- a e b <-> and a b
-inductive and (a b : Prop) : Prop
-| intro : a → b → and a b
+-- p e q <-> and p q
+inductive and (p q : Prop) : Prop
+| intro : p → q → and p q
 
-inductive or (a b : Prop) : Prop
-| inl : a → or a b
-| inr : b → or a b
+inductive or (p q : Prop) : Prop
+| inl : p → or p q
+| inr : q → or p q

diff --git a/examples/types.py b/examples/types.py
@@ -1,5 +1,5 @@
-class AndAB:
-    """A e B <-> AndAB"""
-    def __init__(self, a: A, b: B):
-        self.left = a
-        self.right = b
+class AndPQ:
+    """P e Q <-> AndPQ"""
+    def __init__(self, h1: P, h2: Q):
+        self.left = h1
+        self.right = h2

diff --git a/main.tex b/main.tex
@@ -203,9 +203,9 @@
 \begin{frame}{A Correspondência de Curry-Howard}
   \begin{center}
     \begin{tabular}{rcl}
-      Provar que vale \(A\)
+      Provar que vale \(P\)
         & \(\leftrightsquigarrow\)
-        & Encontrar \(a \in \{ \text{provas de}\ A\}\)
+        & Encontrar \(h \in \{ \text{provas de}\ P\}\)
     \end{tabular}
   \end{center}
 
@@ -215,18 +215,18 @@
     \item Proposições como tipos
       \begin{center}
         \begin{tabular}{rcl}
-          \(A\)
+          \(P\)
             & \(\leftrightsquigarrow\)
-            & \(\{\text{provas de}\ A \}\) \\
-          \(A\ \text{e}\ B\)
+            & \(\{\text{provas de}\ P \}\) \\
+          \(P\ \text{e}\ Q\)
             & \(\leftrightsquigarrow\)
-            & \(\{\text{provas de}\ A \} \times \{\text{provas de}\ B \}\) \\
-          \(A\ \text{ou}\ B\)
+            & \(\{\text{provas de}\ P \} \times \{\text{provas de}\ Q \}\) \\
+          \(P\ \text{ou}\ Q\)
             & \(\leftrightsquigarrow\)
-            & \(\{\text{provas de}\ A \} \cup \{\text{provas de}\ B \}\) \\
-          \(A \implies B\)
+            & \(\{\text{provas de}\ P \} \cup \{\text{provas de}\ Q \}\) \\
+          \(P \implies Q\)
             & \(\leftrightsquigarrow\)
-            & \(\{\text{provas de}\ A \} \to \{\text{provas de}\ B \}\) \\
+            & \(\{\text{provas de}\ P \} \to \{\text{provas de}\ Q \}\) \\
         \end{tabular}
       \end{center}
 
@@ -255,12 +255,15 @@
 
   \begin{center}
     \begin{tabular}{rcl}
-      Provar que vale \(A\)
+      Provar que vale \(P\)
         & \(\leftrightsquigarrow\)
-        & Construir \(a : \{ \text{provas de}\ A\}\) \\
+        & Construir \(h : \{ \text{provas de}\ P\}\) \\
       Checar a prova
         & \(\leftrightsquigarrow\)
-        & Checar os tipos
+        & Checar os tipos \\
+      Inconsistência na prova
+        & \(\leftrightsquigarrow\)
+        & Tipos não batem
     \end{tabular}
   \end{center}
 \end{frame}
@@ -317,7 +320,7 @@
   \end{itemize}
 \end{frame}
 
-\begin{frame}{Provadores de Teoremas}
+\begin{frame}{Proof Checkers}
   \begin{itemize}
     \item Coq (\url{https://coq.inria.fr/})
 
@@ -442,9 +445,22 @@
            {Advancing mathematics by guiding human intuition with AI}
 
     \item
+      \href{https://www.youtube.com/watch?v=IOiZatlZtGU}
+           {Propositions as Types}
+
+    \item
       \href{https://www.hedonisticlearning.com/posts/understanding-typing-judgments.html}
            {Understanding typing judgments}
   \end{enumerate}
+  \begin{align*}
+    \frac{\Gamma \vdash_\Sigma a : A}
+         {\Gamma \vdash_\Sigma \operatorname{inl} a : A \vee B}
+    \rightarrow D_1
+    & &
+    \frac{\Gamma \vdash_\Sigma b : B}
+         {\Gamma \vdash_\Sigma \operatorname{inr} b : A \vee B}
+    \rightarrow D_2
+  \end{align*}
 \end{frame}
 \end{document}