More edits
This commit is contained in:
parent
887b6de1d6
commit
8ffa0b644a
@ -67,7 +67,7 @@ $$
|
||||
$$
|
||||
This is very similar to the usual way we call functions: we usually write $f(5)$. \par
|
||||
Above, we define our function $f$ \say{in-line} using lambda notation, \par
|
||||
and we ommit the parentheses around 5 for the sake of simpler notation.
|
||||
and we omit the parentheses around 5 for the sake of simpler notation.
|
||||
|
||||
|
||||
\vspace{2mm}
|
||||
@ -147,8 +147,13 @@ The first \say{pure} functions we'll define are $I$ and $M$:
|
||||
\item $I = \lm x . x$
|
||||
\item $M = \lm x . x x$
|
||||
\end{itemize}
|
||||
Both $I$ and $M$ take one function ($x$) as an input. \par
|
||||
$I$ does nothing, it just returns $x$. \par
|
||||
$M$ is a bit more interesting: it applies the function $x$ on a copy of itself.
|
||||
|
||||
Note that $I$ and $M$ don't have a meaning on their own. They are not formal functions. \par
|
||||
\vspace{4mm}
|
||||
|
||||
Also, note that $I$ and $M$ don't have a meaning on their own. They are not formal functions. \par
|
||||
Rather, they are abbreviations that say \say{write $\lm x.x$ whenever you see $I$.}
|
||||
|
||||
|
||||
@ -163,11 +168,38 @@ Reduce the following expressions. \par
|
||||
|
||||
\begin{itemize}[itemsep=2mm]
|
||||
\item $I~I$
|
||||
\item $M~I$
|
||||
\item $(I~I)~I$
|
||||
\item $\Bigl(~ \lm a .(a~(a~a)) ~\Bigr) ~ I$
|
||||
\item $\Bigl(~(\lm a . (\lm b . a)) ~ M~\Bigr) ~ I$
|
||||
\end{itemize}
|
||||
|
||||
\begin{examplesolution}
|
||||
\textbf{Solution for $(I~I)$:}\par
|
||||
Recall that $I = \lm x.x$. First, we rewrite the left $I$ to get $(\lm x . x )~I$. \par
|
||||
Applying this function by replacing $x$ with $I$, we get $I$:
|
||||
|
||||
$$
|
||||
I ~ I =
|
||||
(\lm x . \tzm{b}x )~\tzm{a}I =
|
||||
I
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture,
|
||||
out=-90,
|
||||
in=-90,
|
||||
distance=0.5cm
|
||||
]
|
||||
\draw[->,gray,shorten >=5pt,shorten <=3pt]
|
||||
(a.center) to (b.east);
|
||||
\end{tikzpicture}
|
||||
$$
|
||||
\vspace{0.5mm}
|
||||
|
||||
So, $I~I$ reduces to itself. This makes sense, since the identity
|
||||
function doesn't change its input!
|
||||
\end{examplesolution}
|
||||
|
||||
|
||||
\vfill
|
||||
|
||||
@ -204,8 +236,8 @@ Remember that lambda calculus is left-associative.
|
||||
|
||||
\generic{Currying:}
|
||||
|
||||
In lambda calculus, functions are only allowed to take one argument.
|
||||
However, we can emulate multivariable functions through \textit{currying}\footnotemark{}\hspace{-1ex}.
|
||||
In lambda calculus, functions are only allowed to take one argument. \par
|
||||
If we want multivariable functions, we'll have to emulate them through \textit{currying}\footnotemark{}\hspace{-1ex}.
|
||||
|
||||
\footnotetext{After Haskell Brooks Curry\footnotemark{}\hspace{-1ex}, a logician that contributed to the theory of functional computation.}
|
||||
\footnotetext{
|
||||
@ -216,9 +248,9 @@ However, we can emulate multivariable functions through \textit{currying}\footno
|
||||
\vspace{1ex}
|
||||
|
||||
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).
|
||||
Consider the expression $A$ below. It takes one input $f$ and returns the function $\lm a. f~(f~a)$ (underlined).
|
||||
$$
|
||||
A = \lm f .(\tzm{a} ~ \lm a . f(f(a)) ~ \tzm{b})
|
||||
A = \lm f .(\tzm{a} ~ \lm a . f~(f~a) ~ \tzm{b})
|
||||
\begin{tikzpicture}[
|
||||
overlay,
|
||||
remember picture
|
||||
@ -230,11 +262,11 @@ A = \lm f .(\tzm{a} ~ \lm a . f(f(a)) ~ \tzm{b})
|
||||
\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$:
|
||||
For example, let's apply $A$ to an arbirary function $n$:
|
||||
$$
|
||||
A~N =
|
||||
\lm \tzm{b}f.(~\lm a.f(f(a))~)~\tzmr{a}N =
|
||||
\lm a.N(N(a))
|
||||
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,
|
||||
@ -244,13 +276,15 @@ $$
|
||||
]
|
||||
\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
|
||||
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. (\lm g. \lm x. (g(f(x))))$. What does $B$ do? \par
|
||||
Let $C = \lm f. \Bigl[\lm g. \Bigl( \lm x. [~ g(f(x)) ~] \Bigr)\Bigr]$. What does $C$ do? \par
|
||||
Evaluate $(C~a~b~x)$ for arbitary expressions $a$ and $b$. \par
|
||||
\hint{Place parentheses first. Remember, function application is left-associative.}
|
||||
|
||||
@ -269,16 +303,16 @@ If we have an expression with repeated function definitions, we'll combine their
|
||||
|
||||
\vspace{1ex}
|
||||
|
||||
For example, $A = \lm f . (\lm a . f(f(a)))$ will become $A = \lm fa . f(f(a))$
|
||||
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.
|
||||
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.
|
||||
Substituting all curried variables at once will cause errors.
|
||||
|
||||
\pagebreak
|
||||
|
||||
@ -311,63 +345,70 @@ Substituting all curried variables at once may cause errors, as we'll see below.
|
||||
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}
|
||||
\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
|
||||
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}
|
||||
\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.
|
||||
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}
|
||||
|
||||
|
||||
\vspace{4mm}
|
||||
|
||||
%\iftrue
|
||||
\iffalse
|
||||
\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.
|
||||
|
||||
\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}
|
||||
|
||||
\vspace{2mm}
|
||||
Variables inside functions are \say{scoped.} We must take care to keep separate variables separate.
|
||||
|
||||
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$
|
||||
|
||||
For example, take the functions \par
|
||||
$A = \lm a b . a$ \par
|
||||
$B = \lm b . b$
|
||||
\vspace{2ex}
|
||||
|
||||
\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}
|
||||
$$
|
||||
|
||||
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.
|
||||
This problem arises because 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.
|
||||
|
||||
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}
|
||||
|
||||
\vspace{2ex}
|
||||
|
||||
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$.
|
||||
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$.
|
||||
\fi
|
||||
|
||||
\problem{}
|
||||
Let $Q = \lm abc.b$ \par
|
||||
Reduce $(Q~a~c~b)$.
|
||||
Let $Q = \lm abc.b$. Reduce $(Q~a~c~b)$. \par
|
||||
\hint{
|
||||
You may want to rename a few variables. \\
|
||||
The $a,b,c$ in $Q$ are different than the $a,b,c$ in the expression!
|
||||
}
|
||||
|
||||
\begin{solution}
|
||||
I'll rewrite $(Q~a~c~b)$ as $(Q~a_1~c_1~b_1)$:
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user