Due by midnight on Monday September 24th. Either hand in in class or deliver to Kenny's office. You mail also email a completed assignment to him at kzhu@cs.princeton.edu. Please put "COS 441 A1" in the subject line of any such email.
0. (a) [0 Points] Subscribe to the course mailing list. All students in COS 441 are required to sign up for the class mailing list. If you have questions about assignments or other information you can send email to cos441 "atsign" lists.cs.princeton.edu.
To subscribe to the list go to https://lists.cs.princeton.edu/mailman/listinfo/cos441.
(b) [0 Points] The next assignment will involve some programming in SML. Get yourself prepared for next week by: (1) Finding a reference manual for SML either online or in the bookstore (see here) (2) Figuring out how to install and run the SML compiler (see here), and (3) Writing the "hello world" program that prints out "hello world".
One of the important elements of this class is learning how to write down proofs of properties in a clear, precise and exacting fashion. You will be graded both on correctness and clarity of your proofs. Hand-waving is not acceptable! Normally, you will lay out your proofs in a similar way as in this document. In particular, always remember to state the proof methodology you are using in your proof ("Induction on ..."). Points will be automatically deducted from answers in which the proof methodology is not stated clearly.
There are 15 points to gain on this assignment.
Recall the following inductive definitions of natural numbers and addition from class:
|- n nat
----------- -------------
|- Z nat |- S n nat
|- n nat |- add n1 n2 n3
------------------- ------------------------------
|- add Z n n |- add (S n1) n2 (S n3)
1. [3 Points] Prove that for all n1, n2, n3, addition is commutative:
If |- add n1 n2 n3 then |- add n2 n1 n3.
2. [3 Points] Inductively define multiplication as the repeated addition of natural numbers. Here is the judgment form:
|- mult n1 n2 n3
The following are valid judgments (among many others of course):
|- mult Z (S Z) Z
|- mult (S Z) (S Z) (S Z)
|- mult (S S Z) (S S Z) (S S S S Z)
3. [2 Points] Convert the following recursive equations into an inductively defined relation in our notation
fact(0) = 1
fact(n+1) = (n+1) * fact(n)
4. [2 points] Suppose for a second, we redefined the natural numbers, leaving out the zero case so we are just left with this:
|- n nat
--------------
|- S n nat
Now, let's define the even numbers:
|- even n
-------------------
|- even (S S n)
Given these definitions, is it possible to prove all natural numbers are even numbers? If so, state the lemma you would prove precisely and prove it. If not, explain why the proof cannot be done.
5. [5 points] Here is an inductive definition of trees that carry numbers in their internal nodes. I'll use metavariable t to range over trees. These judgements have the general form |- t tree :
--------------- leaf
|- leaf tree
|- n nat |- t1 tree |- t2 tree
---------------------------------------
|- node(n,t1,t2) tree
Give a collection of inductive definitions that cumulatively define those trees that are "in order." In other words, those trees for which all numbers in the left subtree are less than or equal to the number in the current node and all numbers in the right subtree are greater than or equal to the number in the current node. This should be the form of one of your judgments, but you will have to define auxiliary judgements to complete the task:
|- t inorder