diff --git a/paper/gtt.tex b/paper/gtt.tex
index 466ca070c64c5abea076b2c850d83cc62d51965a..db65307516a7d625b416e3abe82643dd38ea701b 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2709,10 +2709,9 @@ typed version of scheme's \emph{case-lambda} construct.
Because we give the dynamic types the universal property of a
sum/lazy product type respectively, we can derive the
implementations of the ``checking'' casts.
-
- We could just invoke the uniqueness of adjoints to prove these, but
- we present a few proofs \emph{in} GTT because they are somewhat
- interesting.
+ %
+ All of the proofs are direct from the uniqueness of adjoints
+ lemma.
\begin{theorem}[Boolean to Unit Downcast]
In Scheme-like GTT, we can prove
@@ -2722,9 +2721,6 @@ typed version of scheme's \emph{case-lambda} construct.
\bindXtoYinZ \bullet x \ifXthenYelseZ x {\ret()}{\err}
\]
\end{theorem}
- \begin{proof}
- % TODO
- \end{proof}
\begin{theorem}[Tagged Value to Sum]
In Scheme-like GTT, we can prove
@@ -2742,9 +2738,6 @@ typed version of scheme's \emph{case-lambda} construct.
\]
and the upcasts are given by lemma (TODO)
\end{theorem}
- \begin{proof}
- TODO
- \end{proof}
\begin{theorem}[Ground Mismatches are Errors]
In Schemish GTT we can prove
@@ -2757,6 +2750,24 @@ typed version of scheme's \emph{case-lambda} construct.
\force\upcast{U\u F\dynv}{U\dync}V \equidyn \dyncocaseFunF{\err}{\force V}\\
\end{mathpar}
\end{theorem}
+
+ Finally, we note now that all of these axioms are satisfied when
+ using the Scheme-like dynamic type interpretation and extending the
+ translation of GTT into CBPV* with the following, tediously
+ explicit definition:
+ \begin{align*}
+ &\sem{\bool} = 1+1\\
+ &\sem{\tru} =\inl()\\
+ &\sem{\fls} =\inr()\\
+ &\sem{\ifXthenYelseZ V {E_t} {E_f}} = \caseofXthenYelseZ {\sem V}{x. E_t}{x.E_f}\\
+ &\sem{\dyncaseofXthenBoolUPair x {x_\bool. E_\bool}{x_U. E_U}{x_\times. E_\times}}
+ =\\
+ &\quad\pmmuXtoYinZ {(x:\dynv)} {x'} \pmmuXtoYinZ {x' : \texttt{Tree}[(1+1)+U\dync]}t \caseofX t\\
+ &\qquad\thenY{l. \caseofXthenYelseZ l {x_\bool. \sem{E_\bool}}{x_U. \sem{E_U}}}\\
+ &\qquad\elseZ{x_\times. \sem{E_\times}}\\
+ &\sem{\dyncocaseFunF{M_\to}{M_{\u F}}}
+ = \rollty{\nu \u Y. (\dynv \to \u Y)\with \u F\dynv}\pair{\sem{M_\to}}{\sem{M_{\u F}}}
+ \end{align*}
\end{longonly}
Next, we easily see that if we want to limit to just the CBV types
@@ -2795,8 +2806,15 @@ First, we define in figure \ref{fig:cast-to-contract} the extension of
the dynamic type interpretation to an interpretation of \emph{all}
casts in GTT.
%
-We extend this to a full translation from GTT to CBPV* by intepreting
-all other value and term constructors as themselves.
+The definition should be interpreted as ordered, since multiple cases
+could apply (though we will ultimately show they are equivalent).
+%
+The definition is also not obviously total: we need to verify that it
+covers every possible case where $A \ltdyn A'$ and $\u B \ltdyn \u
+B'$.
+%
+As in previous work, this is proven correct by an analysis of the type
+dynamism relation.
\begin{figure}
\begin{mathpar}
@@ -2857,23 +2875,168 @@ all other value and term constructors as themselves.
\label{fig:cast-to-contract}
\end{figure}
-\begin{lemma}[Type Preservation of Contract Translation]
+We present a normalized set of rules for type dynamism in figure
+\ref{fig:normalized}.
+%
+We can see that the definition of casts is defined by recursion on
+these derivations, so to prove that our definition is defined for all
+possible upcasts and downcasts it is sufficient to show that every
+rule of the original system is admissible in the normalized system.
+%
+Furthermore, it is clear that the normalized system is a subset of the
+original: every rule corresponds directly to a rule of the original
+system except the $A \ltdyn \dynv$ and similar $\u B \ltdyn \dync$
+rules use the $\dynv, \dync$ are top rules and transitivity.
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {A \in \{\dynv, 1\}}
+ {A \ltdyn A}
+
+ \inferrule
+ {A \in \{\dynv, 0\}}
+ {0 \ltdyn A}
+
+ \inferrule
+ {A \ltdyn \floor A\and
+ A \not\in\{0,\dynv \}}
+ {A \ltdyn \dynv}\\
+
+ \inferrule
+ {\u B \ltdyn \u B'}
+ {U B \ltdyn U B'}
+
+ \inferrule
+ {A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ {A_1 + A_2 \ltdyn A_1' + A_2'}
+
+ \inferrule
+ {A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ {A_1 \times A_2 \ltdyn A_1' \times A_2'}\\
+
+ \inferrule
+ {}
+ {\dync \ltdyn \dync}
+
+ \inferrule
+ {\u B \in \{ \dync, \top \}}
+ {\top \ltdyn \u B}
+
+ \inferrule
+ {\u B \ltdyn \floor {\u B} \and \u B \not\in \{ \top, \dync \}}
+ {\u B \ltdyn \dync}\\
+
+ \inferrule
+ {A \ltdyn A'}
+ {\u F A \ltdyn \u F A'}
+
+ \inferrule
+ {\u B_1 \ltdyn \u B_1' \and \u B_2 \ltdyn \u B_2'}
+ {\u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
+
+ \inferrule
+ {A \ltdyn A' \and \u B \ltdyn \u B'}
+ {A \to \u B \ltdyn A' \to \u B'}
+ \end{mathpar}
+ \caption{Normalized Type Dynamism Relation}
+\end{figure}
+
+\begin{lemma}[Normalized Type Dynamism is Equivalent to Original]
+ $T \ltdyn T'$ is provable in the normalized typed dynamism
+ definition if and only if it is provable in the original typed
+ dynamism definition.
+\end{lemma}
+\begin{longproof}
+ The forward direction is clear by an argument above. First we show
+ by induction that reflexivity is admissible:
+ \begin{enumerate}
+ \item If $A \in \{\dynv, 1, 0\}$, we use a normalized rule.
+ \item If $A \not\in\{\dynv, 1, 0\}$, we use the inductive hypothesis
+ and the monotonicity rule.
+ \item If $\u B\in \{\dync, \top\}$ use the normalized rule.
+ \item If $\u B \not\in\{\dync, \top\}$ use the inductive hypothesis
+ and monotonicity rule.
+ \end{enumerate}
+ Next we show that transitivity is admissible:
+ \begin{enumerate}
+ \item Assume we have $A \ltdyn A' \ltdyn A''$
+ \begin{enumerate}
+ \item If the left rule is $0 \ltdyn A'$, then either $A' = \dynv$
+ or $A' = 0$. If $A' = 0$ the right rule is $0 \ltdyn A''$ and we
+ can use that proof. Otherwise, $A' = \dynv$ then the right rule
+ is $\dynv \ltdyn \dynv$ and we can use $0 \ltdyn \dynv$.
+ \item If the left rule is $A \ltdyn A$ where $A \in \{ \dynv, 1\}$
+ then either $A = \dynv$, in which case $A'' = \dynv$ and we're
+ done. Otherwise the right rule is either $1 \ltdyn 1$ (done) or
+ $1 \ltdyn \dynv$ (also done).
+ \item If the left rule is $A \ltdyn \dynv$ with
+ $A\not\in\{0,\dynv\}$ then the right rule must be $\dynv \ltdyn
+ \dynv$ and we're done.
+ \item Otherwise the left rule is a monotonicity rule for one of
+ $U, +, \times$ and the right rule is either monotonicity (use
+ the inductive hypothesis) or the right rule is $A' \ltdyn \dynv$
+ with a sub-proof of $A' \ltdyn \floor{A'}$. Since the left rule
+ is monotonicity, $\floor{A} = \floor{A'}$, so we inductively use
+ transitivity of the proof of $A \ltdyn A'$ with the proof of $A'
+ \ltdyn \floor{A'}$ to get a proof $A \ltdyn \floor{A}$ and thus
+ $A \ltdyn \dynv$.
+ \end{enumerate}
+ \item Assume we have $\u B \ltdyn \u B' \ltdyn \u B''$.
+ \begin{enumerate}
+ \item If the left rule is $\top \ltdyn \u B'$ then $\u B'' \in
+ \{\dync, \top\}$ so we apply that rule.
+ \item If the left rule is $\dync\ltdyn \dync$, the right rule must
+ be as well.
+ \item If the left rule is $\u B \ltdyn \dync$ the right rule must
+ be reflexivity.
+ \item If the left rule is a monotonicity rule for $\with, \to, \u
+ F$ then the right rule is either also monotonicity (use the
+ inductive hypothesis) or it's a $\u B \ltdyn \dync$ rule and we
+ proceed with $\dynv$ above
+ \end{enumerate}
+ \end{enumerate}
+ Finally we show $A \ltdyn \dynv$, $\u B \ltdyn \dync$ are admissible
\begin{enumerate}
- \item If $\Gamma \vdash M : \u B$ in GTT, then $\sem{\Gamma} \vdash
- \sem M : \sem {\u B}$ in \cbpvtxt.
- \item If $\Gamma \vdash V : A$ in GTT, then
- $\sem\Gamma \vdash \sem V : \sem{\u B}$ in \cbpvtxt.
- \item If $\Gamma \pipe \u B \vdash S : \u B'$in GTT, then
- $\sem{\Gamma} \pipe \sem{\u B} \vdash \sem S : \sem {\u B'}$ in \cbpvtxt.
+ \item If $A \in \{ \dynv, 0\}$ we use the primitive rule.
+ \item If $A \not\in \{ \dynv, 0 \}$ we use the $A \ltdyn \dynv$ rule
+ and we need to show $A \ltdyn \floor A$. If $A = 1$, we use the
+ $1\ltdyn 1$ rule, otherwise we use the inductive hypothesis and
+ monotonicity.
+ \item If $\u B \in \{ \dync, \top\}$ we use the primitive rule.
+ \item If $\u B \not\in \{ \dync, \top \}$ we use the $\u B \ltdyn
+ \dync$ rule and we need to show $\u B \ltdyn \floor {\u B}$, which
+ follows by inductive hypothesis and monotonicity.
\end{enumerate}
+\end{longproof}
+
+Next, we extend the translation of casts to a translation of all terms.
+%
+Since all term constructions in GTT besides casts are constructions in
+CBPV*, we simply extend it by congruence.
+%
+We note that the translation is clearly type preserving in the
+following sense:
+\begin{lemma}[Type Preservation of Contract Translation]
+ If $\Gamma\pipe\Delta \vdash E : T$ in GTT, then $\sem{\Gamma}
+ \pipe\sem\Delta\vdash \sem E : \sem T$ in CBPV*.
\end{lemma}
+In effect we have now given a model of the types, terms and type
+dynamism proofs of GTT in CBPV*, and we now need to interpret the
+\emph{term dynamism} proofs.
+%
Our goal in the remainder of this section is to establish the
-following ``axiomatic graduality'' theorem, which interprets a term
-dynamism judgment of GTT as an ordering ``up to cast'' in CBPV. In the
-next section, we provide an operational \emph{model} of CBPV and thus
-obtain by composition an operational gradulity theorem (the dynamic
-gradual guarantee).
+following ``axiomatic graduality'' theorem, that defines such an
+interpretation.
+%
+The basic idea is that GTT has \emph{heterogeneous} term dynamism
+rules indexed by type dynamism, but CBPV* has only \emph{homogeneous}
+inequalities between terms with the same types.
+%
+Since every type dynamism judgment has an associated cast, we can
+translate a heterogeneous inequality to a homogeneous inequality
+\emph{up to cast}.
\begin{theorem}[Axiomatic Graduality]
For any dynamic type interpretation, the following are true:
\begin{mathpar}
@@ -2888,152 +3051,96 @@ gradual guarantee).
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn\sem{V'}[\sem\Phi] : \sem {A'}}
\end{mathpar}
+ where we define $\sem{\Phi}, \sem{\Delta}$%
+ \begin{shortonly}
+ in the obvious way, where if $\Delta = \cdot$, then
+ $M[\sem{\Delta}] = M$.
+ \end{shortonly}
+ \begin{longonly}
+ as follows.
+ \begin{enumerate}
+ \item If $\Phi : \Gamma \ltdyn \Gamma'$, then there exists $n$
+ such that $\Gamma = x_1:A_1,\ldots,x_n:A_n$ and $\Gamma' =
+ x_1':A_1',\ldots,x_n':A_n'$ where $A_i \ltdyn A_i'$ for each
+ $i\leq n$.
+ Then $\sem{\Phi}$ is a substitution from $\sem{\Gamma}$ to $\sem{\Gamma'}$
+ defined as
+ \[ \sem{\Phi} = \supcast{A_1}{A_1'}x_1/x_1',\ldots\supcast{A_n}{A_n'}x_n/x_n' \]
+ \item If $\Psi : \Delta \ltdyn \Delta'$, then we similarly define
+ $\sem{\Psi}$ as a ``linear substitution''. That is, if $\Delta =
+ \Delta' = \cdot$, then $\sem{\Psi}$ is an empty substitution and
+ $M[\sem{\Psi}] = M$, otherwise $\sem{\Psi}$ is a linear
+ substitution from $\Delta' = \bullet : \u B'$ to $\Delta =
+ \bullet : \u B$ where $\u B \ltdyn \u B'$ defined as
+ \[ \sem\Psi = \sdncast{\u B}{\u B'}\bullet/\bullet \]
+ \end{enumerate}
+ \end{longonly}
\end{theorem}
+We note that in previous work on graduality (\cite{new-ahmed2018}),
+where to insert the casts was seen as an arbitrary choice because all
+casts there were syntactic evaluation contexts.
+%
+Here on the other hand, by using complex values and complex stacks for
+casts, using upcasts between value types and downcasts between
+computation types than the alternatives, which would require many uses
+of bind and thunk.
-Quite frequently we need the following commuting conversions, which
-are derivable from the $\eta$ rules for positive connectives.
-
-We need two versions of each rule for the positive value type
-connectives because of complex values: one when the continuation is a
-value and one when the continuation is a term.
-\begin{lemma}[Commuting Conversions]
- All of the following are provable when both sides are well-typed/scoped:
- % TODO: 1, 0?
- \begin{mathpar}
- E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]
- \equidyn
- \caseofXthenYelseZ V {x_1.E[V_1/y]}{x_2.E[V_2/y]}
-
- S[\caseofXthenYelseZ V {x_1.M_1}{x_2.M_2}]
- \equidyn
- \caseofXthenYelseZ V {x_1.S[M_1]}{x_2.S[M_2]}
-
- E[\pmpairWtoXYinZ V {x}{y} V'/z]
- \equidyn
- \pmpairWtoXYinZ V {x}{y} E[V'/z]
-
- S[\pmpairWtoXYinZ V {x}{y} M']
- \equidyn
- \pmpairWtoXYinZ V {x}{y} S[M']
-
- S[\bindXtoYinZ M x N]
- \equidyn
- \bindXtoYinZ M x S[N]
- \end{mathpar}
-\end{lemma}
-\begin{proof}
- \begin{enumerate}
- \item For $+$, we just show one case since the other is exactly the same:
- \begin{align*}
- &E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]\\
- &\equidyn
- \caseofXthenYelseZ V {x_1'. E[\caseofXthenYelseZ {\inl x_1'} {x_1.V_1}{x_2.V_2}/y]}{x_2'. E[\caseofXthenYelseZ {\inr x_2'} {x_1.V_1}{x_2.V_2}/y]}\tag{$+\eta$}\\
- &\equidyn \caseofXthenYelseZ V {x_1'. E[V_1[x_1'/x_1]]} {x_2'. E[V_2[x_2'/x_2]]}\tag{$+\beta$ twice}\\
- &\equidyn \caseofXthenYelseZ V {x_1. E[V_1]} {x_2. E[V_2]} \tag{$\alpha$}
- \end{align*}
- \item For $\times$
- \begin{align*}
- &E[\pmpairWtoXYinZ V x y V']\\
- &\pmpairWtoXYinZ V {x'}{y'} E[\pmpairWtoXYinZ {(x',y')} x y V']\tag{$\times\eta$}\\
- &\pmpairWtoXYinZ V {x'}{y'} E[V'[x'/x][y'/y]] \tag{$\times\beta$}\\
- &\pmpairWtoXYinZ V {x}{y} E[V'] \tag{$\alpha$}
- \end{align*}
- \item For $\u F$
- \begin{align*}
- &S[\bindXtoYinZ M x N]\\
- &\bindXtoYinZ M y S[\bindXtoYinZ {\ret y} x N]\tag{$\u F\eta$}\\
- &\bindXtoYinZ M y S[N[y/x]]\tag{$\u F\beta$}\\
- &\bindXtoYinZ M y S[N] \tag{$\alpha$}
- \end{align*}
- \end{enumerate}
-\end{proof}
+\begin{shortonly}
+ We present the key lemmas of the proof, and a few demonstrative cases.
+ %
+ The full proofs can be found in the supplementary material.
+\end{shortonly}
+\begin{longonly}
+ First, to keep proofs high-level, we establish the following cast
+ reductions that follow easily from $\beta,\eta$ principles.
\begin{lemma}{Cast Reductions}
The following are all provable
- \begin{mathpar}
- \sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inl V] \equidyn
+ \begin{align*}
+ &\sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inl V] \equidyn \inl \sem{\upcast{A_1}{A_1'}}[V]\\
+ &\sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inr V] \equidyn \inr \sem{\upcast{A_2}{A_2'}}[V]\\
+ &\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inl V] \equidyn
\bindXtoYinZ {\sem{\dncast{A_1}{A_1'}}[\ret V]} {x_1} \ret \inl x_1\\
-
- \sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inr V] \equidyn
+ &\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inr V] \equidyn
\bindXtoYinZ {\sem{\dncast{A_2}{A_2'}}[\ret V]} {x_2} \ret \inr x_2\\
-
- \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inl V] \equidyn \inl \sem{\upcast{A_1}{A_1'}}[V]\\
-
- \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inr V] \equidyn \inr \sem{\upcast{A_2}{A_2'}}[V]\\
-
- \sem{\dncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}}[\ret (V_1,V_2)] \equidyn
+ &\sem{\dncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}}[\ret (V_1,V_2)]\\
+ &\quad\equidyn
\bindXtoYinZ {\sdncast{\u FA_1}{\u F A_1'}[\ret V_1]} {x_1} \bindXtoYinZ {\sdncast{\u FA_2}{\u F A_2'}[\ret V_2]} {x_2} \ret (x_1,x_2)\\
-
- \supcast{A_1\times A_2}{A_1'\times A_2'}[(V_1,V_2)] \equidyn (\supcast{A_1}{A_1'}[V_1], \supcast{A_2}{A_2'}[V_2])\\
-
- (\sdncast{A \to \u B}{A' \to \u B'} M)\, V \equidyn
+ &\supcast{A_1\times A_2}{A_1'\times A_2'}[(V_1,V_2)] \equidyn (\supcast{A_1}{A_1'}[V_1], \supcast{A_2}{A_2'}[V_2])\\
+ &(\sdncast{A \to \u B}{A' \to \u B'} M)\, V \equidyn
(\sdncast{\u B}{\u B'} M)\, (\supcast{A}{A'}{V})\\
-
- (\force (\supcast{U(A\to\u B)}{U(A'\to\u B')} V))\,V' \equidyn
+ &(\force (\supcast{U(A\to\u B)}{U(A'\to\u B')} V))\,V'\\
+ &\quad\equidyn
\bindXtoYinZ {\dncast{\u FA}{\u FA'}[\ret V']} x {\force (\supcast{U\u B}{U\u B'}{(\thunk (\force V\, x))})}\\
-
- \pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
+ &\pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
\sdncast{\u B_1}{\u B_1'} \pi M\\
-
- \pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
+ &\pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
\sdncast{\u B_2}{\u B_2'} \pi' M\\
-
- \pi \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
+ &\pi \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
\equidyn
\force \supcast{U\u B_1}{U\u B_1'}{\thunk (\pi \force V)}\\
-
- \pi' \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
+ &\pi' \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
\equidyn
\force \supcast{U\u B_2}{U\u B_2'}{\thunk (\pi' \force V)}\\
-
- \sdncast{\u F U \u B}{\u F U \u B'}[\ret V] \equidyn \ret\thunk \sdncast{\u B}{\u B'}\force V\\
-
- \force \supcast{U\u FA}{U \u F A'}[V]
+ &\sdncast{\u F U \u B}{\u F U \u B'}[\ret V] \equidyn \ret\thunk \sdncast{\u B}{\u B'}\force V\\
+ &\force \supcast{U\u FA}{U \u F A'}[V]
\equidyn
\bindXtoYinZ {\force V} x \thunk\ret\upcast{A}{A'} x
- \end{mathpar}
+ \end{align*}
\end{lemma}
+\end{longonly}
-\begin{lemma}[EP Pairs Compose]
- \begin{enumerate}
- \item If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
- $(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
- $(V_2[V_1], S_1[S_2])$ is a value ep pair from $A_1$ to $A_3$.
- \item If $(V_1, S_1)$ is a computation ep pair from $\u B_1$ to $\u B_2$ and
- $(V_2,S_2)$ is a computation ep pair from $\u B_2$ to $\u B_3$, then
- $(V_2[V_1], S_1[S_2])$ is a computation ep pair from $\u B_1$ to $\u B_3$.
- \end{enumerate}
-\end{lemma}
-\begin{proof}
- \begin{enumerate}
- \item First, retraction follows from retraction twice:
- \[ S_1[S_2[\ret V_2[V_1[x]]]] \equidyn S_1[\ret [V_1[x]]] \equidyn x \]
- and projection follows from projection twice:
- \begin{align*}
- \bindXtoYinZ {S_1[S_2[\bullet]]} x \ret V_2[V_1[x]]
- &\equidyn
- {\bindXtoYinZ {S_1[S_2[\bullet]]} x \bindXtoYinZ {\ret [V_1[x]]} y \ret V_2[y]}\tag{$\u F\beta$}\\
- &\equidyn
- \bindXtoYinZ {(\bindXtoYinZ {S_1[S_2[\bullet]]} x {\ret [V_1[x]]})} y \ret V_2[y]\tag{Commuting conversion}\\
- &\ltdyn
- \bindXtoYinZ {S_2[\bullet]} y \ret V_2[y]\tag{Projection}\\
- &\ltdyn \bullet \tag{Projection}
- \end{align*}
- \item Again retraction follows from retraction twice:
- \[ S_1[S_2[\force V_2[V_1[z]]]] \equidyn S_1[\force V_1[z]] \equidyn \force z \]
- and projection from projection twice:
- \begin{align*}
- V_2[V_1[\thunk S_1[S_2[\force w]]]]
- &\equidyn V_2[V_1[\thunk S_1[\force \thunk S_2[\force w]]]]\tag{$U\beta$}\\
- &\ltdyn V_2[\thunk S_2[\force w]] \tag{Projection}\\
- &\ltdyn w \tag{Projection}
- \end{align*}
- \end{enumerate}
-\end{proof}
+The first main lemma is the following ``fundamental theorem'' for
+that says that from the basic casts being ep pairs, we can prove that
+all casts are ep pairs.
+%
+\begin{shortonly}
+ This follows mostly from straightforward calculation, but also from
+ some lemmas that say ep pairs compose.
+\end{shortonly}
\begin{lemma}[Casts are EP Pairs]
- For any dynamic type interpretation,
\begin{enumerate}
\item For any $A \ltdyn A'$, the casts $(x.\sem{\upcast{A}{A'}x},
\sem{\dncast{\u F A}{\u F A'}})$ are a value ep pair from
@@ -3043,7 +3150,7 @@ value and one when the continuation is a term.
pair from $\sem{\u B}$ to $\sem{\u B'}$.
\end{enumerate}
\end{lemma}
-\begin{proof}
+\begin{longproof}
By mutual induction on $A, \u B$
\begin{enumerate}
\item TODO: There's a few base cases about the dynamic type
@@ -3402,6 +3509,104 @@ value and one when the continuation is a term.
\end{align*}
\end{enumerate}
\end{enumerate}
+\end{longproof}
+
+\begin{longonly}
+Quite frequently we need the following commuting conversions, which
+are derivable from the $\eta$ rules for positive connectives.
+
+We need two versions of each rule for the positive value type
+connectives because of complex values: one when the continuation is a
+value and one when the continuation is a term.
+\begin{lemma}[Commuting Conversions]
+ All of the following are provable when both sides are well-typed/scoped:
+ % TODO: 1, 0?
+ \begin{mathpar}
+ E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]
+ \equidyn
+ \caseofXthenYelseZ V {x_1.E[V_1/y]}{x_2.E[V_2/y]}
+
+ S[\caseofXthenYelseZ V {x_1.M_1}{x_2.M_2}]
+ \equidyn
+ \caseofXthenYelseZ V {x_1.S[M_1]}{x_2.S[M_2]}
+
+ E[\pmpairWtoXYinZ V {x}{y} V'/z]
+ \equidyn
+ \pmpairWtoXYinZ V {x}{y} E[V'/z]
+
+ S[\pmpairWtoXYinZ V {x}{y} M']
+ \equidyn
+ \pmpairWtoXYinZ V {x}{y} S[M']
+
+ S[\bindXtoYinZ M x N]
+ \equidyn
+ \bindXtoYinZ M x S[N]
+ \end{mathpar}
+\end{lemma}
+\begin{proof}
+ \begin{enumerate}
+ \item For $+$, we just show one case since the other is exactly the same:
+ \begin{align*}
+ &E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]\\
+ &\equidyn
+ \caseofXthenYelseZ V {x_1'. E[\caseofXthenYelseZ {\inl x_1'} {x_1.V_1}{x_2.V_2}/y]}{x_2'. E[\caseofXthenYelseZ {\inr x_2'} {x_1.V_1}{x_2.V_2}/y]}\tag{$+\eta$}\\
+ &\equidyn \caseofXthenYelseZ V {x_1'. E[V_1[x_1'/x_1]]} {x_2'. E[V_2[x_2'/x_2]]}\tag{$+\beta$ twice}\\
+ &\equidyn \caseofXthenYelseZ V {x_1. E[V_1]} {x_2. E[V_2]} \tag{$\alpha$}
+ \end{align*}
+ \item For $\times$
+ \begin{align*}
+ &E[\pmpairWtoXYinZ V x y V']\\
+ &\pmpairWtoXYinZ V {x'}{y'} E[\pmpairWtoXYinZ {(x',y')} x y V']\tag{$\times\eta$}\\
+ &\pmpairWtoXYinZ V {x'}{y'} E[V'[x'/x][y'/y]] \tag{$\times\beta$}\\
+ &\pmpairWtoXYinZ V {x}{y} E[V'] \tag{$\alpha$}
+ \end{align*}
+ \item For $\u F$
+ \begin{align*}
+ &S[\bindXtoYinZ M x N]\\
+ &\bindXtoYinZ M y S[\bindXtoYinZ {\ret y} x N]\tag{$\u F\eta$}\\
+ &\bindXtoYinZ M y S[N[y/x]]\tag{$\u F\beta$}\\
+ &\bindXtoYinZ M y S[N] \tag{$\alpha$}
+ \end{align*}
+ \end{enumerate}
+\end{proof}
+
+\end{longonly}
+
+\begin{lemma}[EP Pairs Compose]
+ \begin{enumerate}
+ \item If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
+ $(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
+ $(V_2[V_1], S_1[S_2])$ is a value ep pair from $A_1$ to $A_3$.
+ \item If $(V_1, S_1)$ is a computation ep pair from $\u B_1$ to $\u B_2$ and
+ $(V_2,S_2)$ is a computation ep pair from $\u B_2$ to $\u B_3$, then
+ $(V_2[V_1], S_1[S_2])$ is a computation ep pair from $\u B_1$ to $\u B_3$.
+ \end{enumerate}
+\end{lemma}
+\begin{proof}
+ \begin{enumerate}
+ \item First, retraction follows from retraction twice:
+ \[ S_1[S_2[\ret V_2[V_1[x]]]] \equidyn S_1[\ret [V_1[x]]] \equidyn x \]
+ and projection follows from projection twice:
+ \begin{align*}
+ \bindXtoYinZ {S_1[S_2[\bullet]]} x \ret V_2[V_1[x]]
+ &\equidyn
+ {\bindXtoYinZ {S_1[S_2[\bullet]]} x \bindXtoYinZ {\ret [V_1[x]]} y \ret V_2[y]}\tag{$\u F\beta$}\\
+ &\equidyn
+ \bindXtoYinZ {(\bindXtoYinZ {S_1[S_2[\bullet]]} x {\ret [V_1[x]]})} y \ret V_2[y]\tag{Commuting conversion}\\
+ &\ltdyn
+ \bindXtoYinZ {S_2[\bullet]} y \ret V_2[y]\tag{Projection}\\
+ &\ltdyn \bullet \tag{Projection}
+ \end{align*}
+ \item Again retraction follows from retraction twice:
+ \[ S_1[S_2[\force V_2[V_1[z]]]] \equidyn S_1[\force V_1[z]] \equidyn \force z \]
+ and projection from projection twice:
+ \begin{align*}
+ V_2[V_1[\thunk S_1[S_2[\force w]]]]
+ &\equidyn V_2[V_1[\thunk S_1[\force \thunk S_2[\force w]]]]\tag{$U\beta$}\\
+ &\ltdyn V_2[\thunk S_2[\force w]] \tag{Projection}\\
+ &\ltdyn w \tag{Projection}
+ \end{align*}
+ \end{enumerate}
\end{proof}
\begin{corollary}[Hom-set formulation of Adjunction]