\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{hw2-macros}

\title{\Large\textbf{
Homework 2: Trees and Parallel Reduction}
\normalsize\\
15-814: Types and Programming Languages\\
TA: Carlo Angiuli (cangiuli@cs.cmu.edu)\\}

\author{}
\date{%
Out: 9/26/13\\
Due: 10/3/13 (12 PM)
}

\begin{document}
\maketitle

In this assignment, we will consider the Church encoding of binary trees, and
prove a lemma used in lecture to prove the Church--Rosser theorem.
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~2'' in the
subject line of your email.

\section{Church trees}

In lecture, we saw that $\lambda$-calculus can express natural numbers via
Church encodings. Recall that a number is either $\zero$ or $\suc(M)$ for some
number $M$. Furthermore, we can define the test function $\ifz(M,N_1,N_2)$
satisfying the specification:
%
\[\begin{aligned}
\ifz(\zero, N_1, N_2) &\equiv_\beta N_1 \\
\ifz(\suc(M), N_1, N_2) &\equiv_\beta N_2
\end{aligned}\]
%
The Church encoding of these constructs is:
%
\[\begin{aligned}
\zero &= \lambda z. \lambda s. z \\
\suc(M) &= \lambda z. \lambda s. s\,(M\,z\,s) \\
\ifz(M, N_1, N_2) &= M\,N_1\,(\lambda x. N_2)
\end{aligned}\]

Your task is to construct the Church encoding of binary trees. For our purposes,
a binary tree is either an unlabeled leaf, or a node with two distinguished
subtrees. You must define:
%
\[\begin{aligned}
&\leaf\\
&\branch(M_1, M_2)\\
&\rec_\tree(M, N_1, N_2)
\end{aligned}\]
%
where the $\rec_\tree$ is a recursor which ``walks through the tree,''
satisfying the specification:
%
\[\begin{aligned}
\rec_\tree(\leaf, N_1, N_2) &\equiv_\beta N_1 \\
\rec_\tree(\branch(M_1, M_2), N_1, N_2) &\equiv_\beta
  N_2\,(\rec_\tree(M_1, N_1, N_2))\,(\rec_\tree(M_2, N_1, N_2))
\end{aligned}\]

\begin{task}
Implement these constructs in $\lambda$ terms.
\end{task}

\begin{task}
Write a $\lambda$ term $M$ which computes the height of a tree (given in the
encoding you defined above).
To be precise, for any tree $T$, $M\,T$ must $\beta$-reduce to a Church numeral
$N$ where $N$ encodes the height of the tree $T$.

Please make your code easy to follow. $\smiley$
You may use $\plus$ and $\pred$ without defining them.
You may define the height of the one-node tree to be either one or zero, but
write down which.

\begin{hint}
Use $\rec_\tree$.
\end{hint}

\begin{hint}
As in real-life programming, it may be helpful to implement some subproblems,
give them names, and use them later.
\end{hint}
\end{task}

\section{Parallel reduction}

Recall the definitions of $\beta$-reduction:
\[
\infer[(\beta\ap_1)]{M\, N \reduces M' \, N}{M \reduces M'}
\quad
\infer[(\beta\ap_2)]{M\, N \reduces M \, N'}{N \reduces N'}
\]
\[
\infer[(\beta\abs)]{(\lambda x.M) \reduces (\lambda x.M')}{M \reduces M'}
\quad
\infer[(\beta)]{(\lambda x. M)\, N \reduces [N/x]M}{}
\]
and parallel reduction:
\[
\infer[({\parallel}\refl)]
  {M \parreduces M}
  {}
\qquad
\infer[({\parallel}\abs)]
  {(\lambda x.M) \parreduces (\lambda x.M')}
  {M \parreduces M'}
\]
\[
\infer[({\parallel}\ap)]
  {M\, N \parreduces M' \, N'}
  {M \parreduces M' & N \parreduces N'}
\quad
\infer[({\parallel}\beta)]
  {(\lambda x. M)\, N \parreduces [N'/x]M'}
  {M\parreduces M' & N\parreduces N'}
\]
%
(Unlike on the previous homework, we include the $(\beta\abs)$ rule so that
$\reduces$ reduces under $\lambda$-abstractions.)

We define the Kleene closure of these relations in the standard way, yielding
the relations $\reduces^*$ and $\parreduces^*$. Note that the $\reduces^*$
relation automatically satisfies the following compatibility properties, which
you may use without proof.

\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-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}

In lecture, we proved that $\reduces$ satisfies the Church--Rosser theorem if
$\reduces^*$ has the diamond property, and that $\parreduces^*$ has the diamond
property. Thus, to prove the Church--Rosser theorem, it suffices to show that
$\reduces^*$ and $\parreduces^*$ coincide. Your task is to prove one direction
of this.

\begin{task}
Prove that if $M\parreduces^* N$, then $M\reduces^* N$.

\begin{hint}
Start by writing out the rules for $\reduces^*$ and $\parreduces^*$.
\end{hint}
\end{task}

\end{document}
