Reworked introduction
This commit is contained in:
parent
b093e368e5
commit
22535a8183
GPG Key ID:
AD62BB059C2AAEE4
@ -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}[
|
||||
A~N =
|
||||
\lm \tzm{b}f.(~\lm a.f(f(a))~)~\tzmr{a}N =
|
||||
\lm a.N(N(a))
|
||||
\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}
|
||||
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{}<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{$\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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user