From: Francesco Mazzoli <f@mazzo.li>
Date: Sun, 23 Jun 2013 12:56:03 +0000 (+0100)
Subject: presentation
X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=f4c389ead3069b573423493b294ff9de82406930

presentation
---

diff --git a/presentation.tex b/presentation.tex
index 3492be8..b0398e8 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -279,6 +279,16 @@
   usable.
 \end{frame}
 
+\begin{frame}
+  \frametitle{Theorem provers, dependent types}
+  \begin{center}
+    \Huge
+    types $\leftrightarrow$ propositions
+
+    programs $\leftrightarrow$ proofs
+  \end{center}
+\end{frame}
+
 \begin{frame}
   \frametitle{Theorem provers, dependent types} First class types: we
   can return them, have them as arguments, etc.
@@ -358,6 +368,10 @@
   \only<2>{
   The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
   \[\myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]}
+  \only<3>{
+    Remember:
+    \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
+  }
 \end{frame}
 
 \begin{frame}
@@ -370,26 +384,7 @@
   Or
   \[ \myfun{head} \myappsp \mylistt{3} : \myunit \myarr \mynat \]
 
-  Will $\mytt : \myunit$ do as an argument?  In other words, when type
-  checking, do we have that
-  \[
-  \begin{array}{@{}c@{\ }c@{\ }c}
-    \myunit & \mydefeq & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
-    \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \mydefeq & \myempty \\
-    (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \mydefeq & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
-    & \vdots &
-  \end{array}
-  \]
-  ?
-\end{frame}
-
-\begin{frame}
-  \frametitle{Definitional equality}
-  
-  The type checker needs a notion of equality between types.
-
-  We reduce terms `as far as possible' (to their \emph{normal form}) and
-  then compare them syntactically:
+  Yes: to typecheck, we reduce terms fully before comparing:
   \[
   \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
     \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
@@ -398,36 +393,44 @@
     & & & \vdots & & & 
   \end{array}
   \]
-
-  This equality, $\mydefeq$, takes the name of \emph{definitional} equality.
-  % TODO add break
+  \[
+  \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
+  \]
 \end{frame}
 
 \begin{frame}
   \frametitle{Propositional equality} Using definitional equality, we
   can give the user a type-level notion of term equality.
   \[
-  (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp
+  (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
   \]
-  We introduce members of $\myeq$ by reflexivity:
+  We introduce members of $\myeq$ by reflexivity, for example
   \[
-  \myrefl\myappsp\mytmt : \mytmt \myeq \mytmt
+  \myrefl\myappsp5 : 5 \myeq 5
   \]
-  So that $\myrefl$ will relate definitionally equal terms:
+  But also
   \[
-  \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\ \text{since}\ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+  \begin{array}{@{}l}
+  \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
+  (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+  \end{array}
   \]
   Then we can use a substitution law to derive other
   laws---transitivity, congruence, etc.
+  \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
 \end{frame}
 
 \begin{frame}
 \frametitle{The problem with prop. equality}
 Going back to $\myfun{map}$, we can prove that
 \[    \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}.\ (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l}    \]
-Because we can prove, by induction on $\myb{l}$, that we will always get definitionally equal lists.
+Because
+\[
+(\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g})\myappsp \myb{l} \mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l}
+\]
+By induction on $\myb{l}$.
 
-But without the $\myb{l}$, we cannot compute, so we are stuck with
+Without the $\myb{l}$ we cannot compute, so we are stuck with
 \[
 \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
 \]
@@ -437,14 +440,20 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   \frametitle{Observational equality}
 
   Instead of basing its equality on definitional equality, look at the
-  structure of the type to decide:
+  structure of the type to decide.
+
+  For functions this will mean that proving
   \[
-  \begin{array}{@{}l}
-    (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} : \mylistt{\myse{A_1}} \myarr \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) : \mylistt{\myse{A_2}} \myarr \mylistt{\myse{C_2}}) \myred \\
-    \myind{2} (\myse{l_1} : \mylistt{\myse{A_1}}) \myarr (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr (\myse{l_1} : \mylistt{\myse{A_1}}) \myeq (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr \\
-    \myind{2} ((\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_2}})
-  \end{array}
+    \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
+  \]
+  Will reduce to proving that
+  \[
+  (\myb{l} : \mylist{\myb{A}}) \myarr 
+    (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g})\myappsp\myb{l} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})\myappsp \myb{l}
   \]
+  Which is what we want.  The interesting part is how to make the system
+  compute nicely.
+  
   This extends to other structures (tuples, inductive types, \dots).
   Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
   values from one to the other.
@@ -542,6 +551,8 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
     \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
   \end{array}
   \]
+  In logic this would be
+  \[ \exists x \in \mathbb{N}.\ even(x) \]
 \end{frame}
 
 \begin{frame}
@@ -581,7 +592,14 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   \begin{itemize}
   \item Describe when two types formed by the defined type constructors
     are equal;
+    \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
   \item Describe when two values of the defined type are equal;
+    \[
+    \begin{array}{@{}c@{\ \ \ \ \ \ }c}
+      \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
+      \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
+    \end{array}
+    \]
   \item Describe how to transport values of the defined type.
   \end{itemize}
 \end{frame}