110 lines
3.2 KiB
TeX
Executable File
110 lines
3.2 KiB
TeX
Executable File
% use [nosolutions] flag to hide solutions.
|
|
% use [solutions] flag to show solutions.
|
|
\documentclass[
|
|
solutions,
|
|
singlenumbering
|
|
]{../../../lib/tex/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} |