congruence rules for the globular cbpv

paper/gtt.tex

@@ -174,10 +174,12 @@
 \newcommand{\kw}[1]{\text{#1}\,\,}
 \newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
 \newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1 \kw{to} (#2,#3). #4}
-\newcommand{\pmmuXtoYinZ}[4]{\kw{unroll} #1 \kw{to} \roll #2. #3}
+\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \kw{to} \roll #2. #3}
 \newcommand{\ret}{\text{ret}\,\,}
 \newcommand{\thunk}{\text{thunk}\,\,}
 \newcommand{\force}{\text{force}\,\,}
+\newcommand{\abort}{\kw {abort}}
+\newcommand{\with}{\mathop{\&}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
@@ -718,10 +720,6 @@ While we have shown
 
 \subsection{Uniqueness Principles for Casts}
 
-From the axiomatics of Gradual Type Theory, we can derive many
-consequences.
-
-
 \section{Contract Translation to Call-by-push-value}
 
 \subsection{Call-by-push-value operational semantics}
@@ -769,7 +767,130 @@ corecursive type.
 Next, we give the inequational theory for our CBPV language.
 %
 
+\begin{figure}
+  \begin{mathpar}
+    \inferrule
+    {}
+    {\Gamma,x : A,\Gamma' \vdash x \ltdyn x : A}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : A \and
+      \Gamma, x : A \vdash M \ltdyn M' : \u B
+    }
+    {\Gamma \vdash \letXbeYinZ V x M \ltdyn \letXbeYinZ {V'} {x} {M'} : \u B}
+
+    \inferrule
+    {\Gamma \vdash V : 0}
+    {\Gamma \vdash \abort V : \u B}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : A_1}
+    {\Gamma \vdash \inl V \ltdyn \inl V' : A_1 + A_2}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : A_2}
+    {\Gamma \vdash \inr V \ltdyn \inr V' : A_1 + A_2}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : A_1 + A_2\and
+      \Gamma, x_1 : A_1 \vdash M_1 \ltdyn M_1' : \u B\and
+      \Gamma, x_2 : A_2 \vdash M_2 \ltdyn M_2' : \u B
+    }
+    {\Gamma \vdash \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2} \ltdyn \caseofXthenYelseZ {V'} {x_1. M_1'}{x_2.M_2'} : \u B}
 
+    \inferrule
+    {}
+    {\Gamma \vdash () \ltdyn () : 1}
+
+    \inferrule
+    {\Gamma \vdash V_1 \ltdyn V_1' : A_1\and
+      \Gamma\vdash V_2 \ltdyn V_2' : A_2}
+    {\Gamma \vdash (V_1,V_2) \ltdyn (V_1',V_2') : A_1 \times A_2}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : A_1 \times A_2\and
+      \Gamma, x : A_1,y : A_2 \vdash M \ltdyn M' : \u B
+    }
+    {\Gamma \vdash \pmpairWtoXYinZ V x y M \ltdyn \pmpairWtoXYinZ {V'} {x} {y} {M'} : \u B}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : A[\mu X.A/X]}
+    {\Gamma \vdash \rollty{\mu X.A} V \ltdyn \rollty{\mu X.A} V' : \mu X.A }
+    
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : \mu X. A\and
+      \Gamma, x : A[\mu X. A/X] \vdash M \ltdyn M' : \u B}
+    {\Gamma \vdash \pmmuXtoYinZ V x M \ltdyn \pmmuXtoYinZ {V'} {x} {M'} : \u B}
+
+    \inferrule
+    {\Gamma \vdash M \ltdyn M' : \u B}
+    {\Gamma \vdash \thunk M \ltdyn \thunk M' : U \u B}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : U \u B}
+    {\Gamma \vdash \force V \ltdyn \force V' : \u B}
+
+    \inferrule
+    {\Gamma \vdash V \ltdyn V' : A}
+    {\Gamma \vdash \ret V \ltdyn \ret V' : \u F A}
+
+    \inferrule
+    {\Gamma \vdash M \ltdyn M' : \u F A\and
+      \Gamma, x: A \vdash N \ltdyn N' : \u B}
+    {\Gamma \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x} {N'} : \u B}
+
+    \inferrule
+    {\Gamma, x: A \vdash M \ltdyn M' : \u B}
+    {\Gamma \vdash \lambda x : A . M \ltdyn \lambda x:A. M' : A \to \u B}
+
+    \inferrule
+    {\Gamma \vdash M \ltdyn M' : A \to \u B\and
+      \Gamma \vdash V \ltdyn V' : A}
+    {\Gamma \vdash M\,V \ltdyn M'\,V' : \u B }
+
+    \inferrule
+    {\Gamma \vdash M_1 \ltdyn M_1' : A_1\and
+      \Gamma \vdash M_2 \ltdyn M_2' : A_2}
+    {\Gamma \vdash \pair {M_1} {M_2} \ltdyn \pair {M_1'} {M_2'} : A_1 \with A_2}
+
+    \inferrule
+    {\Gamma \vdash M \ltdyn M' : A_1 \with A_2}
+    {\Gamma \vdash \pi M \ltdyn \pi M' : A_1}
+
+    \inferrule
+    {\Gamma \vdash M \ltdyn M' : A_1 \with A_2}
+    {\Gamma \vdash \pi' M \ltdyn \pi' M' : A_2}
+
+    \inferrule
+    {\Gamma \vdash M \ltdyn M' : \u B[{\nu \u Y. \u B}/\u Y]}
+    {\Gamma \vdash \rollty{\nu \u Y. \u B} M \ltdyn \rollty{\nu \u Y. \u B} M' : {\nu \u Y. \u B}}
+
+    \inferrule
+    {\Gamma \vdash M \ltdyn M' : {\nu \u Y. \u B}}
+    {\Gamma \vdash \unroll M \ltdyn \unroll M' : \u B[{\nu \u Y. \u B}/\u Y]}
+  \end{mathpar}
+  \caption{Call-by-push-value Inequational Theory (Congruence Rules)}
+\end{figure}
+
+\begin{figure}
+  \begin{mathpar}
+    \inferrule
+    {}
+    {\Gamma \vdash \err \ltdyn M : \u B}
+
+    \inferrule
+    {\Gamma \vdash M_1 \ltdyn M_2 : \u B\and
+      \Gamma \vdash M_2 \ltdyn M_3 : \u B}
+    {\Gamma \vdash M_1 \ltdyn M_3 : \u B}
+
+    \inferrule
+    {\Gamma \vdash V_1 \ltdyn V_2 : A\and
+      \Gamma \vdash V_2 \ltdyn V_3 : A}
+    {\Gamma \vdash V_1 \ltdyn V_3 : A}
+  \end{mathpar}
+  \caption{CBPV Inequational Theory Part 2}
+  
+\end{figure}
 
 \subsection{Cast to Contract Translation}