235 lines
6.0 KiB
TeX
Executable File
235 lines
6.0 KiB
TeX
Executable File
\section{Definitions}
|
|
|
|
\generic{$\lm$ Notation:}
|
|
$\lm$ notation is used to define functions, and looks like $(\lm ~ \text{input} ~ . ~ \text{output})$. \par
|
|
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)$ \par
|
|
In this handout, all types of parentheses ( $(), [~],$ etc ) are equivalent.
|
|
|
|
\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}.
|
|
|
|
\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$. \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:
|
|
$$
|
|
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}~~)
|
|
\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. \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
|
|
\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 variables separate.
|
|
|
|
For example, take the functions \par
|
|
$A = \lm a b . a$ \par
|
|
$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$ \par
|
|
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 |