% use [nosolutions] flag to hide solutions.
% use [solutions] flag to show solutions.
\documentclass[
	solutions,
	singlenumbering
]{../../resources/ormc_handout}
\usepackage{../../resources/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 imperitive



\uptitlel{Advanced 2}
\uptitler{Fall 2023}
\title{Lambda Calculus}
\subtitle{Prepared by \githref{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}