A type environment $\Delta$ is defined by $\Delta ::= \cdot\ |\ \Delta, \alpha$, where $\alpha$ denotes a type variable. A judgement in form of $\Delta\vdash \tau$ states that type $\tau$ is well-formed in $\Delta$, i.e., all free type variables in $\tau$ appear in $\Delta$. An example of judgements of this kind is $\beta \vdash \forall \alpha.\, \alpha\rightarrow \beta$. We lift the judgement to define $\Delta \vdash \Gamma$, meaning $\forall x\in Dom(\Gamma).\,\Delta\vdash\Gamma(x)$. That is, all the types in the range of $\Gamma$ are well-formed in $\Delta$. When we write $\Delta; \Gamma \vdash e:\tau$, we mean $\Gamma \vdash e:\tau$ plus that $\tau$ is well-formed in $\Delta$. A type parameter $\alpha$ is introduced to term $e$ by type abstraction $\Lambda \alpha.\, e$, and eliminated from $e$ by type application $e[\tau]$ (for $e$ in form of $\Lambda \alpha.\, e$). The corresponding typing rules are$$\frac{\Delta, \alpha; \Gamma \vdash e: \tau}{\Delta; \Gamma \vdash \Lambda \alpha.\,e: \forall\alpha.\tau}\quad\mbox{and}\quad\frac{\Delta; \Gamma \vdash e: \forall\alpha.\tau\quad\Delta \vdash \tau'}{\Delta; \Gamma \vdash e[\tau']: \tau[\tau'/\alpha]}.$$In this lecture, we shall consider an extension of STLC with type abstraction and type application. This extension is in fact a terminating fragment of System F.
A context is comprehended as a complete program with a single hole that is capable of accepting an expression of a certain type. Context typing is in general expressed as $C: (\Gamma\vdash \tau) \leadsto (\Gamma'\vdash \tau')$. That is, given a context $C$, we can embed any expression $e$ in it such that $\Gamma\vdash e:\tau$ implies $\Gamma'\vdash C[e]:\tau'$.
Two expressions $e_1$ and $e_2$ are contextual equivalent in $\Gamma$ (written as $\Gamma \vdash e_1 \approx_{ctx} e_2: \tau$) iff $\Gamma \vdash e_1:\tau$, $\Gamma \vdash e_2:\tau$, and for all $C:(\Gamma \vdash \tau) \leadsto (\cdot \vdash bool)$, $\exists v:\tau.$ $e_1 \Downarrow v \wedge e_2 \Downarrow v$.
Note that here we only consider contextual equivalence for terminating programs. We shall extend its definition for general programs a bit later in this lecture. Also, we assume that the context yields a closed Boolean program after $e$ is embedded. This assumption is made without loss of generality: for any two programs of type inhabited by at least two members, there exists a context to differentiate their return values with Boolean if and only if the two programs are not contextual equivalent. (Any two programs of type with only one inhabitant are contextual equivalent by definition.)
The main difficulty of reasoning about contextual equivalence lies in the fact that equivalence must be shown for all contexts $C$. Proving equivalence by inducting on the structure of $C$ is problematic for $C = \lambda x:\tau.\, C$ and $C = \Lambda \alpha.\,C$. Hence, instead of proving contextual equivalence directly, people usually use proof methods such as logical relations or other technical bisimulations. We shall prove the following two interesting theorems in this lecture to demonstrate the technique of logical relations:
Theorem 1. If $\vdash e: \forall \alpha.\, \alpha\rightarrow\alpha$ and $\vdash \tau$ and $\vdash v:\tau$, then $e[\tau]\ v \hookrightarrow^* v$.
Theorem 2. If $\vdash e: \forall \alpha.\, \alpha\rightarrow bool$, $\vdash \tau_1 $, $\vdash \tau_2$, $\vdash v_1:\tau_1$, $\vdash v_2:\tau_2$, then $e[\tau_1]\ v_1 = e[\tau_2]\ v_2$.
The idea is to define logical relations such that contextual equivalent terms can be related by hypothesis. Let's first define value interpretations for some closed types:
$\V[bool]=\{\ (true,true),\ (false,false)\ \}$
The slogan of LRs for function types is "You give me related inputs; I give you related outputs." Do not confuse this with Theorem 2, where the two inputs are not required to be related.
$\V[\tau\rightarrow\tau']=\{\ (\lambda x:\tau.\, e_1,\lambda x:\tau.\, e_2)\ |\ \forall (v_1, v_2)\in \V[\tau].\, (e_1[v_1/x], e_2[v_2/x]) \in \E[\tau']\ \}$
The interpretation for polymorphic types is new.
$\V[\forall \alpha.\, \tau]=\{\ (\Lambda \alpha.\,e_1, \Lambda \alpha.\,e_2)\ |\ \forall \tau_1, \tau_2.\, (e_1[\tau_1/\alpha], e_2[\tau_2/\alpha]) \in \V[\tau](\rho[\alpha\mapsto(\tau_1, \tau_2)])\ \}$
Note that $\tau_1[\tau'/\alpha]$ and $\tau_2[\tau'/\alpha]$ are different types. Hence we relate them with a LR for parametric type $\tau$, and use $\rho$ (called a relational substitution) to remember the types $\tau_1,\ \tau_2$ picked for type parameter $\alpha$. In general, a relational substitution is in form of $\{\alpha_1\mapsto(\tau_{11},\tau_{12}), \alpha_2\mapsto(\tau_{21},\tau_{22}), ... \}$. We shall write $\V[\tau](\rho)$ to express the fact that $\V[\tau]$ is parametrized by substitution $\rho$, assuming that $dom(\rho)\supseteq FTV(\tau)$.
$\V[\alpha]=\{\ (\tau_1, \tau_2)\ |\ \rho(\alpha)=(\tau_1, \tau_2)\ \}$
(to be continued)
No comments:
Post a Comment