Lambda calculus

The Church–Rosser Property

content/lambda-calculus/church-rosser/church-rosser.tex

% Part: lambda-calculus% Chapter: church-rosser\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{lam}{cr}{The Church--Rosser Property}\olimport{definitions-and-properties}\olimport{parallel-beta-reduction}\olimport{beta-reduction}\olimport{parallel-beta-eta-reduction}\olimport{beta-eta-reduction}\OLEndChapterHook\end{document}

content/lambda-calculus/church-rosser/definitions-and-properties.tex

% Part: lambda-calculus% Chapter: church-rosser% Section: definitions-and-properties\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{cr}{dap}\olsection{Definition and Properties}In this chapter we introduce the concept of Church--Rosser property andsome common properties of this property.\begin{defn}[Church--Rosser property, CR] A relation $\xredone$ on  terms is said to satisfy the \emph{Church--Rosser property} iff,  whenever $M \xredone P$ and $M \xredone Q$, then there exists  some~$N$ such that $P \xredone N$ and $Q \xredone N$.\end{defn}We can view the lambda calculus as a model of computation in whichterms in normal form are ``values'' and a reducibility relation onterms are the ``calculation rules.'' The Church--Rosser property statesis that when there is more than one way to proceed with a calculation,there is still only a single value of the expression.To take an example from elementary algebra, there's more than one wayto calculate $4 \times (1+2) + 3$. It can either be reduced to $4\times 3+3$ (if we first reduce $1+2$ to~$3$) or to $4 \times 1+4\times 2+3$ (if we first reduce $4 \times (1+2)$ usingdistributivity). Both of these, however, can be further reduced to$12+3$.If we take $\xredone$ to be $\beta$-reduction, we easily see that aconsequence of the Church--Rosser property is that if a term has anormal form, then it is unique. For suppose $M$ can be reduced to $P$and $Q$, both of which are normal forms. By the Church--Rosser property,there exists some $N$ such that both $P$ and $Q$ reduce to it. Sinceby assumption $P$ and $Q$ are normal forms, the reduction of $P$ and$Q$ to $N$ can only be the trivial reduction, i.e., $P$, $Q$, and $N$are identical. This justifies our speaking of \emph{the} normal formof a term.In viewing the lambda calculus as a model of computation, then, thenormal form of a term can be thought of as the ``final result'' of thecomputation starting with that term. The above corollary means there'sonly one, if any, final result of a computation, just like there isonly one result of computing $4 \times (1+2)+3$, namely~$15$.\begin{thm} \ollabel{thm:str}  If a relation $\xredone$ satisfies the Church--Rosser property, and $\xred$ is the  smallest transitive relation containing $\xredone$, then $\xred$ satisfies  the Church--Rosser property too.\end{thm}\begin{proof}  Suppose   \begin{align*}    M & \xredone P_1 \xredone \dots \xredone P_m \text{ and}\\    M & \xredone Q_1 \xredone \dots \xredone Q_n.  \end{align*}  We will prove the theorem by constructing a grid $N$ of terms of  height is $m + 1$ and width $n + 1$. We use $N_{i,j}$ to denote the  term in the $i$-th row and $j$-th column.    We construct $N$ in such a way that $N_{i,j} \xredone N_{i+1,j}$ and  $N_{i,j} \xredone N_{i,j+1}$. It is defined as follows:  \begin{align*}    N_{0,0} &= M \\    N_{i,0} &= P_i && \text{if } 1 \le i \le m \\    N_{0,j} &= Q_j && \text{if } 1 \le j \le n \\  \intertext{and otherwise:}    N_{i,j} &= R  \end{align*}  where $R$ is a term such that $N_{i-1,j} \xredone R$ and $N_{i,j-1}  \xredone R$. By the Church--Rosser property of $\xredone$, such a  term always exists.  Now we have $N_{m,0} \xredone \dots \xredone N_{m,n}$ and $N_{0,n}  \xredone \dots \xredone N_{m,n}$. Note $N_{m,0}$ is $P$ and $N_{0,n}$  is $Q$. By definition of $\xred$ the theorem follows.\end{proof}\end{document}

content/lambda-calculus/church-rosser/parallel-beta-reduction.tex

% Part: lambda-calculus% Chapter: church-rosser% Section: parallel-beta-reduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{cr}{pb}\olsection{Parallel $\beta$-reduction}We introduce the notion of \emph{parallel $\beta$-reduction}, andprove the it has the Church--Rosser property.\begin{defn}[parallel $\beta$-reduction, $\bredpar$] \ollabel{defn:bredpar}  Parallel reduction ($\bredpar$) of terms is inductively defined as follows:  \begin{enumerate}    \item \ollabel{defn:bredpar1} $x \bredpar x$.    \item \ollabel{defn:bredpar2} If $N \xrightarrow{\beta} N'$ then $\lambd[x][N] \bredpar      \lambd[x][N']$.    \item \ollabel{defn:bredpar3} If $P \bredpar P'$ and $Q \bredpar Q'$ then $PQ \bredpar      P'Q'$.    \item \ollabel{defn:bredpar4} If $N \bredpar N'$ and $Q \bredpar Q'$ then      $(\lambd[x][N])Q \bredpar \Subst{N'}{Q'}{x}$.  \end{enumerate}\end{defn}Parallel $\beta$-reduction allows us to reduce any number of redices in aterm in one step. It is different from $\beta$-reduction in the sense that wecan only contract redices that occur in the original term, but not redicesarising from parallel $\beta$-reduction. For example, the term$(\lambd[f][fx])(\lambd[y][y])$ can only be parallel $\beta$-reducedto itself or to $(\lambd[y][y])x$, but not further to~$x$, although it$\beta$-reduces to~$x$, because this redex arises only after one step of parallel $\beta$-reduction. A second parallel $\beta$-reductionstep yields~$x$, though.\begin{thm}\ollabel{thm:refl}  $M \bredpar M$.\end{thm}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[lam][cr][pb]{thm:refl}.\end{prob}\begin{defn}[$\beta$-complete development]\ollabel{defn:bcd}  The \emph{$\beta$-complete development}~$\bcd{M}$ of $M$ is defined  inductively as follows:  \begin{align}    \bcd{x} &= x \ollabel{defn:bcd1} \\    \bcd{(\lambd[x][N])} &= \lambd[x][\bcd{N}] \ollabel{defn:bcd2}\\    \bcd{(PQ)} &= \bcd{P}\bcd{Q} && \text{if $P$ is not a $\lambd$-abstract}     \ollabel{defn:bcd3} \\    \bcd{((\lambd[x][N])Q)} &= \Subst{\bcd{N}}{\bcd{Q}}{x} \ollabel{defn:bcd4}  \end{align}\end{defn}The $\beta$-complete development of a term, as its name suggests, is a``complete parallel reduction.'' While for parallel $\beta$-reduction we stillcan choose to not contract a redex, for complete development we haveno choice but to contract all of them. Thus the complete developmentof $(\lambd[f][fx])(\lambd[y][y])$ is $(\lambd[y][y])x$, not itself.\begin{editorial}  This definition has the problem that we haven't introduced how to  define functions on ($\lambd$-)terms recursively. Will fix in future.\end{editorial}\begin{lem}\ollabel{lem:comp}  If $M \bredpar M'$ and $R \bredpar R'$, then $\Subst{M}{R}{y}  \bredpar \Subst{M'}{R'}{y}$.\end{lem}\begin{proof}  By induction on the !!{derivation} of $M \bredpar M'$.  \begin{enumerate}    \item The last step is \olref{defn:bredpar1}: Exercise.    \item The last step is \olref{defn:bredpar2}: Then $M$ is       $\lambd[x][N]$ and $M'$ is $\lambd[x][N']$,      where $N \bredpar N'$. We want to prove that      $\Subst{(\lambd[x][N])}{R}{y} \bredpar      \Subst{(\lambd[x][N'])}{R'}{y}$, i.e.,      $\lambd[x][\Subst{N}{R}{y}] \bredpar      \lambd[x][\Subst{N'}{R}{y}]$. This follows immediately by      \olref{defn:bredpar2} and the induction hypothesis.    \item The last step is \olref{defn:bredpar3}: Exercise.    \item The last step is \olref{defn:bredpar4}: $M$ is      $(\lambd[x][N])Q$ and $M'$ is $\Subst{N'}{Q'}{x}$. We want to      prove that $\Subst{((\lambd[x][N])Q)}{R}{y} \bredpar      \Subst{\Subst{N'}{Q'}{x}}{R'}{y}$, i.e.,      $(\lambd[x][\Subst{N}{R}{y}])\Subst{Q}{R}{y} \bredpar      \Subst{\Subst{N'}{R'}{y}}{\Subst{Q'}{R'}{y}}{x}$. This follows      by \olref{defn:bredpar4} and the induction hypothesis.  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][cr][pb]{lem:comp}.\end{prob}\begin{lem}\ollabel{lem:cont}  If $M \bredpar M'$ then $M' \bredpar \bcd{M}$.\end{lem}\begin{proof}  By induction on the !!{derivation} of $M \bredpar M'$.  \begin{enumerate}    \item The last rule is \olref{defn:bredpar1}: Exercise.    \item The last rule is \olref{defn:bredpar2}: $M$ is       $\lambd[x][N]$ and $M'$ is $\lambd[x][N']$ with      $N \bredpar N'$. We want to show that $\lambd[x][N'] \bredpar      \bcd{(\lambd[x][N])}$, i.e., $\lambd[x][N'] \bredpar      \lambd[x][\bcd{N}]$ by \olref{defn:bcd2}. It follows by      \olref{defn:bredpar2} and the induction hypothesis.    \item The last rule is \olref{defn:bredpar3}:$M$ is $PQ$ and $M'$      is $P'Q'$ for some $P$, $Q$, $P'$ and $Q'$, with $P \bredpar P'$      and $Q \bredpar Q'$. By induction hypothesis, we have $P'      \bredpar \bcd{P}$ and $Q' \bredpar \bcd{Q}$.      \begin{enumerate}        \item If $P$ is $\lambd[x][N]$ for some $x$ and $N$, then          $P'$ must be $\lambd[x][N']$ for some $N'$ with           $N \bredpar N'$. By induction hypothesis we have $N' \bredpar \bcd{N}$ and          $Q' \bredpar \bcd{Q}$. Then $(\lambd[x][N'])Q' \bredpar          \Subst{\bcd{N}}{\bcd{Q}}{x}$ by \olref{defn:bredpar4}.        \item If $P$ is not a $\lambd$-abstract, then $P'Q' \bredpar          \bcd{P}\bcd{Q}$ by \olref{defn:bredpar3}, and the right-hand          side is $\bcd{PQ}$ by \olref{defn:bcd3}.      \end{enumerate}    \item The last rule is \olref{defn:bredpar4}: $M$ is      $(\lambd[x][N])Q$  and $M'$ is $\Subst{N'}{Q'}{x}$ for some $x$,      $N$, $Q$, $N'$, and~$Q'$, with $N \bredpar N'$ and $Q \bredpar      Q'$. By induction hypothesis we know $N' \bredpar \bcd{N}$ and      $Q' \bredpar \bcd{Q}$. By \olref{lem:comp} we have      $\Subst{N'}{Q'}{x} \bredpar \Subst{\bcd{N}}{\bcd{Q}}{x}$, the      right-hand side of which is exactly $\bcd{((\lambd[x][N])Q)}$.  \end{enumerate}\end{proof}\begin{prob}  Complete the proof of \olref[lam][cr][pb]{lem:cont}.\end{prob}\begin{thm}\ollabel{thm:cr}  $\bredpar$ has the Church--Rosser property.\end{thm}\begin{proof}  Immediate from \olref{lem:cont}.\end{proof}\end{document}

content/lambda-calculus/church-rosser/beta-reduction.tex

% Part: lambda-calculus% Chapter: church-rosser% Section: beta-reduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{cr}{b}\olsection{$\beta$-reduction}\begin{lem}\ollabel{lem:one-par}  If $M \bredone M'$, then $M \bredpar M'$.\end{lem}\begin{proof} If $M \bredone M'$, then $M$ is    $(\lambd[x][N])Q$, $M'$ is $\Subst{N}{Q}{x}$, for some    $x$, $N$, and~$Q$. Since $N \bredpar N$ and $Q \bredpar Q$ by    \olref[pb]{thm:refl}, we immediately have $(\lambd[x][N])Q    \bredpar \Subst{N}{Q}{x}$ by \olref[pb]{defn:bredpar}\olref[pb]{defn:bredpar4}.\end{proof}\begin{lem}\ollabel{lem:par-red}  If $M \bredpar M'$, then $M \bred M'$.\end{lem}\begin{proof} By induction on the !!{derivation} of $M \bredpar M'$.  \begin{enumerate}  \item The last rule is \olref[pb]{defn:bredpar1}: Then $M$ and $M'$    are just $x$, and $x \bred x$.  \item The last rule is \olref[pb]{defn:bredpar2}: $M$ is     $\lambd[x][N]$ and $M'$ is $\lambd[x][N']$ for some $x$, $N$, $N'$, where    $N \bredpar N'$. By induction hypothesis we have $N \bred N'$. Then    $\lambd[x][N] \bred \lambd[x][N']$ (by the same series of    $\bredone$ contractions as $N \bred N'$).  \item The last rule is \olref[pb]{defn:bredpar3}: $M$ is     $PQ$ and $M'$ is $P'Q'$ for some $P$, $Q$, $P'$, $Q'$, where $P \bredpar P'$    and $Q \bredpar Q'$. By induction hypothesis we have $P \bred P'$ and $Q \bred    Q'$.  So $PQ \bred P'Q'$ by the reduction sequence $P \bred P'$ followed    by the reduction $Q \bred Q'$.  \item The last rule is \olref[pb]{defn:bredpar4}: $M$ is    $(\lambd[x][N])Q$ and $M'$ is  $\Subst{N'}{Q'}{x}$ for some $x$,    $N$, $M'$, $Q$, $Q'$, where $N \bredpar N'$ and $Q \bredpar Q'$.    By induction hypothesis we get $Q \bred Q'$ and $N \bred N'$. So    $(\lambd[x][N])Q \bred \Subst{N'}{Q'}{x}$ by $N \bred N'$ followed    by $Q \bred Q'$ and finally contraction of $(\lambd[x][N'])Q'$ to    $\Subst{N'}{Q'}{x}$.  \end{enumerate}\end{proof}\begin{lem}\ollabel{lem:str}  $\bred$ is the smallest transitive relation containing $\bredpar$.\end{lem}\begin{proof}  Let $\xred$ be the smallest transitive relation containing  $\bredpar$.  $\bred \subseteq \xred$: Suppose $M \bred M'$, i.e., $M \ident M_1  \bredone \dots \bredone M_k \ident M'$. By \olref{lem:one-par}, $M  \ident M_1 \bredpar \dots \bredpar M_k \ident M'$. Since is $\xred$  contains $\bredpar$ and is transitive, $M \xred M'$.  $\xred \subseteq \bred$: Suppose $M \xred M'$, i.e., $M  \ident M_1 \bredpar \dots \bredpar M_k \ident M'$. By \olref{lem:par-red}, $M \ident M_1  \bred \dots \bred M_k \ident M'$. Since $\bred$ is transitive, $M  \bred M'$.\end{proof}\begin{thm}\ollabel{thm:cr}  $\bred$ satisfies the Church--Rosser property.\end{thm}\begin{proof}  Immediate from \olref[dap]{thm:str}, \olref[pb]{thm:cr}, and \olref{lem:str}.\end{proof}\end{document}

content/lambda-calculus/church-rosser/parallel-beta-eta-reduction.tex

% Part: lambda-calculus% Chapter: church-rosser% Section: parallel-beta-eta-reduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{cr}{pbe}\olsection{Parallel $\beta\eta$-reduction}In this section we prove the Church-Rosser property for parallel$\beta\eta$-reduction, the parallel reduction notion corresponding to$\beta\eta$-reduction. \begin{defn}[Parallel $\beta\eta$-reduction, $\beredpar$] \ollabel{defn:beredpar}  \emph{Parallel $\beta\eta$-reduction} ($\beredpar$) on terms is  inductively defined as follows:  \begin{enumerate}    \item \ollabel{defn:beredpar1} $x \beredpar x$.    \item \ollabel{defn:beredpar2} If $N \xrightarrow{\beta} N'$ then $\lambd[x][N] \beredpar      \lambd[x][N']$.    \item \ollabel{defn:beredpar3} If $P \beredpar P'$ and $Q \beredpar Q'$ then $PQ \beredpar      P'Q'$.    \item \ollabel{defn:beredpar4} If $N \beredpar N'$ and $Q \beredpar Q'$ then      $(\lambd[x][N])Q \beredpar \Subst{N'}{Q'}{x}$.    \item \ollabel{defn:beredpar5} If $N \beredpar N'$ then $\lambd[x][Nx]      \beredpar N'$, provided $x \notin FV(N)$.  \end{enumerate}\end{defn}\begin{thm}\ollabel{thm:refl}  $M \beredpar M$.\end{thm}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[lam][cr][pbe]{thm:refl}.\end{prob}\begin{defn}[$\beta\eta$-complete development]\ollabel{defn:becd}  The \emph{$\beta\eta$-complete development}~$\becd{M}$ of~$M$ is defined  as follows:  \begin{align}    \becd{x} &= x \ollabel{defn:becd1} \\    \becd{(\lambd[x][N])} &= \lambd[x][\becd{N}] \ollabel{defn:becd2}\\    \becd{(PQ)} &= \becd{P}\becd{Q} && \text{if $P$ is not a $\lambd$-abstract}     \ollabel{defn:becd3} \\    \becd{((\lambd[x][N])Q)} &= \Subst{\becd{N}}{\becd{Q}}{x}                             \ollabel{defn:becd4} \\    \becd{(\lambd[x][Nx])} &= \becd{N} \ollabel{defn:becd5} & \text{if $x                                                      \notin FV(N)$}  \end{align}\end{defn}\begin{lem}\ollabel{lem:comp}  If $M \beredpar M'$ and $R \beredpar R'$, then $\Subst{M}{R}{y}  \beredpar \Subst{M'}{R'}{y}$.\end{lem}\begin{proof}  By induction on the !!{derivation} of $M \beredpar M'$.  The first four cases are exactly like those in \olref[pb]{lem:comp}.  If the last rule is \olref{defn:beredpar5}, then $M$ is  $\lambd[x][Nx]$, $M'$ is $N'$ for some $x$ and~$N'$ where $x \notin  FV(N)$, and $N \beredpar N'$. We want to show that  $\Subst{(\lambd[x][Nx])}{R}{y} \beredpar \Subst{N'}{R'}{y}$, i.e.,  $\lambd[x][\Subst{N}{R}{y} x] \beredpar \Subst{N'}{R'}{y}$. It  follows by \olref{defn:beredpar}\olref{defn:beredpar5} and the  induction hypothesis.\end{proof}\begin{lem}\ollabel{lem:cont}  If $M \beredpar M'$ then $M' \beredpar \becd{M}$.\end{lem}\begin{proof}  By induction on the !!{derivation} of $M \beredpar M'$.  The first four cases are like those in \olref[pb]{lem:cont}. If the  last rule is \olref{defn:beredpar5}, then $M$ is $\lambd[x][Nx]$ and  $M'$ is $N'$ for some $x$, $N$, $N'$ where $x \notin FV(N)$ and $N  \beredpar N'$. We want to show that $N' \beredpar  \becd{(\lambd[x][Nx])}$, i.e., $N' \beredpar \becd{N}$, which is  immediate by induction hypothesis.\end{proof}\begin{thm}\ollabel{thm:cr}  $\beredpar$ has the Church-Rosser property.\end{thm}\begin{proof}  Immediate from \olref{lem:cont}.\end{proof}\end{document}

content/lambda-calculus/church-rosser/beta-eta-reduction.tex

% Part: lambda-calculus% Chapter: church-rosser% Section: beta-eta-reduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{lam}{cr}{be}\olsection{$\beta\eta$-reduction}The Church--Rosser property holds for$\beta\eta$-reduction ($\bered$).\begin{lem}\ollabel{lem:one-par}  If $M \beredone M'$, then $M \beredpar M'$.\end{lem}\begin{proof}   By induction on the !!{derivation} of $M \beredone M'$. If $M \bredone  M'$ by $\eta$-conversion (i.e., \olref[syn][eta]{defn:beredone}), we  use \olref[pbe]{thm:refl}. The other cases are as in  \olref[b]{lem:one-par}.\end{proof}\begin{lem}\ollabel{lem:par-red}  If $M \beredpar M'$, then $M \bered M'$.\end{lem}\begin{proof} Induction on the !!{derivation} of $M \beredpar M'$.  If the last rule is \olref[pbe]{defn:beredpar5}, then $M$ is  $\lambd[x][Nx]$ and $M'$ is $N'$ for some $x$, $N$, $N'$ where $x  \notin FV(N)$ and $N \beredpar N'$. Thus we can first reduce  $\lambd[x][Nx]$ to $N$ by $\eta$-conversion, followed  by the series of $\beredone$ steps that show that $N \bered N'$,  which  holds by induction hypothesis.\end{proof}\begin{lem}\ollabel{lem:str}  $\bered$ is the smallest transitive relation containing $\beredpar$.\end{lem}\begin{proof}  As in \olref[b]{lem:str}\end{proof}\begin{thm}\ollabel{thm:cr}  $\bered$ satisfies Church--Rosser property.\end{thm}\begin{proof}  By \olref[dap]{thm:str}, \olref[pbe]{thm:cr} and \olref{lem:str}.\end{proof}\end{document}