Improved currying section

Advanced/Lambda Calculus/parts/00 intro.tex

@@ -234,6 +234,71 @@ Remember that lambda calculus is left-associative.
 
 
 
+
+
+\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
+
+\begin{instructornote}
+
+	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.
+
+\end{instructornote}
+
+
+
+\definition{}
+Let $K = \lm a. (\lm b . a)$. We'll call $K$ the \say{constant function function.}
+
+\problem{}
+That's not a typo. Why does this name make sense? \par
+\hint{What is $K~x$?}
+
+\begin{solution}
+	$K x = \lm a . x$, which is a constant function that always outputs $x$. \par
+	Given an argument, $K$ returns a constant function with that value. 
+\end{solution}
+
+\vfill
+
+\problem{}
+Show that associativity matters by evaluating $\bigl((M~K)~I\bigr)$ and $\bigl(M~(K~I)\bigr)$. \par
+What would $M~K~I$ reduce to?
+
+\begin{solution}
+	$\bigl((M~K)~I\bigr) = (K~K)~I = (\lm a.K)~I = K$ \par
+	$\bigl(M~(K~I)\bigr) = M~(\lm a.I) = (\lm a.I)(\lm a.I) = I$
+\end{solution}
+
+
+\vfill
+\pagebreak
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 \generic{Currying:}
 
 In lambda calculus, functions are only allowed to take one argument. \par
@@ -248,44 +313,20 @@ If we want multivariable functions, we'll have to emulate them through \textit{c
 \vspace{1ex}
 
 The idea behind currying is fairly simple: we make functions that return functions. \par
-Consider the expression $A$ below. It takes one input $f$ and returns the function $\lm a. f~(f~a)$ (underlined).
+We've already seen this on the previous page: $K$ takes an input $x$ and uses it to construct a constant function.
-$$
+You can think of $K$ as a \say{factory} that constructs functions using the input we provide.
-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 give it. \par
-For example, let's apply $A$ to an arbirary function $n$:
-$$
-	A~n =
-	\lm f.(~\lm a.\tzm{b}f~(\tzm{c}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);
-		\draw[->,gray,shorten >=5pt,shorten <=3pt]
-			(a.center) to (c.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 provide.
 
 \problem{}<firstcardinal>
-Let $C = \lm f. \Bigl[\lm g. \Bigl( \lm x. [~ g(f(x)) ~] \Bigr)\Bigr]$. What does $C$ do? \par
+Let $C = \lm f. \Bigl[\lm g. \Bigl( \lm x. [~ g(f(x)) ~] \Bigr)\Bigr]$. For now, we'll call it the \say{composer.}
-Evaluate $(C~a~b~x)$ for arbitary expressions $a$ and $b$. \par
+
+\vspace{1mm}
+
+Note that $C$ has three \say{layers} of curry: it makes a function ($\lm g$) that makes another function ($\lm x$). \par
+If we look closely, we'll find that $C$ pretends to take three arguments.
+
+\vspace{1mm}
+
+What does $C$ do? Evaluate $(C~a~b~x)$ for arbitary expressions $a, b,$ and $x$. \par
 \hint{Place parentheses first. Remember, function application is left-associative.}
 
 \vfill
@@ -335,28 +376,6 @@ Substituting all curried variables at once will cause errors.
 
 
 
-
-
-
-
-
-
-\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
-
-\begin{instructornote}
-
-	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.
-
-\end{instructornote}
-
 
 
 %\iftrue