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: 027eae2014fc1fb88d55a11e5dc53ae787f6910a
Parent: d873288e25d7e09f220f8b48bde92434834b2357
Author: Pablo <pablo-escobar@riseup.net>
Date: Sat, 15 Oct 2022 12:33:11 +0000

Adjusted the notation of the natural decduction formulas

Diffstat

1 file changed, 14 insertions, 14 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	main.tex	28	14	14

diff --git a/main.tex b/main.tex
@@ -26,25 +26,26 @@
       \[
         \begin{array}{cc}
           \displaystyle{
-            \frac{\Gamma \vdash_\Sigma a : A \quad \Gamma \vdash_\Sigma b : B}
-                 {\Gamma \vdash_\Sigma \operatorname{intro} a \ b : A \wedge B}
+            \frac
+            {\Gamma \vdash_\Sigma h_1 : P \quad \Gamma \vdash_\Sigma h_2 : Q}
+            {\Gamma \vdash_\Sigma \operatorname{intro} h_1 \ h_2 : P \wedge Q}
             \rightarrow C
           } &
           \displaystyle{
             \frac{
-              \Gamma \vdash_\Sigma a : A \quad
-              \Gamma \vdash_\Sigma f : A \supset B
-            }{\Gamma \vdash_\Sigma f a : B}
+              \Gamma \vdash_\Sigma h : P \quad
+              \Gamma \vdash_\Sigma f : P \supset Q
+            }{\Gamma \vdash_\Sigma f \ h : Q}
             \rightarrow E
           } \\ \\
           \displaystyle{
-            \frac{\Gamma \vdash_\Sigma a : A}
-                 {\Gamma \vdash_\Sigma \operatorname{inl} a : A \vee B}
+            \frac{\Gamma \vdash_\Sigma h : P}
+                 {\Gamma \vdash_\Sigma \operatorname{inl} h : P \vee Q}
             \rightarrow D_1
           } &
           \displaystyle{
-            \frac{\Gamma \vdash_\Sigma b : B}
-                 {\Gamma \vdash_\Sigma \operatorname{inr} b : A \vee B}
+            \frac{\Gamma \vdash_\Sigma h : Q}
+                 {\Gamma \vdash_\Sigma \operatorname{inr} h : P \vee Q}
             \rightarrow D_2
           }
         \end{array}
@@ -453,14 +454,13 @@
            {Understanding typing judgments}
   \end{enumerate}
   \begin{align*}
-    \frac{\Gamma \vdash_\Sigma a : A}
-         {\Gamma \vdash_\Sigma \operatorname{inl} a : A \vee B}
+    \frac{\Gamma \vdash_\Sigma h : P}
+         {\Gamma \vdash_\Sigma \operatorname{inl} h : P \vee Q}
     \rightarrow D_1
     & &
-    \frac{\Gamma \vdash_\Sigma b : B}
-         {\Gamma \vdash_\Sigma \operatorname{inr} b : A \vee B}
+    \frac{\Gamma \vdash_\Sigma h : P}
+         {\Gamma \vdash_\Sigma \operatorname{inr} h : P \vee Q}
     \rightarrow D_2
   \end{align*}
 \end{frame}
 \end{document}
-