From 3ff6aaa6a7697794f849632b1856ffac956b33f2 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Sat, 13 Jan 2024 16:17:57 -0500
Subject: [PATCH] changes to term precision syntax + semantics
---
paper-new/ordering.tex | 46 +++++++++++++++++++++++++++++++-----------
1 file changed, 34 insertions(+), 12 deletions(-)
diff --git a/paper-new/ordering.tex b/paper-new/ordering.tex
index 413461a..d50f647 100644
--- a/paper-new/ordering.tex
+++ b/paper-new/ordering.tex
@@ -54,8 +54,9 @@ derivations is composable, i.e., that the RHS of $\gamlt_1(x)$ is the same as th
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:
+The congruence rules are shown in Figure \ref{fig:term-prec-congruence-rules}.
+\begin{figure*}
\begin{mathpar}
\inferrule*[right = Var]
@@ -96,14 +97,20 @@ The congruence rules are as follows:
\etmprec {\gamlt, x : c} {N} {N'} {d} }
{\etmprec {\gamlt} {\bind {x} {M} {N}} {\bind {x} {M'} {N'}} {d}}
\end{mathpar}
+\caption{Term precision: congruence rules.}
+\label{fig:term-prec-congruence-rules}
+\end{figure*}
-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 then have additional equational axioms as shown in Figure \ref{fig:term-prec-additional-rules}.
+In particular, we have a rule stating that the error term is the bottom element,
+$\beta$ and $\eta$ laws as order-equivalences, and lastly 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{figure*}
\begin{mathpar}
\inferrule*[right = $\err$]
{\phasty {\Gamma} M B }
@@ -138,15 +145,19 @@ We write $M \equidyn N$ to mean that both $M \ltdyn N$ and $N \ltdyn M$.
\etmprec {\gamlt} {M} {N} {c \circ d} }
{ \etmprec {\gamlt} {M} {\dn {B} {C} N} {c} }
\end{mathpar}
+\caption{Term precision: additional rules.}
+\label{fig:term-prec-additional-rules}
+\end{figure*}
% 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
+The rules \textsc{UpR}, \textsc{UpL}, \textsc{DnL}, and \textsc{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}
+Intuitively, rule \textsc{UpR} says that the upcast of $M$ is an upper bound for $M$
+in that $M$ may error more, and \textsc{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
+Conversely, \textsc{DnL} says that the downcast of $M$ is a lower bound, and \textsc{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.
@@ -382,7 +393,11 @@ If $c$ is inj-arr, then when we downcast $M$ from $dyn$ to $\dyntodyn$,
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 right-hand side must be of the form $\theta(\dots)$, and the argument to
+$\theta$ on the LHS must be related to the argument of $\theta$ on the RHS.
+We can accomplish this by inserting a ``delay" on the right, i.e., wrapping the
+RHS in $\delta = \theta \circ \nxt$.
+% Maybe show the correct form of the rule in the special case $c = inj-arr$.
%
The need for delays affects the cast rules involving upcasts as well, because
the upcast for functions involves a downcast on the domain:
@@ -391,10 +406,14 @@ the upcast for functions involves a downcast on the domain:
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)
+The specific manner in which these delays must be inserted for a given type precision
+derivation $c$ is best examined in a more abstract setting, as it is independent of the
+particular concrete model under consideration.
+Thus, we postpone this discussion to the section on the abstract intensional categorical models of
+gradual typing (Section \ref{sec:abstract-intensional-models}).
+\begin{comment}
\subsubsection{Perturbations}
We can describe precisely how the delays are inserted for any type precision
@@ -441,3 +460,6 @@ 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.
+% Delays for function types and for inj-arr(c)
+
+\end{comment}
--
GitLab