Skip to content
Snippets Groups Projects
Commit c5db8fd6 authored by Max New's avatar Max New
Browse files

cast reduction principles, comm conversions, + ep pair case

parent 96a596b0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 192 additions and 20 deletions
paper/gtt.tex
+ 192
− 20
View file @ c5db8fd6
......@@ -116,6 +116,8 @@
\newcommand{\cbpv}{\text{CBPV}_{\mu,\nu,\err,\ltdyn}}
\newcommand{\cbpvtxt}{$\cbpv$}
\newcommand{\sem}[1]{\llbracket#1\rrbracket}
\newcommand{\sdncast}[2]{\sem{\dncast{#1}{#2}}}
\newcommand{\supcast}[2]{\sem{\upcast{#1}{#2}}}
\newcommand{\srho}[1]{\sem{#1}_\rho}
\newcommand{\sdn}[2]{\srho{\dncast{#1}{#2}}}
\newcommand{\hetplug}[1]{\langle#1\rangle}
......@@ -204,6 +206,10 @@
\newcommand{\kw}[1]{\texttt{#1}\,\,}
\newcommand{\absurd}{\kw{absurd}}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\caseofX}[1]{\case #1}
\newcommand{\thenY}{\{}
\newcommand{\elseZ}[1]{\pipe #1 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
\newcommand{\pmpairWtoinZ}[2]{\kw{split} #1\,\kw{to} (). #2}
\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
......@@ -1843,6 +1849,110 @@ is our graduality theorem.
\end{mathpar}
\end{theorem}
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:
% + 1 x F
\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}/y]
\equidyn
\caseofXthenYelseZ V {x_1.S[M_1/y]}{x_2.S[M_2/y]}
E[\pmpairWtoXYinZ V {x}{y} V']
\equidyn
\pmpairWtoXYinZ V {x}{y} E[V']
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{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
\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
\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
\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
(\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
\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
\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
\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)
\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)
\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]
\equidyn
\bindXtoYinZ {\force V} x \thunk\ret\upcast{A}{A'} x
\end{mathpar}
\end{lemma}
\begin{lemma}[Casts are EP Pairs]
For any dynamic type interpretation,
\begin{enumerate}
......@@ -1858,8 +1968,63 @@ is our graduality theorem.
By mutual induction on $A, \u B$
\begin{enumerate}
\item There's a few base cases about the dynamic type, then
\item $0$: TODO
\item $+$: TODO
\item $0$:
\begin{enumerate}
\item Retraction is
\[ x : 0 \vdash \ret x \equidyn \bindXtoYinZ {\ret\absurd x} y \err : \u F A \]
which holds by $0\eta$
\item Projection is
\[ \bullet : \u F A \vdash \bindXtoYinZ {(\bindXtoYinZ \bullet y \err)} x {\ret\absurd x} \ltdyn \bullet : \u F A \]
Which we calculate:
\begin{align*}
&\bindXtoYinZ {(\bindXtoYinZ \bullet y \err)} x {\ret\absurd x}\\
&\equidyn \bindXtoYinZ \bullet y \bindXtoYinZ \err x {\ret\absurd x}\tag{TODO comm conv}\\
&\equidyn \bindXtoYinZ \bullet y \err \tag{Strictness of Stacks}\\
&\ltdyn \bindXtoYinZ \bullet y \ret y \tag{$\err$ is $\bot$}\\
&\equidyn \bullet \tag{$\u F\eta$}
\end{align*}
\end{enumerate}
\item $+$:
\begin{enumerate}
\item Retraction is
\begin{align*}
&x : A_1 + A_2 \vdash\\
&\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[x]]\\
&=\sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\caseofXthenYelseZ x {x_1. \inl\supcast{A_1}{A_1'}[x_1]}{x_1. \inr\supcast{A_2}{A_2'}[x_2]}]\\
&\equidyn
\caseofX x\tag{commuting conversion}\\
&\quad\thenY {x_1. \sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\inl\supcast{A_1}{A_1'}[x_1]]}\\
&\quad\elseZ {x_2. \sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\inr\supcast{A_2}{A_2'}[x_2]]}\\
&\equidyn
\caseofX x\tag{cast computation}\\
&\quad\thenY{x_1. \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret \supcast{A_1}{A_1'}x_1]} {x_1} \ret \inl x_1}\\
&\quad\elseZ{x_2. \bindXtoYinZ {\sdncast{\u F A_2}{\u F A_2'}[\ret \supcast{A_2}{A_2'}x_2]} {x_2} \ret \inr x_2}\\
&\equidyn \caseofXthenYelseZ x {x_1. \ret \inl x_1} {x_2. \ret \inr x_2}\tag{IH retraction}\\
&\equidyn \ret x\tag{$+\eta$}
\end{align*}
\item For Projection:
\begin{align*}
&\bullet : A_1' + A_2' \vdash\\
&\bindXtoYinZ {\sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}} x \supcast{A_1+A_2}{A_1'+A_2'}[x]\\
&=
\bindXtoYinZ {(\bindXtoYinZ \bullet {x'} \caseofXthenYelseZ {x'} {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} \ret\inl x_1}{x_2'. \cdots})} x\\
&\quad\supcast{A_1+A_2}{A_1'+A_2'}\\
%%%%%%%%%%%%%%%
&\equidyn
\bindXtoYinZ \bullet x' \caseofX {x'} \tag{Commuting Conversion}\\
&\qquad \thenY {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} \supcast{A_1+A_2}{A_1'+A_2'}{\ret\inl x_1}}\\
&\qquad \elseZ {x_2'. \bindXtoYinZ {\sem{\dncast{\u FA_2}{\u FA_2'}}[\ret x_2']} {x_2} \supcast{A_1+A_2}{A_1'+A_2'}{\ret\inr x_2}}\\
%%%%%%%%%%%
&\equidyn
\bindXtoYinZ \bullet x' \caseofX {x'}\tag{Cast Computation}\\
&\qquad \thenY {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} {\ret\inl \supcast{A_1}{A_1'}x_1}}\\
&\qquad \elseZ {x_2'. \bindXtoYinZ {\sem{\dncast{\u FA_2}{\u FA_2'}}[\ret x_2']} {x_2} {\ret\inr \supcast{A_2}{A_2'}x_2}}\\
&\ltdyn
\bindXtoYinZ \bullet x' \caseofXthenYelseZ {x'} {x_1'. \ret\inl x_1'} {x_2'. \ret \inr x_2'}\tag{IH projection}\\
&\equidyn \bindXtoYinZ \bullet x' \ret x'\tag{$+\eta$}\\
&\equidyn \bullet \tag{$\u F\eta$}\\
\end{align*}
\end{enumerate}
\item $1$: TODO
\item $\times$: TODO
\item $U$: By inductive hypothesis, $(x.\sem{\upcast{U\u B}{U\u
......@@ -1871,24 +2036,24 @@ is our graduality theorem.
\]
Which we calculate as follows:
\begin{align*}
\bindXtoYinZ {(\ret {\sem{\upcast{U\u B}{U \u B'}}})} y {\ret \thunk \sem{\dncast{\u B}{\u B'}}[\force y]}
&\equidyn {\ret \thunk \sem{\dncast{\u B}{\u B'}}[\force {\sem{\upcast{U\u B}{U \u B'}}}]}
\tag{$\u F\beta$}\\
&\equidyn \ret\thunk \force x \tag{IH computation Retraction}\\
&x : U\u B \vdash \\
&\sdncast{\u FU\u B}{\u FU\u B'}[{(\ret {\sem{\upcast{U\u B}{U \u B'}}[x]})}]\\
&\equidyn
\ret\thunk(\sdncast{\u B}{\u B'}[\force {\sem{\upcast{U\u B}{U \u B'}}}[x]])\tag{Cast Reduction}\\
&\equidyn \ret\thunk \force x \tag{IH Retraction}\\
&\equidyn \ret x \tag{$U\eta$}
\end{align*}
\item To show projection we need to prove:
\[
\bullet : \u F U \u B' \vdash \bindXtoYinZ {(\bindXtoYinZ \bullet y {\ret\thunk \sem{\dncast{\u B}{\u B'}}[\force y]})} x \ret \sem{\upcast{U \u B}{U \u B'}} \ltdyn \bullet : \u F U \u B'
\]
Which we calculate:
\item To show projection we calculate:
\begin{align*}
\bindXtoYinZ {(\bindXtoYinZ \bullet y {\ret\thunk \sem{\dncast{\u B}{\u B'}}[\force y]})} x \ret \sem{\upcast{U \u B}{U \u B'}}
&\equidyn \bindXtoYinZ \bullet y \bindXtoYinZ {\ret\thunk \sem{\dncast{\u B}{\u B'}}[\force y]} x \ret \sem{\upcast{U \u B}{U \u B'}}
\tag{TODO: comm conv lemma $\u F\eta$}\\
&\equidyn \bindXtoYinZ \bullet y \ret \sem{\upcast{U \u B}{U \u B'}}[\thunk \sem{\dncast{\u B}{\u B'}}[\force y]] \tag{$\u F\beta$}\\
&\ltdyn \bindXtoYinZ \bullet y \ret y \tag{IH computation Projection}\\
&\equidyn \bullet \tag{$\u F \eta$}
&\bindXtoYinZ {\sdncast{\u FU\u B}{\u FU\u B'}[\bullet]} x \supcast{U\u B}{U\u B'}[x]\\
&\equidyn
\bindXtoYinZ \bullet {x'} \bindXtoYinZ {\sdncast{\u FU\u B}{\u FU\u B'}[\ret x']} x \supcast{U\u B}{U\u B'}[x]\tag{$\u F\eta$}\\
&\equidyn
\bindXtoYinZ \bullet {x'} \bindXtoYinZ {\ret\thunk(\sdncast{\u B}{\u B'}[\force x'])} x \supcast{U\u B}{U\u B'}[x]\tag{Cast Reduction}\\
&\equidyn
\bindXtoYinZ \bullet {x'} \supcast{U\u B}{U\u B'}[\thunk(\sdncast{\u B}{\u B'}[\force x'])] \tag{$\u F\beta$}\\
&\ltdyn \bindXtoYinZ \bullet {x'} x'\tag{IH Projection}\\
&\equidyn \bullet \tag{$\u F\eta$}
\end{align*}
\end{enumerate}
\end{enumerate}
......@@ -1909,7 +2074,7 @@ is our graduality theorem.
\]
We calculate:
\begin{align*}
\sem{\dncast{\u F A}{\u F A'}}[\force \thunk (\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]
&\sem{\dncast{\u F A}{\u F A'}}[\force \thunk (\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]\\
&\equidyn
\sem{\dncast{\u F A}{\u F A'}}[(\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]\tag{$U\beta$}\\
&\equidyn
......@@ -1921,12 +2086,18 @@ is our graduality theorem.
\item To show projection we need to show
\[
w : U \u F A' \vdash
TODO
\thunk {(\bindXtoYinZ {\force {\thunk \sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})}
\ltdyn w : U \u B'
\]
We calculate as follows
\begin{align*}
&\thunk {(\bindXtoYinZ {\force {\thunk \sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})}\\
&\equidyn\thunk {(\bindXtoYinZ {{\sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})} \tag{$U\beta$}\\
&\ltdyn \thunk {\force w} \tag{IH value projection}\\
& \equidyn w \tag{$U\eta$}
\end{align*}
\end{enumerate}
\end{enumerate}
TODO: tedious
\end{proof}
\begin{corollary}[Hom-set formulation of EP Pairs]
......@@ -1962,6 +2133,7 @@ embeddings but I don't see anywhere where we need that.
$(V_e, S_1)$ and $(V_e, S_2)$ are both value ep pairs, then
\[ S_1 \equidyn S_2 \]
\end{lemma}
\begin{proof}
By symmetry it is sufficient to show $S_1 \ltdyn S_2$.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment