Problem 12 - Typed $\lambda$-calculus

Consider a typed $\lambda$-calculus, whose types and terms are given by the following syntax. (We assume that constants and variables in $\lambda$-prefixes are explicitly annotated with their types.)

$t$($\lambda$-terms)	$::=$	$x$(variable)$\vert$$c^{\tau}$(constant)$\vert$$t_1t_2$(application)$\vert$ $\lambda x:\tau.t$($\lambda$-abstraction)
$\tau$(types)	$::=$	$b$(bases types)$\vert$ $\tau_1\rightarrow\tau_2$(function types)

1.

A type environment $\Gamma = x_1:\tau_1, \dots, x_n:\tau_n$ is a mapping from variables to types. Give a set of inference rules (typing rules) to define the relation ' $\Gamma \vdash t:\tau$' which means that $\lambda$-term $t$ has type $\tau$ under the type environment $\Gamma$.

2.

Using the inference rules in 1., write a derivation tree for the relation $z:int\vdash (\lambda x:int.1^{int})z:int$.

3.

Describe an outline of a proof of the subject reduction theorem: 'If $\Gamma \vdash t:\tau$ holds (i.e., if it is derived by the inference rules in 1.) and $t$ is reduced to $t'$, then $\Gamma \vdash t':\tau$ holds'. Then, by using the theorem, show that, for any closed $\lambda$-term $t$, if $\Gamma \vdash t:\tau$ holds, then no runtime type mismatch error can happen during reductions of $t$.

1.

• Variable $x$ has type $\tau$ under the type environment $\Gamma$ is infered from the empty set:
  $$\frac{\emptyset}{\Gamma \vdash x : \Gamma(x)}$$
  since the type environment $\Gamma$ is already a mapping from all the variables to the types.
• Constant $c^{\tau}$ has type $\tau$ under the type environment $\Gamma$ is also infered from the empty set:
  $$\frac{\emptyset}{\Gamma \vdash c^\tau : \tau}$$

• Application $t_1t_2$ has type $\tau$ under the type environment $\Gamma$ is infered from the types of the $\lambda$-terms $t_1$ and $t_2$:
  $$\frac{\Gamma\vdash t_1 : \tau'\rightarrow\tau \quad \Gamma \vdash t_2 : \tau'}{\Gamma \vdash t_1 t_2 : \tau}$$
  using the classical view of what can be an application.
• The type of any $\lambda$-abstraction under the type environement $\Gamma$ is infered from the types of its components:
  $$\frac{\Gamma,x:\tau \vdash t:\tau'}{\Gamma \vdash (\lambda x : \tau . t) : \tau \rightarrow \tau'}$$

2.

First:

$$\frac{\emptyset}{z:int,x:int\vdash 1^{int}:int} \quad (1)$$

From (1), we obtain (2):

$$\frac{z:int,x:int\vdash 1^{int}:int}{z:int\vdash(\lambda x:int.1^{int}):int\rightarrow int} \quad (2)$$

Then:

$$\frac{\empty}{z:int \vdash z:int} \quad (3)$$

From (2) and (3):

$$\frac{z:int\vdash(\lambda x:int.1^{int}):int\rightarrow int \quad z:int\vdash z:int}{z:int\vdash (\lambda x:int.1^{int})z:int} \quad (4)$$

3.

Let's call the following theorem:

'If $\Gamma \vdash t:\tau$ holds and $t\triangleright_{\beta}t'$ then $\Gamma \vdash t':\tau$ holds.'

the theorem (5). To prove (5), we'll first have to prove the corresponding substitution lemma by induction on the structure of the typed term and use it in a proof by induction on the structure of the term derived by the rules of the operational semantics.

If $\Gamma \vdash t:\tau$, $t$ reduces to $t$, then there is not type mismatch, because this is a reduction with an empty serie of contractions or changes of bound variables. According to (5), if $t$ reduces to $t'$ and if $\Gamma \vdash t:\tau$, then $\Gamma \vdash t':\tau$, which also means that a non-empty serie of contractions or changes of bound variables doesn't cause any type mismatch at run time.