begin appendix

paper-new/appendix.tex

+\section{Details of the Construction of an Extensional Model}
+
+In Section \ref{sec:extensional-model-construction}, we outline the construction
+of an extensional model of gradual typing starting from a step-1 intensional model.
+In this section, we provide the details for each of the constructions mentioned there.
+
+\begin{lemma}\label{lem:step-1-model-to-step-2-model}
+Let $\mathcal M$ be a \hyperref[def:step-1-model]{step-1 intensional model}.
+Suppose we are given the following data:
+
+\begin{enumerate}
+    \item For each value type $A$, a monoid $\pv_A$ and homomorphism 
+    \[ \ptbv_A : \pv_A \to \{ f \in \vf(A,A) \mid f \bisim \id \} \]
+
+    \item For each computation type $B$, a monoid $\pv_B$ and homomorphism
+    \[ \ptbe_B : \pe_B \to \{ g \in \ef(B,B) \mid g \bisim \id \} \]
+
+    \item For each value type $A$, a distinguished endomorphism
+    $\delta_A \in \ef(FA, FA)$ such that $\delta_A \bisim \id_{FA}$.
+\end{enumerate}
+
+Then we can construct a \hyperref[def:step-2-model]{step-2 intensional model}.
+\end{lemma}
+\begin{proof}
+    Write 
+    %
+    \[ \mathcal M = (\vf, \vsq, \ef, \esq, \Ff, \Fsq, \Uf, \Usq, \arrf, \arrsq). \] 
+    %
+    Define a step-2 model as follows:
+    \begin{itemize}
+      \item Value objects are tuples of an object $A$ in $\vf$ along with the monoid
+      $\pv_A$ and homomorphism $\ptbv_A$:
+      $\ob(\vf') = \{ (A, \pv_A, \ptbv_A) \mid A \in \ob(\vf) \}$.
+      
+      \item Morphisms are given by morphisms of the underlying objects in $\vf$, i.e.,
+       $\vf'((A, \pv_A, \ptbv_A), (A', \pv_{A'}, \ptbv_{A'})) = \vf(A, A')$.
+      
+      \item Computation objects are tuples 
+      $\ob(\ef') = \{ (B, \pe_B, \ptbe_B) \mid B \in \ob(\ef) \}$.
+      
+      \item Computation morphisms are $\ef'((B, \pv_B, \ptbv_B), (B', \pv_{B'}, \ptbv_{B'})) = \ef(B, B')$.
+      
+      \item The objects $\vsq'$ and $\esq'$ are the same as those of $\vsq$ and $\esq$.
+      
+      \item The morphisms of $\vsq'$ and $\esq'$ are the same as those of $\vsq$ and $\esq$.
+    %   \item $\ob(\vsq') = \ob(\vsq)$
+    %   \item $\ob(\esq') = \ob(\esq)$
+    %   \item $\vsq'(c, c') = \vsq(c, c')$
+    %   \item $\esq'(d, d') = \esq(d, d')$
+      
+      % Functors \times, +, F, U, arrow
+      \item We define $F$ on objects by $F (A, \pv_A, \ptbv_A) = (FA, (1 + \pv_A), h_F)$
+      where $1$ is the trivial monoid, $+$ is the coproduct in the category of monoids, and $h_F$ is the homomorphism defined as follows:
+
+      \item We define $U$ on objects by $U (B, \pe_B, \ptbe_B) = (UB, \pe_B, h_U)$
+      where $h_U(p_B) = U(\ptbe_B(p_B))$.
+      
+      \item We define $(A, \pv_A, \ptbv_A) \arr (B, \pe_B, \ptbe_B) = (A \arr B, \pv_A \times \pe_B, h_\arr)$
+      where $\times$ is the product in the category of monoids, and $h_\arr$ is defined by 
+      $h_\arr(p_A, p_B) = \ptbv_A(p_A) \arr \ptbe_B(p_B)$.
+    \end{itemize}
+\end{proof}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{lemma}\label{lem:step-2-model-to-step-3-model}
+    Let $\mathcal M$ be a \hyperref[def:step-2-model]{step-2 intensional model}.
+    Suppose we are given the following data:
+
+    Then we can construct a \hyperref[def:step-3-model]{step-3 intensional model}.
+\end{lemma}
+\begin{proof}
+
+\end{proof}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\begin{lemma}\label{lem:step-4-model-to-extensional-model}
+  Let $\mathcal M$ be a \hyperref[def:step-4-model]{step-4 intensional model}.
+  Then we can define an extensional model.
+\end{lemma}
+\begin{proof}
+  
+  
+  % More formally, we define an extensional model $\mathcal M_e$ as follows.
+  % \begin{itemize}
+  %   \item 
+  % \end{itemize}
+\end{proof}
+
+
+
+\section{Adequacy}\label{sec:appendix-adequacy}
+
+In this section, we show an adequacy result for the extensional model of GTT we obtained by
+applying the abstract construction introduced in Section
+\ref{sec:extensional-model-construction} to the concrete model
+
+First we establish some notation. Fix a morphism $f : 1 \to \li \Nat \cong \li \Nat$.
+We write that $f \da n$ to mean that there exists $m$ such that $f = \delta^m(\eta n)$
+and $f \da \mho$ to mean that there exists $m$ such that $f = \delta^m(\mho)$.
+
+Recall that $\ltls$ denotes the relation on value morphisms defined as the bisimilarity-closure
+of the intensional error-ordering on morphisms.
+More concretely, we have $f \ltls g$ iff there exists $f'$ and $g'$ with
+
+\[ f \bisim f' \le g' \bisim g. \]
+
+The result we would like to show is as follows:
+\begin{lemma}
+If $f \ltls g : \li \Nat$, then:
+\begin{itemize}
+  \item If $f \da n$ then $g \da n$.
+  \item If $g \da \mho$ then $f \da \mho$.
+  \item If $g \da n$ then $f \da n$.
+\end{itemize}
+\end{lemma}
+
+Unfortunately, this result is actually not provable!
+Roughly speaking, the issue is that this is a ``global'' result, and it is not possible
+to prove such results inside of the guarded setting. 
+In particular, if we tried to prove a result such as the above in the guarded setting,
+we would run into a problem where we would have a natural number ``stuck'' under a $\later$
+with no way to get at the underlying number.
+
+Thus, to prove our adequacy result, we need to leave the guarded setting and pass back
+to the normal set-theoretic world.
+As mentioned in the Technical Background section (Section \ref{sec:sgdt}), we can do this
+using \emph{clock quantification}.
+
+Recall that all of the constructions we have made in SGDT take place in the context of a clock $k$.
+All of our uses of the later modality and guarded recursion happen with respect to this clock.
+For example, consider the definition of the lift monad by guarded recursion in Section \ref{TODO}.
+% We define the lift monad $\li^k X$ as the guarded fixpoint of $\lambda \tilde{T}. X + 1 + \later^k_t (\tilde{T}_t)$.
+We can view this definition as being parameterized by a clock $k$: $\li^k : \type \to \type$.
+Then for $X$ satisfying a certain technical requirement, we can define the ``global lift'' monad as $\li^{gl} X = \forall k. \li^k X$.
+
+
+It can be shown that the global lift monad is isomorphic to the so-called Delay monad of Capretta \cite{TODO}.
+
+
+% We have been writing the type as $\li X$, but it is perhaps more accurate to write it as $\li^k X$ to
+% emphasize that the construction is parameterized by a clock $k$.
+

paper-new/paper.tex

@@ -146,6 +146,14 @@
 
 \input{discussion}
 
+
+\bibliographystyle{ACM-Reference-Format}
+\bibliography{references}
+
+\appendix
+\input{appendix}
+
+
 % \section{Discussion}\label{sec:discussion}
 
 % \subsection{Synthetic Ordering}
@@ -162,7 +170,4 @@
 % treatment of the error ordering as well.
 
 
-\bibliographystyle{ACM-Reference-Format}
-\bibliography{references}
-
 \end{document}