\documentclass[11pt,twoside]{article}
\usepackage{latex-macros/course}
\graphicspath{{/toc/a/class/6.042/fall02/problemrepository/figures/}}

\renewcommand{\coursecopyrightnames}{Prof.~Albert~R.~Meyer}

\newcommand{\subst}[3]{#1[#2 := #3]}

\def\lexle{\mathrel{\preceq_{\text{lex}}}}
\def\lex<{\mathrel{\prec_{\text{lex}}}}
\def\coordle{\mathrel{\preceq_{\text{c}}}}
\def\coord<{\mathrel{\prec_{\text{c}}}}
\def\tto{\textbf{$\rightarrow$}}
\def\lam{\texttt{lambda}}
\newcommand{\nil}{\texttt{nil}}


\def\mkp{\mathop{\text{mkfirst}}}
\def\lp{\texttt{(}}
\def\rp{\texttt{)}}

\newcommand{\meas}[1]{\mu(#1)}

\iffalse
\newcommand{\sz}{\mbox{size}}
\newcommand{\sbtr}{\mbox{subtrees}}

%\hidesolutions
%\showsolutions


\fi



\renewcommand{\reading}{Week 6 Notes.}

\begin{document}

\problemset{5}

\begin{problem}
Provide simple \emph{recursive} definitions of the following sets:

\begin{problemparts}

\problempart The set $S \eqdef \set{ 2^k 3^m 5^n \suchthat k,m,n \in
\naturals}$.

\solution{We can define the set $S$ recursively as follows:

\begin{enumerate}
\item $1 \in S$
\item If $n \in S$, then $2n$, $3n$, and $5n$ are in $S$.
\end{enumerate}
}

\problempart  The set $T \eqdef \set{2^k 3^{2k+m} 5^{m+n} \suchthat k,m,n \in
\naturals}$.

\solution{We can define the set $T$ recursively as follows:

\begin{enumerate}
\item $1 \in T$
\item If $n \in S$, then $18n$, $15n$, and $5n$ are in $T$.
\end{enumerate}
}

\problempart The set $L \eqdef \set{ (a, b) \in \integers^2
\suchthat a + 2b = 3k\text{ for some }k \in \integers }$.

\solution{We can define the set $L$ recursively as follows:

\begin{enumerate}
\item $(0, 0) \in L$
\item If $(a, b) \in L$, then $(a + 3, b)$, $(a - 3, b)$, $(a + 2, b -
1)$, and $(a - 2, b + 1)$ are in $L$.
\end{enumerate}
}

\end{problemparts}
\end{problem}


\begin{problem} %{S01-PS2} 		

The set, $W$, of ``well-formed parenthesis strings'' can be defined by
the following rules:

\begin{enumerate}
\item the empty string, $\emptystring$, is in $W$, and
\item if $s$ and $t$ are in W then the string $\lp s\rp t$ is
in $W$.
\end{enumerate}

For example, the string
\begin{quote}
\texttt{(()())()}
\end{quote}
is a well-formed parenthesis string, but the string
\begin{quote}
\texttt{)(())}
\end{quote}
isn't.

Use structural induction to prove that any prefix of any well-formed
parenthesis string has at least as many left parentheses as right
parentheses.

\solution{Let $L(t)$ be the predicate that $t$ is a string of parentheses
with at least as many left as right parentheses, and define
\[
P(t) \eqdef\quad  \forall p\  [\text{($p$ is a prefix of $t$)} \implies L(p)].
\]
We prove by structural induction that $P(r)$ holds for all $r \in W$.

\textbf{Base Case} ($r = \emptystring$): $P(r)$ holds because the only
prefix of $r$ is $r$ itself, and $L(r)$ holds because $r$ has the
\emph{same} number of left or right parentheses, namely, none.

\textbf{Inductive Step:} Let $s, t$ be any strings in $W$, and let $r\eqdef
\lp s\rp t$.  Assuming that $P(s)$ and $P(t)$ hold, we want to prove
$P(r)$.  So we let $p$ be any prefix of $r$ and prove $L(p)$ by considering
the following exhaustive set of cases:

\begin{itemize}

\item \text{} [$p = \emptystring$] We already observed that $L(p)$ holds.

\item  \text{} [$p = \lp $] $L(p)$ holds immediately.

\item  \text{} [$p = \lp u$, for some prefix, $u$, of $s$].  Since $P(s)$
holds, it follows that $L(u)$ holds.  But $p$ has the same number of right
parentheses and one more left parenthesis than $u$, so $L(p)$ holds \emph{a
fortiori}.

\item \text{} [$p = \lp s\rp u$, for some (possibly empty) prefix,
$u$, of $t$].  Say $s$ has $m_1$ left parentheses and $n_1$ right
parentheses.  Since $P(s)$, and hence $L(s)$, holds, we have $m_1 \ge n_1$.
Similarly, suppose $u$ has has $m_2$ left parentheses and $n_2$ right
parentheses.  Since $P(t)$ holds, we have that $L(u)$ holds, namely, $m_2
\ge n_2$.  So the number of left parentheses in $p$ is $m_1+m_2 +1 \ge
n_1+n_2 +1$ which equals the number of right parentheses in $p$.
This proves $L(p)$.
\end{itemize}

Thus, for any prefix, $p$, of $r$, we conclude that satisfies $L(p)$ holds,
that is, $P(r)$ holds, completing the proof by structural induction.
}

\end{problem}

\begin{problem}

\emph{Pure list expressions (PLEs)} are defined recursively as follows:
\begin{enumerate}
\item $\lp\rp$ is a PLE,
\item if $T_1,\dots,T_n$ are PLEs for $n\ge 1$, then
\begin{quote} $\lp T_1\ \dots\ T_n\rp$ is a PLE.
\end{quote}
\end{enumerate}

\emph{Pure Cons-cell Expressions (PCEs)} are defined recursively as
follows:
\begin{enumerate}
\item \nil\ is a PCE,
\item if $P_1,P_2$ are PCE's, then \texttt{(cons $P_1$ $P_2$)} is a PCE.
\end{enumerate}
A PCE can be understood as an expression whose \emph{value} is a PLE.  We
can define this value function, $\nu:\text{PCE} \to \text{PLE}$,
by recursion on the definition of PCE.  First, let $\mkp:\text{PLE}^2 \to
\text{PLE}$ be defined by the rules:
\begin{eqnarray}
\mkp(T, \lp\rp) &\eqdef& \lp T\rp, \label{mkone} \\
\mkp(T, \lp T_1\ \dots\ T_n \rp) &\eqdef &\lp T\ T_1\ \dots\ T_n \rp \label{mkmore}.
\end{eqnarray}

Now we define:
\begin{eqnarray}
\nu(\nil) &\eqdef& \lp\rp, \label{nunil} \\
\nu(\texttt{(cons $P_1$ $P_2$)}) &\eqdef& \mkp(\nu(P_1),\nu(P_2)) \label{nucon}.
\end{eqnarray}

\bparts

\ppart For any PCE, $P$, let $\#P$ be the number of occurrences of
\texttt{cons} in $P$.  We use the notation $\card{s}$ for the length of a
string, $s$.  Prove that
\begin{equation}\label{1P}
1+ \#P = \card{\nu(P)}/2.
\end{equation}


\solution{
\begin{proof}
The proof is by structural induction on the definition of a PCE,
$P$, with~(\ref{1P}) as the induction hypothesis.

\textbf{Base case} $P = \nil$: So $\nu(P) = \lp\rp$,
and
\[
1 + \#P = 1 + 0 = 1 = 2/2 = \card{\lp\rp}/2,
\]
so~(\ref{1P}) holds for \nil.

\textbf{Inductive case} $P = \texttt{(cons $P_1$ $P_2$)}$ for some PCEs
$P_1,P_2$ satisfying~(\ref{1P}), \ie
\begin{eqnarray}
1+ \#P_1 & = &\card{\nu(P_1)}/2,\label{P1}\\
1+ \#P_2 & = & \card{\nu(P_2)}/2.\label{P2}
\end{eqnarray}
We now prove that~(\ref{1P}) holds:

\begin{align*}
1+\#P & = 1+ (1+ \#P_1 + \#P_2) & \text{by def of $\#P$}\\
      & = (1+ \#P_1) + (1 + \#P_2)\\
      & = \card{\nu(P_1)}/2 + \card{\nu(P_2)}/2 & \text{by~(\ref{P1}) and~(\ref{P2})}\\
      & = \frac{\card{\nu(P_1)} + \card{\nu(P_2)}}{2}\\
      & = \frac{\card{\mkp(\nu(P_1),\nu(P_2))}}{2} & \text{by def of $\mkp$}\\
      & = \frac{\card{\nu(\texttt{(cons $P_1$ $P_1$)})}}{2}
          & \text{by def of $\nu$}\\
      & = \frac{\card{\nu(P)}}{2}.
\end{align*}


This completes the proof of the inductive case, and we conclude by
structural induction that~(\ref{1P}) holds for all PCEs, $P$.

\end{proof}
}

\eparts
 
The correspondence between a PCE, $P$, and the PLE, $\nu(P)$, is exact.
More precisely, there is a function $q:\text{PLE} \to \text{PCE}$ which is
the inverse of $\nu$, namely,
\begin{eqnarray}
\nu(q(T)) = & T  & \text{for all PLEs, $T$},\label{nq}\\
q(\nu(P)) = & P  & \text{for all PCEs, $P$.}\label{qn}
\end{eqnarray}

\bparts

\ppart\label{defq} Give a recursive definition of the function $q$.

\solution{
\begin{itemize}
\item $q(\lp \rp) \eqdef \nil$.

\item $q(\lp T_1\rp) \eqdef \texttt{(cons $q(T_1)$ \nil)}$.

\item For, $n \geq 2$,
\[
q(\lp T_1\ T_2 \dots\ T_n\rp) \eqdef \texttt{(cons $q(T_1)$ $q(\lp T_2\
\dots\ T_n\rp)$)}.
\]

\end{itemize}
}

\ppart Prove one of the equations~(\ref{nq}) or~(\ref{qn}).

\solution{

\begin{proof}
First, we prove~(\ref{nq}) by structural induction on definition of a PLE, $T$,
with induction hypothesis $\nu(q(T)) = T$.

\textbf{Base case} $T = \lp \rp$: 
\begin{align*}
\nu(q(T)) & = \nu(q(\lp \rp)) \\
          & = \nu(\nil) & \text{by def in part~(\ref{defq})} \\
          & = \lp \rp   & \text{by~(\ref{nunil})} \\
          & = T
\end{align*}

\textbf{Inductive case} $T = \lp T_1 \rp$:
\begin{align*}
\nu(q(T)) & = \nu(q(\lp T_1 \rp)) \\
          & = \nu(\texttt{(cons $q(T_1)$ \nil)}) & \text{by def in part~(\ref{defq})} \\
          & = \mkp(\nu(q(T_1),\nu(\nil))) & \text{by~(\ref{nucon})} \\
          & = \mkp(T_1, \lp\rp) & \text{by induction hypothesis} \\
          & = \lp T_1 \rp & \text{by~(\ref{mkone})} \\
          & = T
\end{align*}

\textbf{Inductive case} for $n \ge 2$, $T = \lp T_1 T_2 \dots\ T_n\rp$:
\begin{align*}
\nu(q(T)) & = \nu(q(\lp T_1 T_2 \dots\ T_n\rp)) \\
          & = \nu(\texttt{cons $q(T_1)$ $q(\lp T_2 \dots\ T_n \rp)$}) & \text{by def in part~(\ref{defq})} \\
          & = \nu(\texttt{cons $P_1$ $P_2$}) & \text{by func $q:\text{PLE} \to \text{PCE}$} \\
          & = \mkp(\nu(P_1),\nu(P_2)) & \text{by~(\ref{nucon})} \\
          & = \mkp(\nu(q(T_1)),\nu(q(\lp T_2 \dots\ T_n \rp))) \\
          & = \mkp(T_1, \lp T_2 \dots\ T_n \rp) & \text{by induction hypothesis} \\
          & = \lp T_1 T_2 \dots\ T_n \rp & \text{by~(\ref{mkmore})} \\
          & = T
\end{align*}

We conclude by structural induction that~(\ref{nq}) holds for all PLEs, $T$.

We then prove~(\ref{qn}) by structural induction on definition of a PCE, $P$,
with induction hypothesis $q(\nu(P)) = P$.

\textbf{Base case} $P = \nil$:
\begin{align*}
q(\nu(P)) & = q(\nu(\nil)) \\
          & = q(\lp \rp) & \text{by~(\ref{nunil})} \\
          & = \nil & \text{by def in part~(\ref{defq})} \\
          & = P
\end{align*}

\textbf{Inductive case} $P = (\texttt{cons $P_1$ $P_2$})$:
\begin{align*}
q(\nu(P)) & = q(\nu(\texttt{cons $P_1$, $P_2$})) \\
          & = q(\mkp(\nu(P_1),\nu(P_2))) & \text{by~(\ref{nucon})} \\
          & = q(\mkp(T_1, T_2)) & \text{by func $\nu:\text{PCE} \to \text{PLE}$} \\
          & = (\texttt{cons $q(T_1)$ $q(T_2)$}) & \text{by def in part~(\ref{defq})} \\
 	  & = (\texttt{cons $q(\nu(P_1))$ $q(\nu(P_2))$}) \\
          & = (\texttt{cons $P_1$ $P_2$}) & \text{by induction hypothesis} \\
          & = P
\end{align*}

We conclude by structural induction that~(\ref{qn}) holds for all PCEs, $P$.

\end{proof}
}

\ppart Conclude that for all $n\ge 1$ there are the same number of PCEs
with $n-1$ occurrences of \textbf{cons} as there are PLEs of length $2n$.

\solution{
$\nu:\text{PCE} \to \text{PLE}$ defines a function from PCEs to PLEs,
and the existence of $q:\text{PLE} \to \text{PCE}$ implies that
$\nu$ defines a bijection between PLEs and PCEs. $q$
defines a bijection between PCEs and PLEs as well.

From~(\ref{1P}), if $\#P = n-1$ (\eg PCEs with $n-1$ occurrences of 
cons) then $\card{\nu(P)} = 2n$ (\eg PLEs of length $2n$). 
That is, $\nu$ maps a PCE with $n-1$ cons to a PLE with length $2n$. 
Since $\nu$ is a bijection,  $\text{(number of PCEs
with $n-1$ occurrences of cons)} \le \text{(number of PLEs with length $2n$)}$.

On the other hand, we re-write~(\ref{1P}) as
\begin{equation}
1+ \#q(T) = \card{T}/2.
\end{equation}
If $\card{T} = 2n$ then $\#q(T) = n-1$. That is, $q$ maps a PLE with
length $2n$ to a PCE with $n-1$ cons. Since $q$ is a bijection, $\text{(number
of PLEs with length $2n$)} \le \text{(number of PCEs with $n-1$ cons)}$.

In summary, for all $n\ge 1$ there are the same number of PCEs
with $n-1$ occurrences of \textbf{cons} as there are PLEs of length $2n$.
}

\eparts

\end{problem}


\begin{problem}
Ackermann's function is an extremely fast-growing function of two natural
number arguments, whose inverse -- which is extremely slow-growing --
turns out to characterize the average efficiency of the Union-Find
algorithm for maintaining finite equivalence classes that was mentioned in
lecture.  We won't go further into the story of the Union-Find algorithm
and how Ackermann's function enters into its analysis; you will learn
about this if you take the Algorithms course, 6.046.  In this problem, we
simply examine the somewhat unusual recursive definition of Ackermann's
function, $A(m,n)$.

Ackermann's function is usually described as being defined by the
following equations:
\begin{align}
f(m,n) &=  2n, &&\text{if $m=0$ or $n \le 1$},\label{Am0}\\ 
f(m,n) &=  f(m-1,f(m,n-1)), &&\text{if $m > 0$ and $n > 1$}.\label{AA}
\end{align}
That is, if we regard equations~(\ref{Am0}) and~(\ref{AA}) as defining a
predicate $P(f,m,n)$ on numbers $m, n \in \naturals$ and a function
$f:\naturals^2 \to \naturals$, then $A$ is \emph{defined} to be the
\emph{unique} two-argument function on natural numbers such that $\forall
m,n\ P(A,m,n)$.

But how do we know that equations~(\ref{Am0}) and~(\ref{AA}) actually
define anything, and in particular that they define a total function?
Justifying this definition really breaks down into two parts, namely
\begin{itemize}
\item \emph{existence}: $\exists f: \naturals^2 \to \naturals\, \forall m,n\
P(f,m,n)$,

\item \emph{uniqueness}: $[\forall m,n\ P(f,m,n) \land P(g,m,n)] \implies f = g$.
\end{itemize}

\bparts

\ppart Use the well-ordering principle for lexicographic order, $\lexle$,
on $\naturals^2$ to prove uniqueness.  \hint Suppose $\forall m,n\
P(f,m,n) \land \forall m,n\ P(g,m,n)$.  Consider the least pair $(m,n) \in
\naturals^2$ such that $f(m,n) \neq g(m,n)$ and reach a contradiction.

\solution{
\begin{proof}
This proof is by contradiction. Assume that $\exists f,g\ f \ne g  [\forall m,n\ P(f,m,n) 
\land P(g,m,n)]$. That is, there exists a nonempty set $S$ of pairs $(m,n)$ such that 
$f(m,n) \ne g(m,n)$. Let's order all pairs $(m,n)$ on $\naturals^2$ in lexicographic order.
By well-ordering principle, there is a least pair $(m_0,n_0) \in S$,
such that $f(m_0,n_0) \ne g(m_0,n_0)$.

We can show that $m_0 > 0$ and $n_0 > 1$, since according to (\ref{Am0})
if $m_0 = 0$ or $n_0 > 1$, then
\begin{align*}
f(m_0,n_0) & = 2n_0 & \text{by $P(f,m_0,n_0)$}\\
           & = g(m_0,n_0) & \text{by $P(g,m_0,n_0)$}
\end{align*}

So,
\begin{align*}
f(m_0,n_0) & = f(m_0-1,f(m_0,n_0-1)) \\
g(m_0,n_0) & = g(m_0-1,g(m_0,n_0-1))
\end{align*}

Since $(m_0,n_0-1)$ is less than $(m_0,n_0)$ for $\lexle$,
$(m_0, n_0-1) \notin S$. That is, $f(m_0, n_0-1) = g(m_0,n_0-1) = j$.

Since $(m_0-1,j)$ is less than $(m_0,n_0)$ for $\lexle$,
$(m_0-1,j) \notin S$. That is, $f(m_0-1,j) = g(m_0-1,j) = k$.

So,
\begin{align*}
f(m_0,n_0) & = f(m_0-1,f(m_0,n_0-1)) \\
	   & = f(m_0-1,j) \\
	   & = k \\
  	   & = g(m_0-1,j) \\
	   & = g(m_0-1,g(m_0,n_0-1)) \\
	   & = g(m_0,n_0)
\end{align*}

There is a contradiction. Therefore, $[\forall m,n\ P(f,m,n) \land P(g,m,n)] \implies f = g$.

\end{proof}
}

\eparts

One way to prove existence is to use~(\ref{Am0}) and~(\ref{AA}) to give a
recursive definition of the graph of a \emph{relation}, $A$, and then to
prove that the relation is actually a function satisfying these equations.

Namely, define a set, $A$, of pairs in $\naturals^2 \cross \naturals$
recursively as follows:
\begin{enumerate}
\item $((m,n),2n) \in A$ if $m=0$ or $n \le 1$, \label{rel1}
\item if $(m-1,j),k) \in A$ and $((m,n-1),j) \in A$, then $((m,n),k)
\in A$, for all $j,k \in \naturals$, when $m > 0$ and $n > 1$. \label{rel2}
\end{enumerate}

\bparts

\ppart\label{relation} Use the well-ordering principle for $\lexle$ to show that $A$ is a
\emph{total} relation, \ie $\domain{A} = \naturals^2$.  \hint
Consider the \emph{least} $(m,n) \notin \domain{A}$ and reach a
contradiction.

\solution{
\begin{proof}
This proof is by contradiction. Assume that $\domain{A} \ne \naturals^2$. That is, there
exists a nonempty set $S$ of pairs $(m,n)$ such that $(m,n) \notin \domain{A}$. 
Let's order all pairs $(m,n)$ on $\naturals^2$ in lexicographic order.
By well-ordering principle, there is a least pair $(m_0,n_0) \in S$
such that $(m_0,n_0) \notin \domain{A}$.

We can show that $m_0 > 0$ and $n_0 > 1$, since according to~[\ref{rel1}] 
$((m_0,n_0),2n_0) \in A$ if $m_0 = 0$ or $n_0 \le 1$, 
which implies $(m_0,n_0) \in \domain{A}$.

Since $(m_0,n_0-1)$ is less than $(m_0,n_0)$ for $\lexle$,
$(m_0,n_0-1) \notin S$. That is, $\exists j \in \naturals ((m_0,n_0-1),j) \in A$.

Since $(m_0-1,j)$ is less than $(m_0,n_0)$ for $\lexle$,
$(m_0-1,j) \notin S$. That is, $\exists k \in \naturals ((m_0-1,j),k) \in A$.

According to~[\ref{rel2}], since $\exists j,k \in \naturals ((m_0-1,j),k) \in A$ and
$((m_0,n_0-1),j) \in A$, then $((m_0,n_0),k) \in A$, 
which implies $(m_0,n_0) \in \domain{A}$. It leads to a contradiction. 

Therefore, $\domain{A} = \naturals^2$. That is, $A$ is a total relation.

\end{proof}
}

\ppart\label{func} Use the well-ordering principle for $\lexle$ to prove
that $A$ is the graph of a \emph{function}.  \hint Consider the
\emph{least} $(m,n)$ such that $((m,n),x) \in A$ and $((m,n),y) \in A$ and
$x \neq y$, and reach a contradiction.

\solution{
\begin{proof}
This proof is by contradiction. Assume that $A$ is not the graph of a function.
Since we already proved in part~(\ref{relation}) that $\domain{A} = \naturals$, 
which means $\forall m,n \in \naturals \exists x \in \naturals ((m,n),x) \in A$.
If $A$ is not the graph of a function, it means that there exists a nonempty
set $S$ of pairs $(m,n)$ such that $((m,n),x) \in A$ and $((m,n),y) \in A$ and
$x \ne y$. Let's order all pairs $(m,n)$ on $\naturals^2$ in lexicographic order.
By well-ordering principle, there is a least pair $(m_0,n_0) \in S$.

We can show that $m_0 > 0$ and $n_0 > 1$, since according to~[\ref{rel1}]
$((m_0,n_0),2n_0) \in A$ if $m_0 = 0$ or $n_0 \le 1$, which implies a unique value
$2n_0$ is assigned to $(m_0,n_0)$.

Since $(m_0,n_0-1)$ is less than $(m_0,n_0)$ for $\lexle$,
$(m_0,n_0-1) \notin S$. That is, $\exists! j \in \naturals ((m_0,n_0-1),j) \in A$.

Since $(m_0-1,j)$ is less than $(m_0,n_0)$ for $\lexle$,
$(m_0-1,j) \notin S$. That is, $\exists! k \in \naturals ((m_0-1,j),k) \in A$.

According to~[\ref{rel2}], since $\exists! j,k \in \naturals ((m_0-1,j),k) \in A$ and
$((m_0,n_0-1),j) \in A$, then $((m_0,n_0),k) \in A$. Since $k$ has unique value, 
$(m_0,n_0) \notin S$. It leads to a contradiction.

Therefore, $A$ is the graph of a function.

\end{proof}
}

\ppart Use part~(\ref{func}) and the well-ordering principle for $\lexle$ to
prove that $A$ satisfies equations~(\ref{Am0}) and~(\ref{AA}).

\solution{
\begin{proof}
This proof is by contradiction. Assume that A does not satisfy equations~(\ref{Am0})
and~(\ref{AA}). There exists a nonempty set $S'$ of pairs in $\naturals^2 \cross
\naturals$ $((m,n),k)$ such that $((m,n),k) \in A$ but not satisfies equations~(\ref{Am0})
or (\ref{AA}). Let's order all pairs in $S'$ in lexicographic order on $\naturals^2$, 
that is, $(m,n)$. By well-ordering principle, there is a least pair $((m_0,n_0),k_0) \in S$.

We can show that $m_0 > 0$ and $n_0 > 1$, since according to~[\ref{rel1}],
let $k_0 = 2n_0$ such that $((m_0,n_0),k_0) \in A$ and $f(m_0,n_0)=k_0$.

Since $(m_0,n_0-1)$ is less than $(m_0,n_0)$ for $\lexle$,
$((m_0,n_0-1),j) \in A$ and satisfies~(\ref{Am0}) and~(\ref{AA}).

Since $(m_0-1,j)$ is less than $(m_0,n_0)$ for $\lexle$,
$((m_0-1,j),k) \in A$ and satisfies~(\ref{Am0}) and~(\ref{AA}).

According to~(\ref{AA})
\begin{align*}
k & = f(m_0-1,j) \\
  & = f(m_0-1,f(m_0,n_0-1)) \\
  & = f(m_0,n_0)
\end{align*}

According to~[\ref{rel2}] $((m_0,n_0),k) \in A$.

According to part~(\ref{func}), $k = k_0$ and $f(m_0,n_0) = k_0$,
which satisfies~(\ref{AA}). So $((m_0,n_0),k_0) \notin S$. It leads to a contradiction.

Therefore, $A$ satisfies~(\ref{Am0}) and~(\ref{AA}).

\end{proof}
}

\ppart Generalize the way Ackerman's function was defined.  Namely, describe a
format for recursively defining functions on \emph{any} well-founded
partial order that is guaranteed to uniquely define a total function on
the domain of the partial order.  The definition of Ackerman's function
should be a special case of the format you describe.  You need \emph{not}
prove that your format guarantees existence and uniqueness.

\solution{
The generalization is described as follows:

In order to define $f:A \to B$ where $A$ is the domain of a well-founded
partial order, $\preceq$, it is enough to have a rule:
\[
f(a) \eqdef h(\set{(a',f(b)) \suchthat a' \prec a \land b \prec a})
\]
for some total function, $h:\power(A \cross B) \to B$.

In particular, in Ackerman's function
$A = \naturals^2$, $B = \naturals$, and 
$h$ is a total function described by a recursive definition of 
a set $H$ in $\naturals^2 \cross \naturals$:
\begin{enumerate}
\item $((m,n),2n) \in H$ if $m=0$ or $n \le 1$,
\item if $(m-1,j),k) \in H$ and $((m,n-1),j) \in H$, then $((m,n),k)
\in H$, for all $j,k \in \naturals$, when $m > 0$ and $n > 1$.
\end{enumerate}
}

\eparts

\end{problem}

\begin{problem}
Define \emph{simple type expressions} and their \emph{depth} recursively by
\begin{enumerate}
\item \texttt{b} is a simple type expression of depth 0,
\item if $s$ and $t$ are simple type expressions of depths $m$ and $n$,
then $\lp s\tto t \rp$ is a simple type expression of depth $1 + \max(m,n)$.
\end{enumerate}

\emph{Simply typed lambda expressions, (STLs),} and their types are defined
recursively as follows:
\begin{enumerate}

\item A pair consisting of a variable $x$ and a simple type expression,
  $t$, is an STL of type $t$.  The pair of $x$ and $t$ is called a
  \emph{variable of type $t$} and is conventionally written as $x^t$.

\item If $M$ is an STL of type $\lp s\tto t \rp$, and $N$ is an STL of type
     $s$, then $\lp M\ N\rp$ is an STL of type $t$.

\item If $M$ is an STL of type $t$, then $\lp\lam \lp x^s\rp\ M\rp$ is an
  STL of type $\lp s\tto t\rp$.
\end{enumerate}

\begin{example*}
The expression
\begin{quote}
\texttt{(g$^{\texttt{(b\tto b)}}$ x$^{\texttt{b}}$)}
\end{quote}
is an STL of type \texttt{b} and hence
\begin{quote}
\texttt{(f$^{\texttt{(b\tto b)}}$ (g x))}
\end{quote}
is also an STL of type \texttt{b}.  Note that to avoid clutter, we're
omitting the type superscripts on \texttt{g} and \texttt{x} since their
types have already been specified.

Continuing, we have that
\begin{quote}
\texttt{(\lam (x) (f (g x)))}
\end{quote}
is an STL of type \texttt{(b\tto b)}, and so
\begin{quote}
\texttt{(\lam (g) (\lam (x) (f (g x))))}
\end{quote}
is an STL of type $\tau$, where
\[
\tau \eqdef \texttt{((b\tto b)\tto (b\tto b))}.
\]
Now letting
\[
N \eqdef \texttt{(\lam (f) (\lam (g) (\lam (x) (f (g x)))))},
\]
we conclude that $N$ is an STL of type
\begin{quote}
\texttt{((b\tto b)\tto $\tau$)},
\end{quote}
and
\begin{quote}
\texttt{($N$ (\lam (w$^{\texttt{b}}$) w))}
\end{quote}
is an STL of type $\tau$.  Similarly,
\[
M \eqdef \texttt{(\lam (u$^\tau$) (\lam (h$^{\texttt{(b\tto b)}}$) (u (u (u h)))))}
\]
is an STL of type \texttt{($\tau$\tto $\tau$)}.
Finally, letting
\begin{equation}\label{L}
L \eqdef \texttt{(($M$ ($N$ (\lam (w) w))) g)},
\end{equation}
we conclude that $L$ is an STL of type \texttt{b\tto b}.

\end{example*}

Now for any simply typed variable, $v$, and STLs $M$ and $N$, we define
the result of \emph{substituting $N$ for $v$ in $M$}, written,
$\subst{M}{v}{N}$, recursively on the structure of $M$ as follows:
\begin{enumerate}
\item if $M$ is a simply typed variable, then
\[
\subst{M}{v}{N} \eqdef
\begin{cases}
N, & \text{if $M$ is $v$},\\
M, & \text{if $M$ is not identical to $v$.}
\end{cases}
\]

\item
\[
\subst{\lp M_1\ M_2 \rp}{v}{N} \ \eqdef \quad
       \lp \subst{M_1}{v}{N}\ \; \subst{M_2}{v}{N} \rp.
\]

\item
\[
\subst{\lp \lam\ \lp x \rp\ M_1 \rp}{v}{N} \eqdef
\begin{cases}
\lp \lam\ \lp x \rp\ M_1 \rp, & \text{ if }x = v,\\
\lp \lam\ \lp x \rp\ \subst{M_1}{v}{N}\rp, & \text{ if } x \neq v.\\
\end{cases}
\]

\end{enumerate}


There is a standard way to ``simplify'' STLs by carrying out substitutions
specified by the $\beta$-rule:
\begin{equation}\tag{$\beta$}
\lp \lp \lam\ \lp v \rp\ M \rp\ N\rp \longrightarrow \subst{M}{v}{N}
\end{equation}

Notice that if there are several occurrences of $v$ in $M$, then these
occurrences may all be replaced by $N$'s in the righthand side of the
$(\beta)$-rule, so this ``simplification'' rule may result in larger
expressions with more subexpressions to which rule $(\beta)$ applies.

In general, \emph{applying} rule $(\beta)$ to an STL, $L$, means finding a
subexpression, $K$, of $L$ that matches the lefthand side of $(\beta)$,
then replacing $K$ by the corresponding righthand side expression.

\begin{example*}
The ($\beta$)-rule is applicable at two different subexpressions of the
expression $L$ given above in~(\ref{L}). First, the subexpression
\begin{quote}
\texttt{($N$ (\lam (w) w))}
\end{quote}
could be rewritten into
\begin{quote}
\texttt{(\lam (g) (\lam (x) ((\lam (w) w) (g x)))))}.
\end{quote}
In this case, the result of applying ($\beta$) to $L$ would be
\begin{quote}
\texttt{(($M$ (\lam (g) (\lam (x) ((\lam (w) w) (g x))))) g)}.
\end{quote}
Alternatively, the subexpression
\begin{quote}
\texttt{($M$ ($N$ (\lam (w) w)))}
\end{quote}
could be rewritten into
\[\begin{array}{rl}
\texttt{(\lam (h) (}&\!\!\!\!\!\!\texttt{($N$ (\lam (w) w))}\\
            &\!\!\!\texttt{(($N$ (\lam (w) w))}\\
            &\texttt{(($N$ (\lam (w) w)) h))))}.
\end{array}\]
This way of applying ($\beta$) to $L$ would yield $L' \eqdef$
\[\begin{array}{rll}
\lp&\!\!\!\!\!\!\texttt{(\lam (h) (}&\!\!\!\!\!\!\texttt{($N$ (\lam (w) w))}\\
                        &&\!\!\!\texttt{(($N$ (\lam (w) w))}\\
                         &&\texttt{(($N$ (\lam (w) w)) h))))}\\
   &\!\!\!\!\!\!\texttt{ g)}.
\end{array}\]
Notice that $L'$ is larger than $L$ and contains more subexpressions (3
instead of 2) where the ($\beta$)-rule could be applied.

\end{example*}

If $(\beta)$ is not applicable to an expression, $L$, that is, no
subexpression of $L$ matches the lefthand side of $(\beta)$, then $L$ is
said to be \emph{stuck}.  Stuck expressions are also called \emph{normal
forms}.

\begin{claim*}
If we start with any STL, $M$, and continue applying ($\beta$) to a
subexpressions, then we \emph{must} eventually get stuck.
\end{claim*}

We can prove this Claim by defining the \emph{measure}, $\meas{M}$, of an
STL, $M$, to be a natural number vector of length $d$, where $d$ is the
maximum of the depths of the types of all the subexpressions in $M$.  In
particular,
\[
\meas{M} \eqdef (n_d,n_{d-1},\dots,n_1,n_0)
\]
where $n_i$ is the number of subexpressions of $M$ whose type has depth
$i$.

Let $\naturals^*$ be the set of natural number vectors.  Define a total
order on $\naturals^*$ by the rule that $a \prec b$ when $a$ is shorter
than $b$, or when $a$ and $b$ are the same length and $a \lex< b$.

\bparts

\ppart Prove that $\prec$ is a well-order (a well-founded total order) on 
$\naturals^*$.

\solution{TBA}


\ppart Prove that each application of the ($\beta$) rule strictly decreases
the measure of an expression.

\solution{TBA}

\ppart Conclude the Claim.  \solution{The claim now follows because
starting with $M$ the sequence of expressions obtained by each application
of $(\beta$) has a strictly smaller measure than the previous one, and
since $\prec$ is well-founded, any such sequence must be finite.  The last
expression in this finite sequence must be stuck.}

\eparts
\end{problem}


\end{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{problem}
Define planar embeddings, and their faces, for connected graphs
recursively by adding a chord across the infinite face.  Prove some stuff,
eg,

* that anything you build by adding a chord across any face is also planar
* Euler's formula
* the bridges defined by any cycle can be split into those occurring
  inside and those occurring outside, with no clashes among those on the
  same side (refer to Diestel)
\end{problem}


\eparts

Let $\preceq$ be a reflexive partial order.  An infinite sequence $t_1,
t_2, \dots, t_n, \dots$ of elements from the domainX<  of $\preceq$ is called
\emph{good} iff there are positive integers $i,j$ such that $i<j$ and $t_i
\preceq t_j$; otherwise it is called a \emph{bad} sequence.  A reflexive
partial order is called \emph{good} providing there are no bad infinite
sequences of elements from its domain.

\bparts

\ppart\label{g->w} Prove that a good partial order is a well-quasi-order.
\hint Observe that a good partial order must be well-founded.  Then suppose
there was a subset of the domain with infinitely many minimal elements
$t_1,t_2,\dots,t_n,\dots$.

\solution{Suppose $\preceq$ was a good partial order.  If it is not also
well-founded, we know from Week 5 Notes that it has an infinite decreasing
chain.  But such a chain is a bad sequence, contradicting the goodness of
$\preceq$.

To prove that $\preceq$ is a well-quasi-order, we now need only show that
every nonempty subset of the domain contains only finitely many minimal
elements.  So suppose to the contrary that some subset of the domain has
infinitely many minimal elements $m_1,m_2,\dots$.  In particular, these
minimal elements must be an antichain.  But then any sequence of all these
minimal elements is a bad sequence, contradicting the goodness of
$\preceq$.}

\ppart\label{w->g} Prove conversely, that every reflexive well-quasi-order
is good.

\solution{ Let $\preceq$ be a reflexive well-quasi-order, and let $t_1,
t_2, \dots, t_n, \dots$ be an infinite sequence of elements from its
domain.  We want to show that this sequence is good.

Let $T \eqdef \set{t_i \suchthat i \ge 1}$.  Since $\preceq$ is a
well-quasi-order, $T$ has only finitely many minimal elements.  We now
consider two cases:
\begin{enumerate}

\item Some minimal element, $m$, occurs more than once, say at positions
$i$ and $j>i$.  Then these $i,j$ show that the sequence is good, because
$t_i = m \preceq m = t_j$,

\item No minimal element occurs more than once.  Then there must be a last
occurrence of a minimal element, that is, a positive integer, $n$, such
that if $t_i$ is minimal then $i \leq n$.  So let $j = n+1$.  Then $t_j$
is not minimal, so by part~(\ref{abovem}), there must be a minimal element
$t_i$ with $i \le n < j$ such that $t_i \prec t_j$.  So these $i,j$ show
that the sequence is good.
\end{enumerate}
}



\iffalse

The \emph{size} of a tree is the number of nodes in it (including leaf
nodes).

\bparts
              
\ppart   Give a recursive definition of $\sz(T)$ for $T \in \ROT$.

\eparts
\solution{

\begin{eqnarray*}
\sz(\nil)            & \eqdef & 1,\\
\sz((T_1,\dots,T_n)) & \eqdef & 1 + \sum_{i=1}^n \sz(T_i).
\end{eqnarray*}
}

\eparts

We define $brep$ to
be the function that maps any rooted, ordered tree to its representation as
a full binary tree.  Conversely, the function $unrep$ maps any full binary
tree to the rooted tree in $\ROT$ that it represents.

To give the mathematical definitions of $brep!$ and $unrep$, we first
define the \emph{\cons} function on tuples as follows:
\begin{eqnarray*}
\cons(t,\nil) &\eqdef & (t),\\
\cons(t_0,(t_1,\dots,t_n)) & \eqdef & (t_0,t_1,\dots,t_n),
\end{eqnarray*}
for $n \geq 1$.

\bparts

\ppart  Prove that
\[
sz(\cons(T_1,T_2)) = sz(T_1) + sz(T_2).
\]
for all $T_1,T_2 \in \ROT$.

\solution{There are two cases:
\begin{enumerate}

\item If $T_2 = \nil$, then
\[
\begin{array}{rclr}
sz(\cons(T_1,\nil)) & = & sz((T_1)) & \mbox{by def of \cons}\\
   & = & 1 + sz(T_1) & \mbox{by 2nd clause of def of sz}\\
   & = & sz(\nil) + sz(T_1) & \mbox{by 1st clause of def of sz}\\
   & = & sz(T_1) + sz(T_2).
\end{array}
\]

\item: Otherwise $T_2 = (T_3,T_4)$ for some $T_3,T_4 \in \ROT$, and
\[
\begin{array}{rclr}
sz(\cons(T_1,(T_3,T_4))) & = & sz((T_1,T_3,T_4)) & \mbox{by def of \cons}\\
   & = & 1 + sz(T_1) + sz(T_3) + sz(T_4) & \mbox{by 2nd clause of def of sz}\\
   & = & sz(T_1) + (1+ sz(T_3) + sz(T_4))\\
   & = & sz(T_1) + sz((T_3,T_4))  & \mbox{by 1st clause of def of sz}\\
   & = & sz(T_1) + sz(T_2).
\end{array}
\]

\end{enumerate}

Notice that there was no need for induction in the proof.

}

\eparts
\fi
