Added historical note

Advanced/Lambda Calculus/main.tex

@@ -58,6 +58,48 @@
 
 	\vspace{4mm}
 
+	\makeatletter
+	\if@solutions
+		\begin{instructornote}
+			\textbf{Context \& Computability:} (or, why do we need lambda calculus?)\par
+			\note{From Peter Selinger's \textit{Lecture Notes on Lambda Calculus}}
+
+			\vspace{2mm}
+
+			In the 1930s, several people were interested in the question: what does it mean for
+			a function $f : \mathbb{N} \mapsto \mathbb{N}$ to be computable? An informal definition of computability
+			is that there should be a pencil-and-paper method allowing a trained person to
+			calculate $f(n)$, for any given $n$. The concept of a pencil-and-paper method is not
+			so easy to formalize. Three different researchers attempted to do so, resulting in
+			the following definitions of computability:
+
+			\begin{itemize}
+				\item Turing defined an idealized computer we now call a Turing machine, and
+				postulated that a function is \say{computable} if and only
+				if it can be computed by such a machine.
+
+				\item G\"odel defined the class of general recursive functions as the smallest set of
+				functions containing all the constant functions, the successor function, and
+				closed under certain operations (such as compositions and recursion). He
+				postulated that a function is \say{computable} if and only
+				if it is general recursive.
+
+				\item Church defined an idealized programming language called the lambda calculus,
+				and postulated that a function is \say{computable} if and only if it can be written as a lambda term.
+			\end{itemize}
+
+			It was proved by Church, Kleene, Rosser, and Turing that all three computational
+			models were equivalent to each other --- each model defines the same class
+			of computable functions. Whether or not they are equivalent to the \say{intuitive}
+			notion of computability is a question that cannot be answered, because there is no
+			formal definition of \say{intuitive computability.} The assertion that they are in fact
+			equivalent to intuitive computility is known as the Church-Turing thesis.
+		\end{instructornote}
+		\vfill
+		\pagebreak
+	\fi
+	\makeatother
+
 	\input{parts/00 intro}
 	\input{parts/01 combinators}
 	\input{parts/02 boolean}