From 22535a8183847ab75af1374616ec45d50aa0a7f2 Mon Sep 17 00:00:00 2001 From: Mark Date: Mon, 16 Oct 2023 16:06:39 -0700 Subject: [PATCH] Reworked introduction --- Advanced/Lambda Calculus/parts/00 intro.tex | 234 +++++++++++++------- 1 file changed, 148 insertions(+), 86 deletions(-) diff --git a/Advanced/Lambda Calculus/parts/00 intro.tex b/Advanced/Lambda Calculus/parts/00 intro.tex index 66b3e81..a28e14e 100755 --- a/Advanced/Lambda Calculus/parts/00 intro.tex +++ b/Advanced/Lambda Calculus/parts/00 intro.tex @@ -28,15 +28,39 @@ Functions are left-associative: If $A$ and $B$ are functions, $(A~B~\star)$ is e 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. - -Let's make another function: +$\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 $$ -$M$ takes a function as an input and calls it on itself. What is $(M~I)$? +The function $M$ simply repeats its input. What is $(M~I)$? $$ (M~I) = ((\lm \tzm{b}f.f f)~\tzmr{a}I) = @@ -56,7 +80,9 @@ $$ (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}. +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: @@ -70,99 +96,142 @@ Reduce the following expressions: \vfill \pagebreak + + + + + + + + + + + + + + + \generic{Currying:} -Lambda functions are only allowed to take one argument, but we can emulate multivariable functions through \say{currying.} +In lambda calculus, functions are only allowed to take one argument. +However, we can emulate multivariable functions through \textit{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$. \par -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: +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). $$ - C = \lm f . (\lm g . (\lm x . f(g(x)))) -$$ - -\vspace{1ex} - -This looks awfully scary, so let's take this expression apart. \par -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}~~) +A = \lm f .(\tzm{a} ~ \lm a . f(f(a)) ~ \tzm{b}) \begin{tikzpicture}[ overlay, remember picture ] - \node[below = 1ex] at (a.center) (aa) {}; - \node[below = 1ex] at (b.center) (bb) {}; + \node[below = 0.8mm] at (a.center) (aa) {}; + \node[below = 0.8mm] 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: +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$: $$ -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} + 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. -\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. \par -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$ \par -Then, evaluate $C~I~M~I$ \par +\problem{} +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{$\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 = ...$ + + + + + + + + + + + + + + + + + + + + + + + + +\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. @@ -190,29 +259,22 @@ $$ $$ 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} -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 -$$ - +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 $C = \lm abc.b$ \par -Reduce $(C~a~c~b)$. +Let $Q = \lm abc.b$ \par +Reduce $(Q~a~c~b)$. \begin{solution} - I'll rewrite $(C~a~c~b)$ as $(C~a_1~c_1~b_1)$: + I'll rewrite $(Q~a~c~b)$ as $(Q~a_1~c_1~b_1)$: \begin{align*} - C = (\lm abc.b) &= (\lm a.\lm b.\lm c.b) \\ + 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