handouts/Advanced/Lambda Calculus/parts/00 intro.tex

\section{Definitions}

\generic{$\lm$ Notation:}
$\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}.

To apply functions, put them next to their inputs. We'll omit the usual parentheses to save space.
$$
(I~\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}
$$
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.


\problem{}
Rewrite the following expressions with as few parentheses as possible, without changing their meaning or structure.
Remember that lambda calculus is left-associative.
\vspace{2mm}
\begin{itemize}[itemsep=2mm]
	\item $(\lm x. (\lm y. \lm (z. ((xz)(yz)))))$
	\item $((ab)(cd))((ef)(gh))$
	\item $(\lm x. ((\lm y.(yx))(\lm v.v)z)u) (\lm w.w)$
\end{itemize}


\vfill
\pagebreak











\generic{$\beta$-Reduction:}

$\beta$-reduction is a fancy name for \say{simplifying an expression.} We've already done it once above,
while evaluating $(I \star)$. Let's make another function:
$$
	M = \lm f . f f
$$
The function $M$ simply repeats its input. 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 go any further, so we stop. Our expression is now in \textit{$\beta$-normal} or \say{reduced} form.



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

In lambda calculus, functions are only allowed to take one argument.
However, we can emulate multivariable functions through \textit{currying}\footnotemark{}\hspace{-1ex}.

\footnotetext{After Haskell Brooks Curry\footnotemark{}\hspace{-1ex}, a logician that contributed to the theory of functional computation.}
\footnotetext{
	There are three programming languages named after him: Haskell, Brook, and Curry. \par
	Two of these are functional, and one is an oddball GPU language last released in 2007.
}

\vspace{1ex}

The idea behind currying is fairly simple: we make functions that return functions. \par
Consider the expression $A$ below. As before, it takes one input $f$ and returns the function $\lm a. f(f(a))$ (underlined).
$$
A = \lm f .(\tzm{a} ~ \lm a . f(f(a)) ~ \tzm{b})
\begin{tikzpicture}[
	overlay,
	remember picture
]
	\node[below = 0.8mm] at (a.center) (aa) {};
	\node[below = 0.8mm] at (b.center) (bb) {};

	\path[draw = gray] (aa) to (bb);
\end{tikzpicture}
$$
When we evaluate $A$ with one input, it constructs a new function with the argument we gave it. \par
For example, let's apply $A$ to an arbirary function $N$:
$$
	A~N =
	\lm \tzm{b}f.(~\lm a.f(f(a))~)~\tzmr{a}N =
	\lm a.N(N(a))
	\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}
$$
Above, $A$ replaced every $f$ in its definition with an $N$. \par
You can think of $A$ as a \say{factory} that constructs functions using the inputs we gave it.

\problem{}<firstcardinal>
Let $C = \lm f. (\lm g. \lm x. (g(f(x))))$. What does $B$ do? \par
Evaluate $(C~a~b~x)$ for arbitary expressions $a$ and $b$. \par
\hint{Place parentheses first. Remember, function application is left-associative.}

\vfill

\problem{}
Using the definition of $C$ above, evaluate $C~M~I~\star$ \par
Then, evaluate $C~I~M~I$ \par

\vfill

As we saw above, currying allows us to create multivariable functions by nesting single-variable functions.
You may have notice that curried 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, $A = \lm f . (\lm a . f(f(a)))$ will become $A = \lm fa . f(f(a))$

\problem{}
Rewrite $C = \lm f. (\lm g. \lm x. (g(f(x))))$ from \ref{firstcardinal} using this shorthand.

\vspace{25mm}

Remember that this is only notation. \textbf{Curried functions are not multivariable functions, they are simply shorthand!}
Any function presented with this notation must still be evaluated one variable at a time, just like an un-curried function.
Substituting all curried variables at once may cause errors, as we'll see below.

\pagebreak


























\definition{Equivalence}
We say two functions are \textit{equivalent} if they differ only by the names of their variables:
$I = \lm a.a = \lm b.b = \lm \heartsuit . \heartsuit = ...$ \par

\vspace{2mm}

The idea behind this is very similar to the idea behind \say{equivalent groups} in group theory: \par
we do not care which symbols a certain group or function uses, we care about their \textit{structure}. \par

\vspace{2mm}

If we have two groups with different elements with the same multiplication table, we look at them as identical groups.
The same is true of lambda functions: two lambda functions with different variable names that behave in the same way are identical.


\vspace{4mm}


\generic{$\alpha$-Conversion:}
There is one more operation we need to discuss. Those of you that have worked with any programming language may
find that this section sounds like something you've seen before.

\vspace{2mm}

Variables inside functions are \say{scoped.} We must take care to keep separate variables separate.

For example, take the functions \par
$A = \lm a b . a$ \par
$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.
Both $A$ and $B$ use the input $b$. However, each $b$ is \say{bound} to a different function:
One $b$ is bound to $A$, and the other to $B$. They are therefore distinct.

\vspace{2ex}

Let's rewrite $B$ as $\lm b_1 . b_1$ and try again: $(A~B) = \lm b . ( \lm b_1 . b_1) = \lm bb_1 . b_1$ \par
Now, we correctly find that $(A~B~I) = (\lm bc . c)~I = \lm c . c = B = I$.

\problem{}
Let $Q = \lm abc.b$ \par
Reduce $(Q~a~c~b)$.

\begin{solution}
	I'll rewrite $(Q~a~c~b)$ as $(Q~a_1~c_1~b_1)$:
	\begin{align*}
		Q = (\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