From 46a4d010d94087ef0293b52590f9ba06a1cb0860 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 30 Jan 2020 13:26:43 -0500
Subject: [PATCH] expanding figures
---
jfp-paper/jfp-gtt.tex | 280 ++++++++++++++++--------------------------
1 file changed, 106 insertions(+), 174 deletions(-)
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index d0695fb..1c8fd81 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -627,6 +627,7 @@ The main contributions of the paper are as follows.
\end{enumerate}
\begin{shortonly}
+ TODO: update this
\textbf{Extended version:} An extended version of the paper, which
includes the omitted cases of definitions, lemmas, and proofs is
available in \citet{newlicataahmed19:extended}.
@@ -810,49 +811,45 @@ orderings on types and terms.
\begin{figure}
\begin{small}
\[
- \begin{array}{l}
- \begin{array}{rl|rl}
- A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 &
+ \begin{array}{rl}
+ A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 \\
\u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
-
+ T ::= & A \mid \u B \\\\
V ::= & \begin{array}{l}
- \colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \abort{V} \\
- \mid \inl{V} \mid \inr{V} \\
- \mid \caseofXthenYelseZ V {x_1. V_1}{x_2.V_2} \\
- \mid () \mid \pmpairWtoinZ V V' \\
- \mid (V_1,V_2) \mid \pmpairWtoXYinZ V x y V' \\
- \mid \thunk{M}
- \end{array} &
+ \colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \thunk{M} \mid \abort{V} \mid \inl{V} \mid \inr{V} \mid \caseofXthenYelseZ V {x_1. V_1}{x_2.V_2} \\
+ \mid () \mid \pmpairWtoinZ V V' \mid (V_1,V_2) \mid \pmpairWtoXYinZ V x y V' \\
+ \end{array} \\\\
M,S ::= & \begin{array}{l}
- \colorbox{lightgray}{$\dncast{\u B} {\u B'} M$} \mid \bullet \mid \err_{\u B} \\
- \mid \abort{V} \mid \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2}\\
+ \colorbox{lightgray}{$\dncast{\u B} {\u B'} M$} \mid \bullet \mid \err_{\u B} \mid \force{V} \mid \abort{V} \mid \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2}\\
\mid \pmpairWtoinZ V M \mid\pmpairWtoXYinZ V x y M \\
- \mid \force{V} \mid \ret{V} \mid \bindXtoYinZ{M}{x}{N}\\
- \mid \lambda x:A.M \mid M\,V\\
- \mid \emptypair \mid \pair{M_1}{M_2} \\
+ \mid \ret{V} \mid \bindXtoYinZ{M}{x}{N}
+ \mid \emptypair \mid \pair{M_1}{M_2}
\mid \pi M \mid \pi' M
- \end{array}\\
-
- \Gamma ::= & \cdot \mid \Gamma, x : A &
+ \mid \lambda x:A.M \mid M\,V\\
+ \end{array}\\\\
+ E ::= & V \mid M \\\\
+
+ \Gamma ::= & \cdot \mid \Gamma, x : A \\
\Delta ::= & \cdot \mid \bullet : \u B \\
- \colorbox{lightgray}{$\Phi$} ::= & \colorbox{lightgray}{$\cdot \mid \Phi, x \ltdyn x': A \ltdyn A'$} &
+ \colorbox{lightgray}{$\Phi$} ::= & \colorbox{lightgray}{$\cdot \mid \Phi, x \ltdyn x': A \ltdyn A'$} \\
\colorbox{lightgray}{$\Psi$} ::= & \colorbox{lightgray}{$\cdot \mid \bullet \ltdyn \bullet : \u B \ltdyn \u B'$} \\
- \end{array}\\\\
-\iflong
- \begin{array}{c}
- \hspace{2.5in} T ::= A \mid \u B \\
- \hspace{2.5in} E ::= V \mid M \\
- \end{array}\\\\
-\fi
- %
- \begin{array}{c}
- \framebox{$\Gamma \vdash V : A$ and $\Gamma \mid \Delta \vdash M : \u B$} \qquad
+ \end{array}
+ \]
+\end{small}
+ \caption{GTT Type and Term Syntax}
+ \label{fig:gtt-syntax}
+\end{figure}
+
+\begin{figure}
+ \begin{small}
+ \begin{mathpar}
+ \framebox{$\Gamma \vdash V : A$ and $\Gamma \mid \Delta \vdash M : \u B$} \and
\colorbox{lightgray}{
$\inferrule*[lab=UpCast]
{\Gamma \vdash V : A \and A \ltdyn A'}
{\Gamma \vdash \upcast A {A'} V : A'}$
- \qquad
+ \and
$\inferrule*[lab=DnCast]
{\Gamma\pipe \Delta \vdash M : \u B' \and \u B \ltdyn \u B'}
{\Gamma\pipe \Delta \vdash \dncast{\u B}{\u B'} M : \u B}$
@@ -861,29 +858,45 @@ orderings on types and terms.
\inferrule*[lab=Var]
{ }
{\Gamma,x : A,\Gamma' \vdash x : A}
- \qquad
+ \and
\inferrule*[lab=Hole]
{ }
{\Gamma\pipe \bullet : \u B \vdash \bullet : \u B}
- \qquad
+ \and
\inferrule*[lab=Err]
{ }
{\Gamma \mid \cdot \vdash \err_{\u B} : \u B}
- \\
-\iflong
+ \and
+ \inferrule*[lab=$U$I]
+ {\Gamma \mid \cdot \vdash M : \u B}
+ {\Gamma \vdash \thunk M : U \u B}
+ \and
+ \inferrule*[lab=$U$E]
+ {\Gamma \vdash V : U \u B}
+ {\Gamma \pipe \cdot \vdash \force V : \u B}
+ \and
+ \inferrule*[lab=$F$I]
+ {\Gamma \vdash V : A}
+ {\Gamma \pipe \cdot \vdash \ret V : \u F A}
+ \and
+ \inferrule*[lab=$F$E]
+ {\Gamma \pipe \Delta \vdash M : \u F A \\
+ \Gamma, x: A \pipe \cdot \vdash N : \u B}
+ {\Gamma \pipe \Delta \vdash \bindXtoYinZ M x N : \u B}
+
\\
\inferrule*[lab=$0$E]
{\Gamma \vdash V : 0}
{\Gamma \mid \Delta \vdash \abort V : T}
- \qquad
+ \and
\inferrule*[lab=$+$Il]
{\Gamma \vdash V : A_1}
{\Gamma \vdash \inl V : A_1 + A_2}
- \qquad
+ \and
\inferrule*[lab=$+$Ir]
{\Gamma \vdash V : A_2}
{\Gamma \vdash \inr V : A_1 + A_2}
- \qquad
+ \and
\inferrule*[lab=$+$E]
{
\Gamma \vdash V : A_1 + A_2 \\\\
@@ -891,78 +904,55 @@ orderings on types and terms.
\Gamma, x_2 : A_2 \mid \Delta \vdash E_2 : T
}
{\Gamma \mid \Delta \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} : T}
- \\\\
- \fi
+ \and
\inferrule*[lab=$1$I]
{ }
{\Gamma \vdash (): 1}
- \,\,\,
+ \and
\inferrule*[lab=$1$E]
{\Gamma \vdash V : 1 \and
\Gamma \mid \Delta \vdash E : T
}
{\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
- \,\,\,
+ \and
\inferrule*[lab=$\times$I]
{\Gamma \vdash V_1 : A_1\and
\Gamma\vdash V_2 : A_2}
{\Gamma \vdash (V_1,V_2) : A_1 \times A_2}
- \,\,\,
+ \and
\inferrule*[lab=$\times$E]
{\Gamma \vdash V : A_1 \times A_2 \\\\
\Gamma, x : A_1,y : A_2 \mid \Delta \vdash E : T
}
{\Gamma \mid \Delta \vdash \pmpairWtoXYinZ V x y E : T}
- \\\\
- \inferrule*[lab=$U$I]
- {\Gamma \mid \cdot \vdash M : \u B}
- {\Gamma \vdash \thunk M : U \u B}
- \,\,\,
- \inferrule*[lab=$U$E]
- {\Gamma \vdash V : U \u B}
- {\Gamma \pipe \cdot \vdash \force V : \u B}
- \,\,\,
- \inferrule*[lab=$F$I]
- {\Gamma \vdash V : A}
- {\Gamma \pipe \cdot \vdash \ret V : \u F A}
- \,\,\,
- \inferrule*[lab=$F$E]
- {\Gamma \pipe \Delta \vdash M : \u F A \\
- \Gamma, x: A \pipe \cdot \vdash N : \u B}
- {\Gamma \pipe \Delta \vdash \bindXtoYinZ M x N : \u B}
- \\\\
+ \and
\inferrule*[lab=$\to$I]
{\Gamma, x: A \pipe \Delta \vdash M : \u B}
{\Gamma \pipe \Delta \vdash \lambda x : A . M : A \to \u B}
- \quad
+ \and
\inferrule*[lab=$\to$E]
{\Gamma \pipe \Delta \vdash M : A \to \u B\and
\Gamma \vdash V : A}
{\Gamma \pipe \Delta \vdash M\,V : \u B }
-\iflong
- \\\\
+ \and
\inferrule*[lab=$\top$I]{ }{\Gamma \mid \Delta \vdash \emptypair : \top}
- \quad
+ \and
\inferrule*[lab=$\with$I]
{\Gamma \mid \Delta \vdash M_1 : \u B_1\and
\Gamma \mid \Delta \vdash M_2 : \u B_2}
{\Gamma \mid \Delta \vdash \pair {M_1} {M_2} : \u B_1 \with \u B_2}
- \quad
+ \and
\inferrule*[lab=$\with$E]
{\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
{\Gamma \mid \Delta \vdash \pi M : \u B_1}
- \quad
+ \and
\inferrule*[lab=$\with$E']
{\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
{\Gamma \mid \Delta \vdash \pi' M : \u B_2}
-\fi
- \end{array}
- \end{array}
- \]
-\end{small}
- \vspace{-0.1in}
- \caption{GTT Syntax and Term Typing \ifshort{($+$ and $\with$ typing rules in extended version)}\fi}
- \label{fig:gtt-syntax-and-terms}
+ \end{mathpar}
+ \end{small}
+ \caption{GTT Typing}
+ \label{fig:gtt-typing}
\end{figure}
\subsection{Background: Call-by-Push-Value}
@@ -977,7 +967,7 @@ computations: for example, we might have an error computation $\err_{\u
if $V : \kw{string}$ and $M : \u B$, which prints $V$ and then behaves as
$M$.
-\emph{Value types and complex values.}
+\paragraph{Value types and complex values}
The value types include \emph{eager} products $1$ and $A_1 \times A_2$
and sums $0$ and $A_1 + A_2$, which behave as in a call-by-value/eager
language (e.g. a pair is only a value when its components are). The
@@ -993,10 +983,8 @@ class of ``pure functions'' from $A$ to $A'$ (though there is no pure
function \emph{type} internalizing this judgement), which can be treated
like values by a compiler because they have no effects (e.g. they can be
dead-code-eliminated, common-subexpression-eliminated, and so on).
-\begin{longonly}
In focusing~\cite{andreoli92focus} terminology, complex
values consist of left inversion and right focus rules.
-\end{longonly}
For each pattern-matching construct (e.g. case analysis on a sum,
splitting a pair), we have both an elimination rule whose branches are
values (e.g. $\pmpairWtoXYinZ{p}{x_1}{x_2}{V}$) and one whose branches
@@ -1017,7 +1005,7 @@ $\letXbeYinZ{V}{x}{\letXbeYinZ{V'}{x'}{M}} \equiv
\letXbeYinZ{V'}{x'}{\letXbeYinZ{V}{x}{M}}$ --- complex values can be
reordered, while arbitrary computations cannot).
-\emph{Shifts.}
+\paragraph{Shifts}
A key notion in CBPV is the \emph{shift} types $\u F A$ and $U \u B$,
which mediate between value and computation types: $\u F A$ is the
computation type of potentially effectful programs that return a value
@@ -1033,26 +1021,21 @@ The introduction and elimination rules for $U$ are written $\thunk{M}$
and $\force{V}$, and say that computations of type $\u B$ are bijective
with values of type $U \u B$. As an example of the action of the
shifts,
-\begin{longonly}
$0$ is the empty value type, so $\u F 0$ classifies effectful
computations that never return, but may perform effects (and then, must
e.g. non-terminate or error), while $U \u F 0$ is the value type where
such computations are thunked/delayed and considered as values.
-\end{longonly}
$1$ is the trivial value type, so $\u F 1$ is the type of computations
that can perform effects with the possibility of terminating
successfully by returning $()$, and $U \u F 1$ is the value type where
such computations are delayed values.
-\begin{longonly}
$U \u F$ is a monad on value
types~\citep{moggi91}, while $\u F U$ is a comonad on computation types.
-\end{longonly}
-\emph{Computation types.}
-The computation type constructors in CBPV include lazy unit/products
-$\top$ and $\u B_1 \with \u B_2$, which behave as in a call-by-name/lazy
-language (e.g. a component of a lazy pair is evaluated only when it is
-projected). Functions $A \to \u B$ have a value type as input and a
+\paragraph{Computation types}
+The computation type constructors in CBPV include first the lazy unit
+$\top$ and lazy product $\u B_1 \with \u B_2$, which behave as in a call-by-name language (e.g. a component of a lazy pair is evaluated only when it is
+projected). Functions $A \to \u B$ have a value type as input and a
computation type as a result. The equational theory of effects in CBPV
computations may be surprising to those familiar only with
call-by-value, because at higher computation types effects have a
@@ -1066,16 +1049,13 @@ computation means supplying it with an argument, and applying both of
the above to an argument $V$ is defined to result in $\print c;M[V/x]$.
This does \emph{not} imply that the corresponding equations holds for
the call-by-value function type, which we discuss below.
-\begin{longonly}
As another
example, \emph{all} computations are considered equal at type $\top$,
even computations that perform different effects ($\print c$ vs. $\{\}$
-vs. $\err$), because there is by definition \emph{no} way to extract an
-observable of type $\u F A$ from a computation of type $\top$.
+vs. $\err$), because there is by definition \emph{no} way to extract an observable type $\u F A$ from a computation of type $\top$.
Consequently, $U \top$ is isomorphic to $1$.
-\end{longonly}
-\emph{Complex stacks.} Just as the complex values $V$ are a syntactic
+\paragraph{Complex stacks} Just as the complex values $V$ are a syntactic
class terms that have no effects, CBPV includes a judgement for
``stacks'' $S$, a syntactic class of terms that reflect \emph{all}
effects of their input. A \emph{stack} $\Gamma \mid \bullet : \u B
@@ -1093,11 +1073,9 @@ introduction forms for the stack's output type. For example, $\bullet :
than once, because running it requires choosing a projection to get to
an observable of type $\u F A$, so \emph{each time it is run} it uses
$\bullet$ exactly once.
-\begin{longonly}
In
focusing terms, complex stacks include both left and right inversion,
and left focus rules.
-\end{longonly}
In the equational theory of CBPV, $\u F$ and $U$
are \emph{adjoint}, in the sense that stacks $\bullet : \u F A \vdash S
: \u B$ are bijective with values $x : A \vdash V : U \u B$, as both are
@@ -1108,7 +1086,7 @@ we use a typing judgement $\Gamma \mid \Delta \vdash M : \u B$ with a
``stoup'', a typing context $\Delta$ that is either
empty or contains exactly one assumption $\bullet : \u B$, so $\Gamma
\mid \cdot \vdash M : \u B$ is a computation, while $\Gamma \mid \bullet
-: \u B \vdash M : \u B'$ is a stack. The \ifshort{(omitted) }\fi typing
+: \u B \vdash M : \u B'$ is a stack. The typing
rules for $\top$ and $\with$ treat the stoup additively
(it is arbitrary in the conclusion and the same in all premises); for a
function application to be a stack, the stack input must occur in the
@@ -1116,7 +1094,7 @@ function position. The elimination form for $U \u B$, $\force{V}$, is
the prototypical non-stack computation ($\Delta$ is required to be
empty), because forcing a thunk does not use the stack's input.
-\emph{Embedding call-by-value and call-by-name.} To translate
+\paragraph{Embedding call-by-value and call-by-name.} To translate
call-by-value (CBV) into CBPV, a judgement $x_1 : A_1, \ldots, x_n : A_n
\vdash e : A$ is interpreted as a computation $x_1 : A_1^v, \ldots, x_n
: A_n^v \vdash e^v : \u F A^v$, where call-by-value products and sums
@@ -1166,7 +1144,7 @@ every CBPV program with a CBV or CBN type can be back-translated.
%% %% \to A_2 \to \u B$ \emph{supplies all of the arguments}
%% %% if the conclusion of the stack is an F?
-\emph{Extensionality/$\eta$ Principles.} The main advantage of CBPV for
+\paragraph{Extensionality/$\eta$ Principles} The main advantage of CBPV for
our purposes is that it accounts for the $\eta$/extensionality
principles of both eager/value and lazy/computation types, because
value types have $\eta$ principles relating them to the value
@@ -1201,7 +1179,6 @@ dynamism below.
%% {\Gamma \vdash S[\print V; M] \equidyn \print V; S[M] : \u C}
%% \end{mathpar}
-\ifshort \vspace{-0.1in} \fi
\subsection{The Dynamic Type(s)}
Next, we discuss the additions that make CBPV into our gradual type
@@ -1223,7 +1200,6 @@ would like constructions in GTT to imply results for many different
possible implementations of them. Instead, the terms for the dynamic
types will arise from type dynamism and casts.
-\ifshort \vspace{-0.12in} \fi
\subsection{Type Dynamism}
The \emph{type dynamism} relation of gradual type theory is written $A
@@ -1300,24 +1276,21 @@ in the domain~\citep{newahmed18,newlicata2018-fscd}.
\inferrule*[lab=$\to$Mon]{A \ltdyn A' \and \u B \ltdyn \u B'}
{A \to \u B \ltdyn A' \to \u B'}
-\begin{longonly}
\\
\framebox{Dynamism contexts}
-\quad
+\and
\inferrule{ }{\cdot \, \dynvctx}
-\quad
+\and
\inferrule{\Phi \, \dynvctx \and
A \ltdyn A'}
{\Phi, x \ltdyn x' : A \ltdyn A' \, \dynvctx}
-\quad
+\\
\inferrule{ }{\cdot \, \dyncctx}
-\quad
+\and
\inferrule{\u B \ltdyn \u B'}
{(\bullet \ltdyn \bullet : \u B \ltdyn \u B') \, \dyncctx}
-\end{longonly}
\end{mathpar}
- \vspace{-0.2in}
-\caption{GTT Type Dynamism \iflong and Dynamism Contexts \fi}
+\caption{GTT Type Dynamism and Dynamism Contexts}
\label{fig:gtt-type-dynamism}
\end{small}
\end{figure}
@@ -1472,62 +1445,24 @@ our design choice is forced for all casts, as long as the casts between ground t
\Phi \pipe \bullet \ltdyn \bullet : \u B_1 \ltdyn \u B_1' \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'
}
{\Phi \mid \Psi \vdash M_2[M_1/\bullet] \ltdyn M_2'[M_1'/\bullet] : \u B_2 \ltdyn \u B_2'}
- \\\\
- \ifshort
- \inferrule*[lab=$\times$ICong]
- {\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
- \Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
- {\Phi \vdash (V_1,V_2) \ltdyn (V_1',V_2') : A_1 \times A_2 \ltdyn A_1' \times A_2'}
- \quad
- \inferrule*[lab=$\to$ICong]
- {\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
- {\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
-
- \\\\
- \inferrule*[lab=$\times$ECong]
- {\Phi \vdash V \ltdyn V' : A_1 \times A_2 \ltdyn A_1' \times A_2' \\\\
- \Phi, x \ltdyn x' : A_1 \ltdyn A_1', y \ltdyn y' : A_2 \ltdyn A_2' \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
- }
- {\Phi \mid \Psi \vdash \pmpairWtoXYinZ V x y E \ltdyn \pmpairWtoXYinZ {V'} {x'} {y'} {E'} : T \ltdyn T'}
- \,\,
- \inferrule*[lab=$\to$ECong]
- {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
- \Phi \vdash V \ltdyn V' : A \ltdyn A'}
- {\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
- \\\\
- \inferrule*[lab=$F$ICong]
- {\Phi \vdash V \ltdyn V' : A \ltdyn A'}
- {\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
- \qquad
- \inferrule*[lab=$F$ECong]
- {\Phi \pipe \Psi \vdash M \ltdyn M' : \u F A \ltdyn \u F A' \\\\
- \Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'}
- {\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'}
- \\\\
- \fi
\end{array}
\]
- \vspace{-0.25in}
- \caption{GTT Term Dynamism (Structural \ifshort and Congruence\fi Rules) \ifshort
- (Rules for $U,1,+,0,\with,\top$ in extended version)
- \fi}
+ \caption{GTT Term Dynamism (Structural and Congruence Rules)}
\label{fig:gtt-term-dynamism-structural}
-\end{small}
+ \end{small}
\end{figure}
-\iflong
\begin{figure}
- \begin{small}
- \[
- \begin{array}{c}
+ \begin{footnotesize}
+ \begin{mathpar}
\inferrule*[lab=$+$IlCong]
{\Phi \vdash V \ltdyn V' : A_1 \ltdyn A_1'}
{\Phi \vdash \inl V \ltdyn \inl V' : A_1 + A_2 \ltdyn A_1' + A_2'}
- \qquad
+ \and
\inferrule*[lab=$+$IrCong]
{\Phi \vdash V \ltdyn V' : A_2 \ltdyn A_2'}
{\Phi \vdash \inr V \ltdyn \inr V' : A_1 + A_2 \ltdyn A_1' + A_2'}
- \\\\
+ \and
\inferrule*[lab=$+$ECong]
{
\Phi \vdash V \ltdyn V' : A_1 + A_2 \ltdyn A_1' + A_2' \\\\
@@ -1535,19 +1470,19 @@ our design choice is forced for all casts, as long as the casts between ground t
\Phi, x_2 \ltdyn x_2' : A_2 \ltdyn A_2' \mid \Psi \vdash E_2 \ltdyn E_2' : T \ltdyn T'
}
{\Phi \mid \Psi \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} \ltdyn \caseofXthenYelseZ V {x_1'. E_1'}{x_2'.E_2'} : T'}
- \qquad
+ \and
\inferrule*[lab=$0$ECong]
{\Phi \vdash V \ltdyn V' : 0 \ltdyn 0}
{\Phi \mid \Psi \vdash \abort V \ltdyn \abort V' : T \ltdyn T'}
- \\\\
+ \and
\inferrule*[lab=$1$ICong]{ }{\Phi \vdash () \ltdyn () : 1 \ltdyn 1}
- \qquad
+ \and
\inferrule*[lab=$1$ECong]
{\Phi \vdash V \ltdyn V' : 1 \ltdyn 1 \\\\
\Phi \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
}
{\Phi \mid \Psi \vdash \pmpairWtoinZ V E \ltdyn \pmpairWtoinZ V' E' : T \ltdyn T'}
- \\\\
+ \and
\inferrule*[lab=$\times$ICong]
{\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
\Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
@@ -1557,56 +1492,54 @@ our design choice is forced for all casts, as long as the casts between ground t
{\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
- \\\\
+ \and
\inferrule*[lab=$\times$ECong]
{\Phi \vdash V \ltdyn V' : A_1 \times A_2 \ltdyn A_1' \times A_2' \\\\
\Phi, x \ltdyn x' : A_1 \ltdyn A_1', y \ltdyn y' : A_2 \ltdyn A_2' \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
}
{\Phi \mid \Psi \vdash \pmpairWtoXYinZ V x y E \ltdyn \pmpairWtoXYinZ {V'} {x'} {y'} {E'} : T \ltdyn T'}
- \,\,
+ \and
\inferrule*[lab=$\to$ECong]
- {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
+ {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \and
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
- \\\\
+ \and
\inferrule*[lab=$U$ICong]
{\Phi \mid \cdot \vdash M \ltdyn M' : \u B \ltdyn \u B'}
{\Phi \vdash \thunk M \ltdyn \thunk M' : U \u B \ltdyn U \u B'}
- \qquad
+ \and
\inferrule*[lab=$U$ECong]
{\Phi \vdash V \ltdyn V' : U \u B \ltdyn U \u B'}
{\Phi \pipe \cdot \vdash \force V \ltdyn \force V' : \u B \ltdyn \u B'}
- \\\\
+ \and
\inferrule*[lab=$F$ICong]
{\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
- \qquad
+ \and
\inferrule*[lab=$F$ECong]
{\Phi \pipe \Psi \vdash M \ltdyn M' : \u F A \ltdyn \u F A' \\\\
\Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'}
{\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'}
- \\\\
+ \and
\inferrule*[lab=$\top$ICong]{ }{\Phi \mid \Psi \vdash \{\} \ltdyn \{\} : \top \ltdyn \top}
- \qquad
+ \and
\inferrule*[lab=$\with$ICong]
{\Phi \mid \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1'\and
\Phi \mid \Psi \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'}
{\Phi \mid \Psi \vdash \pair {M_1} {M_2} \ltdyn \pair {M_1'} {M_2'} : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
- \\\\
+ \and
\inferrule*[lab=$\with$ECong]
{\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
{\Phi \mid \Psi \vdash \pi M \ltdyn \pi M' : \u B_1 \ltdyn \u B_1'}
- \qquad
+ \and
\inferrule*[lab=$\with$E'Cong]
{\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
{\Phi \mid \Psi \vdash \pi' M \ltdyn \pi' M' : \u B_2 \ltdyn \u B_2'}
- \end{array}
- \]
- \caption{GTT Term Dynamism (Congruence Rules)}
- \label{fig:gtt-term-dynamism-ext-congruence}
-\end{small}
+ \end{mathpar}
+ \caption{GTT Term Dynamism (Congruence Rules)}
+ \label{fig:gtt-term-dynamism-ext-congruence}
+ \end{footnotesize}
\end{figure}
-\fi
The final piece of GTT is the \emph{term dynamism} relation, a syntactic
judgement that is used for reasoning about the behavioral properties of
@@ -4483,7 +4416,6 @@ of the operational behavior of a standard Call-by-value cast calculus.
\end{itemize}
\end{proof}
-
\section{Contract Models of GTT}
\label{sec:contract}
--
GitLab