This is the part II of my lecture note based on the lecture series "Logical Relations" given by Amal Ahmed at Oregon Programming Languages Summer School, 2015. See here for the Part I of this note.
Type safety. The slogan for type safety is "if a term is well-typed, it won't get stuck." Formally, this means that if $\vdash e:\tau$ and $e\hookrightarrow^* e'$, then either $e'$ is a value, or there exists $e''$ such that $e'\hookrightarrow e''$. Note that type safety doesn't require termination, and thus is weaker than strong normalization we proved earlier. On the other hand, type safety can be proved for Turing-complete languages such as STLC with recursive types (whereas strong normalization can not).
A well-known approach to prove type safety is via proving progress and preservation (note that these are proof methods for type safety, not the definition of it):
Progress lemma. If $\vdash e:\tau$, then either $e'$ is a value, or $\exists e''.\, e'\hookrightarrow e''.$
Preservation lemma. If $\vdash e:\tau$ and and $e'\hookrightarrow e''$, then $\vdash e'':\tau$.
Once these lemmas are established, type safety can be proved easily by induction. In this lecture, however, we shall use logical relations instead of the above lemmas to prove type safety.
We need a bunch of definitions before we proceed. Define that $val(e)$ holds iff $e$ is a value;
$red(e)$ holds iff $\exists e'.\, e\hookrightarrow e'$;
$safe(e)$ holds iff $\forall e'.\, e \hookrightarrow^* e' \implies red(e') \vee val(e')$. Now the definition of type safety can be stated as $\vdash e:\tau \implies safe(e)$. Recall that to prove strong normalization, we introduced a logical predicate $SN_\tau$ and used it to break statement $\vdash e:\tau \implies e\Downarrow$ into $\vdash e:\tau \implies SN_\tau(e)$ and $SN_\tau(e) \implies e\Downarrow$. Here we shall adopt a similar strategy. To begin with, we define the value interpretations of type-safe values and closed expressions as
$\V[bool] = \{\ false,\, true\ \}$
$\V[\tau\rightarrow\tau']=\{\ \lambda x:\tau.\, e\ |\ \forall v \in \V[\tau].\, e[v/x] \in \E[\tau']\ \}$
$\E[\tau]=\{\ e\ |\ \forall e'.\, e \hookrightarrow e' \implies red(e') \vee e' \in \V[\tau]\ \}$
Now, to prove $\vdash e:\tau \implies safe(e)$, it suffices to prove that $\vdash e:\tau \implies e \in \E[\tau]$ and $e \in \E[\tau] \implies safe(e)$. As before, the main difficulty lies in proving the first part, since the second follows immediately from the definition of $\E[\tau]$. Also, while we are proving type safety for closed terms, we need to use a hypothesis about open terms so as to apply induction to lambda expressions. For this purpose, we define a value interpretation for environments as follows:
$\G[\emptyset] = \{\emptyset\}$
$\G[\,\Gamma, x:\tau\,] = \{\ \gamma[x\mapsto v]\ |\ \gamma \in \G[\Gamma] \wedge v \in \V[\tau]\ \}$
Hence, a substitution $\gamma$ is in $\G[\Gamma]$ iff it maps variables to values that are type-safe and consistent with $\Gamma$. An expression is called semantically type-safe in $\Gamma$, written as $\Gamma \models e:\tau$, if and only if $\gamma(e) \in \E[\tau]$ for all substitutions $\gamma \in \G[\Gamma]$. That is, $\Gamma \models e:\tau$ iff $e$ always reduces to a type-safe closed term after its free variables are replaced by type-safe values consistent with $\Gamma$.
As mentioned above, to prove type-safety it suffices to show A) $\vdash e:\tau \implies \models e:\tau$, and B) $\models e:\tau \implies safe(e)$. Part A says that the syntactic notion of type safety (ie., well-typedness) implies a semantic notion of type safety which says that a term will not get stuck in execution. It is in fact a special case of the so-called "Fundamental Property" of logical relation $\ \Gamma \vdash e:\tau \implies \Gamma \models e:\tau$. Part B can be shown directly as follows. Recall that $safe(e)$ holds iff $\forall e'.\, e \hookrightarrow^* e' \implies red(e') \vee val(e')$. Suppose that $e \hookrightarrow^* e'$. If $\models e:\tau$, then we have $e\in \E[\tau]$ since $\emptyset(e)=e$. But this means $red(e') \vee e' \in \V[\tau]$, that is, $e'$ is reducible or $e'$ is a value. This concludes the proof.
You can see here and in the example of strong normalization that the property of interest follows almost immediately from the definition of the logical relations we use. This is often the case if you construct suitable logical relations to assist your proof.
Now we are going to prove the Fundamental Property, i.e., $\Gamma \vdash e:\tau \implies \Gamma \models e:\tau$. As we did in the proof of strong normalization, we perform induction on the type derivations case by case.
(to be continued)
No comments:
Post a Comment