\documentclass{article}

\oddsidemargin=0pt
\textwidth=6.5in


\usepackage{amssymb}
\usepackage{proof}

\input{defs}

\newcommand{\blankd}[4]{\ensuremath{\mathcal{#1}[\![#2]\!]^{\delta+\{\a\mapsto#3\}}
_{\eta+\{\alpha\mapsto#4\}}}}
\newcommand{\val}[1]{\ensuremath{\mathcal{V}[\![#1]\!]^{\delta}_\eta}}
\newcommand{\comp}[1]{\ensuremath{\mathcal{C}[\![#1]\!]^{\delta}_\eta}}
\newcommand{\vald}[3]{\blankd{V}{#1}{#2}{#3}}
\newcommand{\compd}[3]{\blankd{C}{#1}{#2}{#3}}

\newcommand{\cand}[1]{\ensuremath{\mathit{Cand}_{#1}}}



\begin{document}


\section*{All System F programs terminate}

This proof is based on notes by Bob Harper and Greg Morrisett. 

Extend System F with a new constant \z\ of type $\all\a.\a$. For every
type $\tau$, $\z[\tau]$ is a value. At higher types, we have the
following evaluation rules for \z.
\[
\z[\tau_1\arrow\tau_2]v \stepsto \z[\tau_2]
\]
\[
\z[\all\a.\tau][\tau'] \stepsto \z[\tau\{\tau'/\a\}]
\]

\begin{definition} A {\em candidate} for a closed type $\tau$ is a non-empty 
  set of closed values of type $\tau$ such that $\z[\tau] \in T$ for
  every $T \in \cand{\tau}$. (Where \cand{\tau}\ is the set of all
  candidates for type $\tau$.)
\end{definition}

\begin{definition} Define the interpretation of types as sets of {\em compuations}
  and {\em values} by induction on the structure of types. Below, \d\ 
  is a closed type substitution for the free type variables of
  $\tau$ and $\e$ assigns a candidate for $\delta(\a)$ to each
  variable $\a$.
\[
\begin{array}{lll}
\comp{\tau} &=& \{ e \alt e \red v \in \val{\tau} \}
\\
\\
\val{\intw} &=& \{ i , 0[\intw] \} \\
\val{\tau_1\arrow\tau_2} &=& \{ v \alt \vdash v :
    \delta(\tau_1\arrow\tau_2), \mbox{ for all }v'\in \val{\tau_1},
    vv'\in\comp{\tau_2} \} \\
\val{\a} &=& \eta(\a)\\
\val{\all\a.\tau} &=& \{ v \alt \vdash v : \delta (\all\a.\tau), 
    \mbox{ for all closed } \tau', \\
  && \qquad v[\tau'] \in \bigcap_{T\in\cand{\tau'}}
    \compd{\tau}{\tau'}{T} \}  \\
\end{array}
\]
\end{definition}


\begin{observation} All values are computations.
If $e \in \val{\tau}$ then $e \in \comp{\tau}$.
\end{observation}

\begin{observation} Anything that steps to a computation is a computation.
  If $e \in \comp{\tau}$ and $e' \stepsto e$, then $e' \in
  \comp{\tau}$.
\end{observation}

\begin{lemma}
  If $\Delta\vdash\tau$ then $\val{\tau} \in \cand{\delta(\tau)}$ for
  every closed type substitution $\d$ for $\Delta$ and every
  candidate assignment $\e$ for $\d$.
\end{lemma}
By inspection of the definition, we can see that \val{\tau}\ contains
only closed values of the correct type. What remains to be shown is
that it contains $\z[\tau]$.
\begin{proof} Proof is by induction on $\Delta\vdash\tau$.
\begin{itemize}
  \item If $\Delta\vdash\a$, by definition $\e(\a) \in
  \cand{\d(\a)}$.  
  
  \item If $\Delta\vdash\intw$, by definition
  $\z[\intw] \in \val{\intw}$.  
  
  \item If $\Delta\vdash \tau_1\arrow\tau_2$. To show that
  $\z[\delta(\tau_1\arrow\tau_2)]$ is a member of
  \val{\delta(\tau_1\arrow\tau_2)}, suppose that $v_1 \in
  \val{\tau_1}$.  By the evaluation rule,
  $\z[\delta(\tau_1\arrow\tau_2)] v_1 \stepsto \z[\delta{\tau_2}]$. By
  induction, \mbox{$\z[\delta(\tau_2)] \in \val{\tau_2}$}, so
  $\z[\delta(\tau_1\arrow\tau_2)] \in \comp{\tau_1\arrow\tau_2}$.
  
  \item If $\Delta\vdash \all\a.\tau$. Do this branch yourself.

\end{itemize}
\end{proof}

\begin{lemma}[Substitution] The interpretation of types is compositional.
  \[ \val{\tau\{\tau'/\a\}} = \vald{\tau}{\d(\tau')}{\val{\tau'}} \]
\end{lemma}
The proof of this lemma is by a straightforward induction on the
structure of $\tau$. Because the value sets are the same, we can
extend this result to the computation sets.
\begin{corollary}
 \[ \comp{\tau\{\tau'/\a\}} = \compd{\tau}{\d(\tau')}{\val{\tau'}} \]
\end{corollary}

\begin{lemma}
  If $\Delta\Gamma \vdash e : \tau$ then $\g(\d(e)) \in \comp{\tau}$
  for every closed type substitution \d\ for $\Delta$, every candidate
  assignment \e\ for \d, and every closed value substitution $\g$ such that 
  $\g(x) \in \val{\Gamma(x)}$ for every $x \in dom(\Gamma)$.
\end{lemma}

\begin{proof}
Proof is by induction on $\Delta\Gamma \vdash e :\tau$.
\begin{itemize}
\item If $\Delta\Gamma \vdash x : \Gamma(x)$.
  
\item If the last rule of the derivation was 
\[
\infer{\Delta\Gamma\vdash e_1 e_2 : \tau_1} 
{\Delta\Gamma \vdash e_1 : \tau_1\arrow \tau 
  \quad \Delta\Gamma \vdash e_1:\tau_1}
\]

Let \g, \d\ and \e\ be arbitrary. We want to show that
$\g(\d(e_1e_2))\in\comp{\tau_2}$.  

By induction $\g(\d(e_1))\in \comp{\tau_1\arrow\tau_2}$ and
$\g(\d(e_2))\in \comp{\tau_1}$, so $\g(\d(e_1))\red v_1 \in \val
{\tau_1\arrow\tau_2}$ and $\g(\d(e_2)) \red v_2 \in \val{\tau_1}$.

Therefore $\g(\d(e_1e_2))$ evaluates to $v_1 v_2$, and by the definition of 
\val {\tau_1\arrow\tau_2}, this expression is in $\comp{\tau_2}$.

\item If the last rule of the derivation was 
\[
\infer{\Delta\Gamma\vdash e [\tau'] : \tau \{\tau'/\a\}}
{\Delta\Gamma \vdash e : \all\a.\tau \qquad \Delta \vdash \tau'}
\]

Let \g, \d\ and \e\ be arbitrary. We want to show that
$\g(\d(e[\tau']))\in\comp{\tau\{\tau'/\a\}}$.  

By induction $\g(\d(e))\in \comp{\all\a.\tau}$ so $\g(\d(e))\red v \in
\val{\all\a.\tau}$

Therefore $\g(\d(e[\tau']))$ evaluates to $v[\d(\tau')]$, and by the definition of 
\val {\all\a.\tau},  $v[\d(\tau')]\in 
\bigcap_{T\in\cand{\d{\tau'}}} \compd{\tau}{\delta(\tau')}{T}$.

Because $\val{\tau'}$ is in \cand{\delta{\tau'}},
$v[\d(\tau')] \in \compd{\tau}{\delta(\tau')}{\val{\tau'}}$.
  By the substitution lemma, this set is equivalent to
  \comp{\tau\{\tau'/\a\}}.


\item If the last rule of the derivation was 
\[
\infer{\Delta\Gamma\vdash \lambda x:\tau_1.e :\tau_1\arrow\tau_2}
{\Delta\Gamma,x:\tau_1 \vdash e : \tau_2 \qquad \Delta\vdash \tau_1}
\]

(Do yourself.)

\item If the last rule of the derivation was 
\[
\infer{\Delta\Gamma\vdash \Lambda\a.e : \all\a.\tau}
{\Delta, \a\ \Gamma \vdash e : \tau}
\]

(Do yourself.)

\end{itemize}
\end{proof}


\begin{thm}
If $\vdash e : \tau$ then there exists $v$ such that $e\red v$.
\end{thm}
\begin{proof}
  By the above lemma, $e\in \comp{\tau}$ where $\d$ and $\e$ are
  empty.
\end{proof}

\end{document}