\documentclass[11pt]{article}

\usepackage{amsmath,amssymb}
\usepackage{amsthm,color}
%\usepackage{bk0,bk11}

\input{../thms.inc}
\input{../lambda.tex}


\newcommand\qedd{~\rule{3mm}{3mm}}
\newcommand\weg[1]{{}}
\newcommand\black[1]{{\textcolor{black}{#1}}}
\newcommand\eqdf{{\mathbin{\textcolor{black}{\triangleq}}}}
\newcommand\eqb{{\mathbin{\textcolor{black}{=_\beta}}}}
\newcommand{\gr}[2]{\mathcal G_{#2}({#1})}
\newcommand{\thra}{\twoheadrightarrow}
\newcommand\beqn{\begin{eqnarray*}}
\newcommand\eeqn{\end{eqnarray*}}
\newcommand\dwn{\\[1.2em]}
\newcommand\lr[1]{\hr{\langle #1\rangle}}
\newcommand\myred[1]{{\textcolor{red}{#1}}}
\newcommand\hr[1]{{\myred{#1}}}
\newcommand\hoog[1]{\rule{0mm}{#1}}
\newcommand\hoogm{\hoog{1.1em}}
\def\pair#1#2{\langle#1,#2\rangle}
\def\tto{\mathrel{\twoheadrightarrow}}
\def\key#1{\mathop{\textsf{#1}}}
\def\bar{\begin{array}}
\def\ear{\end{array}}
\renewcommand\l{\lambda}
\newcommand\bl{\mbox{\boldmath{$\lambda$}}}
\newcommand\Lo{\Lambda^\emptyset}
\newcommand\cnum[1]{{{\church}_{#1}}}
\newcommand\church{\hr{\mathbf c}}
\renewcommand\cn[1]{{\church_{#1}}}
\newcommand\dn[1]{{\hr{\mathbf d}}_{#1}}
\newcommand\ceil[1]{\lceil #1\rceil}
\newcommand\real{{\mathbb R}}
\renewcommand\int{{\mathbb Z}}
\let\esti=\in
\def\in{{\,\esti\,}}
\newcommand\euro{\hr{\hspace{.1em}\raisebox{-.05em}{\large\sf C}\hspace{-.8em}\raisebox{.109em}{\small =}{}}}
\newcommand\false{\text{false}\;}

\newcommand\redd{\mathrel{\black{\twoheadrightarrow}}}
\newcommand\reddb{\mathrel{\black{\redd_{{\beta}}}}}


\newcommand{\lh}{\mathopen{\mbox{\hspace{0.05cm}\rule[0.8ex]{0.01ex}{1ex}
\kern-.35em{\rule[1.8ex]{0.6ex}{0.01ex}}}}}
\newcommand{\rh}{\mathclose{\mbox{\rule[1.8ex]{0.6ex}{0.01ex}
\kern-.35em{\rule[0.8ex]{0.01ex}{1ex}\hspace{0.05cm}}}}}
\newcommand{\num} [1] {\lh{#1}\rh}%%                     for numerals

\renewcommand\comb[1]{{\sf #1}}
\newcommand\Y{\comb{Y}}
%\newcommand\isb{=_\beta}
\renewcommand\L{\Lambda}



\newif\ifanswers
\answersfalse
%\answerstrue

\begin{document}

\section*{Lambda Calculus, Week 3}

\subsubsection*{In-class problems}

\begin{enumerate}
\item 
Let $F,G\in\Lo$. Show that if $Fx=Gx$, then for all $M\in\L$ one has $FM=GM$.
 The assumption that $F,G$ are closed is necessary.
\item
Write down a lambda term $F\in\Lo$ such that
$$F\num{xy}=x,$$
where we use the encoding of lambda terms by Mogensen.
\item Let $W\in\Lo$. Show that
there are $M,F\in\Lo$ such that
$$\bar{rcl}
FM&=&MW\\
Mf&=&f\num{M}
\ear$$
Conclude $FM=W\num{M}\hoog{1.2em}$.
\weg{{\sc Proof.} Construction $M$.
$$M=\l f.f\num{M}=(\l mf.fm)\num{M}=H\num{M}$$
and exists by the second fixed point theorem.\qedd\dwn}
\item For a given $T$ there exists a program $P$ such that 
$$\bar{rcll}
P\cnum{k}&=&\cnum{k+1},&\text{if $k$ is even},\\
&=&T\num{P}\cnum{k},&\text{otherwise}.
\ear$$
\end{enumerate}

\subsubsection*{Take-home problems}
A finite list ${M_{n_1},\ldots,M_0}\in\L$ is represented in $\L$ by
$[M_{n_1},\ldots,M_0]\in\L$ defined as follows.
\begin{eqnarray*}
[\,]&\eqdf&\false;\\
{}[M_n,M_{n-1},\ldots,M_0]&\eqdf&\pi M_n[M_{n-1},\ldots]
\end{eqnarray*}
Then
\[ [M_0, \dots, M_n] := \seqof{M_0, \seqof{M_1, \seqof{M_2, \cdots
\seqof { M_n, \fc} \cdots}}}\]
We can also represent an infinite \emph{stream} of terms
$\setof{M_0, M_1, \dots}$ by a term that looks like
\[ [M] = \seqof{M_0, \seqof{M_1, \cdots}} \]
In this case, the term $[M]$ is called the \emph{uniform enumeration}
of $\seqof{M_n}$.

For example, using the fixed-point theorem, we can define a term
\[ \nat x = \pi\; x\; (\nat (S^+ x)) \]
Where $S^+$ is the successor on Church numerals.
Then $[M] = \nat \cn{0}$ is a uniform enumeration of
$\setof{\cn{0}, \cn{1}, \cn{2}, \dots}$.

  \begin{enumerate}
  \item 
Given $n$, define a term $\pc_n$ such that
\[ \pc_n [M] = M_n \]
for any uniform enumeration $[M]$.

[Hint.  It could be easier to solve 2 first.]
\item Define a term $\pc$ such that
\[ \pc \cn{n} [M] = M_n \]
\item Given a term $N$, define a term $@_N$ such that, for any uniform enumeration $\seqof{M_n}$,
$@_N$ is a uniform enumeration of $\seqof{M_n N}$.

Then define a term $@$ such that
$@_N = @ N$ for each $N$.
\item
Define a term $\mathtt{zip}$, such that
\[ \mathtt{zip} [M] [N] = \seqof{M_0, \seqof{N_0, \seqof{M_1,
      \seqof{N_1, \dots}}}}\]
is a uniform enumeration of $\setof{M_0,N_0,M_1,N_1, \dots}$.
\item 
If for every fixed $n$, the sequence $\setof{M_{n,m}}_m$ is uniformly
enumerated by $[M_n]$, and the sequence of terms
$\setof{[M_n]}_n$ is uniformly enumerated by $[M]$, define a term
$[M^+]$ which uniformly enumerates the countable set $\setof{M_{n,m}}$
(using any ordering you wish).
\item Use the fixed-point theorem to define a uniform enumeration
  $\mathbb{C}$ of
  the set of combinators $\mathcal C$.  Prove that every combinator
  indeed occurs in the stream enumerated by $\mathbb C$.

[Hint. Take $\mathbb C = [\ic,\kc,\Sc,
\underline{\qquad}]$, where
``\underline{\qquad}'' depends on $\mathbb C$.]
\item Give a term $E$ with the following property: For every \emph{closed} lambda term $t \in \Lambda^0$, there exists an $n$ such that
\[ E \cn{n} = t \]
  \end{enumerate}

\end{document}

\begin{enumerate}
\item 
\begin{enumerate}
\item A \emph{fixed point combinator} is a term $Y\in\Lo$ such that
for all $F\in \L$ 
$$Y F\eqb F(YF)$$
$Y$ is called a \emph{reducing fixed point combinator} 
if moreover
$$Y F\reddb F(YF).$$
\item Define $\Y\eqdf\l f.(\l x.f(xx))(\l x.f(xx))$. 
Show that $\Y$ is a fixed point combinator.
\item Verify that $\Y$ is not reducing.
\item (Turing) Define $\Theta\eqdf TT$, where $T\eqdf \l ab.b(aab)$. Show that
$\Theta$ is a reducing fixed point combinator.
\item (B\"ohm, van der Mey)
Show that if $\comb{SI}Y=Y$, then $Y$ is a fixed point combinator.
\item (B\"ohm) Define $\Y_0\eqdf\Y$, $\Y_{n+1}\eqdf \Y_n(\comb{SI})$.
Show that $\Y_1\eqb\Theta$.
\item Show 
that $\Y_n$ is a reducing fixed point combinator except for $n=0$.
\end{enumerate}
\item
Show that there is a term $\Y^2$ such that
$\Y^2\num{F}=F\num{\Y^2\num{F}}$. Is it possible to have
$\Y^2F=F\num{\Y^2F}$, for all (closed) terms?
\item
Show that `$M\in\L$ reduces to a closed term' is undecidable.
\end{enumerate}
\end{document}


\newpage
\section{Simple type theory}
\begin{enumerate}
\item 
  \begin{enumerate}
  \item 
Prove that the set of normal inhabitants of the type
\[ N = o \to (o \to o) \to o \]
is precisely the set $\setof{\cn{n} \mid n \in \nat}$
\item Prove that there are no closed terms of type $o$.
  \end{enumerate}
\item Let $A$ be a set, $j,m \in A$, and $L \subseteq A \times A$.

\end{enumerate}
\end{document}
