\documentclass{report} 
\begin{document}
\begin{center}
        {\bf CS 319---The Lambda Calculus}\\
        {\bf Assignment 2 Winter 2000}\\
        Due Monday, 31 January\\
\end{center}
\begin{enumerate}
        \item Show how the Turing fixpoint term $Y_T$ can be used for
                mutually recursive functions.  That is, given
                $\lambda$ terms $\alpha_1\ldots,\alpha_m$, where each $\alpha_i$ involves the
                variables $x_1,\ldots,x_m$ and $y_1,\ldots,y_{p_i}$, construct
                terms $S_1,\ldots,S_m$ such that
                $$S_1 y_1\cdots y_{p_1}\rightarrow_\beta
                        {[}S_1/x_1,\ldots,S_m/x_m{]}\alpha_1$$
                $$S_2 y_1\cdots y_{p_2}\rightarrow_\beta
                        {[}S_1/x_1,\ldots,S_m/x_m{]}\alpha_2$$
                $$\vdots$$
                $$S_m y_1\cdots y_{p_m}\rightarrow_\beta \alpha_m
                        {[}S_1/x_1,\ldots,S_m/x_m{]}\alpha_m$$
        \item Generalize the method above to allow definitions analogous to
                $$\mathord{\mbox\it car}(\mathord{\mbox\it cons}(x,y))=x$$
                $$\mathord{\mbox\it cdr}(\mathord{\mbox\it cons}(x,y))=y$$
                which defines $\mathord{\mbox\it car}$,
                $\mathord{\mbox\it cdr}$, and $\mathord{\mbox\it cons}$ by
                a more general sort of mutual recursion.
        \item Generalize the solution methods above as much as you can.  For
                example, certain infinite systems are solvable.

                
        \item Define $\alpha\beta^{\sim n}$ by
                $\alpha\beta^{\sim 0}=\alpha$, $\alpha\beta^{\sim
                  n+1}\equiv(\alpha\beta^{\sim n}\beta)$.  Define an
                alternate encoding of the integers by
                $\tilde{i}=\lambda x,y.xy^{\sim i}$.  Prove that
                the $\tilde{i}$                 encoding is equivalent
                to Church's $\bar{i}$ encoding by exhibiting two
                translating terms, $A$ and $B$, such that for all $i$,
                $A\bar{i}\rightarrow_\beta \tilde{i}$ and
                $B\tilde{i}\rightarrow_\beta \bar{i}$.
\end{enumerate}
\end{document}