m2-pas-dm/sections/correctness.tex

\subsection{Correctness}

\begin{definition}[Well typed value]
\label{wt-value}
A value $v \in Value$ is well typed regarding to a type $T$ (noted $v |- T$) when:
\begin{align*}
v |- int &<=> v \in \mathbb{N} \\
v |- \{f_1 : T_1, \dots, f_n : T_n\} &<=> v \in Field \rightharpoonup Value\text{ and }\forall f_i, f_i \in dom(v) \land v(f_i) |- T_i
\end{align*}
\end{definition}

\begin{definition}[Well typed state]
\label{wt-state}
A state $\sigma \in State$, $\sigma \neq \bot$ is well typed with regards to a type system $\Gamma$ (noted $\sigma |- \Gamma$) when
\[\forall x \in Var,\ \Gamma |- x : T => \sigma x |- T\]
\end{definition}

\begin{lemma}[Well typed expressions cannot go wrong]
$\forall e \in AExpr, \sigma \in State, \Gamma$ such as $\sigma |- \Gamma$:
\[\Gamma |- e : T => \mathcal{A}|[e|] \sigma |- T\]
In particular, $\mathcal{A}|[e|] \sigma \neq \bot$.
\end{lemma}

\begin{proof}
We demonstrate this property by induction on the structure of the expression $e$.
First let assume that $\Gamma |- e : T$.
We can eliminate all trivial cases in contradiction with this assumption (for example when $e = 1 + 1$ and $T = \{\}$).
Here are the other base cases:
\begin{itemize}
\item $e = n, T = int$.

$\mathcal{A}|[e|] \sigma = \mathcal{N}|[n|] \sigma$.

$\mathcal{N}|[n|] \sigma \in \mathbb{N}$ so we have $\mathcal{A}|[e|] \sigma \in \mathbb{N}$ which means that $\mathcal{A}|[e|] \sigma |- T$.

\item $e = x$.

By definition $\mathcal{A}|[x|]\sigma = \sigma x$.

$\sigma$ is well typed, so by definition \ref{wt-state}, $\sigma x |- T$. 
So we have $\mathcal{A}|[e|] \sigma |- T$.
\end{itemize}

Now the inductive cases:
\begin{itemize}
\item $e = e_1\ o\ e_2, T = int$.

By definition $\mathcal{A}|[e|]\sigma = \mathcal{A}|[e_1|]\sigma\ o\ \mathcal{A}|[e_2|]\sigma$.

We also know that $\Gamma |- e_1 : int$ and $\Gamma |- e_2 : int$ (by definition of $|-$).
So by our hypothesis of induction, we have $\mathcal{A}|[e_1|]\sigma |- int$ and $\mathcal{A}|[e_2|]\sigma |- int$.

This means that both $\mathcal{A}|[e_1|]\sigma$ and $\mathcal{A}|[e_2|]\sigma$ are in $\mathbb{N}$,
$\mathcal{A}|[e_1|]\sigma\ o\ \mathcal{A}|[e_2|]\sigma$ is defined and returns a value in $\mathbb{N}$.

So we have $\mathcal{A}|[e|] \sigma |- T$.

\item $e = e_1.f$.

By definition, $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[e_1|] \sigma f$.
But is it defined?

By definition of $|-$,
\[
  \inference{\Gamma \vdash e_1 : \{f : T\}}{\Gamma \vdash e_1.f : T}
\]

By our hypothesis of induction, we have $\mathcal{A}|[e_1|]\sigma |- T$.
So by definition \ref{wt-state} we have:
\begin{itemize}
\item $\mathcal{A}|[e_1|]\sigma \in Field \rightharpoonup Value$
\item $f \in dom(\mathcal{A}|[e_1|]\sigma)$
\item $\mathcal{A}|[e_1|]\sigma f |- T$
\end{itemize}

This means that $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[e_1|] \sigma f$ is defined,
and $\mathcal{A}|[e|] \sigma |- T$.

\item $e = e_1[f \mapsto e_2]$.

By definition, $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |] \sigma ]$.
We need to ensure that it is defined, and well typed.

By definition of $|-$,
\[
  \inference[append ]{\Gamma \vdash e_2 : T' & \Gamma \vdash e_1 : \{f_1 : T_1; \dots; f_n : T_n\}}{\Gamma \vdash e_1[f \mapsto e_2] : T = \{f : T'; f_1 : T_1; \dots; f_n : T_n\}}
\]

or

\[
  \inference[override ]{\Gamma \vdash e_2 : T' & \Gamma \vdash e_1 : \{f_1 : T_1; \dots; f_i : T_i; \dots; f_n : T_n\}}{\Gamma \vdash e_1[f_i \mapsto e_2] : T = \{f_1 : T_1; \dots; f_i : T'; \dots; f_n : T_n\}}
\]

Let consider the first case (the other case works the same).
By our hypothesis of induction, we have $\mathcal{A}|[e_1|]\sigma |- \{f_1 : T_1; \dots; f_n : T_n\}$.
So by definition \ref{wt-state} we have:
\begin{itemize}
\item $\mathcal{A}|[e_1|]\sigma \in Field \rightharpoonup Value$
\item $f \in dom(\mathcal{A}|[e_1|]\sigma)$
%\item $\mathcal{A}|[e_1|]\sigma f |- T$
\end{itemize}

We also have (by induction again), $\mathcal{A}|[e_2|]\sigma |- T'$.

So $\mathcal{A} |[ e |] \sigma = \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |]]$ is defined,
and moreover:
\begin{itemize}
\item $\mathcal{A}|[e|] \sigma \in Field \rightharpoonup Value$
\item $\forall f_i, 1 \leq i \leq n, f_i \in dom(\mathcal{A}|[e|]\sigma)$ (because it is in $dom(\mathcal{A}|[e_1|]\sigma)$)
\item $f \in dom(\mathcal{A}|[e|]\sigma)$ (because it has just been added), and finally,
\item $\mathcal{A}|[e|]\sigma f |- T'$.
\end{itemize}

This matches the definition of $\mathcal{A}|[e|] \sigma |- T = \{f : T'; f_1 : T_1; \dots; f_n : T_n\}$.

\item $e = \{f_1 = e_1; \dots; f_n = e_n\}$.

By definition,
\[\mathcal{A} |[e|] \sigma f_i = \mathcal{A}|[e_i|] \sigma\]
This means that, $\forall f_i, 1 \leq i \leq n$:
\begin{itemize}
\item $\mathcal{A}|[e|] \sigma \in Field \rightharpoonup Value$
\item $f_i \in dom(\mathcal{A}|[e|]\sigma)$
\item $\mathcal{A}|[e|]\sigma f_i = \mathcal{A}|[e_i|]\sigma |- T_i$ (by induction).
\end{itemize}

This matches the definition for $\mathcal{A}|[e|] \sigma |- T$.

\end{itemize}
\end{proof}

\begin{lemma}[Well typed programs cannot go wrong]
\label{wt-state-dgw}
\[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma |- \Gamma,\; ((P, \sigma) \reduce \sigma' => \sigma' |- \Gamma) \land ((P, \sigma) \reduce (S, \sigma') => \sigma' |- \Gamma)\]
In particular this also means that:
\[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma |- \Gamma,\; (P, \sigma) \not\reduce \bot \land (P, \sigma) \not\reduce (S, \bot)\]
\end{lemma}

\begin{proof}
This proof can be done by induction on the length of the execution path of the program $P$.
Let's consider $\Gamma |- P$ and a state $\sigma |- \Gamma$.
\begin{itemize}
\item Let's prove that if $(P, \sigma) \rightarrow^0 \sigma' or (P, \sigma) \rightarrow^0 (S, \sigma')$ then $\sigma' |- \Gamma$.
Because $\sigma = (S, \sigma')$ is impossible, we are in the case where $\sigma = \sigma'$.
By hypothesis, $\sigma |- \Gamma$, so $\sigma' |- \Gamma$.

\item We name $s$ the intermediate state such as $(P, \sigma) \rightarrow^k s$ for any $k$.
We have two cases:
\begin{itemize}
\item $s = \sigma'' \in State$
There is no transition from a terminal state, so this is trivially true.
\item $s = (S, \sigma'')$
By induction we know that $\sigma'' |- \Gamma$.

We can prove by induction on the structure of $S$ that
$(S, \sigma'') \rightarrow \sigma' => \sigma' |- \Gamma$ and
$(S, \sigma'') \rightarrow (S', \sigma') => \sigma' |- \Gamma$.

Sadely, We don't have time to terminate the proof...
\end{itemize}
\end{itemize}
\end{proof}