% -*- 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}