From e77e255aa8b0ae51fc52b3c50d6e1fe8093918a9 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 6 Jan 2020 15:46:41 -0500
Subject: [PATCH] some more cbv gtt
---
jfp-paper/jfp-gtt.tex | 132 +++++++++++++++++++++++++++++++++++++-----
1 file changed, 116 insertions(+), 16 deletions(-)
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index 10067a4..aded643 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -11,19 +11,19 @@
\title{Gradual Type Theory}
-\author[M.S. New]
+\author[M.S. New, D.R. Licata and Amal Ahmed]
{Max S. New\\
Northeastern University\\
%% \email{maxnew@ccs.neu.edu}
}
-\author[D.R. Licata]
+\author[M.S. New, D.R. Licata and Amal Ahmed]
{Daniel R. Licata \\
Wesleyan University\\
%% \email{drlicata@wesleyan.edu}
}
-\author[A. Ahmed]
+\author[M.S. New, D.R. Licata and A. Ahmed]
{Amal Ahmed \\
Northeastern University\\
%% \email{amal@ccs.neu.edu}
@@ -60,15 +60,20 @@ computational $\lambda$-calculus $\lambda_c$.
\begin{array}{rl}
A ::= & \colorbox{lightgray}{\dyn} \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 \mid A_1 \to A_2\\
+ V ::= & x \mid \lambda x:A. M
+ \mid \inl{V} \mid \inr{V} \\
+ \mid () \\
+ \mid (V_1,M_2) \\
+
M ::= & \begin{array}{l}
\colorbox{lightgray}{$\upcast{A}{A'} M$}
\colorbox{lightgray}{$\dncast{A} {A'} M$}
\mid x \\
\mid \err_{A} \\
- \mid \inl{V} \mid \inr{V} \\
- \mid \abort{V} \mid \caseofXthenYelseZ M {x_1. M_1}{x_2.M_2}\\
+ \mid \inl{M} \mid \inr{M} \\
+ \mid \abort{M} \mid \caseofXthenYelseZ M {\inl x_1. M_1}{\inr x_2.M_2}\\
\mid () \\
- \mid (V_1,V_2) \\
+ \mid (V_1,M_2) \\
\mid \pmpairWtoinZ M N \mid\pmpairWtoXYinZ M x y N \\
\mid \letXbeYinZ{M}{x}{N}\\
\mid \lambda x:A.M \mid M\,N\\
@@ -110,20 +115,20 @@ computational $\lambda$-calculus $\lambda_c$.
Uniqueness Principles Proofs
\begin{mathpar}
- \inferrule
+ \inferrule*[Right=UL]
{
- \inferrule
+ \inferrule*[Right=Trans]
{
- M \ltdyn \letXbeYinZ M f f \and
- \inferrule
- {
- \inferrule
+ \inferrule*[Right=Let-Id]{}{M \ltdyn \letXbeYinZ M f f} \and
+ \inferrule*[Right=Let-Cong]
+ {M \ltdyn M \and
+ \inferrule*[Right=Trans]
{f \ltdyn \lambda x:A_1. f x\and
- \inferrule
+ \inferrule*[Right=Lam-Cong]
{
- \inferrule
+ \inferrule*[Right=UR]
{
- \inferrule
+ \inferrule*[Right=App-Cong]
{
f \ltdyn g, x \ltdyn y \vdash f \ltdyn g\and
\inferrule
@@ -182,12 +187,99 @@ Translation of CBV into CBPV
{\Gamma \vdash M : A}
{\bvtopv{\Gamma} \vdash \bvtopv{M} : F \bvtopv{A}}
+ \inferrule
+ {\Gamma \vdash V : A}
+ {\bvtopv{\Gamma} \vdash \bvtopvpure{M} : \bvtopv A}
+
\inferrule
{\Phi \vdash M \ltdyn M' : A \ltdyn A'}
{\bvtopv{\Phi} \vdash \bvtopv{M} \ltdyn \bvtopv{M'} : \bvtopv{A} \ltdyn \bvtopv{A'}}
+
+ \inferrule
+ {\Phi \vdash V \ltdyn V' : A \ltdyn A'\and}
+ {\bvtopv{\Phi} \vdash \bvtopvpure{V} \ltdyn \bvtopvpure{V'} : \bvtopv{A} \ltdyn \bvtopv{A'}}
+
+ \inferrule
+ {\Gamma \vdash V : A}
+ {\bvtopv\Gamma \vdash \bvtopv{V} \equidyn \ret \bvtopvpure{V} : F \bvtopv{A}}
+
+ \inferrule
+ {\Gamma \vdash V : A \and \Gamma, x:A \vdash M : B}
+ {\bvtopv\Gamma \vdash \bvtopv{(M[V/x])} \equidyn \bvtopv{M}[\bvtopvpure{V}/x] : \bvtopv{B}}
+\end{mathpar}
+
+Order-stuff
+\begin{mathpar}
+ \inferrule
+ {M \ltdyn M' \ltdyn M''}
+ {M \ltdyn M''}
+
+ \inferrule
+ {}
+ {M \ltdyn M}
+
+ \inferrule
+ {x \ltdyn x' \vdash M \ltdyn M' \and V \ltdyn V'}
+ {M[V/x] \ltdyn M'[V'/x']}
+\end{mathpar}
+
+Let-reasoning
+\begin{mathpar}
+ \inferrule
+ {}
+ {\letXbeYinZ M x x \equidyn M}
+
+ \inferrule
+ {x \not\in FV(N)}
+ {\letXbeYinZ M x \letXbeYinZ {M'} {x'} N \equidyn
+ \letXbeYinZ {(\letXbeYinZ M x M')} {x'} N
+ }
+
+ \inferrule
+ {}
+ {\letXbeYinZ V x M \equidyn M[V/x]}
+\end{mathpar}
+
+Evaluation Order Rules
+\begin{mathpar}
+ \inferrule
+ {}
+ {M\,N \equidyn \letXbeYinZ M f \letXbeYinZ N x f\,x}
+
+ \inferrule
+ {}
+ {\pmpairWtoinZ M N \equidyn \letXbeYinZ M z \pmpairWtoinZ z N}
+
+ \inferrule
+ {}
+ {(M,N) \equidyn \letXbeYinZ M x \letXbeYinZ N y (x,y)}
+
+ \inferrule
+ {}
+ {\pmpairWtoXYinZ M x y N \equidyn \letXbeYinZ M z \pmpairWtoXYinZ z x y N}
+
+ \inferrule
+ {}
+ {\inl M \equidyn \letXbeYinZ M z \inl z}
+
+ \inferrule
+ {}
+ {\inr M \equidyn \letXbeYinZ M z \inr z}
+
+ \inferrule
+ {}
+ {\caseofXthenYelseZ M {\inl x_1. N_1}{\inr x_2. N_2}
+ \equidyn \letXbeYinZ M z \caseofXthenYelseZ z {\inl x_1. N_1}{\inr x_2. N_2}
+ }
+\end{mathpar}
+
+$\beta\eta$ Rules
+\begin{mathpar}
+
\end{mathpar}
\begin{align*}
+ \bvtopv{(x_0:A_0,\ldots)} &= x_0:\bvtopv{A_0},\ldots\\
\bvtopv{\dyn} &= \dynv\\
\bvtopv{1} &= 1\\
\bvtopv{(A_1 \times A_2)} &= \bvtopv{A_1} \times \bvtopv{A_2}\\
@@ -201,9 +293,17 @@ Translation of CBV into CBPV
\bvtopv{(\lambda x:A. M)} &= \ret \thunk {\lambda x:\bvtopv{A}. \bvtopv{M}}\\
\bvtopv{(M \, N)} &= \bindXtoYinZ {\bvtopv{M}} f \bindXtoYinZ {\bvtopv{N}} x {(\force f)\, x}\\
\bvtopv{(M_1,M_2)} &= \bindXtoYinZ {\bvtopv{M_1}} {x_1} \bindXtoYinZ {\bvtopv{M_2}} {x_2} \ret (x_1,x_2)\\
- \bvtopv{\pmpairWtoXYinZ M {x_1}{x_2} N} &= \bindXtoYinZ {\bvtopv M} x \pmpairWtoXYinZ x {x_1}{x_2} {\bvtopv N}
+ \bvtopv{\pmpairWtoXYinZ M {x_1}{x_2} N} &= \bindXtoYinZ {\bvtopv M} x \pmpairWtoXYinZ x {x_1}{x_2} {\bvtopv N}\\\\
+ \bvtopvpure{x} &= x\\
+ \bvtopvpure{(\lambda x:A. M)} &= \thunk {\lambda x:\bvtopv{A}. \bvtopv{M}}\\
+ \bvtopvpure{(\inl V)} &= \inl \bvtopvpure {V}\\
+ \bvtopvpure{(\inr V)} &= \inl \bvtopvpure {V}\\
+ \bvtopvpure{(V_1,V_2)} &= (\bvtopvpure{V_1}, \bvtopvpure{V_2})\\
\end{align*}
+%% List of Types:
+%% ?, ->, 1, *, 0, +
+
%% \label{lastpage}
\end{document}
--
GitLab