\documentclass{article}
\usepackage{graphics}
\usepackage{fancyheadings}

\newcommand{\coursenumber}{131}
\newcommand{\coursetitle}{Principles of Programming Languages}

\topmargin  18pt  	% 27pt
\headheight 12pt  	% 12pt
\headsep    35pt 	% 45pt
\textheight 8.0in
\textwidth  6.2in

\oddsidemargin   22pt      % Left margin on odd-numbered pages.
\evensidemargin  22pt      % Left margin on even-numbered pages.
\marginparwidth  72pt       % Width of marginal notes.
\marginparsep    11pt      % Horizontal space between outer margin and 
                           % marginal note

\pagestyle{fancy}
\lhead{CSCI \coursenumber}
\chead{}
\rhead{\semester}
\lfoot{}
\cfoot{\thepage}
\rfoot{}
\setlength{\headrulewidth}{0pt}
\setlength{\footrulewidth}{0pt}

\newcommand{\semester}[0]{
     \ifnum\month>7{Fall}\fi
     \ifnum\month<8{Spring}\fi\  \number\year
}

\newcommand{\points}[1]{(#1 points)}
\newcommand{\phead}[2]{\points {#1} \textbf{#2}}

\begin{document}

\begin{center}
    \Large Homework 2\\ \vspace{1 ex} Due Thursday, 9/18/14 at 
    midnight.
\end{center}

\vspace{2 ex} 

Please turn in your homework solutions online at  
\texttt{http://www.dci.pomona.edu/tools-bin/cs131upload.php}
before midnight on the due date. 

\vspace{2 ex}

\begin{enumerate}
    
    \item \phead{10}{Parsing}
    
    Please do problem 4.1 from Mitchell, page 83.
        
    \item \phead{5}{Lambda Calculus Reduction}
    
    Please do problem 4.3 from Mitchell, page 83.
    
    \item \phead{10}{Symbolic Reduction}
    
    Please do problem 4.4 from Mitchell, page 83.
    
    \item \phead{10}{Programming the lambda calculus}
    
    Because Grace has anonymous functions, we can translate the 
    lambda calculus terms for booleans, numbers, operations, etc.
    into Grace.  For example,
    \underline{true} = $\lambda u. \lambda v. u$
    translates to
    \begin{verbatim}
    def lamTrue = {u -> {v -> u}}
    \end{verbatim}
    Notice that in the above, \texttt{lamTrue} is just a name
    for the anonymous function in Grace that takes two arguments
    and returns the first.
    
    Here are terms representing, false, cond, 0, 1, and some of the operations
    we defined in class.
    \begin{verbatim}
    def lamFalse = {u -> {v -> v}}
    def lamCond = {b -> {tVal -> {fVal -> b.apply(tVal).apply(fVal)}}}
    def lamZero = {s -> {z -> z}}
    def lamOne = {s -> {z -> s.apply(z)}}

    def lamSucc = {n -> {s -> {z -> s.apply(n.apply(s).apply(z))}}}
    def lamPlus = {n -> {m -> {s -> {z -> m.apply(s).apply(n.apply(s).apply(z))}}}}
    def lamMult = {n -> {m -> m.apply(lamPlus.apply(n)).apply(lamZero)}}
    def lamIsZero = {n -> n.apply{x -> lamFalse}.apply(lamTrue)}   
    \end{verbatim}
    
    Because these terms are built using blocks in Grace, function application takes
    place using the \texttt{apply} method.  Thus \texttt{lamSucc.apply(lamOne)}
    will return the representation of the successor of one (which we could call \texttt{lamTwo})
    
    Of course we can't easily print out the answers to these computations because, for example, all of the
    numbers will be anonymous functions taking two arguments.  However, I have
    written functions that can used to convert lambda encodings of numbers and
    booleans to actual numbers and booleans.
    \begin{verbatim}
    def succ = {n -> n+1}
    method lamToNumber(n) -> Number {
         n.apply(succ).apply(0)
    }
    
    method lamToBool(b) -> Boolean {
          b.apply(true).apply(false)
    }
    \end{verbatim}
    All that \texttt{lamToNumber} does is to apply
    the lambda calculus representation of the number
    to the successor function and to zero in order to give
    you the number it represents.  Thus you won't be surprised
    to know that \texttt{lamToNumber(lamSucc.apply(lamOne))}
    will return the number 2.
    
    Play with these in order to make sure you understand how they work.
    Then write a lambda calculus term representing exponentiation.
    \emph{Hint: its definition looks very similar to that for multiplication.}  Translate
    your into Grace and show that it gives the right answers to computations
    such as $3^{4}$.
    
    Your function should be named \texttt{lamExp} and take arguments n and m 
    that are lambda expressions corresponding to numbers such that
    \texttt{lamExp.apply(n).apply(m)} returns a lambda expression corresponding
    to n to the mth power.
    
    \item \phead{10}{Lambda Reduction with Sugar}
    
    Here is a ``sugared'' lambda-expression using {\tt let}
    declarations:
    \[
    \begin{array}{l}
	{\tt let}\ \mathit{compose} = \lambda f.\,\lambda g.\,
	\lambda x.\, f (g\,x)\ {\tt in} \\
	\ \ \ \ \
	{\tt let}\ h = \lambda x.\,x+x\ {\tt in} \\
	\ \ \ \ \ \ \ \ \ \
	((\mathit{compose}\,h)\,h)\,3
    \end{array}
    \]
    The ``de-sugared''  lambda-expression, obtained by replacing
    each ${\tt let}\ z = U ~{\tt in}~ V$ by $(\lambda z.\,V)\,U$
    is
    \[
    \begin{array}{l}
	(\lambda \mathit{compose}.\, \\
	
	\ \ \ \ \ (\lambda h.\; ((\mathit{compose}\; h)\; h)\; 3) \ \
	(\lambda x.\, x+x)) \\
	\ \ \ \ \ (\lambda f.\, \lambda g.\,
	\lambda x.\, f(g\ x))
    \end{array}
    \]
    This is written using the same variable names as the {\tt
    let}-form in order to make it easier to compare the expressions.

    Simplify the desugared lambda expression using reduction.  Write
    one or two sentences explaining why the simplified expression is
    the answer you expected.


    \item \phead{20}{Defining Terms in Lambda Calculus}
    
    In class we defined Church numerals and booleans, and showed how
    to define more complex functions in the pure lambda calculus.
    Please show how to define the following functions in the pure
    lambda calculus.  (You may use the functions defined in class
    in defining these new functions.)

    \begin{enumerate}
  
	\item \points{5}
  
	Define a function \underline{Minus} such that \underline{Minus} 
	\underline{m} \underline{n} = \underline{m - n} if
	m $>$ n and 0 otherwise.  Do not use recursion, but instead
	define it directly.  You may assume that you are given the function \underline{Pred} defined (but not
	explained) in class that computes the predecessor of a number (where the predecessor
	of 0 is 0, predecessor of 1 is 0, 2 is 1, etc.).  That is, your answer may include the term
	\underline{Pred} without providing a definition of it.
  
	\item \points{5}
  
	Define a function \underline{LessThan} such that \underline{LessThan} 
	\underline{m} \underline{n} =
	\underline{true} iff \underline{m} $<$ n.
	
	You might want to test your answer using the Grace code given in problem 4.
  
	\item \points{5}
  
	Define the recursive fibonacci function \underline{fib} such that
	fib 0 = 1, fib 1 = 1, and fib n = fib (n-1) + fib~(n-2) for n
	$>$ 1.  \emph{This is tricky as you are not allowed to name 
	the function and use the name in the definition.  You must use the 
	Y-combinator and emulate what we did in class defining factorial.}
  
	\item \points{5}
  
	Use your definition of \underline{fib} from above to calculate 
	\underline{fib} 2.  Do
	it step by step, showing all of your work.  You may assume
	that \underline{fib} \underline{1} = \underline{1}, 
	\underline{fib} \underline{0} = \underline{1} and that 
	\underline{Plus} \underline{1} \underline{1} = \underline{2} without
	showing all of the reduction steps.  All other steps in the
	reduction should be shown.
  
    \end{enumerate}
    
    \item \phead{10}{Fixed Points}

    We showed in class that every function f definable in the lambda
    calculus has a fixed point, i.e., there is a term {a} such that
    {f(a) = a}.  In class we defined the function \underline{Succ} as the
    successor function.  I.e., \underline{Succ} \underline{n} = 
    \underline{n+1} for all encodings of integers, \underline{n}.  
    Needless to say, we don't expect the successor
    function to have a fixed point, yet we proved that every function
    has a fixed point!
    
    Compute the fixed point of \underline{Succ}.  What can you say about it?  In
    particular, why doesn't this contradict our expectations that the
    successor function on the natural numbers does not have a fixed
    point.  \emph{Yes, this is supposed to be tricky and puzzling, but
    you need to deal with this type of seemingly contradictory information.
    A hint is that you should think about what all encodings of numbers look like.}



\end{enumerate}

\end{document}