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})$. \\
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)$ \\
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);
\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