CS430/530 Assignment 5

Due: October 26, Wednesday, 2011

1. In the language $L\{\mu_i\mu_f\}$ of chapter 17, write the following terms:
   • MULT: Multiplication of two natural numbers
   • PRED: The predecessor function for natural numbers. (Hint: read chapter 19.2!)
   • MINUS: The subtraction operation for natural numbers.
   • GT: For two natural numbers $n_1$ and $n_2$, returns true if $n_1 > n_2$, and false otherwise.
   • LENGTH: Returns the length of a list.
   • APPEND: Appends one list to another.
   • POWER: Given a natural number N, the stream of successive powers of N: (N^0, N^1, N^2, ...)
   • FACTORIAL: The stream of factorials of successive numbers ([n!] = 1, 2, 6, 24, ...)
   • TAKE: Given a stream S and a natural number N, returns a list having the N first numbers in S.
   • MERGE: Given two increasing streams, returns a merged increasing stream.
   Notes:
   • The type of natural numbers is: $\mu_i t.unit + t$, of lists: $\mu_i t.unit + nat \times t$, and of streams: $\mu_f t.nat \times t$.
   • If you want, you can develop these in Coq, using the following file: chap17.v. The function PLUS is provided as an example. Please don't use Coq's native types and pattern matching constructs; this file is provided so that you can stay close to Harper's syntax.
2. Show the evaluation steps (as defined from the operational semantics) for PRED (SUCC (SUCC ZERO)).
3. How would we define lists in the untyped lambda-calculus? (Hint: Read chapter 22.2.2 to understand the intuition behind the Church encodings of natural numbers, and do something similar for lists.)

Sample Solutions