% -*- mode: LaTeX; compile-command: "mk" -*-
\documentclass{tufte-handout}
%include polycode.fmt
\usepackage{../../hshw}
\usepackage{qrcode}
\title{\thecourse\ problem set 5}
\date{\small Revision 2: compiled \today\ at \currenttime}
\author{Due Tuesday, February 23}
%% NOTE: 18 Feb 2016. We didn't make it through the Y combinator in
%% class so I took that part off this assignment.
\begin{document}
\maketitle
While working on this problem set you may find it helpful to make use
of the $\lambda$-calculus evaluator available at
\url{https://fling.seas.upenn.edu/~cis39903/cgi-bin/LC.cgi}. There is
also a command-line $\lambda$-calculus interpreter; you can download
an installer from the course website.
You will not need to formally prove your answers on this problem set,
but you should justify them, \emph{e.g.} by giving an example
reduction sequence that illustrates the behavior of some
$\lambda$-calculus term you have defined, or by giving an informal
argument explaining why your solution is correct.
\section{What to turn in}
\begin{itemize}
\item A document in both \verb|.lhs| and \verb|.pdf| form, as
usual. In particular the \verb|.lhs| document should load cleanly in
\verb|ghci| and allow your solution to \pref{ex:fv} to be run.
\item A text file with the definitions of your lambda calculus terms,
in a format suitable for loading into the lambda calculus evaluator.
\end{itemize}
To typeset your lambda calculus terms in \LaTeX, you can just use
\verb|verbatim| environments; there's no need to get fancy typesetting
them with actual lambdas and so on. However, if you \emph{do} want to
typeset them in a fancy way, you can use the \verb|\lam| and
\verb|\app| commands defined in \verb|hshw.sty|. For example,
\[ \verb|\lam{x}{\lam{y}{\app{x}{y}}}| \] produces \[
\lam{x}{\lam{y}{\app{x}{y}}}. \] These commands ensure proper spacing
after the period and between terms in an application.
\section{Rubric}
\label{sec:rubric}
For full credit, your solutions should demonstrate a proficient
understanding of the following topics:
\begin{itemize}
\item Lambda calculus syntax and semantics (\emph{e.g.}
$\alpha\beta\eta$-equivalence, bound and free variables,
substitution, reduction)
\item Church numerals
\item Generalized Church encoding
% \item Recursion and the Y combinator
\end{itemize}
\section{The untyped $\lambda$-calculus}
\label{sec:lambda-calc}
\exercise \label{ex:fv} Consider the Haskell data type
\begin{spec}
data Term where
Var :: String -> Term
Lam :: String -> Term -> Term
App :: Term -> Term -> Term
\end{spec}
which represents a na\"ive encoding of $\lambda$-calculus terms as
Haskell values. Write a function\marginnote{For extra (brownie) points,
make sure it takes linear time\dots} \[ |freeVars :: Term ->
[String]| \] which computes the set of all free variables of a term.
For example, \[ |freeVars (App (Var "z") (Lam "y" (App (Var "y") (Var
"x")))) = ["z","x"]|. \]
\section{Natural numbers}
\label{sec:natural-numbers}
Recall from lecture that we can represent natural numbers in the
$\lambda$-calculus by their \term{Church encoding}, that is, the
natural number $n$ is represented by the $\lambda$-calculus term \[
\lam s {\lam z {\app s {(\app s {\dots (\app s z)})}}} \] where the
$s$ is repeated $n$ times. In other words, a natural number is
\emph{represented by its own fold}, that is, a function which takes as
arguments a function $s$ and starting value $z$, and applies $s$ to
$z$ a certain number of times.
We will abbreviate Church-encoded natural numbers as $n_\lambda$. For
example, \[ 3_\lambda = \lam s {\lam z {\app s {(\app s {(\app s
z)})}}}. \] The following exercises ask you to build up
facilities for doing computation with natural numbers.
\exercise Define the natural number $0_\lambda$,\marginnote{In
order to test your natural number functions in the
$\lambda$-calculus evaluator, you will want to evaluate things like,
\emph{e.g.}, \texttt{plus two three S Z} instead of just
\texttt{plus two three}. The reason is that reduction gets
``stuck'' when the outermost term constructor is a $\lambda$. In
order to ``fully reduce'' a Church-encoded number like \texttt{plus
two three}, you can apply it to some arguments, in this case, just
two free variables \texttt{S} and \texttt{Z} to stand in for
successor and zero.} and define a function $\mathit{succ}$ which
takes a (Church-encoded) natural number and yields its
(Church-encoded) successor.
\exercise Define a $\lambda$-calculus term $\mathit{plus}$ that adds
Church numerals. That is, $\mathit{plus}$ should have the property
that \[ \app {\app {\mathit{plus}} {m_\lambda}} {n_\lambda} \equiv
(m+n)_\lambda, \] where $\equiv$ denotes
$\alpha\beta\eta$-equivalence of $\lambda$-calculus terms.
\exercise Define a $\lambda$-calculus term $\mathit{mul}$ that
multiplies Church numerals.
\exercise Define a $\lambda$-calculus term $\mathit{exp}$ that
exponentiates Church numerals, that is, \[ \app {\app {\mathit{exp}}
{m_\lambda}} {n_\lambda} \equiv (m^n)_\lambda. \]
\marginnote{Feel free to define other named $\lambda$-calculus terms
if it makes your solutions more modular/elegant/readable.}
\exercise Define a $\lambda$-calculus term $\mathit{iszero}$ that
decides whether a Church numeral is zero. That is, when applied to a
Church numeral, it should evaluate to an appropriate Church-encoded
boolean.
% \exercise Now define $\mathit{iseven}$, which tests whether a Church
% numeral is even.
\section{Church pairs}
\label{sec:church-pairs}
\newcommand{\pair}{\mathit{pair}}
\newcommand{\fst}{\mathit{fst}}
\newcommand{\snd}{\mathit{snd}}
\exercise Define $\lambda$-calculus terms\marginnote{\emph{Hint}:
\qrcode{What\ is\ the\ fold\ for\ (a,b)?\ Think\ of\ it\ as\ having\
a\ single\ constructor\ Pair\ ::\ a\ ->\ b\ ->\ (a,b).}} $\pair$, $\fst$,
and $\snd$ such that \[ \app \fst {(\app {\app \pair x} y)} \equiv
x \] (and similarly for $\snd$).
\newcommand{\pred}{\mathit{pred}} \exercise Define
\marginnote{This problem is tricky! If you are stuck, feel
free to ask me for a hint.} a $\lambda$-calculus term
$\mathit{pred}$ such that when $n$ is positive, $\mathit{pred}$
applied to $n_\lambda$ is equivalent to $(n-1)_\lambda$ ($\pred$
applied to zero can just yield zero).
\exercise Now define a $\lambda$-calculus term $\mathit{sub}$ that
subtracts Church numerals (truncating at zero in the case of
subtracting a larger number from a smaller).
% \exercise Define a $\lambda$-calculus term $\mathit{gte}$ that tests
% whether one Church numeral is greater than or equal to another. That is, for
% example, \[ \app {\app {\mathit{gte}} {5_\lambda}} {4_\lambda} \equiv
% \mathit{true}. \]
\section{Church lists}
\label{sec:church-lists}
\newcommand{\nil}{\mathit{nil}}
\newcommand{\cons}{\mathit{cons}}
\exercise Define $\lambda$-calculus terms $\nil$ and $\cons$ which
represent the constructors for (Church-encoded) lists.
\exercise Define a
$\lambda$-calculus term $\mathit{sum}$ such that, for example, \[
\mathit{sum}\;(\cons \; 3_\lambda \; (\cons \; 1_\lambda \; (cons \;
4_\lambda \; \nil))) \equiv 8_\lambda. \]
\exercise Define a $\lambda$-calculus term $\mathit{filter}$ which
works similarly to Haskell's standard |filter| function.
% \section{Recursion and the Y combinator}
% \label{sec:Y-combinator}
% \exercise Using the Y combinator, define a $\lambda$-calculus term
% $\mathit{factorial}$ which computes the factorial of any Church numeral.
% \exercise Look up the \emph{Ackermann function} and encode it as a
% $\lambda$-calculus term, using the Y combinator.
\end{document}