Minor cleanup
This commit is contained in:
parent
0744a88c00
commit
ab410dbe74
@ -1,13 +1,13 @@
|
||||
\section{Definitions}
|
||||
|
||||
\generic{$\lm$ Notation:}
|
||||
$\lm$ notation is used to define functions, and looks like $(\lm ~ \text{input} ~ . ~ \text{output})$. \\
|
||||
$\lm$ notation is used to define functions, and looks like $(\lm ~ \text{input} ~ . ~ \text{output})$. \par
|
||||
Consider the following statement:
|
||||
$$
|
||||
I = \lm a . a
|
||||
$$
|
||||
|
||||
This tells us that $I$ is a function that takes its input, $a$, to itself. We'll call this the \textit{identity function}. \\
|
||||
This tells us that $I$ is a function that takes its input, $a$, to itself. We'll call this the \textit{identity function}.
|
||||
|
||||
To apply functions, put them next to their inputs. We'll omit the usual parentheses to save space.
|
||||
|
||||
@ -27,7 +27,8 @@ $$
|
||||
\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)$ \\
|
||||
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)$ \par
|
||||
In this handout, all types of parentheses ( $(), [],$ etc ) are equivalent.
|
||||
|
||||
\vfill
|
||||
@ -88,8 +89,7 @@ Before we begin, let's review \textit{function composition}. With \say{normal} f
|
||||
|
||||
\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$. \\
|
||||
|
||||
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$. \par
|
||||
In other words, we want a $C$ so that $C~f~g~x = f~(g~x)$
|
||||
|
||||
\vspace{1ex}
|
||||
@ -101,7 +101,7 @@ $$
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This looks awfully scary, so let's take this expression apart. \\
|
||||
This looks awfully scary, so let's take this expression apart. \par
|
||||
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}~~)
|
||||
@ -138,7 +138,7 @@ This last function $\lm x. f(g(x))$ takes one argument, and returns $f(g(x))$. S
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
So, currying allows us to create multivariable functions by nesting single-variable functions. \\
|
||||
So, currying allows us to create multivariable functions by nesting single-variable functions. \par
|
||||
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}
|
||||
@ -154,11 +154,12 @@ $$
|
||||
|
||||
\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.
|
||||
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$ \\
|
||||
Evaluate $C~M~I~\star$ \par
|
||||
Then, evaluate $C~I~M~I$ \par
|
||||
\hint{Place parentheses first. Remember, function application is left-associative.}
|
||||
|
||||
|
||||
@ -174,8 +175,8 @@ $I = \lm a.a = \lm b.b = \lm \heartsuit . \heartsuit = ...$
|
||||
|
||||
Variables inside functions are \say{scoped.} We must take care to keep separate variables separate.
|
||||
|
||||
For example, take the functions \\
|
||||
$A = \lm a b . a$ \\
|
||||
For example, take the functions \par
|
||||
$A = \lm a b . a$ \par
|
||||
$B = \lm b . b$
|
||||
|
||||
\vspace{2ex}
|
||||
@ -214,7 +215,7 @@ $$
|
||||
Now, we correctly find that $(A~B~I) = (\lm bc . c)~I = \lm c . c = B = I$.
|
||||
|
||||
\problem{}
|
||||
Let $C = \lm abc.b$ \\
|
||||
Let $C = \lm abc.b$ \par
|
||||
Reduce $(C~a~c~b)$.
|
||||
|
||||
\begin{solution}
|
||||
|
@ -1,17 +1,17 @@
|
||||
\section{Combinators}
|
||||
|
||||
\definition{}
|
||||
A \textit{free variable} in a $\lm$-expression is a variable that isn't bound to any input. \\
|
||||
A \textit{free variable} in a $\lm$-expression is a variable that isn't bound to any input. \par
|
||||
For example, $b$ is a free variable in $\lm a. b$. The same is true of $\star$ in any of the previous pages.
|
||||
|
||||
A \textit{combinator} is a function with no free variables.
|
||||
|
||||
\definition{The Kestrel}
|
||||
|
||||
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)) ~)$ \\
|
||||
Notable combinators are often named after birds.\hspace{-0.5ex}\footnotemark{} We've already met a few: \par
|
||||
The \textit{Idiot}, $I = \lm a.a$ \par
|
||||
The \textit{Mockingbird}, $M = \lm f.ff$ \par
|
||||
The \textit{Cardinal}, $C = \lm fgx.(~ f(g(x)) ~)$
|
||||
|
||||
\footnotetext{Raymond Smullyan's \textit{To Mock a Mockingbird} is responsible for this.}
|
||||
|
||||
@ -22,17 +22,17 @@ $$
|
||||
K = \lm ab . a
|
||||
$$
|
||||
\problem{}
|
||||
What does the Kestrel do? Explain in plain English. \\
|
||||
What does the Kestrel do? Explain in plain English. \par
|
||||
\hint{What is $(K~\heartsuit~\star)$?}
|
||||
|
||||
\vspace{2cm}
|
||||
|
||||
\problem{}
|
||||
Reduce $(K~I)$ to derive the \textit{Kite}. How does the Kite compare to the Kestrel? \\
|
||||
Reduce $(K~I)$ to derive the \textit{Kite}. How does the Kite compare to the Kestrel? \par
|
||||
We'll call the Kite KI.
|
||||
|
||||
\begin{solution}
|
||||
$\text{KI} = \lm ab . b$. \\
|
||||
$\text{KI} = \lm ab . b$.
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
@ -4,16 +4,16 @@ The Kestrel selects its first argument, and the Kite selects its second. This \s
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Let $T = K\phantom{I} = \lm ab . a$ \\
|
||||
Let $F = KI = \lm ab . b$ \\
|
||||
Let $T = K\phantom{I} = \lm ab . a$ \par
|
||||
Let $F = KI = \lm ab . b$
|
||||
|
||||
\problem{}
|
||||
Write a function $\text{NOT}$ so that $(\text{NOT} ~ T) = F$ and $(\text{NOT}~F) = T$. \\
|
||||
Write a function $\text{NOT}$ so that $(\text{NOT} ~ T) = F$ and $(\text{NOT}~F) = T$. \par
|
||||
\hint{What is $(T~\heartsuit~\star)$? How about $(F~\heartsuit~\star)$?}
|
||||
|
||||
|
||||
\begin{solution}
|
||||
$\text{NOT} = \lm a . (a~F~T)$ \\
|
||||
$\text{NOT} = \lm a . (a~F~T)$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
@ -51,7 +51,7 @@ Write functions $\text{AND}$, $\text{OR}$, and $\text{XOR}$ that satisfy the fol
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
To complete our boolean algebra, write the boolean equality check EQ. \\
|
||||
To complete our boolean algebra, write the boolean equality check EQ. \par
|
||||
What inputs should it take? What outputs should it produce?
|
||||
|
||||
\begin{solution}
|
||||
|
@ -1,10 +1,10 @@
|
||||
\section{Numbers}
|
||||
|
||||
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 ...) \\
|
||||
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 ...)
|
||||
|
||||
\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}. \\
|
||||
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}. \par
|
||||
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
|
||||
@ -18,13 +18,13 @@ Write $1$, $2$, and $3$. We will call these \textit{Church numerals}.\hspace{-0.
|
||||
\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$ calls a function once on its argument: \par
|
||||
$1 = \lm fa . (f~a)$.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Naturally, \\
|
||||
$2 = \lm fa . [~f~(f~a)~]$ \\
|
||||
Naturally, \par
|
||||
$2 = \lm fa . [~f~(f~a)~]$ \par
|
||||
$3 = \lm fa . [~f~(f~(f~a))~]$
|
||||
|
||||
\vspace{1ex}
|
||||
@ -49,7 +49,7 @@ What is $(4~I)~\star$?
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
What is $(3~NOT~T)$? \\
|
||||
What is $(3~NOT~T)$? \par
|
||||
How about $(8~NOT~F)$?
|
||||
|
||||
\vfill
|
||||
@ -57,13 +57,13 @@ How about $(8~NOT~F)$?
|
||||
\pagebreak
|
||||
|
||||
\problem{}
|
||||
This handout may remind you of Professor Oleg's handout on Peano's axioms. Good. \\
|
||||
Recall the tools we used to build the natural numbers: \\
|
||||
This handout may remind you of Professor Oleg's handout on Peano's axioms. Good. \par
|
||||
Recall the tools we used to build the natural numbers: \par
|
||||
We had a zero element and a \say{successor} operation so that $1 \coloneqq S(0)$, $2 \coloneqq S(1)$, and so on.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
Create a successor operation for the Church numerals. \\
|
||||
Create a successor operation for the Church numerals. \par
|
||||
\hint{A good signature for this function is $\lm nfa$, or more clearly $\lm n.\lm fa$. Do you see why?}
|
||||
|
||||
\begin{solution}
|
||||
@ -83,14 +83,14 @@ Verify that $S(0) = 1$ and $S(1) = 2$.
|
||||
\pagebreak
|
||||
|
||||
|
||||
Assume that only Church numerals will be passed to the functions in the following problems. \\
|
||||
Assume that only Church numerals will be passed to the functions in the following problems. \par
|
||||
We make no promises about their output if they're given anything else.
|
||||
|
||||
\problem{}
|
||||
Define a function ADD that adds two Church numerals.
|
||||
|
||||
\begin{solution}
|
||||
$\text{ADD} = \lm mn . (m~S~n) = \lm mn . (n~S~m)$ \\
|
||||
$\text{ADD} = \lm mn . (m~S~n) = \lm mn . (n~S~m)$
|
||||
\end{solution}
|
||||
|
||||
\begin{instructornote}
|
||||
@ -111,8 +111,8 @@ Define a function ADD that adds two Church numerals.
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Adding is nice, but we can do better. \\
|
||||
Design a function MULT that multiplies two numbers. \\
|
||||
Adding is nice, but we can do better. \par
|
||||
Design a function MULT that multiplies two numbers. \par
|
||||
\hint{The easy solution uses ADD, the elegant one doesn't. Find both!}
|
||||
|
||||
\begin{solution}
|
||||
@ -126,22 +126,22 @@ Design a function MULT that multiplies two numbers. \\
|
||||
|
||||
|
||||
\problem{}
|
||||
Define the functions $Z$ and $NZ$. $Z$ should reduce to $T$ if its input was zero, and $F$ if it wasn't. \\
|
||||
Define the functions $Z$ and $NZ$. $Z$ should reduce to $T$ if its input was zero, and $F$ if it wasn't. \par
|
||||
$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]$\\
|
||||
$Z\phantom{N} = \lm n .[n~(\lm a.F)~T]$ \par
|
||||
$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$ \\
|
||||
Data structures will be useful. Design an expression PAIR that constructs two-value tuples. \par
|
||||
For example, say $A = \text{PAIR}~1~2$. Then, \par
|
||||
$(A~T)$ should reduce to $1$ \par
|
||||
$(A~F)$ should reduce to $2$
|
||||
|
||||
\begin{solution}
|
||||
@ -149,21 +149,21 @@ $(A~F)$ should reduce to $2$
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
From now on, I'll write (PAIR $A$ $B$) as $\langle A,B \rangle$. \\
|
||||
From now on, I'll write (PAIR $A$ $B$) as $\langle A,B \rangle$. \par
|
||||
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: \\
|
||||
Write a function $H$, which we'll call \say{shift and add.} \par
|
||||
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$ \\
|
||||
Given an input pair, it should shift its right argument left, then add one. \par
|
||||
$H~\langle 0, 1 \rangle$ should reduce to $\langle 1, 2\rangle$ \par
|
||||
$H~\langle 1, 2 \rangle$ should reduce to $\langle 2, 3\rangle$ \par
|
||||
$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$
|
||||
@ -177,8 +177,8 @@ $H~\langle 10, 4 \rangle$ should reduce to $\langle 4, 5\rangle$ \\
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Design a function $D$ that un-does $S$. That means \\
|
||||
$D(1) = 0$, $D(2) = 1$, etc. $D(0)$ should be zero. \\
|
||||
Design a function $D$ that un-does $S$. That means \par
|
||||
$D(1) = 0$, $D(2) = 1$, etc. $D(0)$ should be zero. \par
|
||||
\hint{$H$ will help you make an elegant solution.}
|
||||
|
||||
\begin{solution}
|
||||
@ -186,8 +186,8 @@ $D(1) = 0$, $D(2) = 1$, etc. $D(0)$ should be zero. \\
|
||||
\end{solution}
|
||||
|
||||
\begin{solution}
|
||||
Here's a different solution. \\
|
||||
Can you figure out how it works? \\
|
||||
Here's a different solution. \par
|
||||
Can you figure out how it works?
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
|
@ -12,7 +12,7 @@ We cannot re-create this in lambda notation. Functions in lambda calculus are \t
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
As an example, consider the statement $A = \lm a. A~a$ \\
|
||||
As an example, consider the statement $A = \lm a. A~a$ \par
|
||||
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}
|
||||
@ -20,7 +20,7 @@ This means \say{write $(\lm a.A~a)$ whenever you see $A$.} However, $A$ is \text
|
||||
|
||||
\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. \\
|
||||
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}
|
||||
|
||||
@ -28,12 +28,12 @@ This means \say{write $(\lm a.A~a)$ whenever you see $A$.} However, $A$ is \text
|
||||
\end{instructornote}
|
||||
|
||||
\problem{}
|
||||
Write an expression that resolves to itself. \\
|
||||
Write an expression that resolves to itself. \par
|
||||
\note{Your answer should be short and sweet.}
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
This expression is often called $\Omega$, after the last letter of the Greek alphabet. \\
|
||||
This expression is often called $\Omega$, after the last letter of the Greek alphabet. \par
|
||||
$\Omega$ useless on its own, but gives us a starting point for recursion.
|
||||
|
||||
\begin{solution}
|
||||
@ -41,20 +41,20 @@ $\Omega$ useless on its own, but gives us a starting point for recursion.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
An uninspired mathematician might call the Mockingbird $\omega$, \say{little omega}. \\
|
||||
An uninspired mathematician might call the Mockingbird $\omega$, \say{little omega}.
|
||||
\end{solution}
|
||||
|
||||
\vfill
|
||||
|
||||
\definition{}
|
||||
This is the \textit{Y-combinator}, easily the most famous $\lm$ expression. \\
|
||||
This is the \textit{Y-combinator}, easily the most famous $\lm$ expression. \par
|
||||
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? \\
|
||||
What does this thing do? \par
|
||||
Evaluate $Y f$.
|
||||
|
||||
\vfill
|
||||
|
@ -1,18 +1,19 @@
|
||||
\section{Challenges}
|
||||
|
||||
Do \ref{Yfac} first, then finish the rest in any order. \\
|
||||
Do \ref{Yfac} first, then finish the rest in any order.
|
||||
|
||||
\problem{}<Yfac>
|
||||
Design a recursive factorial function using $Y$. \\
|
||||
Design a recursive factorial function using $Y$.
|
||||
|
||||
\vfill
|
||||
|
||||
\problem{}
|
||||
Design a non-recursive factorial function. \\
|
||||
Design a non-recursive factorial function. \par
|
||||
\note{This one is a lot easier than \ref{Yfac}, but I don't think it will help you solve it.}
|
||||
|
||||
\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}. \\
|
||||
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}. \par
|
||||
Lists have a defined length, so you should be able to tell when you're on the last element.
|
||||
|
||||
\problem{}
|
||||
@ -61,15 +62,15 @@ Write a MOD $a$ $b$ function that reduces to the remainder of $a \div b$.
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
\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. \\
|
||||
\say{is last} is a boolean, true iff this is the last item in the list. \par
|
||||
\say{item} is the thing you're storing \par
|
||||
\say{next...} is another one of these list fragments.
|
||||
|
||||
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$] \\
|
||||
Here, $\text{GET} = \lm nL.[(n~L~F)~T~F$]
|
||||
|
||||
This will break if $n$ is out of range.
|
||||
\end{solution}
|
||||
@ -77,5 +78,5 @@ Write a MOD $a$ $b$ function that reduces to the remainder of $a \div b$.
|
||||
\vfill
|
||||
|
||||
\problem{Bonus}
|
||||
Play with \textit{Lamb}, an automatic lambda expression evaluator. \\
|
||||
Play with \textit{Lamb}, an automatic lambda expression evaluator. \par
|
||||
\url{https://git.betalupi.com/Mark/lamb}
|
Loading…
x
Reference in New Issue
Block a user