// @(#)$Id: extra.txt,v 1.3 1997/02/13 00:20:46 leavens Exp $

Extra credit problems:

(a)
The implications in a trait don't add anything to the theory,
but state things that are supposed to be true.
How would you prove the implications hold, based on the
assertions about factorial?

(b)
We limited the form of the trait artificially for this problem.
Another way one might try to specify factorial would be to use a trait of the
following form.

	extra1: trait
	  includes Integer(int for Int)
	  introduces
	    factorial: int -> int
	  asserts
	    \forall n: int
	      factorial(0) == ...;
	      factorial(succ(n)) == ...;
	  implies
	    equations
	      factorial(0) == 1;
	      factorial(1) == 1 * factorial(0);
	      factorial(2) == 2 * factorial(1);
	      factorial(3) == 3 * factorial(2);

Although this format works in many examples, it is not good in this case.
To see why, try to fill in the dots (...) in the above trait,
and then prove the implied equations.  (Advanced: use LP to debug this.)
Hint: is it true that for all integers n, succ(n) > 0?

(c)
What could you do to solve the problem pointed out by (b) above,
but still use roughly the same format for the trait specification.

(d)
The trait in the problem uses Integer(int for Int).
What's the effect of the "int for Int"?

(e)
Respecify the trait using the sort N from the trait Natural
in Guttag and Horning's LSL Handbook (p. 201).
What advantages and disadvantages are there to using N instead of int?

(f)
What properties of numbers are really needed to specify factorial?
Can you write the trait, using an assumes clause (see Guttag and Horning's
book, section 4.6), that only uses the minimal properties?