handouts/Advanced/Lambda Calculus/parts/03 numbers.tex

\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}. \\
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}

	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$:
	$$
		I~\heartsuit~\star = 1~\heartsuit~\star
	$$

	Zero is false, and one is the identity. Isn't that wonderful?
\end{solution}

\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. \\
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.

\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?}

\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. \\
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{}
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.

\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}

	Note that $H~\langle 0, 0 \rangle$ reduces to $\langle 0, 1 \rangle$
\end{solution}


\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.}

\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? \\

	\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