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:
{\sc Rule 13 (fixpoint expansion)}
...em} M) \underset{\beta}{\rightarrow} (M (Y\hspace{0.25em} M))$
\end{center} }
Verification of the expansion formula:
{\sc Proof 1 (fixpoint expansion )}
...arrow_\beta (M (Y\hspace{0.25em} M)).
\end{split}\end{equation}\end{center} }

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