Fixpoint expansion by -reduction

Next: Using the Y-Combinator to Up: Basic Usage of Y-Combinator Previous: Generation of fixpoint using Contents Start

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

Georg P. Loczewski 2004-03-05

Impressum und Datenschutz