Differences

This shows you the differences between two versions of the page.

--- fuss:lambda_calculus [2016/11/22 04:28] – [Exponentiation with Church Numerals] office
+++ fuss:lambda_calculus [2022/08/01 05:20] (current) – [η-Reduction and η-Expansion] office
@@ Line 1: / Line 1: @@
+====== Implementing the Y-Combinator ======
+Curry defines the $Y$-combinator as:
+\begin{eqnarray*}
+Y &=& \lambda f .(\lambda x.f(xx))(\lambda x.f(xx))
+\end{eqnarray*}
+which, when applied to a lambda term $g$, $\beta$-reduces in two steps to:
+\begin{eqnarray*}
+Y g &=& g (Y g)
+\end{eqnarray*}
+An equivalent $Y$-combinator definition is the following:
+\begin{eqnarray*}
+Y &=& \lambda f.(\lambda x.xx)(\lambda x.f(xx))
+\end{eqnarray*}
+which consists of part of the $\Omega$ combinator $\Omega = (\lambda x.xx)(\lambda x.xx)$ named $\omega = \lambda x.xx$ and the term $\lambda x.f(xx)$.
+If we $\beta$-reduce the equivalent form once:
+\begin{eqnarray*}
+Y &=& \lambda f.(\lambda x.xx)(\lambda x.f(xx))
+\end{eqnarray*}
+we would obtain Curry's form of the $Y$-combinator.
+Whilst the Curry form should work perfectly fine in Scheme and untyped lambda calculus, a statically typed language will not accept a function application such as $x x$ since the type system will forbid it. In order to do that, we start by applying an additional $\eta$-abstraction to obtain the form:
+\begin{eqnarray*}
+Y &=& \lambda f.(\lambda x.xx)(\lambda x.(f (\lambda y.((x x) y))))
+\end{eqnarray*}
+which can be re-written as:
+\begin{eqnarray*}
+Y &=& \lambda f.(\lambda x.xx)(f (\lambda y.((\lambda x.xx) y)))
+\end{eqnarray*}
+We notice that the $\omega$ combinator ($\lambda x.xx$) appears twice in the resulting $Y$-combinator which lets us express the $Y$-combinator using the $\omega$ combinator:
+\begin{eqnarray*}
+\omega &=& \lambda x.xx \\
+Y' &=& \lambda f.\omega(f (\lambda y.\omega y))
+\end{eqnarray*}
+where $Y'$ and $Y$ are $\beta$-equivalent.
+Expressing the $Y$ combinator in terms of $\omega$ allows us to implement the $Y$ combinator in statically typed programming languages.
+===== Implementations =====
+  * [[fuss/python#Y-combinator|Python]]
+  * [[fuss/php#Y-combinator|PHP]]
+====== Exponentiation with Church Numerals ======
+You may have seen the definition of exponentiation as the combinator $\mathbbold{EXP}$ (or $\mathbbold{POW}$) given by the lambda abstraction:
+\begin{eqnarray*}
+\mathbbold{EXP} &\equiv& \lambda m.\lambda n.mn
+\end{eqnarray*}
+where $n$ and $m$ are both Church numerals. $\mathbbold{EXP}$ will perform the mathematical equivalent of $m^{n}$ using Church numerals.
+Therefore the application of a Church numeral $n$ to another Church numeral $\mathbbold{m}$ will yield the Church numeral equivalent to $m^n$. For instance, applying the Church numeral $\mathbbold{1}$ to Church numeral $\mathbbold{2}$ should yield $m^{n} = 2^{1} \equiv \mathbbold{2}$. While all the numerals work out, the application of the Church numeral zero to any other Church numeral $\beta$-reduces to the identity function $\mathbbold{I}$. For instance, applying the Church numeral $\mathbbold{0}$ to $\mathbbold{2}$ we have:
+\begin{eqnarray*}
+\mathbbold{0}(\mathbbold{2}) &\equiv& (\lambda f.\lambda x.x)(\lambda f.\lambda x.f(f(x))) \\
+&\xrightarrow{\beta-reduce: \lambda f}& \lambda x.x \\
+&\equiv& \mathbbold{I}
+\end{eqnarray*}
+Since the identity function $\mathbbold{I}$ is not a Church numeral, it would seem that the application is not defined. However, by the rules of exponentiation, any number to the power zero should yield one; in other words: $2^{0} = 1$.
+The trick here is that the identity function $\mathbbold{I}$ is equivalent with the Church numeral $\mathbbold{I}$ under the $\eta$-expansion.
+The $\eta$-expansion is given by:
+\begin{eqnarray*}
+f &\xrightarrow{\eta-expand: f}& \lambda x.f(x)
+\end{eqnarray*}
+so we can re-work the application of the Church numeral zero to the Church numeral two:
+\begin{eqnarray*}
+\mathbbold{0}(\mathbbold{2}) &\equiv& (\lambda f.\lambda x.x)(\lambda f.\lambda x.f(f(x))) \\
+&\xrightarrow{\beta-reduce: \lambda f}& \lambda x.x \\
+&\xrightarrow{\alpha-convert: x \mapsto f}& \lambda f.f \\
+&\xrightarrow{\eta-expand: f \mapsto \lambda x.f(x)}& \lambda f.\lambda x.f(x) \\
+&\equiv& \mathbbold{1}
+\end{eqnarray*}
+which yields the expected result.
+====== η-Reduction and η-Expansion ======
+$\eta$-reduction is given by:
+\begin{eqnarray*}
+\lambda x.f(x) &\xrightarrow{\eta-reduce: \lambda x.f(x)}& f
+\end{eqnarray*}
+$\eta$-expansion is given by:
+\begin{eqnarray*}
+f &\xrightarrow{\eta-expand: f}& \lambda x.f(x)
+\end{eqnarray*}
+====== Aggregators ======
+{{indexmenu>/fuss/lambda_calculus/functional_programming/aggreagators}}