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

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

\input{hw5-macros}

\title{\Large\textbf{
Homework 5: Representation Independence in System F}
\normalsize\\
15-814: Types and Programming Languages\\
TA: Carlo Angiuli (cangiuli@cs.cmu.edu)\\}

\author{}
\date{%
Out: 11/23/13 (updated 11/27/13) \\
Due: 12/6/13 (end of day)\\
}

\begin{document}
\maketitle

Please submit your work as a PDF to {\tt cangiuli@cs.cmu.edu}. Include the
phrase ``15-814 Homework~5'' in the subject line of your email. In this
assignment, we assume the same statics and dynamics for System F as in the
previous assignment.

\section{Logical Equivalence}

The fact that logical equivalence is reflexive is the key result in our study of
System F. For the most part, the proof proceeds along the same lines as the
proof of hereditary termination for G\"{o}del's T, which you completed in
Homework 3.

However, the situation is more complicated here. We wish to define logical
equivalence inductively on types, but the $\forall$ quantifier requires that we
define it also for open types, in the same way that we had to consider
hereditary termination of open terms in G\"{o}del's T.

Say that $\delta$ is a \emph{total substitution for a type context $\D$} if it
is a mapping from $\dom{\D}$ to closed types---that is, for each $t\type$ in
$\D$, $\cdot\vdash\delta(t)\type$. Given a total substitution $\delta$ for $\D$
and a type $\D\vdash\tau\type$, we can form a closed type $\hat\delta(\tau)$ by
performing the substitution. Since terms can also contain free type variables,
we can similarly substitute into any $\D;\G\vdash M:\tau$ to obtain
$\cdot;\G\vdash\hat\delta(M):\hat\delta(\tau)$.

As in Homework 3, $\gamma$ is a \emph{total substitution for a term context
$\G$} if it is a mapping from $\dom{\G}$ to closed terms; then given $\gamma$
and $\D;\G\vdash M:\tau$, we can perform the substitution and obtain
$\D;\cdot\vdash \hat\gamma(M):\tau$.

Given two total substitutions $\delta,\delta'$ for $\D$, an \emph{assignment of
splendid relations} between them is a choice of splendid relation $\eta(t)$
between $\delta(t)$ and $\delta'(t)$, for each $t\in\dom\D$. We notate this
situation as $\rels\eta\delta{\delta'}$, and we notate the extension of $\eta$
mapping $t$ to $R$ by $\eta,t\relto R$. The relation $R$ is \emph{splendid} if
it is closed under head expansion (a.k.a. converse evaluation) and observational
equivalence.

For any type $\D\vdash\tau\type$, and an assignment of relations
$\rels\eta\delta{\delta'}$ for $\D$, we define a binary relation $\LR\tau\eta$
in the following way, by induction on $\tau$:

\begin{definition}[Logical equivalence]~
For two terms $\D;\G\vdash M,N:\tau$, two total substitutions $\delta,\delta'$
for $\D$, an assignment $\rels\eta\delta{\delta'}$, and total substitutions
$\gamma,\gamma'$ such that $(\gamma,\gamma')\in\LR{\G}{\eta}$, we say that
\begin{itemize}
\item $(M,N)\in\LR\bool\eta$
if $\gd M,\gdp N$ terminate,
and $\gd M\simeq \gdp N$.

\item $(M,N)\in\LR{\tau_1\to\tau_2}\eta$
\cbstart
if $\gd M\reduces^*\lam{x:\tau_1}M'$ and
$\gdp N\reduces^*\lam{x:\tau_1}N'$,
\cbend
and for any $(M'',N'')\in\LR{\tau_1}\eta$,
$([M''/x]M',[N''/x]N')\in\LR{\tau_2}\eta$.

\item $(M,N)\in\LR t\eta$
if $\gd M,\gdp N$ terminate,
and $(\gd M,\gdp N)\in \eta(t)$.

\item $(M,N)\in\LR{\forall t.\tau}\eta$
if $\gd M\reduces^*\Lambda t.M'$ and
\cbstart
$\gdp N\reduces^*\Lambda t.N'$,
\cbend
and for any closed types $\tau_1,\tau_2$ and splendid relation $R$ between them,
$([\tau_1/t]M',[\tau_2/t]N')\in\LR{\tau}{\eta,t\relto R}$.
\end{itemize}
Finally, $(\gamma,\gamma')\in\LR\G\eta$ if for each $(x:\tau)\in\G$,
$(\gamma(x),\gamma'(x))\in\LR\tau\eta$.
\end{definition}

\textbf{Warning:} There are a lot of symbols here, so stop and make sure you
understand the idea behind the definition. Although it looks much more
complicated, this is just a generalization of the definitions of hereditary
termination and of logical equivalence from the previous two homework
assignments.

We are simply extending the usual relation to open terms by saying that free
term variables can be instantiated with any closed terms in the relation, and
free type variables can be ``instantiated'' with any splendid relation between
closed types (where the instantiation is accomplished via an environment $\eta$
of interpretations of the type variables, since we cannot literally substitute
the relation $R$ for the type variable $t$).

We need the following lemma, which says that this latter notion of instantiation
coincides with substitution, in the case that we instantiate a type variable to
$\LR\tau\cdot$ for some closed type $\tau$.

\cbstart
\begin{lemma}\label{lem:inst}
For $\D\vdash\tau\type$ and $\D,t\type\vdash\tau_1\type$, total substitutions
$\delta,\delta'$ for $\D$, and $\rels\eta{\delta}{\delta'}$, we have
$(M,N)\in\LR{\tau_1}{\eta,t\relto\LR{\tau}{\eta}}$ iff
$(M,N)\in\LR{[\tau/t]\tau_1}\eta$.
\end{lemma}

Note that, for this lemma to make sense, we need to know that logical
equivalence is itself splendid. Now we are ready to prove that logical
equivalence is reflexive!
\cbend

\begin{task}\label{task:fundthm}
Prove that, if $\D;\G\vdash M:\tau$, then for any total substitutions
$\delta,\delta'$ for $\D$, assignment $\rels\eta\delta{\delta'}$, and total
substitutions $\gamma,\gamma'$ for $\G$ with $(\gamma,\gamma')\in\LR\G\eta$, it
is the case that $(\gd M,\gdp M)\in\LR\tau\eta$.


\ \\\noindent
\textbf{Prove only the cases corresponding to the following two rules:}
\[
\infer[]
  {\D;\G\vdash \Lambda t.M:\forall t.\tau}
  {\D,t\type;\G \vdash M:\tau}
\qquad
\infer[]
  {\D;\G \vdash M[\tau]:[\tau/t]\tau_1}
  {\D;\G\vdash M:\forall t.\tau_1 & \D\vdash\tau\type}
\]
(The other cases work out similarly to those on Homework 3.)
\end{task}

\section{Free Theorems}

We can prove very strong theorems about arbitrary terms in System F, purely by
virtue of their types. For example, in class, we proved that all terms of type
$\forall t.t\to t$ are observationally equivalent to the polymorphic identity
function $\Lambda t.\lam{x:t}x$.

These are often called ``free theorems'' because they are systematic to
verify---they are all straightforward corollaries of \autoref{task:fundthm}.
These serve as concrete motivations for our abstract definition of logical
equivalence.

\begin{task}
Every term of type $\forall t.t\to t\to t$ (i.e., every Church boolean) is
observationally equivalent to either
$\Lambda t.\lam{x:t}\lam{y:t}x$ or
$\Lambda t.\lam{x:t}\lam{y:t}y$.
\end{task}
\begin{hint}
The proof is similar to the one for $\forall t.t\to t$, and mostly involves
unwinding the definition of logical equivalence at the given type.
\end{hint}

\section{Representation Independence}

Recall from the definition of logical equivalence that if we instantiate any
polymorphic type at two different types whose terms we can relate, then the two
instantiations must also be related. Because we can encode existential types
using polymorphism, we are able to reason about two different implementations of
any interface.

In this task, we will consider two implementations of an existential type
representing a list interface, and we will prove that users of either
implementation will obtain the same result, modulo the relation between the two
implementations. This is the essence of the abstraction theorem we discussed in
class.

\begin{task}
True or false---The abstraction theorem is the most important theorem in
computer science. Justify your answer.
\end{task}
\begin{hint}
Answer freely, but justify your answer in either case.
\end{hint}

To set up our example, we will extend System F with natural numbers, lists of
natural numbers, and products. Since these can be Church-encoded, doing so does
not add expressive power; it is purely for convenience.

\[\begin{aligned}
\tau &:= \cdots \mid \Nat \mid \List \mid \tau\times\tau \\
M &:= \cdots \mid \z \mid \suc(M) \mid \natrec(M,N_0,x.N_1) \mid
             \nil \mid \cons(M,M) \mid \foldr(M,N_0,x.y.N_1) \\ &\qquad\quad\!\mid
             (M,M) \mid \fst(M) \mid \snd(M) \\
\end{aligned}\]

\[
\infer
  {\D;\G\vdash \z:\Nat}
  {}
\qquad
\infer
  {\D;\G\vdash \suc(M):\Nat}
  {\D;\G\vdash M:\Nat}
\]
\[
\infer
  {\D;\G\vdash \natrec(M,N_0,x.N_1):\tau}
  {\D;\G\vdash M:\Nat
  &\D;\G\vdash N_0:\tau
  &\D;\G,x:\tau\vdash N_1:\tau}
\]
\[
\infer
  {\D;\G\vdash \nil:\List}
  {}
\qquad
\infer
  {\D;\G\vdash \cons(M,N):\List}
  {\D;\G\vdash M:\Nat
  &\D;\G\vdash N:\List}
\]
\[
\infer
  {\D;\G\vdash \foldr(M,N_0,x.y.N_1):\tau}
  {\D;\G\vdash M:\List
  &\D;\G\vdash N_0:\tau
  &\D;\G,x:\tau,y:\Nat\vdash N_1:\tau}
\]
\[
\infer
  {\D;\G\vdash (M,N):\tau_1\times\tau_2}
  {\D;\G\vdash M:\tau_1
  &\D;\G\vdash N:\tau_2}
\qquad
\infer
  {\D;\G\vdash \fst(M):\tau_1}
  {\D;\G\vdash M:\tau_1\times\tau_2}
\qquad
\infer
  {\D;\G\vdash \snd(M):\tau_2}
  {\D;\G\vdash M:\tau_1\times\tau_2}
\]

We use the usual dynamics for these constructs. In particular,
\[\begin{aligned}
\foldr(\nil,N_0,x.y.N_1)
&\reduces N_0 \\
\foldr(\cons(M,L),N_0,x.y.N_1)
&\reduces [\foldr(L,N_0,x.y.N_1)/x][M/y]N_1
\end{aligned}\]

Our first implementation of lists will be the $\nil,\cons,\foldr$ above. Our
second will be pairs of a $\Nat$ and $\Nat\to\Nat$, where the first is the
length of the list, and the second sends any $n$ to the $n$th element from the
end of the list. Both of these implement the existential type
\[ \exists t. (t\times (\Nat\to t\to t))\times
              (\forall u.t\to u\to (u\to\Nat\to u)\to u) \]

In the below definition, $\pred$ is the proper predecessor, and $\sub$ is proper
subtraction. (If they would mathematically yield negative numbers, they instead
return $\z$.) Note that $\ohead$ and $\otail$ are not needed to satisfy the list
interface, but we define them for convenience.

\[\begin{aligned}
\oList &:= \Nat\times(\Nat\to\Nat) \\
\onil &:= (\z,\lam{x:\Nat}x) \\
\ocons &:= \lam{n:\Nat}\lam{\ell:\oList}
           (\suc(\fst(\ell)),\lam{x:\Nat}\natrec(\sub\,\fst(\ell)\,x,
                                          n,y.\snd(\ell)\,x)) \\
\ofoldr &:= \forall u.\lam{\ell:\oList}\lam{m:u}\lam{n:(u\to\Nat\to u)}\ \\&\qquad
              \fst(\natrec(\fst(\ell),
                           (m,\z),
                           x.(n\,\fst(x)\,(\snd(\ell)\,\snd(x)),\suc(\snd(x)))))\\
\ohead &:= \lam{\ell:\oList}\snd(\ell)\,\pred(\fst(\ell)) \\
\otail &:= \lam{\ell:\oList}(\pred(\fst(\ell)),\snd(\ell))
\end{aligned}\]

\textbf{Warning:} It will be very difficult to complete the following tasks
unless you convince yourself this implements lists. I recommend playing around
with this code on paper, or in your favorite functional language.

Given $L:\List$ and $P:\oList$, say that $(L,P)\in S$ iff:
\begin{itemize}
\item $L\cong\nil$ and $\fst(P)\cong\z$, or
\item $L\cong\cons(N,L')$, $\fst(P)\cong\suc(M)$ for some $M$, $\ohead(P)\cong
N$, and $(L',\otail(P))\in S$.
\end{itemize}
Because $S$ is defined only in terms of observational equivalence, it is clear
that $S$ is splendid. Your task will be to prove that $\nil,\onil$,
$\cons,\ocons$, and $\foldr,\ofoldr$ all preserve this relation in a certain
sense. This implies that $\List$ and $\oList$ cannot be distinguished as
implementations of the existential interface for lists.

You may use any theorems from this assignment or proven during class, including
the fact that \autoref{task:fundthm} remains true in the presence of $\Nat$,
$\List$, and $\times$. (For example, you will need that $\cong$ is a congruence,
and is closed under reduction.) You will also need the following more specific
lemmas:
\begin{lemma}\label{lem:pred-suc}
If $M:\Nat$, then $\pred(\suc(M))\cong M$. 
\end{lemma}
\begin{lemma}\label{lem:sub-id}
If $M:\Nat$, then $\sub\,M\,M\cong\z$.
\end{lemma}
\begin{lemma}\label{lem:tail-cons}
If $(L,P)\in S$, then for any $N:\Nat$, $(L,\otail(\ocons\,N\,P))\in S$.
\end{lemma}
\begin{lemma}\label{lem:snd-len}
For $M:\Nat$ and $m,n,\ell$ of the correct types,
\[ \snd(\natrec(M,(m,\z),x.(n\,\fst(x)\,(\snd(\ell)\,\snd(x)),\suc(\snd(x)))))
\cong M \]
(The idea is that the second component keeps track of the current position in
the list, so it ends at the length of the list.)
\end{lemma}

If you feel you need any other lemmas (within reason), feel free to state them
and assume them without proof. The goal of these tasks is not to force you to
prove mundane lemmas about proper subtraction, etc.

\begin{task}
Prove that $(\nil,\onil)\in S$.
\end{task}

\begin{task}
Prove that for closed terms $L:\List$, $P:\oList$, and $N:\Nat$ such that
$(L,P)\in S$, $(\cons(N,L),\ocons\,N\,P)\in S$.
\end{task}

\begin{task}
Prove that for any closed type $\tau$, and any closed terms $L:\List$,
$P:\oList$, $M:\tau$, and $N:\tau\to\Nat\to\tau$ such that $(L,P)\in
S$, $(\foldr(L,M,x.y.N\,x\,y),\ofoldr[\tau]\,P\,M\,N)\in\sem\tau$.
\end{task}
\begin{hint}
Consider the two ways that $(L,P)\in S$ could be true.
\end{hint}

\end{document}
