Q1.

Read the question carefully.

*Why* are you offered two choices?

'+' has no meaning to CafeOBJ

eg
		module SPLODGE {
			** Sort names do not have to start with a capital
			** but that is the convention
			[Splodge]
	
			op _bing_ : Splodge Splodge -> Splodge

			vars S S' : Splodge

			eq S bing S' = S' .
		}

parse in SPLODGE : S bing S bing S .

brain flip required to write these spec.s
	we never tell CafeOBJ what it means to add two numbers
	we tell it what happens when the symbol '+' is used

obviously, Splodge and bing don't mean as much to us as Nat and '+', but
CafeOBJ treats them _exactly_ the same.

		module BAD-NAT {
			[Nat]

			op _+_ : Nat Nat : Nat

			vars X Y : Nat 

			eq X + Y = Y .
		}

parse in BAD-NAT : X + Y + X .

The reason CafeOBJ offers you two choices is that there are two valid parse
trees for the term. It has _nothing_ to do with the result of the equation.
There is no result of S:Splodge bing S. CafeOBJ is not concerned with that.
What it does 'know' is that according to the rules you have given it,

                bing                   is as                   bing
                /  \                 valid as                  /  \
             bing   S                                         S   bing
             /  \                                                 /  \
            S   S                                                 S   S


                 +                    is as                      +
                /  \                 valid as                  /  \
               +    X                                         X    +
             /  \                                                 /  \
            X   Y                                                 Y   X

Q2.

From BAD-NAT I think it's clear that we need to add something if we're going to
be able to define Natural addition.

The first step is to think of Natural numbers differently. We tend to think of
integers as fundamental, something which cannot be broken down any further. But
they aren't actually fundamental. We can define them recursively. We have to do
this in CafeOBJ, because it doesn't have a concept of fundamental sorts (unlike
Java, for instance). We need to build them up from things that CafeOBJ
'understands'.

Operators, constants, axioms.

Recursive definition: build the whole natural set up from the constant 0 and
the operator s (successor). Once we have this recursive definition, we can
start defining operators that manipulate it.

Recursive defn : 
	base case: 0 - a Nat
	recursion: s(Nat) is a Nat

in CafeOBJ syntax:

		module BASIC-NAT {

			[Nat]

			op 0 : -> Zero

----

		module BASIC-NAT {

			[Zero < Nat]

			op 0 : -> Zero
			op s : Nat -> Nat
			op s : Zero -> Nat

			op _+_ : Nat Nat -> Nat
			op _+_ : Zero Nat -> Nat
			op _+_ : Nat Zero -> Nat

----

		module BASIC-NAT {
		    signature {
			[Zero NzNat < Nat]

			op 0 : -> Zero
			op s : Nat -> Nat

			op _+_ : Nat Nat -> Nat
		    }
		    axioms {
			vars X Y : Nat
			
			eq X + 0 : X .

spend time over this one:
			eq X + s(Y) = s(X + Y) .
		    }
		}

----

reduce in BASIC-NAT : s(s(s(0))) + s(s(0)) .

-- write steps on the board

step one: find the operators and operands
step two: find first matching axiom
   three: rewrite

-- go through them
-- get someone up to do 0 + s(s(0)) .

-- add     eq 0 + X : X .

get them to do multiplication on their own.

add 
		op _*_ : Nat Nat -> Nat
		eq X * 0 : 0 .
		eq X * s(Y) = (X * Y) + X .

get someone up to write in those rules 
get someone else to reduce (follow steps)
		s(s(s(0))) * s(s(s(0))) .


Many people seemed to have a problem with where axioms go in the module,
repeating an axiom and even including conflicting axioms. From now on, you'll
lose marks if you leave out imports, signature, and axioms blocks.