next up previous contents index
Next: Using the Y-Combinator to Up: Basic Usage of Y-Combinator Previous: Generation of fixpoint using   Contents   Index

Fixpoint expansion by $ _\beta $-reduction

It looks like magic that expansion can be obtained by reduction as well as by abstraction. The first of these alternatives is shown below:
\fbox{
\parbox{12.5cm}{
{\sc Rule 13 (fixpoint expansion)}
\begin{center}$(Y\h...
...em} M) \underset{\beta}{\rightarrow} (M (Y\hspace{0.25em} M))$
\end{center} }
}
Verification of the expansion formula:
\fbox{
\parbox{12.5cm}{
{\sc Proof 1 (fixpoint expansion )}
\begin{center}\beg...
...arrow_\beta (M (Y\hspace{0.25em} M)).
\end{split}\end{equation}\end{center} }
}



domain access counter Georg P. Loczewski 2004-03-05