Advanced handouts

Add missing file
Co-authored-by: Mark <mark@betalupi.com>
Co-committed-by: Mark <mark@betalupi.com>

src/Advanced/Lambda Calculus/main.tex

@@ -0,0 +1,110 @@
+% use [nosolutions] flag to hide solutions.
+% use [solutions] flag to show solutions.
+\documentclass[
+	solutions,
+	singlenumbering
+]{../../../lib/tex/ormc_handout}
+\usepackage{../../../lib/tex/macros}
+
+
+\usepackage{mathtools} % for \coloneqq
+
+% An invisible marker, used to
+% draw arrows in equations.
+\newcommand{\tzmr}[1]{
+	\tikz[
+		overlay,
+		remember picture,
+		right = 0.25ex
+	] \node (#1) {};
+}
+\newcommand{\tzm}[1]{
+	\tikz[
+		overlay,
+		remember picture
+	] \node (#1) {};
+}
+
+\newcommand{\lm}{\lambda}
+
+
+
+% TODO:
+% Lazy evaluation (alternate Y)
+% Add a few theorems
+% Better ending -> applications?
+% - nix, comparison to imperative
+
+
+
+\uptitlel{Advanced 2}
+\uptitler{\smallurl{}}
+\title{Lambda Calculus}
+\subtitle{Prepared by Mark on \today{}}
+
+\begin{document}
+
+	\maketitle
+
+	\hfill
+	\begin{minipage}{8cm}
+		Beware of the Turing tar pit, in which everything is possible but nothing of interest is easy.
+
+		\vspace{2ex}
+
+		Alan Perlis, \textit{Epigrams of Programming}, \#54
+	\end{minipage}
+	\hfill\null
+
+	\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}
+	\input{parts/03 numbers}
+	\input{parts/04 recursion}
+	\input{parts/05 challenges}
+
+\end{document}