From 5307ddfb000a5f9d105ecce84b0801d6f634681f Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Thu, 16 Nov 2023 11:44:31 -0500
Subject: [PATCH] begin rearranging: discuss term syn/sem and then ordering
syn/sem
---
paper-new/defs.tex | 9 +
paper-new/graduality.tex | 47 ++-
paper-new/intro.tex | 232 +++++++++-----
paper-new/ordering.tex | 443 +++++++++++++++++++++++++++
paper-new/paper.tex | 16 +-
paper-new/technical-background.tex | 63 +++-
paper-new/terms.tex | 473 +++++++++++++++++++++++++++++
7 files changed, 1176 insertions(+), 107 deletions(-)
create mode 100644 paper-new/ordering.tex
create mode 100644 paper-new/terms.tex
diff --git a/paper-new/defs.tex b/paper-new/defs.tex
index 2c54f38..3ec98ba 100644
--- a/paper-new/defs.tex
+++ b/paper-new/defs.tex
@@ -71,6 +71,15 @@
\newcommand{\Dwn}{\Downarrow}
\newcommand{\qte}[1]{\text{quote}({#1})}
+\newcommand{\elab}[1]{\text{Elab}({#1})}
+
+% Perturbations
+\newcommand{\pertp}{\text{Pert}^\text{P}}
+\newcommand{\perte}{\text{Pert}^\text{E}}
+\newcommand{\pertdyn}[2]{\text{pert-dyn}({#1}, {#2})}
+\newcommand{\delaypert}[1]{\text{delay-pert}({#1})}
+
+
% SGDT and Intensional Stuff
\newcommand{\later}{\vartriangleright}
diff --git a/paper-new/graduality.tex b/paper-new/graduality.tex
index b5e4f66..9be65c0 100644
--- a/paper-new/graduality.tex
+++ b/paper-new/graduality.tex
@@ -1,18 +1,49 @@
-\section{Unary Canonicity}
-Before discussing graduality, we seek to prove its ``unary'' analogue.
-Namely, instead of considering inequality between terms, we start by considering equality.
-
-
\section{Graduality}\label{sec:graduality}
+Now we move to the proof of graduality.
The main theorem we would like to prove is the following:
+% TODO use the etmprec notation
\begin{theorem}[Graduality]
If $\cdot \vdash M \ltdyn N : \nat$, then
\begin{enumerate}
- \item If $N = \mho$, then $M = \mho$
- \item If $N = `n$, then $M = \mho$ or $M = `n$
- \item If $M = V$, then $N = V$
+ \item $M \Downarrow$ iff $N \Downarrow$
+ \item If $M \Downarrow v_?$ and $N \Downarrow v'_?$ then either $v_? = \mho$, or $v_? = v'_?$.
\end{enumerate}
\end{theorem}
+\subsection{Proof Overview}
+
+We split the proof into three main steps. The first concerns the translation
+of the surface syntax $\extlc$ to the intensional syntax $\intlc$.
+
+\begin{lemma}[]
+ If $\etmprec{\gamlt}{M}{N}{c}$, then there exist $M'$ and $N'$ such that
+
+ \[ i(M) \synbisim M' \ltdyn_i N' \synbisim i(N). \]
+\end{lemma}
+
+Next we show that the notions of intensional syntactic term precision and
+syntactic bisimilarity imply their corresponding semantic counterparts:
+
+\begin{lemma}[]
+ If $\itmprec{\gamlt}{M}{N}{c}$, then $\sem{M} \semlt {\sem{N}}$
+\end{lemma}
+
+\begin{lemma}
+ If $M \synbisim N$, then $\sem{M} \bisim \sem{N}$.
+\end{lemma}
+
+Finally, we need an adequacy result stating that the semantic notions of error
+ordering and bisimilarity for natural numbers imply that the values of the
+lift monad that they relate have the expected behavior.
+
+\begin{lemma}
+ Let $l, l' : \li \Nat$.
+ If $l \semlt l'$, then either (1) $l = \delta^n(\mho)$ for some $n$, or (2)
+ $l = l' = \delta^n(\eta m)$ for some $n$ and $m$, or (3) $l$ and $l'$ fail to terminate.
+\end{lemma}
+\begin{lemma}
+ If $l \bisim l'$, then either (1) $l = \delta^n(\mho)$ and $l' = \delta^{n'}(\mho)$ for some $n$ and $n'$,
+ (2) $l = \delta^n(\eta m)$ and $l' = \delta^{n'}(\eta m)$, or $l$ and $l'$ fail to terminate.
+\end{lemma}
\ No newline at end of file
diff --git a/paper-new/intro.tex b/paper-new/intro.tex
index d5f1b03..19d3ae4 100644
--- a/paper-new/intro.tex
+++ b/paper-new/intro.tex
@@ -7,27 +7,29 @@ whether they are \emph{static} or \emph{dynamic}.
In static typing, the code is type-checked at compile time, while in dynamic typing,
the type checking is deferred to run-time. Both approaches have benefits: with static typing,
the programmer is assured that if the program passes the type-checker, their program
-is free of type errors. Meanwhile, dynamic typing allows the programmer to rapidly prototype
+is free of type errors, and moreover, the equational theory implies that program optimizations are valid.
+Meanwhile, dynamic typing allows the programmer to rapidly prototype
their application code without needing to commit to fixed type signatures for their functions.
-\emph{Gradually-typed languages} \cite{siek-taha06} allow for both static and dynamic typing disciplines
-to be used in the same codebase, and support smooth interoperability between statically-typed
-and dynamically-typed code.
+\emph{Gradually-typed languages} \cite{siek-taha06, tobin-hochstadt06} allow
+for both static and dynamic typing disciplines to be used in the same codebase,
+and support smooth interoperability between statically-typed and dynamically-typed code.
This flexibility allows programmers to begin their projects in a dynamic style and
enjoy the benefits of dynamic typing related to rapid prototyping and easy modification
while the codebase ``solidifies''. Over time, as parts of the code become more mature
and the programmer is more certain of what the types should be, the code can be
-\emph{gradually} migrated to a statically typed style without needing to start the project
-over in a completely differnt language.
+\emph{gradually} migrated to a statically typed style without needing to
+rewrite the project in a completely different language.
-Gradually-typed languages should satisfy two intuitive properties.
+%Gradually-typed languages should satisfy two intuitive properties.
+The following two properties have been identified as useful for gradually typed languages.
First, the interaction between the static and dynamic components of the codebase
-should be safe -- i.e., should preserve the guarantees made by the static types.
+should preserve the guarantees made by the static types.
In particular, while statically-typed code can error at runtime in a gradually-typed language,
such an error can always be traced back to a dynamically-typed term that
violated the typing contract imposed by statically typed code.
% In other words, in the statically-typed portions of the codebase, type soundness must be preserved.
-Second, gradually-typed langugaes should support the smooth migration from dynamic typing
+Second, gradually-typed languages should support the smooth migration from dynamic typing
to static typing, in that the programmer can initially leave off the
typing annotations and provide them later without altering the meaning of the
program.
@@ -36,7 +38,7 @@ program.
Formally speaking, gradually typed languages should satisfy the
\emph{dynamic gradual guarantee}, originally defined by Siek, Vitousek, Cimini,
and Boyland \cite{siek_et_al:LIPIcs:2015:5031}.
-This property is also referred to as \emph{graduality}, by analogy with parametricity.
+This property is also referred to as \emph{graduality} \cite{new-ahmed2018}, by analogy with parametricity.
Intuitively, graduality says that going from a dynamic to static style should not
introduce changes in the meaning of the program.
More specifically, making the types more precise by adding typing annotations
@@ -48,19 +50,26 @@ or will result in a type error.
\subsection{Current Approaches to Proving Graduality}
Current approaches to proving graduality include the methods of Abstracting Gradual Typing
-\cite{garcia-clark-tanter2016} and the formal tools of the Gradualier \cite{cimini-siek2016}.
-These allow the language developer to start with a statically typed langauge and derive a
-gradually typed language that satisfies the gradual guarantee. The downside to these approaches
-is that the semantics of the resulting languages are too lazy: the frameworks consider only
-the $\beta$ rules and not the $\eta$ equalities. Furthermore, while these frameworks do prove
+\cite{garcia-clark-tanter2016} and the formal tools of the Gradualizer \cite{cimini-siek2016}.
+These allow the language developer to start with a statically typed language and derive a
+gradually typed language that satisfies the gradual guarantee. The main downside to
+these approaches lies in their inflexibility: since the process in entirely mechanical,
+the language designer must adhere to the predefined framework.
+Many gradually typed languages do not fit into either framework, e.g., Typed Racket
+\cite{tobin-hochstadt06, tobin-hochstadt08}.
+%
+Furthermore, while these frameworks do prove
graduality of the resulting languages, they do not show the correctness of the equational theory,
which is equally important to sound gradual typing. For example, programmers often refactor their
-code without thinking about whether the refactoring has broken the semantics of the program.
-It is the validity of the laws in the equational theory that guarantees that such refactorings are sound.
+code, and in so doing they rely implicitly on the validity of the laws in the equational theory.
Similarly, correctness of compiler optimizations rests on the validity of the corresponding equations
-from the equational theory. It is therefore important that the langages that claim to be gradually typed
+from the equational theory. It is therefore important that the languages that claim to be gradually typed
have provably correct equational theories.
+% The approaches are too inflexible... the fact that the resulting semantics are too lazy
+% is a consequence of that inflexibility.
+% The validity of the equational theory captures the programmer's intuitive thinking when they refactor their code
+
%The downside is that
%not all gradually typed languages can be derived from these frameworks, and moreover, in both
%approaches the semantics is derived from the static type system as opposed to the alternative
@@ -75,33 +84,100 @@ gradual guarantee.
Moreover, their axiomatic account of program equivalence allows for type-based reasoning
about program equivalences.
%
-In this approach, a logical relation is constructed and shown to be sound with respect to
-the notion of observational approximation that specifies when one program is more precise than another.
+In this approach, a logical relation is constructed and used to show that the equational theory
+is sound with respect to the operational semantics.
+%and shown to be sound with respect to
+%the notion of observational approximation that specifies when one program is more precise than another.
The downside of this approach is that each new language requires a different logical relation
to prove graduality. Furthermore, the logical relations tend to be quite complicated due
-to a technical requirement known as \emph{step-indexing}.
+to a technical requirement known as \emph{step-indexing}, where the stepping behavior of terms
+must be accounted for in the logical relation.
As a result, developments using this approach tend to require vast effort, with the
corresponding technical reports having 50+ pages of proofs.
+%
+Additionally, while the axioms of gradual type theory are compositional at a ``global'' level,
+they do not compose in the step-indexed setting. One of the main goals of the present work
+is to formulate a composable theory of gradual typing in a setting where the stepping behavior
+is tracked.
An alternative approach, which we investigate in this paper, is provided by
\emph{synthetic guarded domain theory}.
-The tecnhiques of synthetic guarded domain theory allow us to internalize the
+The techniques of synthetic guarded domain theory allow us to internalize the
step-index reasoning normally required in logical relations proofs of graduality,
ultimately allowing us to specify the logical relation in a manner that looks nearly
identical to a typical, non-step-indexed logical relation.
-In this paper, we report on work we have done to mechanize proofs of graduality and
-correctness of equational theories using SGDT techniques in Agda.
-Our goal in this work is to mechanize these proofs in a reusable way,
+In this paper, we report on work we have done towards mechanizing proofs of graduality
+and soundness of the equational theory of cast calculi using the techniques of SGDT.
+We take a step toward mechanization in the Agda proof assistant by describing a compositional
+denotational semantics for gradual typing in a setting where the steps taken by terms are tracked.
+
+Our longer-term goal is to mechanize these proofs in a reusable way,
thereby providing a framework to use to more easily and
-conveniently prove that existing languages satsify graduality and have
+conveniently prove that existing languages satisfy graduality and have
sound equational theories. Moreover, the aim is for designers of new languages
-to utlize the framework to facilitate the design of new provably-correct
-gradually-typed languages with nontrivial features.
+to utilize the framework to facilitate the design of new provably-correct
+gradually-typed languages with more complex features.
+
+
+\subsection{Contributions}
+Our main contribution is a compositional denotational semantics for step-aware gradual typing,
+analogous to Gradual Type Theory but now in the ``intensional" setting.
+In parallel, we are developing a reusable framework in
+Guarded Cubical Agda for developing machine-checked proofs of graduality of a cast calculus.
+To demonstrate the feasibility and utility of our approach, we are applying the framework
+to prove graduality for the simply-typed gradual lambda calculus.
+% Along the way, we have developed an ``intensional" theory of graduality that is of
+% independent interest.
+
+
+\subsection{Overview of Remainder of Paper}
+
+In Section \ref{sec:overview}, we give an overview of the gradually-typed lambda
+calculus and the graduality theorem.
+%
+In Section \ref{sec:technical-background}, we provide technical background on gradually typed languages and
+on synthetic guarded domain theory.
+%
+In Section \ref{sec:gtlc-terms}, we introduce the gradually-typed cast calculus
+for which we will prove graduality. We give a semantics to the terms
+using the tools of guarded type theory.
+% Important here are the notions of syntactic
+% type precision and term precision. For reasons we describe below, we
+% introduce two related calculi, one in which the stepping behavior of terms is
+% implicit (an \emph{extensional} calculus, $\extlc$), and another where this behavior
+% is made explicit (an \emph{intensional} calculus, $\intlc$).
+%
+
+In Section \ref{sec:gtlc-precision}, we define the term precision ordering
+and describe our approach to assigning a denotational semantics to this ordering.
+This approach builds on the semantics constructed in the previous section,
+but extending it to the term ordering presents new challenges.
+
+
+% In Section \ref{sec:domain-theory}, we define several fundamental constructions
+% internal to SGDT that will be needed when we give a denotational semantics to
+% the gradual lambda calculus.
+%This includes the Lift monad, predomains and error domains.
+%
+% In Section \ref{sec:semantics}, we define the denotational semantics for the
+% intensional gradually-typed lambda calculus using the domain theoretic
+% constructions defined in the previous section.
+%
+In Section \ref{sec:graduality}, we outline in more detail the proof of graduality for the
+extensional gradual lambda calculus.
+%
+In Section \ref{sec:discussion}, we discuss the benefits and drawbacks to our approach in comparison
+to the traditional step-indexing approach, as well as possibilities for future work.
-\subsection{Proving Graduality in SGDT}
-\textbf{TODO:} This section should probably be moved to after the relevant background has been introduced?
+
+
+\section{Overview}\label{sec:overview}
+
+% This section used to be part of the intro.
+% \subsection{Proving Graduality in SGDT}
+% TODO This section should probably be moved to after the relevant background has been introduced?
% TODO introduce the idea of cast calculus and explicit casts?
@@ -128,7 +204,7 @@ The graduality theorem is shown below.
\begin{theorem}[Graduality]
If $\cdot \vdash M \ltdyn N : \nat$, then
\begin{enumerate}
- \item $M \Downarrow$ iff $N \Downarrow$
+ \item $M \Downarrow$ iff $N \Downarrow$.
\item If $M \Downarrow v_?$ and $N \Downarrow v'_?$ then either $v_? = \mho$, or $v_? = v'_?$.
\end{enumerate}
\end{theorem}
@@ -140,69 +216,61 @@ Details can be found in later sections, but we provide a brief explanation of th
$M$ is ``syntactically more precise'' than $N$, or equivalently, $N$ is
``more dynamic'' than $M$. Intuitively this means that $M$ and $N$ are the
same except that in some places where $M$ has explicit typing annotations,
- $N$ has $\dyn$ instead.
+ $N$ has $\dyn$ instead. The relation $\ltdyn$ on terms is called ``term precision''.
+ Term precision is intended to model the situation where a term $M$ behaves the
+ same as another term $N$ except that $M$ may error more than $N$.
+ Term precision is defined by a set of axioms that capture this intuitive notion.
+ This will be described in more detail in Section \ref{sec:GTLC}.
+
\item $\cdot \Downarrow$ is a relation on terms that is defined such that $M \Downarrow$ means
that $M$ terminates, either with a run-time error or a value $n$ of type $\nat$.
+
\item $\mho$ is a syntactic representation of a run-time type error, which
happens, for example, when a programmer tries to call a function with a value whose type
is found to be incompatible with the argument type of the function.
+
\item $v_?$ is shorthand for the syntactic representation of a term that is either equal to
$\mho$, or equal to the syntactic representation of a value $n$ of type $\nat$.
\end{itemize}
% We also should be able to show that $\mho$, $\zro$, and $\suc\, N$ are not equal.
-Our first step toward proving graduality is to formulate an \emph{step-sensitive}, or \emph{intensional},
-gradual lambda calculus, which we call $\intlc$, in which the computation steps taken by a term are made explicit.
-The ``normal'' gradual lambda calculus for which we want to prove graduality will be called the
-\emph{step-insensitive}, or \emph{extensional}, gradual lambda calculus, denoted $\extlc$.
-We will define an erasure function $\erase{\cdot} : \intlc \to \extlc$ which takes a program in the intensional lambda calculus
-and ``forgets'' the syntactic information about the steps to produce a term in the extensional calculus.
-
-Every term $M_e$ in $\extlc$ will have a corresponding program $M_i$ in $\intlc$ such that
-$\erase{M_i} = M_e$. Moreover, we will show that if $M_e \ltdyn_e M_e'$ in the extensional theory,
-then there exists terms $M_i$ and $M_i'$ such that $\erase{M_i}=M_e$, $\erase{M_i'}=M_e'$ and
-$M_i \ltdyn_i M_i'$ in the intensional theory.
-
-We formulate and prove an analogous graduality theorem for the intensional lambda calculus.
-We define an interpretation of the intensional lambda calculus into a model in which we prove
-various results. Using the observation above, given $M_e \ltdyn M_e' : \nat$, we can find
-intensional programs $M_i$ and $M_i'$ that erase to them and are such that $M_i \ltdyn M_i'$.
-We will then apply the intensional graduality theorem to $M_i$ and $M_i'$, and translate the result
-back to $M_e$ and $M_e'$.
-
-\subsection{Contributions}
-Our main contribution is a reusable framework in Guarded Cubical Agda for developing machine-checked proofs
-of graduality of a cast calculus.
-To demonstrate the feasability and utility of our approach, we have used the framework to prove
-graduality for the simply-typed gradual lambda calculus. Along the way, we have developed an ``intensional" theory
-of graduality that is of independent interest.
+To prove graduality and validate the equational theory, we construct a model of the types
+and terms and show that all of the axioms for term precision and for equality of terms
+hold in this model. Modeling the dynamic type presents a challenge in the presence of a
+language with functions: we want the dynamic type to represent a sum of all possible types
+in the language, so we write down an recursive equation that the semantic object modeling
+dynamic type should satisfy. When the language includes function types, this equation involves a
+negative occurrence of the variable for which we are solving, and so the equation
+does not have inductive or coinductive solutions.
+%
+To model the dynamic type, we therefore use guarded recursion to define a suitable
+semantic object that satisfies the unfolding isomorphism expected of the dynamic type.
+The key is that we do not actually get an exact solution to the equation in the style
+of traditional domain theory; rather, we get a ``guarded'' solution that holds ``up to a time step''.
+%
+That is, we introduce a notion of ``time'' and in the equation for the dynamic type,
+we guard the negative occurrences of the variable by a special operator that
+specifies that its argument is available ``later''.
+%This can be seen as a logic that internalizes the notion of step-indexing.
+See Section \ref{sec:technical-background} for more details on guarded type theory.
+At a high level, the key parts of our proof are as follows:
-\subsection{Overview of Remainder of Paper}
+% TODO revise this
+\begin{itemize}
+ \item Our first step toward proving graduality is to formulate a \emph{step-sensitive},
+ or \emph{intensional}, gradual lambda calculus, which we call $\intlc$, in which the
+ computation steps taken by a term are made explicit.
+ The ``normal'' gradual lambda calculus for which we want to prove graduality will be called the
+ \emph{surface}, \emph{step-insensitive}, or \emph{extensional}, gradual lambda calculus,
+ denoted $\extlc$.
-In Section \ref{sec:technical-background}, we provide technical background on gradually typed languages and
-on synthetic guarded domain theory.
-%
-In Section \ref{sec:GTLC}, we introduce the gradually-typed cast calculus
-for which we will prove graduality. Important here are the notions of syntactic
-type precision and term precision. We introduce both the \emph{extensional} gradual lambda calculus
-($\extlc$) and the \emph{intensional} gradual lambda calculus ($\intlc$).
-%
-In Section \ref{sec:domain-theory}, we define several fundamental constructions
-internal to SGDT that will be needed when we give a denotational semantics to
-our intensional lambda calculus.
-This includes the notion of Predomains as well as the concept
-of EP-Pairs.
-%
-In Section \ref{sec:semantics}, we define the denotational semantics for the
-intensional gradually-typed lambda calculus using the domain theoretic constructions in the
-previous section.
-%
-In Section \ref{sec:graduality}, we outline in more detail the proof of graduality for the
-extensional gradual lambda calculus, which will make use of prove properties we prove about
- the intensional gradual lambda calculus.
-%
-In Section \ref{sec:discussion}, we discuss the benefits and drawbacks to our approach in comparison
-to the traditional step-indexing approach, as well as possibilities for future work.
+ \item We define a translation from the surface syntax to the intensional syntax, and
+ prove a theorem relating the term precision in the surface to term precision in the
+ intensional syntax.
+
+ \item We define a semantics for the intensional syntax in guarded type theory, for both the
+ terms and for the term precision ordering $\ltdyn$.
+\end{itemize}
diff --git a/paper-new/ordering.tex b/paper-new/ordering.tex
new file mode 100644
index 0000000..d32c105
--- /dev/null
+++ b/paper-new/ordering.tex
@@ -0,0 +1,443 @@
+\section{Extending the Semantics to Precision}\label{sec:gtlc-precision}
+
+In this section, we extend the set-theoretic semantics for terms given in
+the previous section to a semantics for the type and term precision relations
+of the gradually-typed lambda calculus. We first introduce the type and term precision
+relations, then show how to give them a semantics using SGDT.
+
+% TODO mention intensional syntax
+
+
+\subsection{Term Precision for GTLC}
+
+% ---------------------------------------------------------------------------------------
+% ---------------------------------------------------------------------------------------
+
+%\subsubsection{Term Precision}\label{sec:term-precision}
+
+We allow for a \emph{heterogeneous} term precision judgment on values $V$ of type
+$A$ and $V'$ of type $A'$ provided that $A \ltdyn A'$ holds. Likewise, for producers,
+if $M$ has type $A$ and $M'$ has type $A'$, we can form the judgment that $M \ltdyn M'$.
+We use the same notation for the precision relation on both values and producers.
+
+% Type precision contexts
+In order to deal with open terms, we will need the notion of a type precision \emph{context}, which we denote
+$\gamlt$. This is similar to a normal context but instead of mapping variables to types,
+it maps variables $x$ to related types $A \ltdyn A'$, where $x$ has type $A$ in the left-hand term
+and $A'$ in the right-hand term. We may also write $x : d$ where $d : A \ltdyn A'$ to indicate this.
+
+% An equivalent way of thinking of type precision contexts is as a pair of ``normal" typing
+% contexts $\Gamma, \Gamma'$ with the same domain such that $\Gamma(x) \ltdyn \Gamma'(x)$ for
+% each $x$ in the domain.
+% We will write $\gamlt : \Gamma \ltdyn \Gamma'$ when we want to emphasize the pair of contexts.
+% Conversely, if we are given $\gamlt$, we write $\gamlt_l$ and $\gamlt_r$ for the normal typing contexts on each side.
+
+An equivalent way of thinking of a type precision context $\gamlt$ is as a
+pair of ``normal" typing contexts, $\gamlt_l$ and $\gamlt_r$, with the same
+domain and such that $\gamlt_l(x) \ltdyn \gamlt_r(x)$ for each $x$ in the domain.
+We will write $\gamlt : \gamlt_l \ltdyn \gamlt_r$ when we want to emphasize the pair of contexts.
+
+As with type precision derivations, we write $\Gamma$ to mean the ``reflexivity" type precision context
+$\Gamma : \Gamma \ltdyn \Gamma$.
+Concretely, this consists of reflexivity type precision derivations $\Gamma(x) \ltdyn \Gamma(x)$ for
+each $x$ in the domain of $\Gamma$.
+
+Furthermore, we write $\gamlt_1 \relcomp \gamlt_2$ to denote the ``composition'' of $\gamlt_1$ and $\gamlt_2$
+--- that is, the precision context whose value at $x$ is the type precision derivation
+$\gamlt_1(x) \relcomp \gamlt_2(x)$. This of course assumes that each of the type precision
+derivations is composable, i.e., that the RHS of $\gamlt_1(x)$ is the same as the left-hand side of $\gamlt_2(x)$.
+
+% We define the same for computation type precision contexts $\deltalt_1$ and $\deltalt_2$,
+% provided that both the computation type precision contexts have the same ``shape'', which is defined as
+% (1) either the stoup is empty in both, or the stoup has a hole in both, say $\hole{d}$ and $\hole{d'}$
+% where $d$ and $d'$ are composable, and (2) their value type precision contexts are composable as described above.
+
+The rules for term precision come in two forms. We first have the \emph{congruence} rules,
+one for each term constructor. These assert that the term constructors respect term precision.
+The congruence rules are as follows:
+
+\begin{mathpar}
+
+ \inferrule*[right = Var]
+ { c : A \ltdyn B \and \gamlt(x) = (A, B) }
+ { \etmprec {\gamlt} x x c }
+
+ \inferrule*[right = Zro]
+ { } {\etmprec \gamlt \zro \zro \nat }
+
+ \inferrule*[right = Suc]
+ { \etmprec \gamlt V {V'} \nat } {\etmprec \gamlt {\suc\, V} {\suc\, V'} \nat}
+
+ \inferrule*[right = MatchNat]
+ {\etmprec \gamlt V {V'} \nat \and
+ \etmprec \deltalt M {M'} d \and \etmprec {\deltalt, n : \nat} {N} {N'} d}
+ {\etmprec \deltalt {\matchnat {V} {M} {n} {N}} {\matchnat {V'} {M'} {n} {N'}} d}
+
+ \inferrule*[right = Lambda]
+ { c_i : A_i \ltdyn A'_i \and
+ c_o : A_o \ltdyn A'_o \and
+ \etmprec {\gamlt, x : c_i} {M} {M'} {c_o} }
+ { \etmprec \gamlt {\lda x M} {\lda x {M'}} {(c_i \ra c_o)} }
+
+ \inferrule*[right = App]
+ { c_i : A_i \ltdyn A'_i \and
+ c_o : A_o \ltdyn A'_o \\\\
+ \etmprec \gamlt {V_f} {V_f'} {(c_i \ra c_o)} \and
+ \etmprec \gamlt {V_x} {V_x'} {c_i}
+ }
+ { \etmprec {\gamlt} {V_f\, V_x} {V_f'\, V_x'} {{c_o}}}
+
+ \inferrule*[right = Ret]
+ {\etmprec {\gamlt} V {V'} c}
+ {\etmprec {\gamlt} {\ret\, V} {\ret\, V'} {c}}
+
+ \inferrule*[right = Bind]
+ {\etmprec {\gamlt} {M} {M'} {c} \and
+ \etmprec {\gamlt, x : c} {N} {N'} {d} }
+ {\etmprec {\gamlt} {\bind {x} {M} {N}} {\bind {x} {M'} {N'}} {d}}
+\end{mathpar}
+
+We then have additional equational axioms, including $\beta$ and $\eta$ laws, and
+rules characterizing upcasts as least upper bounds, and downcasts as greatest lower bounds.
+For the sake of familiarity, we formulate the cast rules using arbitrary casts; later we
+will state the analogous versions for the version of the calculus without arbitrary casts.
+
+We write $M \equidyn N$ to mean that both $M \ltdyn N$ and $N \ltdyn M$.
+
+\begin{mathpar}
+ \inferrule*[right = $\err$]
+ {\phasty {\Gamma} M B }
+ {\etmprec {\Gamma} {\err_B} M B}
+
+ \inferrule*[right = $\beta$-fun]
+ { \phasty {\Gamma, x : A_i} M {A_o} \and
+ \vhasty {\Gamma} V {A_i} }
+ { \etmequidyn {\Gamma} {(\lda x M)\, V} {M[V/x]} {A_o} }
+
+ \inferrule*[right = $\eta$-fun]
+ { \vhasty {\Gamma} {V} {A_i \ra A_o} }
+ { \etmequidyn \Gamma {\lda x (V\, x)} V {A_i \ra A_o} }
+
+ \inferrule*[right = UpR]
+ { c : A \ltdyn B \and d : B \ltdyn C \and
+ \etmprec {\gamlt} {M} {N} {c} }
+ { \etmprec {\gamlt} {M} {\up {B} {C} N} {c \circ d} }
+
+ \inferrule*[right = UpL]
+ { c : A \ltdyn B \and d : B \ltdyn C \and
+ \etmprec {\gamlt} {M} {N} {c \circ d} }
+ { \etmprec {\gamlt} {\up {A} {B} M} {N} {d} }
+
+ \inferrule*[right = DnL]
+ { c : A \ltdyn B \and d : B \ltdyn C \and
+ \etmprec {\gamlt} {M} {N} {d} }
+ { \etmprec {\gamlt} {\dn {A} {B} M} {N} {c \circ d} }
+
+ \inferrule*[right = DnR]
+ { c : A \ltdyn B \and d : B \ltdyn C \and
+ \etmprec {\gamlt} {M} {N} {c \circ d} }
+ { \etmprec {\gamlt} {M} {\dn {B} {C} N} {c} }
+\end{mathpar}
+
+% TODO explain the least upper bound/greatest lower bound rules
+The rules UpR, UpL, DnL, and DnR were introduced in \cite{new-licata18} as a means
+of cleanly axiomatizing the intended behavior of casts in a way that
+doesn't depend on the specific constructs of the language.
+Intuitively, rule UpR says that the upcast of $M$ is an upper bound for $M$
+in that $M$ may error more, and UpL says that the upcast is the \emph{least}
+such upper bound, in that it errors more than any other upper bound for $M$.
+Conversely, DnL says that the downcast of $M$ is a lower bound, and DnR says
+that it is the \emph{greatest} lower bound.
+% These rules provide a clean axiomatization of the behavior of casts that doesn't
+% depend on the specific constructs of the language.
+
+
+
+\subsection{Semantics for Precision}
+
+As a first attempt at giving a semantics to the ordering, we could try to model types as
+sets equipped with an ordering that models term precision. Since term precision is reflexive
+and transitive, and since we identify terms that are equi-precise, we choose to model types
+as partially-ordered sets. We model the term precision ordering $M \ltdyn N : A \ltdyn B$ as an
+ordering relation between the posets denoted by $A$ and $B$.
+
+However, it turns out that modeling term precision by a relation defined by guarded fixpoint
+is not as straightforward as one might hope.
+A first attempt might be to define an ordering $\semltbad$ between $\li X$ and $\li Y$
+that allows for computations that may take different numbers of steps to be related.
+The relation is parameterized by a relation $\le$ between $X$ and $Y$, and is defined
+by guarded fixpoint as follows:
+% simultaneously captures the notions of error approximation and equivalence up to stepping behavior:
+
+\begin{align*}
+ &\eta\, x \semltbad \eta\, y \text{ if }
+ x \semlt y \\
+%
+ &\mho \semltbad l \\
+%
+ &\theta\, \tilde{l} \semltbad \theta\, \tilde{l'} \text{ if }
+ \later_t (\tilde{l}_t \semltbad \tilde{l'}_t) \\
+%
+ &\theta\, \tilde{l} \semltbad \mho \text{ if }
+ \theta\, \tilde{l} = \delta^n(\mho) \text { for some $n$ } \\
+%
+ &\theta\, \tilde{l} \semltbad \eta\, y \text{ if }
+ (\theta\, \tilde{l} = \delta^n(\eta\, x))
+ \text { for some $n$ and $x : \ty{X}$ such that $x \le y$ } \\
+%
+ &\mho \semltbad \theta\, \tilde{l'} \text { if }
+ \theta\, \tilde{l'} = \delta^n(\mho) \text { for some $n$ } \\
+%
+ &\eta\, x \semltbad \theta\, \tilde{l'} \text { if }
+ (\theta\, \tilde{l'} = \delta^n (\eta\, y))
+ \text { for some $n$ and $y : \ty{Y}$ such that $x \le y$ }
+\end{align*}
+
+Two computations that immediately return $(\eta)$ are related if the underlying
+values are related in the underlying ordering.
+%
+The computation that errors $(\mho)$ is below everything else.
+%
+If both sides step (i.e., both sides are $\theta$),
+then we allow one time step to pass and compare the resulting terms.
+(This is where use the relation defined ``later''.)
+%
+Lastly, if one side steps and the other returns a value, the side that steps should
+terminate with a value in some finite number of steps $n$, and that value should
+be related to the value returned by the other side.
+Likewise, if one side steps and the other errors, then the side that steps
+should terminate with error.
+
+The problem with this definition is that the resulting relation is \emph{provably} not
+transitive: it can be shown (in Clocked Cubical Type Theory) that if $R$ is a
+relation on $\li X$ satisfying three specific properties, one of which is
+transitivity, then that relation is trivial.
+(The other two properties are that the relation is a congruence with respect to $\theta$,
+and that the relation is closed under delays $\delta = \theta \circ \nxt$ on either side.)
+Since the above relation \emph{does} satisfy the other two properties, we conclude
+that it must not be transitive.
+
+%But having a non-transitive relation to model term precision presents a problem
+%for...
+
+We are therefore led to wonder whether we can formulate a version of the relation
+that \emph{is} transitive.
+It turns out that we can, by sacrificing another of the three properties from
+the above lemma. Namely, we give up on closure under delays. Doing so, we end up
+with a \emph{lock-step} error ordering, where, roughly speaking, in order for
+computations to be related, they must have the same stepping behavior.
+%
+We then formulate a separate relation, \emph{weak bisimilarity}, that relates computations
+that are extensionally equal and may only differ in their stepping behavior.
+
+% As a result, we instead separate the semantics of term precision into two relations:
+% an intensional, step-sensitive \emph{error ordering} and a \emph{bisimilarity relation}.
+
+
+\subsubsection{Double Posets}\label{sec:predomains}
+
+As discussed above, there are two relations that we would like to define
+in the semantics: a step-sensitive error ordering, and weak bisimilarity of computations.
+%
+The semantic objects that interpret our types should therefore be equipped with
+two relations. We call these objects ``double posets''.
+A double poset $A$ is a set with two relations: an partial order $\semlt_A$ on $A$, and
+a reflexive, symmetric relation $\bisim_A$ on $A$.
+We write the underling set of $A$ as $\ty{A}$.
+
+We define morphisms of double posets as functions that preserve both
+the ordering and the bisimilarity relation. Given double posets
+$A$ and $B$, we write $f \colon A \monto B$ to indicate that $f$ is a morphism
+from $A$ to $B$, i.e, the following hold:
+(1) for all $a_1 \semlt_A a_2$, we have $f(a_1) \semlt_{B} f(a_2)$, and
+(2) for all $a_1 \bisim_A a_2$, we have $f(a_1) \bisim_{B} f(a_2)$.
+
+
+%%%%% RESUME HERE
+
+We define an ordering on morphisms of double posets as
+$f \le g$ if for all $a$ in $\ty{A_i}$, we have $f(a) \le_{A_o} g(a)$,
+and similarly bisimilarity extends to morphisms via
+$f \bisim g$ if for all $a$ in $\ty{A_i}$, we have $f(a) \bisim_{A_o} g(a)$.
+
+For each type we want to represent, we define a double poset for the corresponding semantic
+type. For instance, we define a double poset for natural numbers, for the
+dynamic type, for functions, and for the lift monad. We
+describe each of these below.
+
+\begin{itemize}
+ \item There is a double poset $\Nat$ for natural numbers, where the ordering and the
+ bisimilarity relations are both equality.
+
+ % TODO explain that there is a theta operator for posets?
+ \item There is a double poset $\Dyn$ to represent the dynamic type. The underlying type
+ for this double poset is defined by guarded fixpoint to be such that
+ $\ty{\Dyn} \cong \mathbb{N}\, +\, \later (\ty{\Dyn} \monto \li \ty{\Dyn})$.
+ This definition is valid because the occurrences of Dyn are guarded by the $\later$.
+ The ordering is defined via guarded recursion by cases on the argument, using the
+ ordering on $\mathbb{N}$ and the ordering on monotone functions described above.
+
+ \item For a double poset $A$, there is a double poset $\li A$ for the ``lift'' of $A$
+ using the lift monad. We use the same notation for $\li A$ when $A$ is a type
+ and $A$ is a double poset, since the context should make clear which one we are referring to.
+ The underling type of $\li A$ is simply $\li \ty{A}$, i.e., the lift of the underlying
+ type of $A$.
+ The ordering on $\li A$ is the ``lock-step error-ordering'' which we describe in
+ \ref{subsec:lock-step}. The bismilarity relation is the ``weak bisimilarity''
+ described in Section \ref{}
+
+ \item For double posets $A_i$ and $A_o$, we form the double poset of monotone functions
+ from $A_i$ to $A_o$, which we denote by $A_i \To A_o$.
+
+ \item Given a double poset $A$, we can form the double poset $\later A$ whose underlying
+ type is $\later \ty{A}$. We define $\tilde{x} \le_{\later A} \tilde{y}$ to be
+ $\later_t (\tilde{x}_t \le_A \tilde{y}_t)$.
+\end{itemize}
+
+\subsubsection{Step-Sensitive Error Ordering}\label{subsec:lock-step}
+
+As mentioned, the ordering on the lift of a double poset $A$ is called the
+\emph{step-sensitive error-ordering} (also called ``lock-step error ordering''),
+the idea being that two computations $l$ and $l'$ are related if they are in
+lock-step with regard to their intensional behavior, up to $l$ erroring.
+Formally, we define this ordering as follows:
+
+\begin{itemize}
+ \item $\eta\, x \ltls \eta\, y$ if $x \le_A y$.
+ \item $\mho \ltls l$ for all $l$
+ \item $\theta\, \tilde{r} \ltls \theta\, \tilde{r'}$ if
+ $\later_t (\tilde{r}_t \ltls \tilde{r'}_t)$
+\end{itemize}
+
+We also define a heterogeneous version of this ordering between the lifts of two
+different double posets $A$ and $B$, parameterized by a relation $R$ between $A$ and $B$.
+
+\subsubsection{Weak Bisimilarity Relation}
+
+For a double poset $A$, we define a relation on $\li A$, called ``weak bisimilarity",
+written $l \bisim l'$. Intuitively, we say $l \bisim l'$ if they are equivalent
+``up to delays''.
+% We introduce the notation $x \sim_A y$ to mean $x \le_A y$ and $y \le_A x$.
+% TODO if A is a poset, then we can just say that x = y
+%
+The weak bisimilarity relation is defined by guarded fixpoint as follows:
+
+\begin{align*}
+ &\mho \bisim \mho \\
+%
+ &\eta\, x \bisim \eta\, y \text{ if }
+ x \bisim_A y \\
+%
+ &\theta\, \tilde{x} \bisim \theta\, \tilde{y} \text{ if }
+ \later_t (\tilde{x}_t \bisim \tilde{y}_t) \\
+%
+ &\theta\, \tilde{x} \bisim \mho \text{ if }
+ \theta\, \tilde{x} = \delta^n(\mho) \text { for some $n$ } \\
+%
+ &\theta\, \tilde{x} \bisim \eta\, y \text{ if }
+ (\theta\, \tilde{x} = \delta^n(\eta\, x))
+ \text { for some $n$ and $x : \ty{A}$ such that $x \sim_A y$ } \\
+%
+ &\mho \bisim \theta\, \tilde{y} \text { if }
+ \theta\, \tilde{y} = \delta^n(\mho) \text { for some $n$ } \\
+%
+ &\eta\, x \bisim \theta\, \tilde{y} \text { if }
+ (\theta\, \tilde{y} = \delta^n (\eta\, y))
+ \text { for some $n$ and $y : \ty{A}$ such that $x \sim_A y$ }
+\end{align*}
+
+When both sides are $\eta$, then we ensure that the underlying values are bisimilar
+in the underlying bisimilarity relation on $A$.
+When one side is a $\theta$ and the other is $\eta x$ (i.e., one side steps),
+we stipulate that the $\theta$-term runs to $\eta y$ where $x$ is related to $y$.
+Similarly when one side is $\theta$ and the other $\mho$.
+If both sides step, then we allow one time step to pass and compare the resulting terms.
+In this way, the definition captures the intuition of terms being equivalent up to
+delays.
+
+It can be shown (by \lob-induction) that the step-sensitive relation is symmetric.
+However, it can also be shown that this relation is \emph{not} transitive:
+The argument is the same as that used to show that the step-insensitive error
+ordering $\semltbad$ described above is not transitive. Namely, we show that
+if it were transitive, then it would have to be trivial in that $l \bisim l'$ for all $l, l'$.
+that if this relation were transitive, then in fact it would be trivial in that
+%This issue will be resolved when we consider the relation's \emph{globalization}.
+
+\subsection{The Cast Rules}
+
+Unfortunately, the four cast rules defined above do not hold in
+the intensional setting where we are tracking the steps taken by terms.
+The source of the problem is that the downcast from the dynamic type to
+a function involves a delay, i.e., a $\theta$.
+So in order to keep the other term in lock-step, we need to insert a ``delay"
+that is extensionally equivalent to the identity function.
+More concretely, consider a simplified version of the DnL rule shown below:
+
+\begin{mathpar}
+ \inferrule*{M \ltdyn_i N : B}
+ {\dn c M \ltdyn_i N : c}
+\end{mathpar}
+
+If $c$ is inj-arr, then when we downcast $M$ from $dyn$ to $\dyn \ra \dyn$,
+semantically this will involve a $\theta$ because the value of type $dyn$
+in the semantics will contain a \emph{later} function $\tilde{f}$.
+Thus, in order for the right-hand side to be related to the downcast,
+we need to insert a delay on the right.
+%
+The need for delays affects the cast rules involving upcasts as well, because
+the upcast for functions involves a downcast on the domain:
+
+\[ \up{c_i \ra c_o}{M} \equiv \lambda (x : B_i). \up{c_o}(M\, (\dn {c_i} x)). \]
+
+Thus, the correct versions of the cast rules involve delays on the side that was not casted.
+
+
+% Delays for function types and for inj-arr(c)
+
+
+\subsubsection{Perturbations}
+
+We can describe precisely how the delays are inserted for any type precision
+derivation $c$.
+
+To do so, we first define simultaneously an inductive type of \emph{perturbations}
+for embeddings $\perte$ and for projections $\pertp$ by the following rules:
+
+\begin{mathpar}
+
+\inferrule{}{\id : \perte A}
+
+\inferrule{}{\id : \pertp A}
+
+\inferrule
+ {\delta_c : \pertp A \and \delta_d : \perte B}
+ {\delta_c \ra \delta_d : \perte (A \ra B)}
+
+\inferrule
+ {\delta_c : \perte A \and \delta_d : \pertp B}
+ {\delta_c \ra \delta_d : \pertp (A \ra B)}
+
+\inferrule
+ {\delta_\nat : \perte \nat \and \delta_f : \perte (\dyn \ra \dyn)}
+ {\pertdyn{\delta_\nat}{\delta_f} : \perte \dyn}
+
+\inferrule
+ {\delta_\nat : \pertp \nat \and \delta_f : \pertp (\dyn \ra \dyn)}
+ {\pertdyn{\delta_\nat}{\delta_f} : \pertp \dyn}
+
+\end{mathpar}
+
+The structure of embedding perturbations is designed to follow the structure
+of the corresponding embeddings, and likewise for the projection perturbations.
+Thus, in the function case, an embedding perturbation consists of a \emph{projection}
+perturbation for the domain and an \emph{embedding} perturbation for the codomain.
+The opposite holds for the projection perturbation for functions.
+
+Another way in which the two kinds of perturbations differ is that there is an additional
+projection perturbation for delaying $\delaypert{\delta}$.
+This corresponds to the actual delay term $\delta = \theta \circ \nxt$ in the semantics,
+and it is the generator/source of all non-trivial perturbations.
+
+Given a perturbation $\delta$, we can turn it into a term, which we also write as
+$\delta$ unless there is opportunity for confusion.
+
diff --git a/paper-new/paper.tex b/paper-new/paper.tex
index c77590d..949a3a9 100644
--- a/paper-new/paper.tex
+++ b/paper-new/paper.tex
@@ -1,12 +1,14 @@
\documentclass[acmsmall,screen]{acmart}
+\let\Bbbk\relax
+
+\usepackage{quiver}
\usepackage{mathpartir}
-\usepackage{tikz-cd}
+% \usepackage{tikz-cd}
\usepackage{enumitem}
\usepackage{wrapfig}
\usepackage{fancyvrb}
\usepackage{comment}
-\usepackage{ stmaryrd }
%% Rights management information. This information is sent to you
@@ -114,13 +116,17 @@
\input{technical-background}
-\input{syntax}
+% \input{syntax}
+
+% \input{semantics}
+
+\input{terms}
-\input{semantics}
+\input{ordering}
\input{graduality}
-\section{Discussion}\label{sec:discussion}
+% \section{Discussion}\label{sec:discussion}
% \subsection{Synthetic Ordering}
diff --git a/paper-new/technical-background.tex b/paper-new/technical-background.tex
index 2a34777..3de6f09 100644
--- a/paper-new/technical-background.tex
+++ b/paper-new/technical-background.tex
@@ -33,7 +33,7 @@ behave the same except that $M$ may error more.
\subsection{Classical Domain Models}
-New and Licata \cite{newlicata} developed an axiomatic account of the
+New and Licata \cite{new-licata18} developed an axiomatic account of the
graduality relation on cast calculus terms and gave a denotational
model of this calculus using classical domain theory based on
$\omega$-CPOs. This semantics has scaled up to an analysis of a
@@ -48,12 +48,12 @@ Racket. Thus if we want a reusable mathematical theory of gradual
typing that can scale to realistic programming languages, we need to
look elsewhere to so-called ``step-indexed'' techniques.
-A series of works \cite{newahmed,newlicataahmed,newjamnerahmed}
+A series of works \cite{new-ahmed2018, new-licata-ahmed2019, new-jamner-ahmed19}
developed step-indexed logical relations models of gradually typed
languages based on operational semantics. Unlike, classical domain
theory, such step-indexed techniques are capable of modeling
higher-order store and runtime-extensible dynamic types
-\cite{amalsthesis,nonpmetricparamorsomething,newjamnerahmed}. However
+\cite{amalsthesis,nonpmetricparamorsomething,new-jamner-ahmed19}. However
their proof developments are highly repetitive and technical, with
each development formulating a logical relation from first-principles
and proving many of the same tedious lemmas without reusable
@@ -72,6 +72,8 @@ make formalization of realistic gradual languages tractible.
Because the dynamic type is modeled as a non-well-founded
recursive type, their logical relation needs to be paramterized by natural numbers
to restore well-foundedness. This technique is known as a \emph{step-indexed logical relation}.
+ Intuitively, step-indexing makes the steps taken by terms observable.
+ %
Reasoning about step-indexed logical relations
can be tedious and error-prone, and there are some very subtle aspects that must
be taken into account in the proofs. Figure \ref{TODO} shows an example of a step-indexed logical
@@ -82,14 +84,14 @@ make formalization of realistic gradual languages tractible.
and another in which the steps of the right-hand term are counted.
Then two terms $M$ and $N$ are related in the ``combined'' logical relation if they are
related in both of the one-sided logical relations. Having two separate logical relations
- complicates the statement of the lemmas used to prove graduality, becasue any statement that
+ complicates the statement of the lemmas used to prove graduality, because any statement that
involves a term stepping needs to take into account whether we are counting steps on the left
or the right. Some of the differences can be abstracted over, but difficulties arise for properties %/results
- as fundamental and seemingly straightforward as transitivty.
+ as fundamental and seemingly straightforward as transitivity.
Specifically, for transitivity, we would like to say that if $M$ is related to $N$ at
index $i$ and $N$ is related to $P$ at index $i$, then $M$ is related to $P$ at $i$.
- But this does not actually hold: we requrie that one of the two pairs of terms
+ But this does not actually hold: we require that one of the two pairs of terms
be related ``at infinity'', i.e., that they are related at $i$ for all $i \in \mathbb{N}$.
Which pair is required to satisfy this depends on which logical relation we are considering,
(i.e., is it counting steps on the left or on the right),
@@ -97,6 +99,42 @@ make formalization of realistic gradual languages tractible.
where $M$ and $N$ must be shown to be related for all $i$, and another where $N$ and $P$ must
be related for all $i$. % This may not even be possible to show in some scenarios!
+ \begin{comment}
+ As another example, the axioms that specify the behavior of casts do not hold in the
+ step-indexed setting. Consider, for example, the ``lower bound'' rule for downcasting:
+
+ \begin{mathpar}
+ \inferrule*
+ {\gamlt \vdash M \ltdyn N : dyn}
+ {\gamlt \vdash \dn{\dyn \ra \dyn}{\dyn} M \ltdyn N}
+ \end{mathpar}
+
+ In the language of the step-indexed logical relation used in prior work, this would
+ take the form
+
+ \begin{mathpar}
+ \inferrule*
+ {(M, N) \in \mathcal{E}^{\sim}_{i}\sem{\dyn}}
+ {(\dn{\dyn \ra \dyn}{\dyn} M, N) \in \mathcal{E}^{\sim}_{i}\sem{\injarr{}}}
+ \end{mathpar}
+
+ where $\sim$ stands for $\mathrel{\preceq}$ or $\mathrel{\succeq}$, i.e.,
+ counting steps on the left or right respectively.
+ %
+ To show this, we would use the fact that the left-hand side steps and
+ apply an anti-reduction lemma, showing that the term to which the LHS steps
+ is related to the RHS where our fuel is now
+
+ The left-hand side steps to a case inspection on $M$,
+ where we unfold the recursive $\dyn$ type into a sum type and see whether the result
+ is a function type.
+
+ One way around these difficulties is to demand that the rules only hold
+ ``extensionally'', i.e., we quantify universally over the step-index and
+ reason about the ``global'' behavior of terms for all possible step indices.
+ This is the approach taken in prior work.
+\end{comment}
+
% These complications introduced by step-indexing lead one to wonder whether there is a
% way of proving graduality without relying on tedious arguments involving natural numbers.
% An alternative approach, which we investigate in this paper, is provided by
@@ -150,9 +188,10 @@ recursion, an idea first introduced by Atkey and McBride \cite{atkey-mcbride2013
\subsubsection{Ticked Cubical Type Theory}
% TODO motivation for Clocked Cubical Type Theory, e.g., delayed substitutions?
-In Ticked Cubical Type Theory \cite{TODO}, there is an additional sort
-called \emph{ticks}. Given a clock $k$, a tick $t : \tick k$ serves
-as evidence that one unit of time has passed according to the clock $k$.
+Ticked Cubical Type Theory \cite{mogelberg-veltri2019} is an extension of Cubical
+Type Theory \cite{CohenCoquandHuberMortberg2017}
+in which there is an additional sort called \emph{ticks}. Given a clock $k$,
+a tick $t : \tick\, k$ serves as evidence that one unit of time has passed according to the clock $k$.
The type $\later A$ is represented as a function from ticks of a clock $k$ to $A$.
The type $A$ is allowed to depend on $t$, in which case we write $\later^k_t A$
to emphasize the dependence.
@@ -162,13 +201,13 @@ to emphasize the dependence.
The rules for tick abstraction and application are similar to those of dependent
$\Pi$ types.
In particular, if we have a term $M$ of type $\later^k A$, and we
-have available in the context a tick $t' : \tick k$, then we can apply the tick to $M$ to get
+have available in the context a tick $t' : \tick\, k$, then we can apply the tick to $M$ to get
a term $M[t'] : A[t'/t]$. We will also write tick application as $M_t$.
-Conversely, if in a context $\Gamma, t : \tick k$ we have that $M$ has type $A$,
+Conversely, if in a context $\Gamma, t : \tick\, k$ we have that $M$ has type $A$,
then in context $\Gamma$ we have $\lambda t.M$ has type $\later A$. % TODO dependent version?
The statements in this paper have been formalized in a variant of Agda called
-Guarded Cubical Agda \cite{TODO}, an implementation of Clocked Cubical Type Theory.
+Guarded Cubical Agda \cite{veltri-vezzosi2020}, an implementation of Clocked Cubical Type Theory.
% TODO axioms (clock irrelevance, tick irrelevance)?
diff --git a/paper-new/terms.tex b/paper-new/terms.tex
new file mode 100644
index 0000000..80e8bc1
--- /dev/null
+++ b/paper-new/terms.tex
@@ -0,0 +1,473 @@
+\section{A Simple Denotational Semantics for the Terms of GTLC}\label{sec:gtlc-terms}
+
+In this section, we introduce the term syntax for the gradually-typed
+lambda calculus (GTLC) and give a set-theoretic denotational semantics
+using tools from SGDT.
+
+In the following section, we will extend the denotational semantics to accommodate
+the type and term precision orderings.
+
+
+\subsection{Syntax}\label{sec:term-syntax}
+
+Our syntax is based on fine-grained call by value, and as such it has
+separate value and producer terms and typing judgments for each.
+
+% Given a term $M$ of type $A$, the term $\bind{x}{M}{N}$ should be thought of as
+% running $M$ to a value $V$ and then continuing as $N$, with $V$ in place of $x$.
+
+
+\begin{align*}
+ &\text{Types } A := \nat \alt \,\dyn \alt (A \ra A') \\
+ &\text{Contexts } \Gamma := \cdot \alt (\Gamma, x : A) \\
+ &\text{Values } V := \zro \alt \suc\, V \alt \lda{x}{M} \alt \up{A}{B} V \\
+ &\text{Producers } M, N := \err_B \alt \matchnat {V} {M} {n} {M'} \\
+ &\quad\quad \alt \ret {V} \alt \bind{x}{M}{N} \alt V_f\, V_x \alt \dn{A}{B} M
+\end{align*}
+
+
+The value typing judgment is written $\vhasty{\Gamma}{V}{A}$ and
+the producer typing judgment is written $\phasty{\Gamma}{M}{A}$.
+
+The typing rules are as expected, with a cast between $A$ to $B$ allowed only when $A \ltdyn B$.
+The precise rules for $A \ltdyn B$ will be given below.
+Notice that the upcast of a value is a value, since it always succeeds, while the downcast
+of a value is a producer, since it may fail.
+
+\begin{mathpar}
+ % Var
+ \inferrule*{ }{\vhasty {\cdot, \Gamma, x : A, \Gamma'} x A}
+
+ % Err
+ \inferrule*{ }{\phasty {\cdot, \Gamma} {\err_A} A}
+
+ % Zero and suc
+ \inferrule*{ }{\vhasty \Gamma \zro \nat}
+
+ \inferrule*{\vhasty \Gamma V \nat} {\vhasty \Gamma {\suc\, V} \nat}
+
+ % Match-nat
+ \inferrule*
+ {\vhasty \Gamma V \nat \and
+ \phasty \Delta M A \and \phasty {\Gamma, n : \nat} {M'} A}
+ {\phasty \Gamma {\matchnat {V} {M} {n} {M'}} A}
+
+ % Lambda
+ \inferrule*
+ {\phasty {\Gamma, x : A} M {A'}}
+ {\vhasty \Gamma {\lda x M} {A \ra A'}}
+
+ % App
+ \inferrule*
+ {\vhasty \Gamma {V_f} {A \ra A'} \and \vhasty \Gamma {V_x} A}
+ {\phasty {\Gamma} {V_f \, V_x} {A'}}
+
+ % Ret
+ \inferrule*
+ {\vhasty \Gamma V A}
+ {\phasty {\Gamma} {\ret\, V} {A}}
+
+ % Bind
+ \inferrule*
+ {\phasty \Gamma M {A} \and \phasty{\Gamma, x : A}{N}{B} } % Need x : A in context
+ {\phasty {\Gamma} {\bind{x}{M}{N}} {B}}
+
+ % Upcast
+ \inferrule*
+ {A \ltdyn A' \and \vhasty \Gamma V A}
+ {\vhasty \Gamma {\up A {A'} V} {A'} }
+
+ \inferrule* % TODO is this correct?
+ {A \ltdyn A' \and \phasty {\Gamma} {M} {A'}}
+ {\phasty {\Gamma} {\dn A {A'} M} {A}}
+
+\end{mathpar}
+
+
+In the equational theory, we have $\beta$ and $\eta$ laws for function type,
+as well a $\beta$ and $\eta$ law for bind.
+
+\begin{mathpar}
+ % Function Beta and Eta
+ \inferrule*
+ {\phasty {\Gamma, x : A} M {B} \and \vhasty \Gamma V A}
+ {(\lda x M)\, V = M[V/x]}
+
+ \inferrule*
+ {\vhasty \Gamma V {A \ra A}}
+ {\Gamma \vdash V = \lda x {V\, x}}
+
+ % Ret Beta and Eta
+ \inferrule*
+ {}
+ {(\bind{x}{\ret\, V}{N}) = N[V/x]}
+
+ \inferrule*
+ {\phasty {\Gamma} {M} {B}}
+ {\bind{x}{M}{\ret x} = M}
+
+ % Match-nat Beta
+ \inferrule*
+ {\phasty \Delta M A \and \phasty {\Gamma, n : \nat} {M'} A}
+ {\matchnat{\zro}{M}{n}{M'} = M}
+
+ \inferrule*
+ {\vhasty \Gamma V \nat \and
+ \phasty \Gamma M B \and \phasty {\Gamma, n : \nat} {M'} B}
+ {\matchnat{\suc\, V}{M}{n}{M'} = M'}
+
+ % Match-nat Eta
+ % This doesn't build in substitution
+ \inferrule*
+ {\hasty {\Gamma , x : \nat} M A}
+ {M = \matchnat{x} {M[\zro / x]} {n} {M[(\suc\, n) / x]}}
+
+\end{mathpar}
+
+\subsubsection{Type Precision}\label{sec:type-precision}
+
+The type precision rules specify what it means for a type $A$ to be more precise than $A'$.
+We have reflexivity rules for $\dyn$ and $\nat$, as well as rules that $\nat$ is more precise than $\dyn$
+and $\dyn \ra \dyn$ is more precise than $\dyn$.
+We also have a congruence rule for function types stating that given $A_i \ltdyn A'_i$ and $A_o \ltdyn A'_o$, we can prove
+$A_i \ra A_o \ltdyn A'_i \ra A'_o$. Note that precision is covariant in both the domain and codomain.
+Finally, we can lift a relation on value types $A \ltdyn A'$ to a relation $\Ret A \ltdyn \Ret A'$ on
+computation types.
+
+\begin{mathpar}
+ \inferrule*[right = \dyn]
+ { }{\dyn \ltdyn\, \dyn}
+
+ \inferrule*[right = \nat]
+ { }{\nat \ltdyn \nat}
+
+ \inferrule*[right = $\ra$]
+ {A_i \ltdyn A'_i \and A_o \ltdyn A'_o }
+ {(A_i \ra A_o) \ltdyn (A'_i \ra A'_o)}
+
+ \inferrule*[right = $\textsf{Inj}_\nat$]
+ { }{\nat \ltdyn\, \dyn}
+
+ \inferrule*[right = $\textsf{Inj}_{\ra}$]
+ { }
+ {(\dyn \ra \dyn) \ltdyn\, \dyn}
+
+ \inferrule*[right = $\injarr{}$]
+ {(R \ra S) \ltdyn\, (\dyn \ra \dyn)}
+ {(R \ra S) \ltdyn\, \dyn}
+
+
+\end{mathpar}
+
+We can prove that transitivity of type precision is admissible, i.e.,
+if $A \ltdyn B$ and $B \ltdyn C$, then $A \ltdyn C$.
+
+% Type precision derivations
+Note that as a consequence of this presentation of the type precision rules, we
+have that if $A \ltdyn A'$, there is a unique precision derivation that witnesses this.
+As in previous work, we go a step farther and make these derivations first-class objects,
+known as \emph{type precision derivations}.
+Specifically, for every $A \ltdyn A'$, we have a derivation $c : A \ltdyn A'$ that is constructed
+using the rules above. For instance, there is a derivation $\dyn : \dyn \ltdyn \dyn$, and a derivation
+$\nat : \nat \ltdyn \nat$, and if $c_i : A_i \ltdyn A_i$ and $c_o : A_o \ltdyn A'_o$, then
+there is a derivation $c_i \ra c_o : (A_i \ra A_o) \ltdyn (A'_i \ra A'_o)$. Likewise for
+the remaining rules. The benefit to making these derivations explicit in the syntax is that we
+can perform induction over them.
+Note also that for any type $A$, we use $A$ to denote the reflexivity derivation that $A \ltdyn A$,
+i.e., $A : A \ltdyn A$.
+Finally, observe that for type precision derivations $c : A \ltdyn A'$ and $c' : A' \ltdyn A''$, we
+can define their composition $c \relcomp c' : A \ltdyn A''$.
+This notion will be used below in the statement of transitivity of the term precision relation.
+
+\subsection{Removing Casts as Primitives}
+
+% We now observe that all casts, except those between $\nat$ and $\dyn$
+% and between $\dyn \ra \dyn$ and $\dyn$, are admissible, in the sense that
+% we can start from $\extlcm$, remove casts except the aforementioned ones,
+% and in the resulting language we will be able to derive the other casts.
+
+We now observe that all casts, except those between $\nat$ and $\dyn$
+and between $\dyn \ra \dyn$ and $\dyn$, are admissible.
+That is, consider a new language ($\extlcprime$) in which
+instead of having arbitrary casts, we have injections from $\nat$ and
+$\dyn \ra \dyn$ into $\dyn$, and a case inspection on $\dyn$.
+We claim that in $\extlcprime$, all of the casts present in $\extlc$ are derivable.
+It will suffice to verify that casts for function type are derivable.
+This holds because function casts are constructed inductively from the casts
+of their domain and codomain. The base case is one of the casts involving $\nat$
+or $\dyn \ra \dyn$ which are present in $\extlcprime$ as injections and case inspections.
+
+
+The resulting calculus $\extlcprime$ now lacks arbitrary casts as a primitive notion:
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% TODO update
+
+\begin{align*}
+ &\text{Types } A := \nat \alt \dyn \alt (A \ra A') \\
+ &\text{Contexts } \Gamma := \cdot \alt (\Gamma, x : A) \\
+ &\text{Values } V := \zro \alt \suc\, V \alt \lda{x}{M} \alt \injnat V \alt \injarr V \\
+ &\text{Producers } M, N := \err_B \alt \ret {V} \alt \bind{x}{M}{N}
+ \alt V_f\, V_x \alt
+ \\ & \quad\quad \casenat{V}{M_{no}}{n}{M_{yes}}
+ \alt \casearr{V}{M_{no}}{f}{M_{yes}}
+\end{align*}
+
+
+% New rules
+Figure \ref{fig:extlc-minus-minus-typing} shows the new typing rules,
+and Figure \ref{fig:extlc-minus-minus-eqns} shows the equational rules
+for case-nat (the rules for case-arrow are analogous).
+
+\begin{figure}
+ \begin{mathpar}
+ % inj-nat
+ \inferrule*
+ {\hasty \Gamma M \nat}
+ {\hasty \Gamma {\injnat M} \dyn}
+
+ % inj-arr
+ \inferrule*
+ {\hasty \Gamma M (\dyn \ra \dyn)}
+ {\hasty \Gamma {\injarr M} \dyn}
+
+ % Case nat
+ \inferrule*
+ {\hasty{\Delta|_V}{V}{\dyn} \and
+ \hasty{\Delta , x : \nat }{M_{yes}}{B} \and
+ \hasty{\Delta}{M_{no}}{B}}
+ {\hasty {\Delta} {\casenat{V}{M_{no}}{n}{M_{yes}}} {B}}
+
+ % Case arr
+ \inferrule*
+ {\hasty{\Delta|_V}{V}{\dyn} \and
+ \hasty{\Delta , x : (\dyn \ra \dyn) }{M_{yes}}{B} \and
+ \hasty{\Delta}{M_{no}}{B}}
+ {\hasty {\Delta} {\casearr{V}{M_{no}}{f}{M_{yes}}} {B}}
+ \end{mathpar}
+ \caption{New typing rules for $\extlcmm$.}
+ \label{fig:extlc-minus-minus-typing}
+\end{figure}
+
+
+\begin{figure}
+ \begin{mathpar}
+ % Case-nat Beta
+ \inferrule*
+ {\hasty \Gamma V \nat}
+ {\casenat {\injnat {V}} {M_{no}} {n} {M_{yes}} = M_{yes}[V/n]}
+
+ \inferrule*
+ {\hasty \Gamma V {\dyn \ra \dyn} }
+ {\casenat {\injarr {V}} {M_{no}} {n} {M_{yes}} = M_{no}}
+
+ % Case-nat Eta
+ \inferrule*
+ {}
+ {\Gamma , x :\, \dyn \vdash M = \casenat{x}{M}{n}{M[(\injnat{n}) / x]} }
+
+
+ % Case-arr Beta
+
+
+ % Case-arr Eta
+
+
+ \end{mathpar}
+ \caption{New equational rules for $\extlcprime$ (rules for case-arrow are analogous
+ and hence are omitted).}
+ \label{fig:extlc-minus-minus-eqns}
+\end{figure}
+
+
+
+
+\section{Term Semantics}\label{sec:term-semantics}
+
+\subsection{Domain-Theoretic Constructions}\label{sec:domain-theory}
+
+In this section, we discuss the fundamental objects of the model into which we will embed
+the gradual lambda calculus.
+It is important to remember that the constructions in this section are entirely
+independent of the syntax described in the previous section; the notions defined
+here exist in their own right as purely mathematical constructs.
+In Section \ref{sec:term-interpretation}, we will link the syntax and semantics
+via a semantic interpretation function.
+
+
+\subsection{Modeling the Dynamic Type}
+
+When modeling the dynamic type $\dyn$, we need a semantic object $D$ that satisfies the
+isomorphism
+
+\[ D \cong \Nat + (D \to (D + 1)). \]
+
+where the $D + 1$ represents the fact that in the function case, the function may return an error.
+Unfortunately, this equation does not have inductive or coinductive solutions. The usual way of
+dealing with such equations is via domain theory, by which we can obtain an exact solution.
+However, the heavy machinery of domain theory can be difficult for language designers to learn
+and apply in the mechanized setting.
+Instead, we will leverage the tools of guarded type theory, considering instead the following
+similar-looking equation:
+
+\[ D \cong \Nat + \later (D \to (D + 1)). \]
+
+Since the negative occurrence of $D$ is guarded under a later, this equation has a (guarded) solution.
+Specifically, we consider the following function $f$ of type
+$\later \type \to \type$:
+
+\[ \lambda (D' : \later \type) . \Nat + \later_t (D'_t \to (D'_t + 1)). \]
+
+(Recall that the tick $t : \tick$ is evidence that time has passed, and since
+$D'$ has type $\later \type$, i.e. $\tick \to \type$, then $D'_t$ has type $\type$.)
+
+Then we define
+
+\[ D = \fix f. \]
+
+% TODO explain better
+As it turns out, this definition is not quite correct; let us try to understand why.
+The price we pay for such a simple solution to the above equation is that we have
+introduced a notion of ``time'', i.e., we must now consider the stepping behavior of terms.
+% Therefore, the semantics of terms will need to allow for terms that potentially
+% do not terminate. This is accomplished using an extension of the guarded lift monad,
+% which we describe in the next section.
+Thus, in the equation for the semantics of $\dyn$, the result of the function should be
+a computation that may return a value, error, \emph{or} take an observable step.
+We model such computations using an extension of the so-called guarded lift monad
+\cite{mogelberg-paviotti2016} which we describe in the next section.
+We will then discuss the correct definition of the semantics of the dynamic type.
+
+\subsubsection{The Lift + Error Monad}
+
+% TODO ensure the previous section flows into this one
+When thinking about how to model gradually-typed programs where we track the steps they take,
+we should consider their possible behaviors. On the one hand, we have \emph{failure}: a program may fail
+at run-time because of a type error. In addition to this, a program may ``think'',
+i.e., take a step of computation. If a program thinks forever, then it never returns a value,
+so we can think of the idea of thinking as a way of intensionally modelling \emph{partiality}.
+
+With this in mind, we can describe a semantic object that models these behaviors: a monad
+for embedding computations that has cases for failure and ``thinking''.
+Previous work has studied such a construct in the setting of the latter, called the lift
+monad \cite{mogelberg-paviotti2016}; here, we augment it with the additional effect of failure.
+
+For a type $A$, we define the \emph{lift monad with failure} $\li A$, which we will just call
+the \emph{lift monad}, as the following datatype:
+
+\begin{align*}
+ \li A &:= \\
+ &\eta \colon A \to \li A \\
+ &\mho \colon \li A \\
+ &\theta \colon \later (\li A) \to \li A
+\end{align*}
+
+Unless otherwise mentioned, all constructs involving $\later$ or $\fix$
+are understood to be with respect to a fixed clock $k$. So for the above, we really have for each
+clock $k$ a type $\li^k A$ with respect to that clock.
+
+Formally, the lift monad $\li A$ is defined as the solution to the guarded recursive type equation
+
+\[ \li A \cong A + 1 + \later \li A. \]
+
+An element of $\li A$ should be viewed as a computation that can either (1) return a value (via $\eta$),
+(2) raise an error and stop (via $\mho$), or (3) think for a step (via $\theta$).
+%
+Notice there is a computation $\fix \theta$ of type $\li A$. This represents a computation
+that runs forever and never returns a value.
+
+Since we claimed that $\li A$ is a monad, we need to define the monadic operations
+and show that they respect the monadic laws. The return is just $\eta$, and extend
+is defined via guarded recursion by cases on the input.
+% It is instructive to give at least one example of a use of guarded recursion, so
+% we show below how to define extend:
+% TODO
+%
+%
+Verifying that the monadic laws hold uses \lob-induction and is straightforward.
+
+%\subsubsection{Model-Theoretic Description}
+%We can describe the lift monad in the topos of trees model as follows.
+
+\subsubsection{Revisiting the Dynamic Type}
+Now we can state the correct definition of the semantics for the dynamic type.
+The set $D$ is defined to be the solution to the guarded equation
+
+\[ D \cong \Nat + \later (D \to \textcolor{red}{\li} D). \]
+
+
+\subsection{Interpretation}\label{sec:term-interpretation}
+
+We can now give a semantics to the gradual lambda calculus we defined
+in Section \ref{sec:step-sensitive-lc}.
+%
+Much of the semantics is similar to a normal call-by-value denotational semantics;
+we highlight the differences.
+We will interpret types as sets, and terms as functions.
+Contexts $\Gamma = x_1 \colon A_1, \dots, x_n \colon A_n$
+will be interpreted as the product $\sem{A_1} \times \cdots \times \sem{A_n}$.
+
+
+The semantics of the dynamic type $\dyn$ is the set $\Dyn$ introduced in Section
+\ref{sec:predomains}.
+%
+The interpretation of a value $\vhasty {\Gamma} V A$ will be a monotone function from
+$\sem{\Gamma}$ to $\sem{A}$. Likewise, a term $\phasty {\Gamma} M {{A}}$ will be interpreted
+as a monotone function from $\sem{\Gamma}$ to $\li \sem{A}$.
+
+Recall that $\Dyn$ is isomorphic to $\Nat\, + \later (\Dyn \to \li \Dyn)$.
+Thus, the semantics of $\injnat{\cdot}$ is simply $\inl$ and the semantics
+of $\injarr{\cdot}$ is simply $\inr \circ \next$.
+The semantics of case inspection on dyn performs a case analysis on the sum.
+
+The interpretation of $\lda{x}{M}$ works as follows. Recall by the typing rule for
+lambda that $\phasty {\Gamma, x : A_i} M {{A_o}}$, so the interpretation of $M$
+has type $(\sem{\Gamma} \times \sem{A_i})$ to $\li \sem{A_o}$.
+The interpretation of lambda is thus a function (in the ambient type theory) that takes
+a value $a$ representing the argument and applies it (along with $\gamma$) as argument to
+the interpretation of $M$.
+%
+The interpretation of bind and of application both make use the monadic extend function on $\li A$.
+%
+The interpretation of case-nat and case-arrow is simply a case inspection on the
+interpretation of the scrutinee, which has type $\Dyn$.
+
+
+\vspace{2ex}
+
+
+\noindent Types:
+\begin{align*}
+ \sem{\nat} &= \Nat \\
+ \sem{\dyn} &= \Dyn \\
+ \sem{A \ra A'} &= \sem{A} \To \li \sem{A'} \\
+\end{align*}
+
+% Contexts:
+
+% TODO check these, especially the semantics of bind, case-nat, and case-arr
+% with respect to their context argument
+\noindent Values and terms:
+\begin{align*}
+ \sem{\zro} &= \lambda \gamma . 0 \\
+ \sem{\suc\, V} &= \lambda \gamma . (\sem{V}\, \gamma) + 1 \\
+ \sem{x \in \Gamma} &= \lambda \gamma . \gamma(x) \\
+ \sem{\lda{x}{M}} &= \lambda \gamma . \lambda a . \sem{M}\, (*,\, (\gamma , a)) \\
+ \sem{\injnat{V_n}} &= \lambda \gamma . \inl\, (\sem{V_n}\, \gamma) \\
+ \sem{\injarr{V_f}} &= \lambda \gamma . \inr\, (\sem{V_f}\, \gamma) \\[2ex]
+ \sem{\nxt\, V} &= \lambda \gamma . \nxt (\sem{V}\, \gamma) \\
+ \sem{\theta} &= \lambda \gamma . \theta \\
+%
+ \sem{\err_B} &= \lambda \delta . \mho \\
+ \sem{\ret\, V} &= \lambda \gamma . \eta\, \sem{V} \\
+ \sem{\bind{x}{M}{N}} &= \lambda \delta . \ext {(\lambda x . \sem{N}\, (\delta, x))} {\sem{M}\, \delta} \\
+ \sem{V_f\, V_x} &= \lambda \gamma . \ext {(\lambda f . (\ext {f} {\sem{V_x}\, \gamma}))} {(\sem{V_f}\, \gamma)} \\
+ \sem{\casenat{V}{M_{no}}{n}{M_{yes}}} &=
+ \lambda \delta . \text{case $(\sem{V}\, \delta)$ of} \\
+ &\quad\quad\quad\quad \alt \inl(n) \to \sem{M_{yes}}(n) \\
+ &\quad\quad\quad\quad \alt \inr(\tilde{f}) \to \sem{M_{no}} \\
+ \sem{\casearr{V}{M_{no}}{\tilde{f}}{M_{yes}}} &=
+ \lambda \delta . \text{case $(\sem{V}\, \delta)$ of} \\
+ &\quad\quad\quad\quad \alt \inl(n) \to \sem{M_{no}} \\
+ &\quad\quad\quad\quad \alt \inr(\tilde{f}) \to \sem{M_{yes}}(\tilde{f})
+\end{align*}
--
GitLab