210 lines
5.5 KiB
TeX
Executable File
210 lines
5.5 KiB
TeX
Executable File
\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 ...)
|
|
|
|
\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}. \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
|
|
$$
|
|
If you look closely, you'll find that $0$ is 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: \par
|
|
$1 = \lm fa . (f~a)$.
|
|
|
|
\vspace{1ex}
|
|
|
|
Naturally, \par
|
|
$2 = \lm fa . [~f~(f~a)~]$ \par
|
|
$3 = \lm fa . [~f~(f~(f~a))~]$
|
|
|
|
\vspace{1ex}
|
|
|
|
The round parentheses are \textit{essential}. Our lambda calculus is left-associative! \par
|
|
Also, note that zero is false and one is the (two-variable) identity.
|
|
\end{solution}
|
|
|
|
\vfill
|
|
|
|
\problem{}
|
|
What is $(4~I)~\star$?
|
|
|
|
\vfill
|
|
|
|
\problem{}
|
|
What is $(3~NOT~T)$? \par
|
|
How about $(8~NOT~F)$?
|
|
|
|
\vfill
|
|
|
|
\pagebreak
|
|
|
|
\problem{}
|
|
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. \par
|
|
\hint{A good signature for this function is $\lm nfa$, or more clearly $\lm n.\lm fa$. Do you see why?}
|
|
|
|
\begin{solution}
|
|
$S = \lm n. [\lm fa . f~(n~f~a)] = \lm nfa . [f~(n~f~a)]$
|
|
|
|
\vspace{1ex}
|
|
|
|
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
|
|
|
|
|
|
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)$
|
|
\end{solution}
|
|
|
|
\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.
|
|
}
|
|
|
|
\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{}
|
|
Design a function MULT that multiplies two numbers. \par
|
|
\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. \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]$ \par
|
|
$NZ = \lm n .[n~(\lm a.T)~F]$
|
|
\end{solution}
|
|
|
|
\vfill
|
|
|
|
\problem{}
|
|
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$ and $(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$. \par
|
|
Like currying, this is only notation. The underlying logic remains the same.
|
|
|
|
\pagebreak
|
|
|
|
\problem{}<shiftadd>
|
|
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 second 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$
|
|
|
|
\vspace{1ex}
|
|
|
|
Note that $H~\langle 0, 0 \rangle$ reduces to $\langle 0, 1 \rangle$
|
|
\end{solution}
|
|
|
|
|
|
\vfill
|
|
|
|
\problem{}<decrement>
|
|
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}
|
|
$D = \lm n . \Bigl[(~n~H~\langle 0, 0 \rangle~)~T\Bigr]$
|
|
\end{solution}
|
|
|
|
\begin{solution}
|
|
Here's a different solution. \par
|
|
Can you figure out how it works?
|
|
|
|
\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
|
|
$
|
|
|
|
\vspace{1ex}
|
|
|
|
$
|
|
D = \lm nfa .
|
|
\Bigl(
|
|
n D_0 \Bigl\langle T, \langle f, a \rangle \Bigr\rangle
|
|
\Bigr)~F~F
|
|
$
|
|
\end{solution}
|
|
|
|
\vfill
|
|
\pagebreak |