CS 319--The Lambda Calculus
Assignment 2 Winter 2000
Due Monday, 31 January

1. 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 \alpha_1{[}S_1/x_1,\ldots,S_m/x_m{]}$$
   
   
   
   
   $$S_2 y_1\cdots y_{p_2}\rightarrow_\beta \alpha_2{[}S_1/x_1,\ldots,S_m/x_m{]}$$
   
   
   
   
   $$\vdots$$
   
   
   
   
   $$S_m y_1\cdots y_{p_m}\rightarrow_\beta \alpha_m {[}S_1/x_1,\ldots,S_m/x_m{]}$$
   
   

2. 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.
3. Generalize the solution methods above as much as you can. For example, certain infinite systems are solvable.

4. 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}$.