2023-10-17 09:15:31 -07:00
|
|
|
\section{Introduction}
|
|
|
|
\textit{Lambda calculus} is a model of computation, much like the Turing machine.
|
|
|
|
As we're about to see, it works in a fundamentally different way, which has a few
|
|
|
|
practical applications we'll discuss at the end of class.
|
2023-02-05 21:02:05 -08:00
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
\vspace{2mm}
|
|
|
|
|
|
|
|
|
|
|
|
A lambda function starts with a lambda ($\lm$), followed by the names of any inputs used in the expression,
|
|
|
|
followed by the function's output.
|
|
|
|
|
|
|
|
For example, $\lm x . x + 3$ is the function $f(x) = x + 3$ written in lambda notation.
|
|
|
|
|
|
|
|
\vspace{4mm}
|
|
|
|
Let's disect $\lm x . x + 3$ piece by piece:
|
|
|
|
|
|
|
|
\begin{itemize}[itemsep=3mm]
|
|
|
|
\item \say{$\lm$} tells us that this is the beginning of an expression. \par
|
|
|
|
$\lm$ here doesn't have a special value or definition; \par
|
|
|
|
it's just a symbol that tells us \say{this is the start of a function.}
|
|
|
|
|
|
|
|
|
|
|
|
\item \say{$\lm x$} says that the variable $x$ is \say{bound} to the function (i.e, it is used for input).\par
|
|
|
|
Whenever we see $x$ in the function's output, we'll replace it with the input of the same name.
|
|
|
|
|
|
|
|
\vspace{1mm}
|
|
|
|
|
|
|
|
This is a lot like normal function notation: In $f(x) = x + 3$, $(x)$ is \say{bound}
|
|
|
|
to $f$, and we replace every $x$ we see with our input when evaluating.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\item The dot tells us that what follows is the output of this expression. \par
|
|
|
|
This is much like $=$ in our usual function notation: \par
|
|
|
|
The symbols after $=$ in $f(x) = x + 3$ tell us how to compute the output of this function.
|
|
|
|
\end{itemize}
|
|
|
|
|
|
|
|
\problem{}
|
|
|
|
Rewrite the following functions using this notation:
|
|
|
|
\begin{itemize}
|
|
|
|
\item $f(x) = 7x + 4$
|
|
|
|
\item $f(x) = x^2 + 2x + 1$
|
|
|
|
\end{itemize}
|
|
|
|
|
|
|
|
\vfill
|
|
|
|
\pagebreak
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
To evaluate $\lm x . x + 3$, we need to input a value:
|
2023-02-05 21:02:05 -08:00
|
|
|
$$
|
2023-10-17 09:15:31 -07:00
|
|
|
(\lm x . x + 3)~5
|
2023-02-05 21:02:05 -08:00
|
|
|
$$
|
2023-10-17 09:15:31 -07:00
|
|
|
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
|
2023-10-17 18:22:07 -07:00
|
|
|
and we omit the parentheses around 5 for the sake of simpler notation.
|
2023-10-17 09:15:31 -07:00
|
|
|
|
|
|
|
|
|
|
|
\vspace{2mm}
|
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
We evaluate this by removing the \say{$\lm$} prefix and substituting $3$ for $x$ wheverever it appears:
|
2023-02-05 21:02:05 -08:00
|
|
|
$$
|
2023-10-17 09:15:31 -07:00
|
|
|
(\lm x . \tzm{b}x + 3)~\tzmr{a}5 =
|
|
|
|
5 + 3 = 8
|
2023-02-05 21:02:05 -08:00
|
|
|
\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}
|
|
|
|
$$
|
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\problem{}
|
2023-10-17 09:15:31 -07:00
|
|
|
Evaluate the following:
|
|
|
|
\begin{itemize}[itemsep = 2mm]
|
|
|
|
\item $(\lm x. 2x + 1)~4$
|
|
|
|
\item $(\lm x. x^2 + 2x + 1)~3$
|
|
|
|
\item $(\lm x. (\lm y. 9y) x + 3)~2$ \par
|
|
|
|
\hint{
|
|
|
|
This function has a function inside, but the evaluation process doesn't change. \\
|
|
|
|
Replace all $x$ with 2 and evaluate again.
|
|
|
|
}
|
2023-10-16 16:06:39 -07:00
|
|
|
\end{itemize}
|
|
|
|
|
|
|
|
|
|
|
|
\vfill
|
2023-10-17 09:15:31 -07:00
|
|
|
|
|
|
|
As we saw above, we denote function application by simply putting functions next to their inputs. \par
|
|
|
|
If we want to apply $f$ to $5$, we write \say{$f~5$}, without any parentheses around the function's argument.
|
|
|
|
|
|
|
|
\vspace{4mm}
|
|
|
|
|
|
|
|
You may have noticed that we've been using arithmetic in the last few problems.
|
|
|
|
This isn't fully correct: addition is not defined in lambda calculus. In fact, nothing is defined:
|
|
|
|
not even numbers!
|
|
|
|
|
|
|
|
In lambda calculus, we have only one kind of object: the function.
|
|
|
|
The only action we have is function application, which works by just like the examples above.
|
|
|
|
|
|
|
|
\vspace{2mm}
|
|
|
|
|
|
|
|
Don't worry if this sounds confusing, we'll see a few examples soon.
|
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\pagebreak
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\definition{}
|
|
|
|
The first \say{pure} functions we'll define are $I$ and $M$:
|
2023-02-05 21:02:05 -08:00
|
|
|
\begin{itemize}
|
2023-10-17 09:15:31 -07:00
|
|
|
\item $I = \lm x . x$
|
|
|
|
\item $M = \lm x . x x$
|
|
|
|
\end{itemize}
|
2023-10-17 18:22:07 -07:00
|
|
|
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.
|
2023-10-17 09:15:31 -07:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
\vspace{4mm}
|
|
|
|
|
|
|
|
Also, note that $I$ and $M$ don't have a meaning on their own. They are not formal functions. \par
|
2023-10-17 11:45:33 -07:00
|
|
|
Rather, they are abbreviations that say \say{write $\lm x.x$ whenever you see $I$.}
|
2023-10-17 09:15:31 -07:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\problem{}
|
2023-10-17 11:45:33 -07:00
|
|
|
Reduce the following expressions. \par
|
|
|
|
\hint{
|
|
|
|
Of course, your final result will be a function. \\
|
|
|
|
Functions are the only objects we have!
|
|
|
|
}
|
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
\begin{itemize}[itemsep=2mm]
|
2023-02-05 21:02:05 -08:00
|
|
|
\item $I~I$
|
2023-10-17 18:22:07 -07:00
|
|
|
\item $M~I$
|
2023-10-17 09:15:31 -07:00
|
|
|
\item $(I~I)~I$
|
|
|
|
\item $\Bigl(~ \lm a .(a~(a~a)) ~\Bigr) ~ I$
|
|
|
|
\item $\Bigl(~(\lm a . (\lm b . a)) ~ M~\Bigr) ~ I$
|
2023-02-05 21:02:05 -08:00
|
|
|
\end{itemize}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
\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}
|
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\vfill
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
In lambda calculus, functions are left-associative: \par
|
2023-10-17 11:45:33 -07:00
|
|
|
$(f~g~h)$ means $((f~g)~h)$, not $(f~(g~h))$
|
2023-10-17 09:15:31 -07:00
|
|
|
|
|
|
|
As usual, we use parentheses to group terms if we want to override this order: $(f~(g~h)) \neq ((f~g)~h)$ \par
|
|
|
|
In this handout, all types of parentheses ( $(), [~],$ etc ) are equivalent.
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
\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}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
|
|
|
|
2023-10-17 09:15:31 -07:00
|
|
|
\vfill
|
|
|
|
\pagebreak
|
2022-11-13 13:02:25 -08:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-10-18 09:16:22 -07:00
|
|
|
|
|
|
|
|
|
|
|
\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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\generic{Currying:}
|
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
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}.
|
2023-10-16 18:54:37 -07:00
|
|
|
|
|
|
|
\footnotetext{After Haskell Brooks Curry\footnotemark{}\hspace{-1ex}, a logician that contributed to the theory of functional computation.}
|
|
|
|
\footnotetext{
|
|
|
|
There are three programming languages named after him: Haskell, Brook, and Curry. \par
|
|
|
|
Two of these are functional, and one is an oddball GPU language last released in 2007.
|
|
|
|
}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\vspace{1ex}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
The idea behind currying is fairly simple: we make functions that return functions. \par
|
2023-10-18 09:16:22 -07:00
|
|
|
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.
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\problem{}<firstcardinal>
|
2023-10-18 09:16:22 -07:00
|
|
|
Let $C = \lm f. \Bigl[\lm g. \Bigl( \lm x. [~ g(f(x)) ~] \Bigr)\Bigr]$. For now, we'll call it the \say{composer.}
|
|
|
|
|
|
|
|
\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
|
2023-10-16 16:06:39 -07:00
|
|
|
\hint{Place parentheses first. Remember, function application is left-associative.}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\vfill
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\problem{}
|
|
|
|
Using the definition of $C$ above, evaluate $C~M~I~\star$ \par
|
|
|
|
Then, evaluate $C~I~M~I$ \par
|
2023-10-17 11:45:33 -07:00
|
|
|
\note[Note]{$\star$ represents an arbitrary expression. Treat it like an unknown variable.}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\vfill
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
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$.
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\vspace{1ex}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
For example, $A = \lm f .[ \lm a . f(f(a))]$ will become $A = \lm fa . f(f(a))$
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\problem{}
|
2023-10-17 18:22:07 -07:00
|
|
|
Rewrite $C = \lm f.\lm g.\lm x. (g(f(x)))$ from \ref{firstcardinal} using this shorthand.
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
\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.
|
2023-10-17 18:22:07 -07:00
|
|
|
Substituting all curried variables at once will cause errors.
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\pagebreak
|
2022-11-13 13:02:25 -08:00
|
|
|
|
|
|
|
|
2023-10-16 16:06:39 -07:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
%\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.
|
2023-10-16 16:06:39 -07:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
\vspace{2mm}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
Variables inside functions are \say{scoped.} We must take care to keep separate variables separate.
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
For example, take the functions \par
|
|
|
|
$A = \lm a b . a$ \par
|
|
|
|
$B = \lm b . b$
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
\vspace{2ex}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
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}
|
|
|
|
$$
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
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.
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
\vspace{2ex}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-10-17 18:22:07 -07:00
|
|
|
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
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\problem{}
|
2023-10-17 18:22:07 -07:00
|
|
|
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!
|
|
|
|
}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\begin{solution}
|
2023-10-16 16:06:39 -07:00
|
|
|
I'll rewrite $(Q~a~c~b)$ as $(Q~a_1~c_1~b_1)$:
|
2023-02-05 21:02:05 -08:00
|
|
|
\begin{align*}
|
2023-10-16 16:06:39 -07:00
|
|
|
Q = (\lm abc.b) &= (\lm a.\lm b.\lm c.b) \\
|
2023-02-05 21:02:05 -08:00
|
|
|
(\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}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\vfill
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\problem{}
|
|
|
|
Reduce $((\lm a.a)~\lm bc.b)~d~\lm eg.g$
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\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}
|
2022-11-13 13:02:25 -08:00
|
|
|
|
2023-02-05 21:02:05 -08:00
|
|
|
\vfill
|
|
|
|
\pagebreak
|