Develop a module GCD which calculates the Greatest Common Divisor of two Naturals. Here is the logic for the module:
GCD(N, M)
if N < M
GCD(M, N)
otherwise
GCD(N - M, M)
You will need to extend the module below to add '-' and '<' operators. Be careful with your implementation of the 'otherwise' clause in GCD, it will depend on the implementation you do of the '-' operator.
module SIMPLE-NAT {
[ Zero NzNat < Nat ]
op 0 : -> Zero
op s : Nat -> NzNat
op _+_ : Nat Nat -> Nat
vars N N' : Nat
eq 0 + N = N .
eq N + 0 = N .
eq s(N) + N' = s(N + N') .
}
Consider the following module:
module FACT {
protecting (RAT)
op _! : Nat -> NzNat
eq 0 ! = 1 .
ceq N:Nat ! = N * (N - 1 !) if N > 0 .
}
Before you try it in CafeOBJ, write out the term rewriting steps you expect for
the following command (this does not have to be in the notation used by
CafeOBJ, write it any way that makes the logic clear).
reduce in FACT : s(0) ! .
| Home | |
|