\documentclass[../main.tex]{subfiles}


\begin{document}

	\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 a . a) ~ \star = \star
	$$

	$$
	(M~\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

\end{document}