Improved intro
This commit is contained in:
		| @ -1,18 +1,82 @@ | ||||
| \section{Definitions} | ||||
| \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. | ||||
|  | ||||
| \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}. | ||||
| \vspace{2mm} | ||||
|  | ||||
| To apply functions, put them next to their inputs. We'll omit the usual parentheses to save space. | ||||
|  | ||||
| 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: | ||||
| $$ | ||||
| (I~\star) = | ||||
| (\lm \tzm{b}a. a)~\tzmr{a}\star = | ||||
| \star | ||||
| 	(\lm x . x + 3)~5 | ||||
| $$ | ||||
| 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. | ||||
|  | ||||
|  | ||||
| \vspace{2mm} | ||||
|  | ||||
|  | ||||
| We evaluate this by removing the \say{$\lm$} prefix and substituting $3$ for $x$ wheverever it appears: | ||||
| $$ | ||||
| (\lm x . \tzm{b}x + 3)~\tzmr{a}5 = | ||||
| 5 + 3 = 8 | ||||
| \begin{tikzpicture}[ | ||||
| 	overlay, | ||||
| 	remember picture, | ||||
| @ -24,10 +88,89 @@ $$ | ||||
| 		(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. | ||||
|  | ||||
| \problem{} | ||||
| 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. | ||||
| 	} | ||||
| \end{itemize} | ||||
|  | ||||
|  | ||||
| \vfill | ||||
|  | ||||
| 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. | ||||
|  | ||||
| \pagebreak | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
| \definition{} | ||||
| The first \say{pure} functions we'll define are $I$ and $M$: | ||||
| \begin{itemize} | ||||
| 	\item $I = \lm x . x$ | ||||
| 	\item $M = \lm x . x x$ | ||||
| \end{itemize} | ||||
|  | ||||
| Note that $I$ and $M$ don't have a meaning on their own. They are not formal functions. \par | ||||
| Rather, it's notation that says \say{write $\lm x.x$ whenever you see $I$.} | ||||
|  | ||||
|  | ||||
|  | ||||
|  | ||||
| \problem{} | ||||
| Reduce the following expressions. | ||||
| \begin{itemize}[itemsep=2mm] | ||||
| 	\item $I~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} | ||||
|  | ||||
|  | ||||
| \vfill | ||||
|  | ||||
| In lambda calculus, functions are left-associative: \par | ||||
| $(f~g~h)$ is equivalent to $((f~g)~h)$, not $(f~(g~h))$ | ||||
|  | ||||
| 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. | ||||
|  | ||||
| \problem{} | ||||
| Rewrite the following expressions with as few parentheses as possible, without changing their meaning or structure. | ||||
| @ -53,63 +196,6 @@ Remember that lambda calculus is left-associative. | ||||
|  | ||||
|  | ||||
|  | ||||
| \generic{$\beta$-Reduction:} | ||||
|  | ||||
| $\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 | ||||
| $$ | ||||
| The function $M$ simply repeats its input. 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 go any further, so we stop. Our expression is now in \textit{$\beta$-normal} or \say{reduced} 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:} | ||||
|  | ||||
|  | ||||
		Reference in New Issue
	
	Block a user