\documentclass{article}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{stmaryrd}
\usepackage{wasysym}
\usepackage{proof}
\usepackage{hyperref}
\usepackage[usenames,svgnames]{xcolor}
\usepackage{framed}
\usepackage[left=3cm,top=3cm,right=4cm,nohead,bottom=3cm]{geometry}

\newtheorem{lemma}{Lemma}[section]
\def\lemmaautorefname{Lemma}
\newenvironment{hint}{\noindent{\bf (Hint)}}{}
\newtheorem{thm}{Theorem}
\newtheorem{definition}{Definition}
\newtheorem{task}{Task}
\newtheorem{bonus}{Bonus Task}
\renewenvironment{proof}{\trivlist \item[\hskip \labelsep{\bf
Proof:}]}{\hfill$\Box$ \endtrivlist}

\input{hw3-macros}

\title{\Large\textbf{
Homework 3: G\"{o}del's T and PCF}
\normalsize\\
15-814: Types and Programming Languages\\
TA: Carlo Angiuli (cangiuli@cs.cmu.edu)\\}

\author{}
\date{%
Out: 10/17/13\\
Due: 10/31/13 (12 PM)\\
}

\begin{document}
\maketitle

Please submit your work by the start of lecture on the due date, as a PDF to
{\tt cangiuli@cs.cmu.edu}. Include the phrase ``15-814 Homework~3'' in the
subject line of your email.

\section{Termination for G\"{o}del's T}

Recall the statics and dynamics for G\"{o}del's T:
% Statics
\[
\infer[]{\G , x : \tau\vdash x : \tau}{}
\qquad
\infer[]{\G \vdash \lam{x:\tau_1} M : \tau_1 \rightarrow \tau_2}
{\G , x : \tau_1 \vdash M : \tau_2}
\qquad
\infer[]{\G \vdash M\, N : \tau_2}{\G \vdash M : \tau_1 \rightarrow
  \tau_2 & \G
  \vdash N : \tau_1}
\]
\[
\infer[]{\G \vdash \z : \nat}{}
\qquad
\infer[]{\G \vdash \suc(M) : \nat}{\G \vdash M : \nat}
\qquad
\infer[]{\G \vdash \natind(M ; N_0 ; x.N_1 ) : \tau}
{\G \vdash M : \nat & \G \vdash N_0 : \tau & \G , x : \tau \vdash
  N_1 : \tau}
\]

% Dynamics
\[
\infer[]{M\,N \reduces M'\,N}{M \reduces M'}
\qquad
\infer[]{M\,N \reduces M\,N'}{M \val & N\reduces N'}
\qquad
\infer[]{(\lam{x:\tau} M)\,N \reduces [N/x]M}{N\val}
\]
\[
\infer[]{\natind(\z ; N_0 ; x.N_1 ) \reduces N_0}{}
\qquad
\infer[]{\natind(\suc(M) ; N_0 ; x.N_1 ) \reduces [\natind(M ; N_0 ; x.N_1)/x]N_1}{M\val}
\]
\[
\infer[]{\suc(M) \reduces \suc(M')}{M \reduces M'}
\qquad
\infer[]
  {\natind(M ; N_0 ; x.N_1 ) \reduces \natind(M' ; N_0 ; x.N_1)}
  {M \reduces M'}
\]
\[
\infer[]{\z \val}{}
\qquad
\infer[]{\suc(M) \val}{M \val}
\qquad
\infer[]{\lam{x:\tau_1} M \val}{}
\]

In class, we proved the progress and preservation theorems for this system.

\begin{lemma}[Preservation]
If $\cdot \vdash M : \tau$ and $M \reduces M'$ then $\G \vdash M' : \tau$.
\end{lemma}
\begin{lemma}[Progress]
If $\cdot \vdash M : \tau$ then either $M\,\mathsf{val}$ or $M \reduces M'$, for
some $M'$.
\end{lemma}

Use these theorems to prove type safety for G\"{o}del's T.

\begin{task}[Type Safety]
Show that if $\cdot\vdash M:\tau$ and $M\reduces^* M'$, then $M'\val$ or
$M'\reduces M''$ for some $M''$.
\end{task}

Type safety ensures that well-typed terms reduce until they reach a value, but
it's possible that some term might never reach a value. In the next few tasks,
we will prove \emph{termination}, the property that every well-typed term
reduces to a value.

We saw in class that a simple inductive proof of termination breaks down for
application. Our fix will be to strengthen the inductive hypothesis to a
property of terms called \emph{hereditary termination}. Hereditary termination
is defined at each type (inductively on the structure of types) as a predicate
on closed terms of that type, as follows:

\begin{samepage}
\begin{definition}[Hereditary Termination]~
\begin{enumerate}
\item $\HT_\nat(M)$ iff $M \reduces^* N$ and $N\val$.
\item $\HT_{\tau_1 \rightarrow \tau_2}(M)$ iff
$M \reduces^* \lam{x:\tau_1}M'$,
and for any $M_1$ such that $\HT_{\tau_1}(M_1)$,
$\HT_{\tau_2}([M_1/x]M')$.
\end{enumerate}
\end{definition}
\end{samepage}

For any context $\G$, a \emph{total substitution} $\gamma$ is a mapping from
$\dom{\G}$ to closed terms which preserves types; that is, for each $x:\tau$ in
$\G$, $\gamma(x) : \tau$. Given a total substitution $\gamma$ and a term
$\G\vdash M:\tau$, we can form a closed term $\hat{\gamma}(M)$ by
performing the substitution. For example, if $\G=(x:\tau\to\tau',y:\tau)$,
$M=x\,y$, and $\gamma$ is a total substitution for $\G$, then
$\hat\gamma(M)=\gamma(x)\,\gamma(y)$.

We say that $\HT_\Gamma(\gamma)$ iff for all $x : \tau$ in $\G$, we have
$\HT_\tau(\gamma(x))$. 

We need one more lemma before proving our main theorem.

\begin{task}[Head Expansion]
Show that if $\HT_\tau(M)$, $\cdot\vdash M' : \tau$, and $M' \reduces M$ then
$\HT_\tau(M')$.
\end{task}

We can now prove all terms are hereditarily terminating. You may use without
proof a canonical forms lemma.

\begin{task}
Show that if $\G \vdash M : \tau$ and $\HT_\G(\gamma)$ then
$\HT_\tau(\hat{\gamma}(M))$.
\end{task}
\begin{hint}
Use induction on the typing derivation. You will need an additional induction
inside the case for the recursor.
\end{hint}

\begin{task}[Termination]
Show that if $\cdot\vdash M:\tau$, then $M$ terminates.
\end{task}
\begin{hint}
Prove that if $\HT_\tau(M)$, then $M$ terminates.
\end{hint}

\section{Big-step operational semantics}

Because reduction in G\"{o}del's T is deterministic and terminating,  we know
that we can compute any term to its unique fully-evaluated form by reducing
until we reach a value.  Because we are describing computation by means of an
iterated process of reduction, $\reduces$ is called a \emph{small-step
operational semantics}.

Another approach is to directly define the relation between any term and its
fully-evaluated form, all in one go; this is called a \emph{big-step operational
semantics}, and is written $M\eval M'$. It is defined by the following rules:

\[
\infer[]
  {M\,N \eval M''}
  {M \eval \lam{x:\tau}M' & N\eval N' & [N'/x]M' \eval M''}
\]
\[
\infer[]
  {\natind(M ; N_0 ; x.N_1 ) \eval N_0'}
  {M \eval \z & N_0 \eval N_0'}
\qquad
\infer[]
  {\natind(M ; N_0 ; x.N_1 ) \eval N_1'}
  {M \eval \suc(M') & [\natind(M' ; N_0 ; x.N_1)/x]N_1 \eval N_1'}
\]
\[
\infer[]{\z \eval \z}{}
\qquad
\infer[]{\suc(M) \eval \suc(M')}{M \eval M'}
\qquad
\infer[]{\lam{x:\tau} M \eval \lam{x:\tau} M}{}
\]

We want to show that the notions of computation described by $\eval$ and
$\reduces$ coincide, in the sense that they associate the same fully-evaluated
form to each term.

As in the previous homework, you may use the fact that $\reduces^*$ is
transitive, and various compatibility lemmas (below).

\begin{lemma}\label{lma:beta-trans}
  If $M \reduces^* M'$ and $M' \reduces^* M''$ then $M \reduces^* M''$.
\end{lemma}
\begin{lemma}\label{lma:beta-suc}
If $M\reduces^* M'$, then $\suc(M)\reduces^*\suc(M')$.
\end{lemma}
\begin{lemma}\label{lma:beta-natind}
If $M\reduces^* M'$, then for any $x,N_0,N_1$, we have 
$\natind(M ; N_0 ; x.N_1) \reduces^* \natind(M' ; N_0 ; x.N_1)$.
\end{lemma}
\begin{lemma}\label{lma:beta-ap1}
  If $M \reduces^* M'$ then for any $M''$ we have $M\,M'' \reduces^* M'\,M''$.
\end{lemma}
\begin{lemma}\label{lma:beta-ap2}
  If $M \reduces^* M'$ then for any $M''$ we have $M''\,M \reduces^* M''\,M'$.
\end{lemma}
\begin{lemma}\label{lma:beta-abs}
  If $M \reduces^* M'$ then for any $x$ we have
  $\lambda x.M \reduces^* \lambda x.M'$.
\end{lemma}

One direction of the correspondence between $\eval$ and $\reduces^*$ is the
following:
\begin{task}
Show that if $M\eval M'$, then $M\reduces^* M'$ and $M'\val$.
\end{task}

To prove the other direction, we need two lemmas:
\begin{task}
Show that if $M\val$, then $M\eval M$.
\end{task}

\begin{task}
Show that if $M\reduces M'$ and $M'\eval M''$, then $M\eval M''$.
\end{task}
\begin{hint}
Use induction on the derivation of $M\reduces M'$. In each case, consider which
rules of $\eval$ could apply to $M'$.
\end{hint}

And now we can complete the proof of the other direction:
\begin{task}
Show that if $M\reduces^* M'$ and $M'\val$, then $M\eval M'$.
\end{task}

\section{Halting Problem in PCF}

In this exercise we will show that there is no PCF term $T$ which, given a PCF
term $M:\nat$, decides whether or not $M$ reduces to a value. Such a term
$T:\nat\to\nat$ must obey the following specification:
\[
\begin{array}{lcl}
T\,M \reduces 0 & \mbox{ or } & T\,M \reduces 1\\
T\,M \reduces 1 && \mbox{iff } M \mbox{ reduces to a value (converges)}\\
T\,M \reduces 0 && \mbox{iff } M \mbox{ does not reduce to a value
(diverges)}\\
\end{array}
\]
To prove that no such $T$ is definable in the $\lambda$-calculus, we will
replicate the diagonal argument used to prove the undecidability of the Halting
Problem, but in a \emph{higher-order} setting.

\begin{task}
Use the $\fix$ operator to write a divergent closed term of type $\nat$.
\end{task}

\begin{task}
Show that $T$ is not definable in PCF.
\end{task}
\begin{hint}
Assume that $T$ is definable, and define another term $D:\nat$ that applies $T$
to $D$ itself, such that if the outcome is $1$ then $D$ diverges, and otherwise
it is equal to $0$. (Use $\natrec$ to check the value of $T\,D$.) Since $D$ is a
PCF term, we can try and observe the behavior of applying $T$ to $D$ itself,
from which a contradiction should arise.
\end{hint}

\end{document}
