This shows you the differences between two versions of the page.
Previous revision | |||
— | 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' | ||
+ | |||
+ | 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/ | ||
+ | * [[fuss/ | ||
+ | |||
+ | ====== 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} & | ||
+ | \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}) & | ||
+ | & | ||
+ | & | ||
+ | \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, | ||
+ | |||
+ | 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 & | ||
+ | \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}) & | ||
+ | & | ||
+ | & | ||
+ | & | ||
+ | & | ||
+ | \end{eqnarray*} | ||
+ | |||
+ | which yields the expected result. | ||
+ | |||
+ | ====== η-Reduction and η-Expansion ====== | ||
+ | |||
+ | $\eta$-reduction is given by: | ||
+ | \begin{eqnarray*} | ||
+ | \lambda x.f(x) & | ||
+ | \end{eqnarray*} | ||
+ | |||
+ | $\eta$-expansion is given by: | ||
+ | \begin{eqnarray*} | ||
+ | f & | ||
+ | \end{eqnarray*} | ||
+ | |||
+ | ====== Aggregators ====== | ||
+ | |||
+ | {{indexmenu>/ |