162 lines
3.7 KiB
TeX
Executable File
162 lines
3.7 KiB
TeX
Executable File
\section{Recursion}
|
|
|
|
|
|
%\iftrue
|
|
\iffalse
|
|
|
|
You now have a choice. Choose wisely --- there's no going back.
|
|
|
|
\begin{tcolorbox}[
|
|
breakable,
|
|
colback=white,
|
|
colframe=gray,
|
|
arc=0pt, outer arc=0pt
|
|
]
|
|
\raggedright
|
|
\textbf{Take the red pill:} You stay on this page and try to solve \ref{thechallenge}. \par
|
|
This will take a while, and it's very unlikely you'll finish before class ends.
|
|
|
|
|
|
\vspace{4mm}
|
|
|
|
I strongly prefer this option. It's not easy, but you'll be very happy if you solve it yourself.
|
|
This is a chance to build your own solution to a fundamental problem in this field, just as
|
|
Curry, Church, and Turing did when first developing the theory of lambda calculus.
|
|
|
|
- Mark
|
|
\end{tcolorbox}
|
|
|
|
\begin{tcolorbox}[
|
|
breakable,
|
|
colback=white,
|
|
colframe=gray,
|
|
arc=0pt, outer arc=0pt
|
|
]
|
|
\textbf{Take the blue pill:} You skip this problem and turn the page.
|
|
Half of the answer to \ref{thechallenge} will be free, and the rest will be
|
|
broken into smaller steps. This is how we usually learn out about interesting
|
|
mathematics, both in high school and in university.
|
|
|
|
\vspace{2mm}
|
|
|
|
This path isn't as rewarding as the one above, but it is well-paved
|
|
and easier to traverse.
|
|
\end{tcolorbox}
|
|
|
|
\problem{}<thechallenge>
|
|
Can you find a way to recursively call functions in lambda calculus? \par
|
|
Find a way to define a recursive factorial function. \par
|
|
|
|
\note{$A = (\lm a. A~a)$ doesn't count. You can't use a macro inside itself.}
|
|
|
|
\vfill
|
|
\pagebreak
|
|
\fi
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Say we want a function that computes the factorial of a positive integer. Here's one way we could define it:
|
|
$$
|
|
x! = \begin{cases}
|
|
x \times (x-1)! & x \neq 0 \\
|
|
1 & x = 0
|
|
\end{cases}
|
|
$$
|
|
|
|
We cannot re-create this in lambda calculus, since we aren't given a way to recursively call functions.
|
|
|
|
\vspace{2mm}
|
|
|
|
One could think that $A = \lm a. A~a$ is a recursive function. In fact, it is not. \par
|
|
Remember that such \say{definitions} aren't formal structures in lambda calculus. \par
|
|
They're just shorthand that simplifies notation.
|
|
|
|
\begin{instructornote}
|
|
We're talking about recursion, and \textit{computability} isn't far away. At one point or another, it may be good to give the class a precise definition of \say{computable by lambda calculus:}
|
|
|
|
\vspace{4ex}
|
|
|
|
Say we have a device that reduces a $\lm$ expression to $\beta$-normal form. We give it an expression, and the machine simplifies it as much as it can and spits out the result.
|
|
|
|
\vspace{1ex}
|
|
|
|
An algorithm is \say{computable by lambda calculus} if we can encode its input in an expression that resolves to the algorithm's output.
|
|
\end{instructornote}
|
|
|
|
\problem{}
|
|
Write an expression that resolves to itself. \par
|
|
\hint{Your answer should be quite short.}
|
|
|
|
\vspace{1ex}
|
|
|
|
This expression is often called $\Omega$, after the last letter of the Greek alphabet. \par
|
|
$\Omega$ useless on its own, but it gives us a starting point for recursion. \par
|
|
|
|
\begin{solution}
|
|
$\Omega = M~M = (\lm x . xx) (\lm x . xx)$
|
|
|
|
\vspace{1mm}
|
|
|
|
An uninspired mathematician might call the Mockingbird $\omega$, \say{little omega}.
|
|
\end{solution}
|
|
|
|
\vfill
|
|
\pagebreak
|
|
|
|
|
|
|
|
|
|
|
|
\definition{}
|
|
This is the \textit{Y-combinator}. You may notice that it's just $\Omega$ put to work.
|
|
$$
|
|
Y = \lm f . (\lm x . f(x~x))(\lm x . f(x~x))
|
|
$$
|
|
|
|
\problem{}
|
|
What does this thing do? \par
|
|
Evaluate $Y f$.
|
|
|
|
|
|
|
|
%\vfill
|
|
|
|
%\definition{}
|
|
%We say $x$ is a \textit{fixed point} of a function $f$ if $f(x) = x$.
|
|
|
|
%\problem{}
|
|
%Show that $Y F$ is a fixed point of $F$.
|
|
|
|
%\vfill
|
|
|
|
%\problem{}
|
|
%Let $b = (\lm xy . y(xxy))$ and $B = b ~ b$. \par
|
|
%Let $N = B F$ for an arbitrary lambda expression $F$. \par
|
|
|
|
%Show that $F N = N$.
|
|
|
|
%\vfill
|
|
|
|
%\problem{Bonus}
|
|
%Find a fixed-point combinator that isn't $Y$ or $\Theta$.
|
|
|
|
\vfill
|
|
\pagebreak |