Cleanup
This commit is contained in:
parent
e3e09c9c95
commit
494e91dc98
@ -1,13 +1,12 @@
|
||||
% use [nosolutions] flag to hide solutions.
|
||||
% use [solutions] flag to show solutions.
|
||||
\documentclass[
|
||||
solutions,
|
||||
nosolutions,
|
||||
singlenumbering
|
||||
]{../../resources/ormc_handout}
|
||||
|
||||
\usepackage{url}
|
||||
\usepackage{mathtools} % for \coloneqq
|
||||
\usepackage{subfiles}
|
||||
|
||||
% An invisible marker, used to
|
||||
% draw arrows in equations.
|
||||
@ -51,11 +50,11 @@
|
||||
\hfill
|
||||
|
||||
|
||||
\subfile{parts/00 intro}
|
||||
\subfile{parts/01 combinators}
|
||||
\subfile{parts/02 boolean}
|
||||
\subfile{parts/03 numbers}
|
||||
\subfile{parts/04 recursion}
|
||||
\subfile{parts/05 challenges}
|
||||
\input{parts/00 intro}
|
||||
\input{parts/01 combinators}
|
||||
\input{parts/02 boolean}
|
||||
\input{parts/03 numbers}
|
||||
\input{parts/04 recursion}
|
||||
\input{parts/05 challenges}
|
||||
|
||||
\end{document}
|
||||
@ -1,29 +1,56 @@
|
||||
\documentclass[../main.tex]{subfiles}
|
||||
\section{Definitions}
|
||||
|
||||
\generic{$\lm$ Notation:}
|
||||
$\lm$ notation is used to define functions, and looks like $(\lm ~ \text{input} ~ . ~ \text{output})$. \\
|
||||
Consider the following statement:
|
||||
$$
|
||||
I = \lm a . a
|
||||
$$
|
||||
|
||||
\begin{document}
|
||||
This tells us that $I$ is a function that takes its input, $a$, to itself. We'll call this the \textit{identity function}. \\
|
||||
|
||||
\section{Definitions}
|
||||
To apply functions, put them next to their inputs. We'll omit the usual parentheses to save space.
|
||||
|
||||
\generic{$\lm$ Notation:}
|
||||
$\lm$ notation is used to define functions, and looks like $(\lm ~ \text{input} ~ . ~ \text{output})$. \\
|
||||
Consider the following statement:
|
||||
$$
|
||||
I = \lm a . a
|
||||
$$
|
||||
$$
|
||||
I ~ \star = (\lm a . a) ~ \star = \star
|
||||
$$
|
||||
|
||||
This tells us that $I$ is a function that takes its input, $a$, to itself. We'll call this the \textit{identity function}. \\
|
||||
$$
|
||||
(M~\star) =
|
||||
(\lm \tzm{b}a. a)~\tzmr{a}\star =
|
||||
\star
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture,
|
||||
out=225,
|
||||
in=315,
|
||||
distance=0.5cm
|
||||
]
|
||||
\draw[->,gray,shorten >=5pt,shorten <=3pt]
|
||||
(a.center) to (b.center);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
To apply functions, put them next to their inputs. We'll omit the usual parentheses to save space.
|
||||
Functions are left-associative: If $A$ and $B$ are functions, $(A~B~\star)$ is equivalent to $((A~B)~\star)$. As usual, we'll use parentheses to group terms if we want to override this order: $(A~(B~\star)) \neq (A~B~\star)$ \\
|
||||
In this handout, all types of parentheses ( $(), [],$ etc ) are equivalent.
|
||||
|
||||
$$
|
||||
I ~ \star = (\lm a . a) ~ \star = \star
|
||||
$$
|
||||
\vfill
|
||||
|
||||
$$
|
||||
(M~\star) =
|
||||
(\lm \tzm{b}a. a)~\tzmr{a}\star =
|
||||
\star
|
||||
\generic{$\beta$-Reduction:}
|
||||
|
||||
$\beta$-reduction is a fancy name for \say{simplifying an expression.} We've already done it once above.
|
||||
|
||||
Let's make another function:
|
||||
$$
|
||||
M = \lm f . f f
|
||||
$$
|
||||
$M$ takes a function as an input and calls it on itself. What is $(M~I)$?
|
||||
$$
|
||||
(M~I) =
|
||||
((\lm \tzm{b}f.f f)~\tzmr{a}I) =
|
||||
(I~I) =
|
||||
((\lm \tzm{d}a.a)~\tzmr{c}I) =
|
||||
I
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture,
|
||||
@ -33,222 +60,188 @@
|
||||
]
|
||||
\draw[->,gray,shorten >=5pt,shorten <=3pt]
|
||||
(a.center) to (b.center);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
Functions are left-associative: If $A$ and $B$ are functions, $(A~B~\star)$ is equivalent to $((A~B)~\star)$. As usual, we'll use parentheses to group terms if we want to override this order: $(A~(B~\star)) \neq (A~B~\star)$ \\
|
||||
In this handout, all types of parentheses ( $(), [],$ etc ) are equivalent.
|
||||
|
||||
\vfill
|
||||
|
||||
\generic{$\beta$-Reduction:}
|
||||
|
||||
$\beta$-reduction is a fancy name for \say{simplifying an expression.} We've already done it once above.
|
||||
|
||||
Let's make another function:
|
||||
$$
|
||||
M = \lm f . f f
|
||||
$$
|
||||
$M$ takes a function as an input and calls it on itself. What is $(M~I)$?
|
||||
$$
|
||||
(M~I) =
|
||||
((\lm \tzm{b}f.f f)~\tzmr{a}I) =
|
||||
(I~I) =
|
||||
((\lm \tzm{d}a.a)~\tzmr{c}I) =
|
||||
I
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture,
|
||||
out=225,
|
||||
in=315,
|
||||
distance=0.5cm
|
||||
]
|
||||
\draw[->,gray,shorten >=5pt,shorten <=3pt]
|
||||
(a.center) to (b.center);
|
||||
\draw[->,gray,shorten >=5pt,shorten <=3pt]
|
||||
(c.center) to (d.center);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
We cannot reduce this any further, so we stop. Our expression is now in \textit{$\beta$-normal form}.
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
\problem{}
|
||||
Reduce the following expressions:
|
||||
\begin{itemize}
|
||||
\item $I~I$
|
||||
\item $I~I~I$
|
||||
\item $(\lm a .(a~a~a)) ~ I$
|
||||
\item $(\lm a . (\lm b . a)) ~ M ~ I$
|
||||
\end{itemize}
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
\generic{Currying:}
|
||||
|
||||
Lambda functions are only allowed to take one argument, but we can emulate multivariable functions through \say{currying.}
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Before we begin, let's review \textit{function composition}. With \say{normal} functions, composition is written as $(f \circ g)(x) = f(g(x))$. This means \say{$f$ of $g$ of $x$}.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
To demonstrate currying, we'll make a function $C$ in lambda calculus, which takes two functions ($f$ and $g$), an input $x$, and produces $f$ applied to $g$ applied to $x$. \\
|
||||
|
||||
In other words, we want a $C$ so that $C~f~g~x = f~(g~x)$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
We'll define this $C$ as follows:
|
||||
$$
|
||||
C = \lm f . (\lm g . (\lm x . f(g(x))))
|
||||
$$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This looks awfully scary, so let's take this expression apart. \\
|
||||
C is a function that takes one argument ($f$) and returns a function (underlined):
|
||||
$$
|
||||
C = \lm f .(~~\tzm{a} \lm g . (\lm x . f(g(x))) \tzm{b}~~)
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture
|
||||
]
|
||||
\node[below = 1ex] at (a.center) (aa) {};
|
||||
\node[below = 1ex] at (b.center) (bb) {};
|
||||
|
||||
\path[draw = gray] (aa) to (bb);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
The function it returns does the same thing. It takes an argument $g$, and returns \textit{another} function:
|
||||
$$
|
||||
C = \lm f . (~~ \lm g . (~~\tzm{a} \lm x . f(g(x)) \tzm{b}~~) ~~)
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture
|
||||
]
|
||||
\node[below = 1ex] at (a.center) (aa) {};
|
||||
\node[below = 1ex] at (b.center) (bb) {};
|
||||
|
||||
\path[draw = gray] (aa) to (bb);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This last function $\lm x. f(g(x))$ takes one argument, and returns $f(g(x))$. Since this function is inside the previous two, it has access to their arguments, $f$ and $g$.
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
So, currying allows us to create multivariable functions by nesting single-variable functions. \\
|
||||
As you saw above, such expressions can get very long. We'll use a bit of shorthand to make them more palatable. If we have an expression with repeated function definitions, we'll combine their arguments under one $\lm$.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
For example,
|
||||
$$
|
||||
C = \lm f . (\lm g . (\lm x . f(g(x))))
|
||||
$$
|
||||
will become
|
||||
$$
|
||||
C = \lm fgx.(~f(g(x))~)
|
||||
$$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This is only notation. \textbf{Curried functions are not multivariable functions!} They must be evaluated one variable at a time, just like their un-curried version. Substituting all curried variables in one go may cause errors, as you'll see below.
|
||||
|
||||
\problem{}
|
||||
Evaluate $C~M~I~\star$ \\
|
||||
Then, evaluate $C~I~M~I$ \\
|
||||
\hint{Place parentheses first. Remember, function application is left-associative.}
|
||||
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
|
||||
\definition{$\alpha$-equivalence}
|
||||
We say two functions are \textit{$\alpha$-equivalent} if they differ only by the names of their variables:
|
||||
$I = \lm a.a = \lm b.b = \lm \heartsuit . \heartsuit = ...$
|
||||
|
||||
\generic{$\alpha$-Conversion:}
|
||||
|
||||
Variables inside functions are \say{scoped.} We must take care to keep separate variable separate.
|
||||
|
||||
For example, take the functions \\
|
||||
$A = \lm a b . a$ \\
|
||||
$B = \lm b . b$
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
We could say that $(A~B) = \lm b . (\lm b . b)$, and therefore
|
||||
$$
|
||||
((A~B)~I)
|
||||
= (~ (\lm \tzm{b}b . (\lm b . b))~\tzmr{a}I ~)
|
||||
= \lm I . I
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture,
|
||||
out=225,
|
||||
in=315,
|
||||
distance=0.5cm
|
||||
]
|
||||
\draw[->,gray,shorten >=5pt,shorten <=3pt]
|
||||
(a.center) to (b.center);
|
||||
(c.center) to (d.center);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
$$
|
||||
|
||||
Which is, of course, incorrect. $\lm I . I$ is not a valid function.
|
||||
We cannot reduce this any further, so we stop. Our expression is now in \textit{$\beta$-normal form}.
|
||||
|
||||
\vspace{2ex}
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
Notice that both $A$ and $B$ use the input $b$. However, each $b$ is \say{bound} to a different function. The two $b$s are therefore distinct.
|
||||
\problem{}
|
||||
Reduce the following expressions:
|
||||
\begin{itemize}
|
||||
\item $I~I$
|
||||
\item $I~I~I$
|
||||
\item $(\lm a .(a~a~a)) ~ I$
|
||||
\item $(\lm a . (\lm b . a)) ~ M ~ I$
|
||||
\end{itemize}
|
||||
|
||||
\vspace{2ex}
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
Let's rewrite $B$ as $\lm c . c$ and try again:
|
||||
\generic{Currying:}
|
||||
|
||||
$$
|
||||
(A~B) = \lm b . ( \lm c . c) = \lm bc . c
|
||||
$$
|
||||
Lambda functions are only allowed to take one argument, but we can emulate multivariable functions through \say{currying.}
|
||||
|
||||
Now, we correctly find that $(A~B~I) = (\lm bc . c)~I = \lm c . c = B = I$.
|
||||
\vspace{1ex}
|
||||
|
||||
\problem{}
|
||||
Let $C = \lm abc.b$ \\
|
||||
Reduce $(C~a~c~b)$.
|
||||
Before we begin, let's review \textit{function composition}. With \say{normal} functions, composition is written as $(f \circ g)(x) = f(g(x))$. This means \say{$f$ of $g$ of $x$}.
|
||||
|
||||
\begin{solution}
|
||||
I'll rewrite $(C~a~c~b)$ as $(C~a_1~c_1~b_1)$:
|
||||
\begin{align*}
|
||||
C = (\lm abc.b) &= (\lm a.\lm b.\lm c.b) \\
|
||||
(\lm a.\lm b.\lm c.b)~a_1 &= (\lm b.\lm c.b) \\
|
||||
(\lm b.\lm c.b)~c_1 &= (\lm c.c_1) \\
|
||||
(\lm c.c_1)~b_1 &= c_1
|
||||
\end{align*}
|
||||
\end{solution}
|
||||
\vspace{1ex}
|
||||
|
||||
\vfill
|
||||
To demonstrate currying, we'll make a function $C$ in lambda calculus, which takes two functions ($f$ and $g$), an input $x$, and produces $f$ applied to $g$ applied to $x$. \\
|
||||
|
||||
\problem{}
|
||||
Reduce $((\lm a.a)~\lm bc.b)~d~\lm eg.g$
|
||||
In other words, we want a $C$ so that $C~f~g~x = f~(g~x)$
|
||||
|
||||
\begin{solution}
|
||||
$((\lm a.a)~\lm bc.b)~d~\lm eg.g$ \\
|
||||
$= (\lm bc.b)~d~\lm eg.g$ \\
|
||||
$= (\lm c.d)~\lm eg.g$ \\
|
||||
$= d$
|
||||
\end{solution}
|
||||
\vspace{1ex}
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
We'll define this $C$ as follows:
|
||||
$$
|
||||
C = \lm f . (\lm g . (\lm x . f(g(x))))
|
||||
$$
|
||||
|
||||
\end{document}
|
||||
\vspace{1ex}
|
||||
|
||||
This looks awfully scary, so let's take this expression apart. \\
|
||||
C is a function that takes one argument ($f$) and returns a function (underlined):
|
||||
$$
|
||||
C = \lm f .(~~\tzm{a} \lm g . (\lm x . f(g(x))) \tzm{b}~~)
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture
|
||||
]
|
||||
\node[below = 1ex] at (a.center) (aa) {};
|
||||
\node[below = 1ex] at (b.center) (bb) {};
|
||||
|
||||
\path[draw = gray] (aa) to (bb);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
The function it returns does the same thing. It takes an argument $g$, and returns \textit{another} function:
|
||||
$$
|
||||
C = \lm f . (~~ \lm g . (~~\tzm{a} \lm x . f(g(x)) \tzm{b}~~) ~~)
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture
|
||||
]
|
||||
\node[below = 1ex] at (a.center) (aa) {};
|
||||
\node[below = 1ex] at (b.center) (bb) {};
|
||||
|
||||
\path[draw = gray] (aa) to (bb);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This last function $\lm x. f(g(x))$ takes one argument, and returns $f(g(x))$. Since this function is inside the previous two, it has access to their arguments, $f$ and $g$.
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
So, currying allows us to create multivariable functions by nesting single-variable functions. \\
|
||||
As you saw above, such expressions can get very long. We'll use a bit of shorthand to make them more palatable. If we have an expression with repeated function definitions, we'll combine their arguments under one $\lm$.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
For example,
|
||||
$$
|
||||
C = \lm f . (\lm g . (\lm x . f(g(x))))
|
||||
$$
|
||||
will become
|
||||
$$
|
||||
C = \lm fgx.(~f(g(x))~)
|
||||
$$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This is only notation. \textbf{Curried functions are not multivariable functions!} They must be evaluated one variable at a time, just like their un-curried version. Substituting all curried variables in one go may cause errors, as you'll see below.
|
||||
|
||||
\problem{}
|
||||
Evaluate $C~M~I~\star$ \\
|
||||
Then, evaluate $C~I~M~I$ \\
|
||||
\hint{Place parentheses first. Remember, function application is left-associative.}
|
||||
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
|
||||
\definition{$\alpha$-equivalence}
|
||||
We say two functions are \textit{$\alpha$-equivalent} if they differ only by the names of their variables:
|
||||
$I = \lm a.a = \lm b.b = \lm \heartsuit . \heartsuit = ...$
|
||||
|
||||
\generic{$\alpha$-Conversion:}
|
||||
|
||||
Variables inside functions are \say{scoped.} We must take care to keep separate variable separate.
|
||||
|
||||
For example, take the functions \\
|
||||
$A = \lm a b . a$ \\
|
||||
$B = \lm b . b$
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
We could say that $(A~B) = \lm b . (\lm b . b)$, and therefore
|
||||
$$
|
||||
((A~B)~I)
|
||||
= (~ (\lm \tzm{b}b . (\lm b . b))~\tzmr{a}I ~)
|
||||
= \lm I . I
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture,
|
||||
out=225,
|
||||
in=315,
|
||||
distance=0.5cm
|
||||
]
|
||||
\draw[->,gray,shorten >=5pt,shorten <=3pt]
|
||||
(a.center) to (b.center);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
|
||||
Which is, of course, incorrect. $\lm I . I$ is not a valid function.
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
Notice that both $A$ and $B$ use the input $b$. However, each $b$ is \say{bound} to a different function. The two $b$s are therefore distinct.
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
Let's rewrite $B$ as $\lm c . c$ and try again:
|
||||
|
||||
$$
|
||||
(A~B) = \lm b . ( \lm c . c) = \lm bc . c
|
||||
$$
|
||||
|
||||
Now, we correctly find that $(A~B~I) = (\lm bc . c)~I = \lm c . c = B = I$.
|
||||
|
||||
\problem{}
|
||||
Let $C = \lm abc.b$ \\
|
||||
Reduce $(C~a~c~b)$.
|
||||
|
||||
\begin{solution}
|
||||
I'll rewrite $(C~a~c~b)$ as $(C~a_1~c_1~b_1)$:
|
||||
\begin{align*}
|
||||
C = (\lm abc.b) &= (\lm a.\lm b.\lm c.b) \\
|
||||
(\lm a.\lm b.\lm c.b)~a_1 &= (\lm b.\lm c.b) \\
|
||||
(\lm b.\lm c.b)~c_1 &= (\lm c.c_1) \\
|
||||
(\lm c.c_1)~b_1 &= c_1
|
||||
\end{align*}
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Reduce $((\lm a.a)~\lm bc.b)~d~\lm eg.g$
|
||||
|
||||
\begin{solution}
|
||||
$((\lm a.a)~\lm bc.b)~d~\lm eg.g$ \\
|
||||
$= (\lm bc.b)~d~\lm eg.g$ \\
|
||||
$= (\lm c.d)~\lm eg.g$ \\
|
||||
$= d$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
@ -1,47 +1,39 @@
|
||||
\documentclass[../main.tex]{subfiles}
|
||||
\section{Combinators}
|
||||
|
||||
\definition{}
|
||||
A \textit{free variable} in a $\lm$-expression is a variable that isn't bound to any input. \\
|
||||
For example, $b$ is a free variable in $\lm a. b$. The same is true of $\star$ in any of the previous pages.
|
||||
|
||||
\begin{document}
|
||||
A \textit{combinator} is a function with no free variables.
|
||||
|
||||
\section{Combinators}
|
||||
\definition{The Kestrel}
|
||||
|
||||
\definition{}
|
||||
A \textit{free variable} in a $\lm$-expression is a variable that isn't bound to any input. \\
|
||||
For example, $b$ is a free variable in $\lm a. b$. The same is true of $\star$ in any of the previous pages.
|
||||
Notable combinators are often named after birds.\hspace{-0.5ex}\footnotemark{} We've already met a few: \\
|
||||
The \textit{Idiot}, $I = \lm a.a$ \\
|
||||
The \textit{Mockingbird}, $M = \lm f.ff$ \\
|
||||
The \textit{Cardinal}, $C = \lm fgx.(~ f(g(x)) ~)$ \\
|
||||
|
||||
A \textit{combinator} is a function with no free variables.
|
||||
\footnotetext{Raymond Smullyan's \textit{To Mock a Mockingbird} is responsible for this.}
|
||||
|
||||
\definition{The Kestrel}
|
||||
\vspace{2ex}
|
||||
|
||||
Notable combinators are often named after birds.\hspace{-0.5ex}\footnotemark{} We've already met a few: \\
|
||||
The \textit{Idiot}, $I = \lm a.a$ \\
|
||||
The \textit{Mockingbird}, $M = \lm f.ff$ \\
|
||||
The \textit{Cardinal}, $C = \lm fgx.(~ f(g(x)) ~)$ \\
|
||||
Another notable combinator is $K$, the \textit{Kestrel}:
|
||||
$$
|
||||
K = \lm ab . a
|
||||
$$
|
||||
\problem{}
|
||||
What does the Kestrel do? Explain in plain English. \\
|
||||
\hint{What is $(K~\heartsuit~\star)$?}
|
||||
|
||||
\footnotetext{Raymond Smullyan's \textit{To Mock a Mockingbird} is responsible for this.}
|
||||
\vspace{2cm}
|
||||
|
||||
\vspace{2ex}
|
||||
\problem{}
|
||||
Reduce $(K~I)$ to derive the \textit{Kite}. How does the Kite compare to the Kestrel? \\
|
||||
We'll call the Kite KI.
|
||||
|
||||
Another notable combinator is $K$, the \textit{Kestrel}:
|
||||
$$
|
||||
K = \lm ab . a
|
||||
$$
|
||||
\problem{}
|
||||
What does the Kestrel do? Explain in plain English. \\
|
||||
\hint{What is $(K~\heartsuit~\star)$?}
|
||||
\begin{solution}
|
||||
$\text{KI} = \lm ab . b$. \\
|
||||
\end{solution}
|
||||
|
||||
\vspace{2cm}
|
||||
|
||||
\problem{}
|
||||
Reduce $(K~I)$ to derive the \textit{Kite}. How does the Kite compare to the Kestrel? \\
|
||||
We'll call the Kite KI.
|
||||
|
||||
\begin{solution}
|
||||
$\text{KI} = \lm ab . b$. \\
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
|
||||
\end{document}
|
||||
\vfill
|
||||
\pagebreak
|
||||
@ -1,71 +1,66 @@
|
||||
\documentclass[../main.tex]{subfiles}
|
||||
\section{Boolean Algebra}
|
||||
|
||||
The Kestrel selects its first argument, and the Kite selects its second. This \say{choosing} behavior is awfully similar to something you may have already seen...
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Let $T = K\phantom{I} = \lm ab . a$ \\
|
||||
Let $F = KI = \lm ab . b$ \\
|
||||
|
||||
\problem{}
|
||||
Write a function $\text{NOT}$ so that $(\text{NOT} ~ T) = F$ and $(\text{NOT}~F) = T$. \\
|
||||
\hint{What is $(T~\heartsuit~\star)$? How about $(F~\heartsuit~\star)$?}
|
||||
|
||||
|
||||
\begin{document}
|
||||
\begin{solution}
|
||||
$\text{NOT} = \lm a . (a~F~T)$ \\
|
||||
\end{solution}
|
||||
|
||||
\section{Boolean Algebra}
|
||||
\vfill
|
||||
|
||||
The Kestrel selects its first argument, and the Kite selects its second. This \say{choosing} behavior is awfully similar to something you may have already seen...
|
||||
\problem{}
|
||||
Write functions $\text{AND}$, $\text{OR}$, and $\text{XOR}$ that satisfy the following table.
|
||||
|
||||
\begin{center}
|
||||
\begin{tabular}{|| c c || c | c | c ||}
|
||||
\hline
|
||||
$A$ & $B$ & $(\text{AND}~A~B)$ & $(\text{OR}~A~B)$ & $(\text{XOR}~A~B)$ \\
|
||||
\hline\hline
|
||||
F & F & F & F & F \\
|
||||
\hline
|
||||
F & T & F & T & T \\
|
||||
\hline
|
||||
T & F & F & T & T \\
|
||||
\hline
|
||||
T & T & T & T & F \\
|
||||
\hline
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
|
||||
\begin{solution}
|
||||
There's more than one way to do this, of course, but make sure the kids understand how the solutions below work.
|
||||
\begin{align*}
|
||||
\text{AND} &= \lm ab . (a~b~F) = \lm ab . aba \\
|
||||
\text{OR} &= \lm ab . (a~T~b) = \lm ab . aab \\
|
||||
\text{XOR} &= \lm ab . (a~ (\text{NOT}~b) ~b)
|
||||
\end{align*}
|
||||
|
||||
It may be worth mentioning that OR $= \lm ab.(M~a~b)$ is also a solution.
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
To complete our boolean algebra, write the boolean equality check EQ. \\
|
||||
What inputs should it take? What outputs should it produce?
|
||||
|
||||
\begin{solution}
|
||||
$\text{EQ} = \lm ab . [a~(bTF)~(bFT)] = \lm ab . [a~b~(\text{NOT}~b)]$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Let $T = K\phantom{I} = \lm ab . a$ \\
|
||||
Let $F = KI = \lm ab . b$ \\
|
||||
$\text{EQ} = \lm ab . [\text{NOT}~(\text{XOR}~a~b)]$
|
||||
\end{solution}
|
||||
|
||||
\problem{}
|
||||
Write a function $\text{NOT}$ so that $(\text{NOT} ~ T) = F$ and $(\text{NOT}~F) = T$. \\
|
||||
\hint{What is $(T~\heartsuit~\star)$? How about $(F~\heartsuit~\star)$?}
|
||||
|
||||
|
||||
\begin{solution}
|
||||
$\text{NOT} = \lm a . (a~F~T)$ \\
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Write functions $\text{AND}$, $\text{OR}$, and $\text{XOR}$ that satisfy the following table.
|
||||
|
||||
\begin{center}
|
||||
\begin{tabular}{|| c c || c | c | c ||}
|
||||
\hline
|
||||
$A$ & $B$ & $(\text{AND}~A~B)$ & $(\text{OR}~A~B)$ & $(\text{XOR}~A~B)$ \\
|
||||
\hline\hline
|
||||
F & F & F & F & F \\
|
||||
\hline
|
||||
F & T & F & T & T \\
|
||||
\hline
|
||||
T & F & F & T & T \\
|
||||
\hline
|
||||
T & T & T & T & F \\
|
||||
\hline
|
||||
\end{tabular}
|
||||
\end{center}
|
||||
|
||||
\begin{solution}
|
||||
There's more than one way to do this, of course, but make sure the kids understand how the solutions below work.
|
||||
\begin{align*}
|
||||
\text{AND} &= \lm ab . (a~b~F) = \lm ab . aba \\
|
||||
\text{OR} &= \lm ab . (a~T~b) = \lm ab . aab \\
|
||||
\text{XOR} &= \lm ab . (a~ (\text{NOT}~b) ~b)
|
||||
\end{align*}
|
||||
|
||||
It may be worth mentioning that OR $= \lm ab.(M~a~b)$ is also a solution.
|
||||
\end{solution}
|
||||
|
||||
\problem{}
|
||||
To complete our boolean algebra, write the boolean equality check EQ. \\
|
||||
What inputs should it take? What outputs should it produce?
|
||||
|
||||
\begin{solution}
|
||||
$\text{EQ} = \lm ab . [a~(bTF)~(bFT)] = \lm ab . [a~b~(\text{NOT}~b)]$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
$\text{EQ} = \lm ab . [\text{NOT}~(\text{XOR}~a~b)]$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
\end{document}
|
||||
\vfill
|
||||
\pagebreak
|
||||
@ -1,226 +1,220 @@
|
||||
\documentclass[../main.tex]{subfiles}
|
||||
\section{Numbers}
|
||||
|
||||
\begin{document}
|
||||
Since the only objects we have in $\lm$-calculus are functions, it's natural to think of quantities as \textit{adverbs} (once, twice, thrice,...) rather than \textit{nouns} (one, two, three ...) \\
|
||||
|
||||
\section{Numbers}
|
||||
\vspace{1ex}
|
||||
|
||||
Since the only objects we have in $\lm$-calculus are functions, it's natural to think of quantities as \textit{adverbs} (once, twice, thrice,...) rather than \textit{nouns} (one, two, three ...) \\
|
||||
We'll start with zero. If our numbers are \textit{once,} \textit{twice,} and \textit{twice}, it may make sense to make zero \textit{don't}. \\
|
||||
Here's our \textit{don't} function: given a function and an input, don't apply the function to the input.
|
||||
$$
|
||||
0 = \lm fa.a
|
||||
$$
|
||||
If you look closely, you'll find that $0$ is $\alpha$-equivalent to the false function $F$.
|
||||
|
||||
\problem{}
|
||||
Write $1$, $2$, and $3$. We will call these \textit{Church numerals}.\hspace{-0.5ex}\footnotemark{} \\
|
||||
\note{\textit{Note:} This problem read aloud is \say{Define \textit{once}, \textit{twice}, and \textit{thrice}.}}
|
||||
|
||||
\footnotetext{after Alonzo Church, the inventor of lambda calculus and these numerals. He was Alan Turing's thesis advisor.}
|
||||
|
||||
\begin{solution}
|
||||
$1$ calls a function once on its argument: \\
|
||||
$1 = \lm fa . (f~a)$.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
We'll start with zero. If our numbers are \textit{once,} \textit{twice,} and \textit{twice}, it may make sense to make zero \textit{don't}. \\
|
||||
Here's our \textit{don't} function: given a function and an input, don't apply the function to the input.
|
||||
Naturally, \\
|
||||
$2 = \lm fa . [~f~(f~a)~]$ \\
|
||||
$3 = \lm fa . [~f~(f~(f~a))~]$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
The round parentheses are \textit{essential}. Our lambda calculus is left-associative!
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
Also, notice that $1$ is very similar to $I$:
|
||||
$$
|
||||
0 = \lm fa.a
|
||||
I~\heartsuit~\star = 1~\heartsuit~\star
|
||||
$$
|
||||
If you look closely, you'll find that $0$ is $\alpha$-equivalent to the false function $F$.
|
||||
|
||||
\problem{}
|
||||
Write $1$, $2$, and $3$. We will call these \textit{Church numerals}.\hspace{-0.5ex}\footnotemark{} \\
|
||||
\note{\textit{Note:} This problem read aloud is \say{Define \textit{once}, \textit{twice}, and \textit{thrice}.}}
|
||||
Zero is false, and one is the identity. Isn't that wonderful?
|
||||
\end{solution}
|
||||
|
||||
\footnotetext{after Alonzo Church, the inventor of lambda calculus and these numerals. He was Alan Turing's thesis advisor.}
|
||||
\vfill
|
||||
|
||||
\begin{solution}
|
||||
$1$ calls a function once on its argument: \\
|
||||
$1 = \lm fa . (f~a)$.
|
||||
\problem{}
|
||||
What is $(4~I)~\star$?
|
||||
|
||||
\vspace{1ex}
|
||||
\vfill
|
||||
|
||||
Naturally, \\
|
||||
$2 = \lm fa . [~f~(f~a)~]$ \\
|
||||
$3 = \lm fa . [~f~(f~(f~a))~]$
|
||||
\problem{}
|
||||
What is $(3~NOT~T)$? \\
|
||||
How about $(8~NOT~F)$?
|
||||
|
||||
\vspace{1ex}
|
||||
\vfill
|
||||
|
||||
The round parentheses are \textit{essential}. Our lambda calculus is left-associative!
|
||||
\pagebreak
|
||||
|
||||
\vspace{2ex}
|
||||
\problem{}
|
||||
This handout may remind you of Professor Oleg's handout on Peano's axioms. Good. \\
|
||||
While you're there, recall the tools we used to build the natural numbers: \\
|
||||
We had a zero element and a \say{successor} operation so that $1 \coloneqq S(0)$, $2 \coloneqq S(1)$, and so on.
|
||||
|
||||
Also, notice that $1$ is very similar to $I$:
|
||||
$$
|
||||
I~\heartsuit~\star = 1~\heartsuit~\star
|
||||
$$
|
||||
\vspace{1ex}
|
||||
|
||||
Zero is false, and one is the identity. Isn't that wonderful?
|
||||
\end{solution}
|
||||
Create a successor operation for the Church numerals. \\
|
||||
\hint{A good signature for this function is $\lm nfa$, or more clearly $\lm n.\lm fa$. Do you see why?}
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
What is $(4~I)~\star$?
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
What is $(3~NOT~T)$? \\
|
||||
How about $(8~NOT~F)$?
|
||||
|
||||
\vfill
|
||||
|
||||
\pagebreak
|
||||
|
||||
\problem{}
|
||||
This handout may remind you of Professor Oleg's handout on Peano's axioms. Good. \\
|
||||
While you're there, recall the tools we used to build the natural numbers: \\
|
||||
We had a zero element and a \say{successor} operation so that $1 \coloneqq S(0)$, $2 \coloneqq S(1)$, and so on.
|
||||
\begin{solution}
|
||||
$S = \lm n. [\lm fa . f~(n~f~a)] = \lm nfa . [f~(n~f~a)]$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Create a successor operation for the Church numerals. \\
|
||||
\hint{A good signature for this function is $\lm nfa$, or more clearly $\lm n.\lm fa$. Do you see why?}
|
||||
Do $f$ $n$ times, then do $f$ one more time.
|
||||
\end{solution}
|
||||
|
||||
\begin{solution}
|
||||
$S = \lm n. [\lm fa . f~(n~f~a)] = \lm nfa . [f~(n~f~a)]$
|
||||
\vfill
|
||||
|
||||
\vspace{1ex}
|
||||
\problem{}
|
||||
Verify that $S(0) = 1$ and $S(1) = 2$.
|
||||
|
||||
Do $f$ $n$ times, then do $f$ one more time.
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Verify that $S(0) = 1$ and $S(1) = 2$.
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
|
||||
Assume that only Church numerals will be passed to the functions in the following problems. \\
|
||||
We make no promises about their output if they're given anything else.
|
||||
Assume that only Church numerals will be passed to the functions in the following problems. \\
|
||||
We make no promises about their output if they're given anything else.
|
||||
|
||||
\problem{}
|
||||
Define a function ADD that adds two Church numerals.
|
||||
\problem{}
|
||||
Define a function ADD that adds two Church numerals.
|
||||
|
||||
\begin{solution}
|
||||
$\text{ADD} = \lm mn . (m~S~n) = \lm mn . (n~S~m)$ \\
|
||||
\end{solution}
|
||||
\begin{solution}
|
||||
$\text{ADD} = \lm mn . (m~S~n) = \lm mn . (n~S~m)$ \\
|
||||
\end{solution}
|
||||
|
||||
\begin{instructornote}
|
||||
Defining \say{equivalence} is a bit tricky. The solution above illustrates the problem pretty well.
|
||||
\begin{instructornote}
|
||||
Defining \say{equivalence} is a bit tricky. The solution above illustrates the problem pretty well.
|
||||
|
||||
\note{Note: The notions of \say{extensional} and \say{intentional} equivalence may be interesting in this context. Do some reading on your own.
|
||||
}
|
||||
\note{Note: The notions of \say{extensional} and \say{intentional} equivalence may be interesting in this context. Do some reading on your own.
|
||||
}
|
||||
|
||||
\vspace{4ex}
|
||||
\vspace{4ex}
|
||||
|
||||
These two definitions of ADD are equivalent if we apply them to Church numerals. If we were to apply these two versions of ADD to functions that behave in a different way, we'll most likely get two different results! \\
|
||||
As a simple example, try applying both versions of ADD to the Kestrel and the Kite.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
To compare functions that aren't $\alpha$-equivalent, we'll need to restrict our domain to functions of a certain form, saying that two functions are equivalent over a certain domain. \\
|
||||
\end{instructornote}
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Adding is nice, but we can do better. \\
|
||||
Design a function MULT that multiplies two numbers. \\
|
||||
\hint{The easy solution uses ADD, the elegant one doesn't. Find both!}
|
||||
|
||||
\begin{solution}
|
||||
$\text{MULT} = \lm mn . [m~(\text{ADD}~n)~m]$
|
||||
|
||||
$\text{MULT} = \lm mnf . [m~(n~f)]$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
|
||||
\problem{}
|
||||
Define the functions $Z$ and $NZ$. $Z$ should reduce to $T$ if its input was zero, and $F$ if it wasn't. \\
|
||||
$NZ$ does the opposite. $Z$ and $NZ$ should look fairly similar.
|
||||
These two definitions of ADD are equivalent if we apply them to Church numerals. If we were to apply these two versions of ADD to functions that behave in a different way, we'll most likely get two different results! \\
|
||||
As a simple example, try applying both versions of ADD to the Kestrel and the Kite.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
\begin{solution}
|
||||
$Z\phantom{N} = \lm n .[n~(\lm a.F)~T]$\\
|
||||
$NZ = \lm n .[n~(\lm a.T)~F]$
|
||||
\end{solution}
|
||||
To compare functions that aren't $\alpha$-equivalent, we'll need to restrict our domain to functions of a certain form, saying that two functions are equivalent over a certain domain. \\
|
||||
\end{instructornote}
|
||||
\vfill
|
||||
|
||||
\vfill
|
||||
\problem{}
|
||||
Adding is nice, but we can do better. \\
|
||||
Design a function MULT that multiplies two numbers. \\
|
||||
\hint{The easy solution uses ADD, the elegant one doesn't. Find both!}
|
||||
|
||||
\problem{}
|
||||
Data structures will be useful. Design an expression PAIR that constructs two-value tuples. \\
|
||||
For example, say $A = \text{PAIR}~1~2$. Then, \\
|
||||
$(A~T)$ should reduce to $1$ \\
|
||||
$(A~F)$ should reduce to $2$
|
||||
\begin{solution}
|
||||
$\text{MULT} = \lm mn . [m~(\text{ADD}~n)~m]$
|
||||
|
||||
\begin{solution}
|
||||
$\text{PAIR} = \lm ab . \lm i . (i~a~b) = \lm abi.iab$
|
||||
\end{solution}
|
||||
$\text{MULT} = \lm mnf . [m~(n~f)]$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
From now on, I'll write (PAIR $A$ $B$) as $\langle A,B \rangle$. \\
|
||||
Like currying, this is only notation. The underlying $\lm$ logic remains the same.
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
\pagebreak
|
||||
|
||||
\problem{}<shiftadd>
|
||||
Write a function $H$, which we'll call \say{shift and add.} \\
|
||||
It does exactly what it says on the tin: \\
|
||||
\problem{}
|
||||
Define the functions $Z$ and $NZ$. $Z$ should reduce to $T$ if its input was zero, and $F$ if it wasn't. \\
|
||||
$NZ$ does the opposite. $Z$ and $NZ$ should look fairly similar.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
\begin{solution}
|
||||
$Z\phantom{N} = \lm n .[n~(\lm a.F)~T]$\\
|
||||
$NZ = \lm n .[n~(\lm a.T)~F]$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Data structures will be useful. Design an expression PAIR that constructs two-value tuples. \\
|
||||
For example, say $A = \text{PAIR}~1~2$. Then, \\
|
||||
$(A~T)$ should reduce to $1$ \\
|
||||
$(A~F)$ should reduce to $2$
|
||||
|
||||
\begin{solution}
|
||||
$\text{PAIR} = \lm ab . \lm i . (i~a~b) = \lm abi.iab$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
From now on, I'll write (PAIR $A$ $B$) as $\langle A,B \rangle$. \\
|
||||
Like currying, this is only notation. The underlying $\lm$ logic remains the same.
|
||||
|
||||
\pagebreak
|
||||
|
||||
\problem{}<shiftadd>
|
||||
Write a function $H$, which we'll call \say{shift and add.} \\
|
||||
It does exactly what it says on the tin: \\
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Given an input pair, it should shift its right argument left, then add one. \\
|
||||
$H~\langle 0, 1 \rangle$ should reduce to $\langle 1, 2\rangle$ \\
|
||||
$H~\langle 1, 2 \rangle$ should reduce to $\langle 2, 3\rangle$ \\
|
||||
$H~\langle 10, 4 \rangle$ should reduce to $\langle 4, 5\rangle$ \\
|
||||
|
||||
\begin{solution}
|
||||
$H = \lm p . \Bigl\langle~(p~F)~,~S(p~F)~\Bigr\rangle$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Given an input pair, it should shift its right argument left, then add one. \\
|
||||
$H~\langle 0, 1 \rangle$ should reduce to $\langle 1, 2\rangle$ \\
|
||||
$H~\langle 1, 2 \rangle$ should reduce to $\langle 2, 3\rangle$ \\
|
||||
$H~\langle 10, 4 \rangle$ should reduce to $\langle 4, 5\rangle$ \\
|
||||
|
||||
\begin{solution}
|
||||
$H = \lm p . \Bigl\langle~(p~F)~,~S(p~F)~\Bigr\rangle$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Note that $H~\langle 0, 0 \rangle$ reduces to $\langle 0, 1 \rangle$
|
||||
\end{solution}
|
||||
Note that $H~\langle 0, 0 \rangle$ reduces to $\langle 0, 1 \rangle$
|
||||
\end{solution}
|
||||
|
||||
|
||||
\vfill
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Design a function $D$ that un-does $S$. That means \\
|
||||
$D(1) = 0$, $D(2) = 1$, etc. $D(0)$ should be zero. \\
|
||||
\hint{$H$ will help you make an elegant solution.}
|
||||
\problem{}
|
||||
Design a function $D$ that un-does $S$. That means \\
|
||||
$D(1) = 0$, $D(2) = 1$, etc. $D(0)$ should be zero. \\
|
||||
\hint{$H$ will help you make an elegant solution.}
|
||||
|
||||
\begin{solution}
|
||||
$D = \lm n . \Bigl[(~n~H~\langle 0, 0 \rangle~)~T\Bigr]$
|
||||
\end{solution}
|
||||
\begin{solution}
|
||||
$D = \lm n . \Bigl[(~n~H~\langle 0, 0 \rangle~)~T\Bigr]$
|
||||
\end{solution}
|
||||
|
||||
\begin{solution}
|
||||
Here's a different solution. \\
|
||||
Can you figure out how it works? \\
|
||||
\begin{solution}
|
||||
Here's a different solution. \\
|
||||
Can you figure out how it works? \\
|
||||
|
||||
\vspace{1ex}
|
||||
\vspace{1ex}
|
||||
|
||||
$
|
||||
D_0 =
|
||||
\lm p . \Bigl[p~T\Bigr]
|
||||
\Bigl\langle
|
||||
F ~,~ p~F
|
||||
\Bigr\rangle
|
||||
\Bigl\langle
|
||||
F
|
||||
~,~
|
||||
\bigl\langle
|
||||
p~F~T ~,~ ( (p~F~T)~(P~F~F) )
|
||||
\bigr\rangle
|
||||
\Bigr\rangle
|
||||
$
|
||||
$
|
||||
D_0 =
|
||||
\lm p . \Bigl[p~T\Bigr]
|
||||
\Bigl\langle
|
||||
F ~,~ p~F
|
||||
\Bigr\rangle
|
||||
\Bigl\langle
|
||||
F
|
||||
~,~
|
||||
\bigl\langle
|
||||
p~F~T ~,~ ( (p~F~T)~(P~F~F) )
|
||||
\bigr\rangle
|
||||
\Bigr\rangle
|
||||
$
|
||||
|
||||
\vspace{1ex}
|
||||
\vspace{1ex}
|
||||
|
||||
$
|
||||
D = \lm nfa .
|
||||
\Bigl(
|
||||
n D_0 \Bigl\langle T, \langle f, a \rangle \Bigr\rangle
|
||||
\Bigr)~F~F
|
||||
$
|
||||
\end{solution}
|
||||
$
|
||||
D = \lm nfa .
|
||||
\Bigl(
|
||||
n D_0 \Bigl\langle T, \langle f, a \rangle \Bigr\rangle
|
||||
\Bigr)~F~F
|
||||
$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
\end{document}
|
||||
\vfill
|
||||
\pagebreak
|
||||
@ -1,67 +1,61 @@
|
||||
\documentclass[../main.tex]{subfiles}
|
||||
\section{Recursion}
|
||||
|
||||
\begin{document}
|
||||
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}
|
||||
$$
|
||||
|
||||
\section{Recursion}
|
||||
We cannot re-create this in lambda notation. Functions in lambda calculus are \textit{anonymous}, which means we can't call them before they've been fully defined.
|
||||
|
||||
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}
|
||||
$$
|
||||
\vspace{1ex}
|
||||
|
||||
We cannot re-create this in lambda notation. Functions in lambda calculus are \textit{anonymous}, which means we can't call them before they've been fully defined.
|
||||
As an example, consider the statement $A = \lm a. A~a$ \\
|
||||
This means \say{write $(\lm a.A~a)$ whenever you see $A$.} However, $A$ is \textit{inside} what we're rewriting. We'd fall into infinite recursion before even starting our $\beta$-reduction!
|
||||
|
||||
\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}
|
||||
|
||||
As an example, consider the statement $A = \lm a. A~a$ \\
|
||||
This means \say{write $(\lm a.A~a)$ whenever you see $A$.} However, $A$ is \textit{inside} what we're rewriting. We'd fall into infinite recursion before even starting our $\beta$-reduction!
|
||||
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}
|
||||
|
||||
\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:}
|
||||
\problem{}
|
||||
Write an expression that resolves to itself. \\
|
||||
\note{Your answer should be short and sweet.}
|
||||
|
||||
\vspace{4ex}
|
||||
\vspace{1ex}
|
||||
|
||||
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. \\
|
||||
This expression is often called $\Omega$, after the last letter of the Greek alphabet. \\
|
||||
$\Omega$ useless on its own, but gives us a starting point for recursion.
|
||||
|
||||
\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. \\
|
||||
\note{Your answer should be short and sweet.}
|
||||
\begin{solution}
|
||||
$\Omega = M~M = (\lm x . xx) (\lm x . xx)$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This expression is often called $\Omega$, after the last letter of the Greek alphabet. \\
|
||||
$\Omega$ useless on its own, but gives us a starting point for recursion.
|
||||
An uninspired mathematician might call the Mockingbird $\omega$, \say{little omega}. \\
|
||||
\end{solution}
|
||||
|
||||
\begin{solution}
|
||||
$\Omega = M~M = (\lm x . xx) (\lm x . xx)$
|
||||
\vfill
|
||||
|
||||
\vspace{1ex}
|
||||
\definition{}
|
||||
This is the \textit{Y-combinator}, easily the most famous $\lm$ expression. \\
|
||||
You may notice that it's just $\Omega$, put to work.
|
||||
$$
|
||||
Y = \lm f . (\lm x . f(x~x))(\lm x . f(x~x))
|
||||
$$
|
||||
|
||||
An uninspired mathematician might call the Mockingbird $\omega$, \say{little omega}. \\
|
||||
\end{solution}
|
||||
\problem{}
|
||||
What does this thing do? \\
|
||||
Evaluate $Y f$.
|
||||
|
||||
\vfill
|
||||
|
||||
\definition{}
|
||||
This is the \textit{Y-combinator}, easily the most famous $\lm$ expression. \\
|
||||
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? \\
|
||||
Evaluate $Y f$.
|
||||
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
\end{document}
|
||||
\vfill
|
||||
\pagebreak
|
||||
|
||||
@ -1,87 +1,82 @@
|
||||
\documentclass[../main.tex]{subfiles}
|
||||
\section{Challenges}
|
||||
|
||||
\begin{document}
|
||||
Do \ref{Yfac} first, then finish the rest in any order. \\
|
||||
Have fun!
|
||||
|
||||
\section{Challenges}
|
||||
\problem{}<Yfac>
|
||||
Design a recursive factorial function using $Y$. \\
|
||||
|
||||
Do \ref{Yfac} first, then finish the rest in any order. \\
|
||||
Have fun!
|
||||
\vfill
|
||||
|
||||
\problem{}<Yfac>
|
||||
Design a recursive factorial function using $Y$. \\
|
||||
\problem{}
|
||||
Design a non-recursive factorial function. \\
|
||||
\note{This one is a lot easier than \ref{Yfac}, but I don't think it will help you solve it.}
|
||||
|
||||
\vfill
|
||||
\problem{}
|
||||
Using pairs, make a \say{list} data structure. Define a GET function, so that $\text{GET}~L~n$ reduces to the nth item in the list. $\text{GET}~L~0$ should give the first item in the list, and $\text{GET}~L~1$, the \textit{second}. \\
|
||||
Lists have a defined length, so you should be able to tell when you're on the last element.
|
||||
|
||||
\problem{}
|
||||
Design a non-recursive factorial function. \\
|
||||
\note{This one is a lot easier than \ref{Yfac}, but I don't think it will help you solve it.}
|
||||
\problem{}
|
||||
Write POW $a$ $b$, which raises $b$ to the $a$th power.
|
||||
|
||||
\problem{}
|
||||
Using pairs, make a \say{list} data structure. Define a GET function, so that $\text{GET}~L~n$ reduces to the nth item in the list. $\text{GET}~L~0$ should give the first item in the list, and $\text{GET}~L~1$, the \textit{second}. \\
|
||||
Lists have a defined length, so you should be able to tell when you're on the last element.
|
||||
\problem{}
|
||||
Write a MOD $a$ $b$ function that reduces to the remainder of $a \div b$.
|
||||
|
||||
\problem{}
|
||||
Write POW $a$ $b$, which raises $b$ to the $a$th power.
|
||||
\begin{solution}
|
||||
\textbf{Factorial with recursion:}
|
||||
\vspace{3ex}
|
||||
|
||||
\problem{}
|
||||
Write a MOD $a$ $b$ function that reduces to the remainder of $a \div b$.
|
||||
$\text{FAC} = \lm yn.[Z~n][1][\text{MULT}~n~(y~(\text{D}~n))]$
|
||||
|
||||
\begin{solution}
|
||||
\textbf{Factorial with recursion:}
|
||||
\vspace{3ex}
|
||||
\linehack{}
|
||||
|
||||
$\text{FAC} = \lm yn.[Z~n][1][\text{MULT}~n~(y~(\text{D}~n))]$
|
||||
\textbf{Factorial without recursion:}
|
||||
\vspace{3ex}
|
||||
|
||||
\linehack{}
|
||||
$\text{FAC}_0 = \lm p .
|
||||
\Bigl\langle~~
|
||||
\Bigl[D~(p~t)\Bigr]
|
||||
~,~
|
||||
\Bigl[\text{MULT}~(p~T)~(p~F)\Bigr]
|
||||
~~\Bigr\rangle
|
||||
$
|
||||
|
||||
\textbf{Factorial without recursion:}
|
||||
\vspace{3ex}
|
||||
\vspace{2ex}
|
||||
|
||||
$\text{FAC}_0 = \lm p .
|
||||
\Bigl\langle~~
|
||||
\Bigl[D~(p~t)\Bigr]
|
||||
$
|
||||
\text{FAC} = \lm n .
|
||||
\bigl( n~\text{FAC}_0~\langle n, 1 \rangle \bigr)
|
||||
$
|
||||
|
||||
\linehack{}
|
||||
|
||||
\textbf{Lists:}
|
||||
\vspace{3ex}
|
||||
|
||||
One possible implementation is
|
||||
$\Bigl\langle
|
||||
\langle \text{is last} ~,~ \text{item} \rangle
|
||||
~,~
|
||||
\Bigl[\text{MULT}~(p~T)~(p~F)\Bigr]
|
||||
~~\Bigr\rangle
|
||||
$
|
||||
\text{next}...
|
||||
\Bigr\rangle$, where:
|
||||
|
||||
\vspace{2ex}
|
||||
\vspace{1ex}
|
||||
|
||||
$
|
||||
\text{FAC} = \lm n .
|
||||
\bigl( n~\text{FAC}_0~\langle n, 1 \rangle \bigr)
|
||||
$
|
||||
\say{is last} is a boolean, true iff this is the last item in the list. \\
|
||||
\say{item} is the thing you're storing \\
|
||||
\say{next...} is another one of these list fragments. \\
|
||||
|
||||
\linehack{}
|
||||
It doesn't matter what \say{next} is in the last list fragment. A dedicated \say{is last} slot allows us to store ANY function in this list.
|
||||
|
||||
\textbf{Lists:}
|
||||
\vspace{3ex}
|
||||
\vspace{1ex}
|
||||
|
||||
One possible implementation is
|
||||
$\Bigl\langle
|
||||
\langle \text{is last} ~,~ \text{item} \rangle
|
||||
~,~
|
||||
\text{next}...
|
||||
\Bigr\rangle$, where:
|
||||
Here, $\text{GET} = \lm nL.[(n~L~F)~T~F$] \\
|
||||
|
||||
\vspace{1ex}
|
||||
This will break if $n$ is out of range.
|
||||
\end{solution}
|
||||
|
||||
\say{is last} is a boolean, true iff this is the last item in the list. \\
|
||||
\say{item} is the thing you're storing \\
|
||||
\say{next...} is another one of these list fragments. \\
|
||||
\vfill
|
||||
|
||||
It doesn't matter what \say{next} is in the last list fragment. A dedicated \say{is last} slot allows us to store ANY function in this list.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Here, $\text{GET} = \lm nL.[(n~L~F)~T~F$] \\
|
||||
|
||||
This will break if $n$ is out of range.
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{Bonus}
|
||||
Play with \textit{Lamb}, an automatic lambda expression evaluator. \\
|
||||
\url{https://git.betalupi.com/Mark/lamb}
|
||||
\end{document}
|
||||
\problem{Bonus}
|
||||
Play with \textit{Lamb}, an automatic lambda expression evaluator. \\
|
||||
\url{https://git.betalupi.com/Mark/lamb}
|
||||
Loading…
x
Reference in New Issue
Block a user