proofs.tex

\subsection{Correctness of Declarative Subtyping}\label{sec:declsub-correct}
%% -----------------------------------------------------------------------------

\begin{figure}
	\begin{mathpar}
		\fbox{$\bjmtch{\ty}{\ty'}$}\\
		
		\inferrule*[right=MT-CName]
		{ }
		{ \bjmtch{\cname}{\cname} }		
		\\
		
		\inferrule[MT-IntReal]
		{ }
		{ \bjmtch{\tyint}{\tyreal} }
		
		\inferrule[MT-FltReal]
		{ }
		{ \bjmtch{\tyflt}{\tyreal} }
		\\
		
		\inferrule[MT-IntNum]
		{ }
		{ \bjmtch{\tyint}{\tynum} }
		
		\inferrule[MT-FltNum]
		{ }
		{ \bjmtch{\tyflt}{\tynum} }
		
		\inferrule[MT-CmplxNum]
		{ }
		{ \bjmtch{\tycmplx}{\tynum} }
		\\
		
		\inferrule*[right=MT-Pair]
		{ \bjmtch{\vty_1}{\ty_1} \\ \bjmtch{\vty_2}{\ty_2} }
		{ \bjmtch{\typair{\vty_1}{\vty_2}}{\typair{\ty_1}{\ty_2}} }
		\\
		
		\inferrule*[right=MT-Union1]
		{ \bjmtch{\vty}{\ty_1}  }
		{ \bjmtch{\vty}{\tyunion{\ty_1}{\ty_2}} }
		
		\inferrule*[right=MT-Union2]
		{ \bjmtch{\vty}{\ty_2}  }
		{ \bjmtch{\vty}{\tyunion{\ty_1}{\ty_2}} }
	\end{mathpar}
	\caption{Matching relation in \BetaJulia}
	\label{fig:bjsem-match}
\end{figure}

In order to show correctness of declarative subtyping,
we need to prove that the declarative definition of subtyping 
is sound and complete with respect to the semantic definition.
Formally, we write this statement as:
\begin{equation}\label{eq:declsub-correct-truesemsub}
\forall \ty_1, \ty_2.\ (\bjsub{\ty_1}{\ty_2} \iff \bjtruesemsub{\ty_1}{\ty_2}).
\end{equation}

Instead of directly proving~\eqref{eq:declsub-correct-truesemsub},
it is more convenient to prove the equivalence of declarative subtyping
to the following relation
(referred to as \defemph{matching-based semantic subtyping}):
\begin{equation}\label{eq:semsub-def}
\bjsemsub{\ty_1}{\ty_2} \quad \defsign \quad
\forall \vty.\ (\bjmtch{\vty}{\ty_1} \implies\ \bjmtch{\vty}{\ty_2}).
\end{equation}
The definition~\eqref{eq:semsub-def}
relies on the relation $\bjmtch{\vty}{\ty}$ 
(defined in~\figref{fig:bjsem-match}), read ``tag~\vty matches type~\ty'', 
which we call the \defemph{matching relation}.

Tag-based and matching-based semantic subtyping relations 
are equivalent:
%\begin{equation}
\[
\forall \ty_1, \ty_2.\ 
(\bjsemsub{\ty_1}{\ty_2} \iff \bjtruesemsub{\ty_1}{\ty_2}).
\]
%\end{equation}
To see why, let us recall that tag-based semantic subtyping~\eqref{eq:truesemsub-def} 
is defined as $\interpty{\ty_1} \subseteq \interpty{\ty_2}$
and the subset relation $X \subseteq Y$ as
$\forall x.\ (x \in X \implies x \in Y)$.
Therefore, the definition~\eqref{eq:truesemsub-def} can be 
rewritten as:
\begin{equation}\label{eq:truesemsub-def-new}
\bjtruesemsub{\ty_1}{\ty_2} \;\defsign \;
%\interpty{\ty_1} \subseteq \interpty{\ty_2} \; \defsign \;
\forall \vty.\ (\vty \in \interpty{\ty_1} \implies \vty \in \interpty{\ty_2}).
\end{equation}
It is easy to show by induction on \ty that the matching relation
is equivalent to the belongs-to relation $\vty \in \interpty{\ty}$. 
Therefore, the definitions~\eqref{eq:semsub-def}
and~\eqref{eq:truesemsub-def-new} are also equivalent.

Since $\bjtruesemsub{\ty_1}{\ty_2}$ is equivalent to $\bjsemsub{\ty_1}{\ty_2}$
and the equivalence relation $\iff$ is transitive,
it suffices to prove the following theorem
to show~\eqref{eq:declsub-correct-truesemsub}.

\begin{theorem}[Correctness of Declarative Subtyping]\label{thm:declsub-correct}
	\[
	\forall \ty_1, \ty_2.\ (\bjsub{\ty_1}{\ty_2} \iff\ \bjsemsub{\ty_1}{\ty_2})
	\]
\end{theorem}

The full proof of~\thmref{thm:declsub-correct} is 
Coq-mechanized~\cite{bib:MiniJlCoq},
so we only discuss some key aspects and leave details to the proof.
First, subtyping a value type coincides with matching:
\begin{equation}\label{eq:mtch-eq-declsub}
\forall \vty, \ty.\ (\bjsub{\vty}{\ty} \iff\ \bjmtch{\vty}{\ty}).
\end{equation}
Having that, we can prove 
$\bjsub{\ty_1}{\ty_2} \implies \bjsemsub{\ty_1}{\ty_2}$,
i.e. the soundness direction of~\thmref{thm:declsub-correct}
(below, we embed the definition~\eqref{eq:semsub-def} of 
matching-based semantic subtyping):
\begin{equation}\label{eq:declsub-imp-semsub}
\forall \ty_1, \ty_2.\ 
(\bjsub{\ty_1}{\ty_2} \implies\ 
\forall \vty.\ [\bjmtch{\vty}{\ty_1} \implies\ \bjmtch{\vty}{\ty_2}]).
\end{equation}
Knowing $\bjsub{\ty_1}{\ty_2}$ and $\bjmtch{\vty}{\ty_1}$,
we need to show that $\bjmtch{\vty}{\ty_2}$.
First, by applying~\eqref{eq:mtch-eq-declsub} to $\bjmtch{\vty}{\ty_1}$,
we get $\bjsub{\vty}{\ty_1}$.
Then, $\bjsub{\vty}{\ty_2}$ follows from $\bjsub{\vty}{\ty_1}$ 
and $\bjsub{\ty_1}{\ty_2}$ by transitivity.
Finally, by applying~\eqref{eq:mtch-eq-declsub} again,
we get $\bjmtch{\vty}{\ty_2}$. \qed

The other direction of~\thmref{thm:declsub-correct} is more challenging: 
\begin{equation}\label{eq:declsub-complete}
\forall \ty_1, \ty_2.\ 
(\bjsemsub{\ty_1}{\ty_2} \implies\ \bjsub{\ty_1}{\ty_2}).
\end{equation}
The key observation here is that~\eqref{eq:declsub-complete} can be shown 
for $\ty_1$ in \emph{normal form},
i.e. $\ty_1 \equiv \vty_1 \cup \vty_2 \cup \ldots \cup \vty_n$
(formally, this fact is denoted by predicate $\InNF(\ty_1)$ 
defined in~\figref{fig:bjsem-innf}, \appref{app:nf}):
\begin{equation}\label{eq:nf-declsub-complete}
\forall \ty_1, \ty_2 \Alt \InNF(\ty_1).\
(\bjsemsub{\ty_1}{\ty_2} \implies\ \bjsub{\ty_1}{\ty_2}).
\end{equation}
In this case, in the definition~\eqref{eq:semsub-def}
of $\bjsemsub{\ty_1}{\ty_2}$, the only
value types $\vty$ that match $\ty_1$ and $\ty_2$ are $\vty_i$ of $\ty_1$. 
By~\eqref{eq:mtch-eq-declsub}, we know that matching implies subtyping,
so we conclude that all $\bjsub{\vty_i}{\ty_2}$.
From the latter, it is easy to show that 
$\bjsub{(\vty_1 \cup \vty_2 \cup \ldots \cup \vty_n)}{\ty_2}$ because,
according to the \RD{UnionL} rule,
subtyping of the left-hand side union amounts to subtyping its components.
To show~\eqref{eq:declsub-complete}, we need several more facts
in addition to~\eqref{eq:nf-declsub-complete}.
\begin{itemize}
  \item Function $\NF$ produces a type in normal form:
	\begin{equation}\label{eq:nf-innf}
	\forall \ty.\ \InNF(\NF(\ty)).
	\end{equation}
  \item Normalized type is equivalent to the source type:
    \begin{equation}\label{eq:nf-declsub-eq}
    \forall \ty.\;\ \bjsub{\NF(\ty)}{\ty}\ \land\ \bjsub{\ty}{\NF(\ty)}.
    \end{equation}
  \item Normalization preserves the subtyping relation:
    \begin{equation}\label{eq:nf-semsub}
    \forall \ty_1, \ty_2.\ 
    (\bjsemsub{\ty_1}{\ty_2} \implies\ \bjsemsub{\NF(\ty_1)}{\ty_2}).
    \end{equation}
\end{itemize}
To prove~\eqref{eq:declsub-complete}, we need to show $\bjsub{\ty_1}{\ty_2}$
given $\bjsemsub{\ty_1}{\ty_2}$. 
For this, we first apply~\eqref{eq:nf-semsub} to $\bjsemsub{\ty_1}{\ty_2}$,
which gives $\bjsemsub{\NF(\ty_1)}{\ty_2}$. 
Then we can apply~\eqref{eq:nf-declsub-complete} to the latter
because of~\eqref{eq:nf-innf} to get $\bjsub{\NF(\ty_1)}{\ty_2}$.
Finally, \eqref{eq:nf-declsub-eq} and transitivity 
gives $\bjsub{\ty_1}{\ty_2}$. \qed

\subsection{Reductive Subtyping}\label{sec:redsub-correct}
%% -----------------------------------------------------------------------------

Since we have already shown that declarative subtyping is
equivalent to semantic subtyping, it suffices to show that
reductive subtyping is equivalent to declarative subtyping:

\begin{theorem}[Correctness of Reductive Subtyping]\label{thm:redsub-correct}
\[
\forall \ty_1, \ty_2.\ (\bjsubr{\ty_1}{\ty_2} \iff\ \bjsub{\ty_1}{\ty_2})
\]
\end{theorem}

The proof is split into two parts: soundness and completeness.
For soundness (completeness), 
%by induction on $\bjsubr{\ty_1}{\ty_2}$ ($\bjsub{\ty_1}{\ty_2}$),
we show that for each \RR{}\!rule (\RD{}\!rule) it is possible to build
a corresponding declarative (reductive) derivation 
using \RD{}\!rules (\RR{}\!rules).

The soundness direction is mostly straightforward, as most \RR{}\!rules
have an immediate \RD{}\!counterpart (or require one extra application
of transitivity).
In the case of \RR{NF}, the induction hypothesis of the proof,
$\bjsub{\NF(\ty_1)}{\ty_2}$, 
and the fact that $\bjsub{\ty_1}{\NF(\ty_1)}$ 
according to~\eqref{eq:nf-declsub-eq},
allow to conclude $\bjsub{\ty_1}{\ty_2}$.

The challenging part of the proof is to show completeness,
as this requires proving that the reductive definition 
is \emph{reflexive}, \emph{transitive}, and \emph{distributive}
(\appref{app:proofs}).

%To prove transitivity and distributivity, 
%we need several auxiliary statements:
%\begin{enumerate}
%  \item $\bjsubr{\ty}{\ty'}\ \implies\ \bjsubr{\NF(\ty)}{\ty'}$,
%  \item $\bjsubr{\NF(\ty_1)}{\NF(\ty_2)}\;\;\ \land\;\; \bjsubr{\NF(\ty_2)}{\ty_3}$\\
%     $\implies \bjsubr{\NF(\ty_1)}{\ty_3}$,
%  \item $\bjsubr{\NF(\ty)}{\NF(\ty')}\ \implies\ \bjsubr{\ty}{\ty'}$.
%\end{enumerate}
%Having all the facts, we can prove completeness by induction
%on a derivation of $\bjsub{\NF(\ty_1)}{\ty_2}$.
%For details, the reader can refer to the full Coq-proof.

\begin{theorem}[Decidability of Reductive Subtyping]\label{thm:redsub-decidable}
\[
\forall \ty_1, \ty_2.\ 
(\bjsubr{\ty_1}{\ty_2}\quad \lor\quad \lnot [\bjsubr{\ty_1}{\ty_2}])
\]
\end{theorem}

To prove the theorem, 
it suffices to show that reductive subtyping is decidable
when $\ty_1$ is in normal form.
This is done by induction on a derivation of $\InNF(\ty_1)$.
We refer the reader to \appref{app:proofs} for more details.

% By induction on a derivation of $\InNF(\ty_1)$, we can show
% that the reductive subtyping is decidable for $\ty_1 | \InNF(\ty_1)$.
% In this case, $\ty_1$ is either a value type or a union of normalized types.
% If it is a value type, subtyping is equivalent to matching,
% and matching is decidable.
% If $\ty_1$ is a union $\tyunion{\ty_a}{\ty_b}$, 
% we use induction hypothesis for components and the fact that
% subtyping union on the left-hand side
% $\bjsubr{\tyunion{\ty_a}{\ty_b}}{\ty'}$ implies $\bjsubr{\ty_a}{\ty'}$
% and $\bjsubr{\ty_b}{\ty'}$.
% Since $\InNF(\NF(\ty_1))$, we can use the decidability 
% of $\bjsubr{\NF(\ty_1)}{\ty_2}$ to prove decidability
% of $\bjsubr{\ty_1}{\ty_2}$.