# Differences

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

 fuss:lambda_calculus [2016/11/21 18:58]office [Exponentiation with Church Numerals] fuss:lambda_calculus [2017/02/22 18:30] (current) Both sides previous revision Previous revision 2016/11/22 04:28 office [Exponentiation with Church Numerals] 2016/11/21 18:58 office [Exponentiation with Church Numerals] 2016/11/21 18:43 office [Exponentiation with Church Numerals] 2016/11/21 15:53 office 2016/10/22 00:14 office [Implementing the Y-Combinator] 2016/10/22 00:09 office [Implementing the Y-Combinator] 2016/10/22 00:08 office [Implementing the Y-Combinator] 2016/10/22 00:06 office 2016/10/22 00:04 office [Implementing the Y-Combinator] 2016/10/21 23:55 office [Implementing the Y-Combinator] 2016/10/21 23:51 office [Implementations] 2016/10/21 23:51 office [Implementing the Y-Combinator] 2016/10/21 23:47 office created2016/10/21 21:21 office removed2016/10/21 21:21 office created Next revision Previous revision 2016/11/22 04:28 office [Exponentiation with Church Numerals] 2016/11/21 18:58 office [Exponentiation with Church Numerals] 2016/11/21 18:43 office [Exponentiation with Church Numerals] 2016/11/21 15:53 office 2016/10/22 00:14 office [Implementing the Y-Combinator] 2016/10/22 00:09 office [Implementing the Y-Combinator] 2016/10/22 00:08 office [Implementing the Y-Combinator] 2016/10/22 00:06 office 2016/10/22 00:04 office [Implementing the Y-Combinator] 2016/10/21 23:55 office [Implementing the Y-Combinator] 2016/10/21 23:51 office [Implementations] 2016/10/21 23:51 office [Implementing the Y-Combinator] 2016/10/21 23:47 office created2016/10/21 21:21 office removed2016/10/21 21:21 office created 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*}