The natural numbers sort hierarchy has top sort Nat and (disjoint)
subsorts Zero and NzNat. The sort Nat is generated
from the constant 0 (of sort Zero) and the successor operator
s_.
fmod NAT is
protecting BOOL .
sorts Zero NzNat Nat .
subsort Zero NzNat < Nat .
*** constructors
op 0 : -> Zero [ctor] .
op s_ : Nat -> NzNat [ctor iter special (...)] .
Having 0 and successor as constructors means that you can define functions on the natural numbers by matching into the successor notation; for example:
fmod FACTORIAL is
protecting NAT .
op _! : Nat -> NzNat .
var N : Nat .
eq 0 ! = 1 .
eq (s N) ! = (s N) * N ! .
endfm
Try entering this module into Maude and then entering the commands
Maude> red 100 ! . Maude> red 1000 ! .
(The results are omitted; the first has 158 digits and the second 2568 digits.)
Natural numbers can be input, and by default will be output, in normal decimal
notation; however 42 is just syntactic sugar
for s_^42(0). The command set print number on/off controls
whether or not decimal notation is used by the pretty printer. Thus executing
the command set print number off will cause numbers to be printed
using iteration notation.
Most of the usual arithmetic operators are provided in NAT. They are not defined algebraically but could be given an algebraic definition by the user if desired, for example for theorem proving purposes.
*** ARITHMETIC OPERATIONS
*** addition
op _+_ : NzNat Nat -> NzNat [assoc comm prec 33 special (...)] .
op _+_ : Nat Nat -> Nat [ditto] .
*** symmetric difference
op sd : Nat Nat -> Nat [comm special (...)] .
*** multiplication
op _*_ : NzNat NzNat -> NzNat [assoc comm prec 31 special (...)] .
op _*_ : Nat Nat -> Nat [ditto] .
*** quotient
op _quo_ : Nat NzNat -> Nat [prec 31 gather (E e) special (...)] .
*** remainder
op _rem_ : Nat NzNat -> Nat [prec 31 gather (E e) special (...)] .
*** exponential n^m = n * .... * n (m times)
op _^_ : Nat Nat -> Nat [prec 29 gather (E e) special (...)] .
op _^_ : NzNat Nat -> NzNat [ditto] .
*** exponential modulo modExp(n,m,p) = n^m mod p
op modExp : Nat Nat NzNat ~> Nat [special (...)] .
*** greatest common divisor
op gcd : NzNat NzNat -> NzNat [assoc comm special (...)] .
op gcd : Nat Nat -> Nat [ditto] .
*** least common multiple
op lcm : NzNat NzNat -> NzNat [assoc comm special (...)] .
op lcm : Nat Nat -> Nat [ditto] .
*** minimum
op min : NzNat NzNat -> NzNat [assoc comm special (...)] .
op min : Nat Nat -> Nat [ditto] .
*** maximum
op max : NzNat Nat -> NzNat [assoc comm special (...)] .
op max : Nat Nat -> Nat [ditto] .
The operators _+_ and _*_ compute the usual addition and
multiplication operations and _^_ is exponentiation.
The symmetric difference operator, sd, subtracts the smaller of its arguments from the larger. Thus, for example,
Maude> red in NAT : sd(4, 9) . result NzNat: 5
Maude> red sd(9, 4) . result NzNat: 5
The quotient and remainder operators, denoted _quo_ and _rem_, satisfy
the equation
Maude> red in NAT : 11 quo 4 . result NzNat: 2
Maude> red 11 rem 4 . result NzNat: 3
The operator modExp computes modular exponentiation, with the third argument being the modulus. For example,
Maude> red in NAT : modExp(7, 1234, 2) . result NzNat: 1
Maude> red modExp(8, 1234, 2) . result Zero: 0
The operators gcd, lcm, min, and max compute the greatest common divisor, the least common multiple, the minimum and the maximum, respectively. Since these operators are associative and commutative, they can be used with any number (at least two) of arguments. For example,
Maude> red in NAT : gcd(6, 15, 21) . result NzNat: 3
Maude> red lcm(6, 15, 21) . result NzNat: 210
Maude> red min(6, 15, 21) . result NzNat: 6
Maude> red max(6, 15, 21) . result NzNat: 21
Maude> red gcd(0, 0) . result Zero: 0
Operators that act on the binary representation of natural numbers interpreted as bit strings are:
_xor_);
_&_);
_|_);
_>>_); and
_<<_).
*** BITSTRING MANIPULATION
*** bitwise exclusive or
op _xor_ : Nat Nat -> Nat [assoc comm prec 55 special (...)] .
*** bitwise and
op _&_ : Nat Nat -> Nat [assoc comm prec 53 special (...)] .
*** bitwise or
op _|_ : NzNat Nat -> NzNat [assoc comm prec 57 special (...)] .
op _|_ : Nat Nat -> Nat [ditto] .
*** right shift -- quotient by power of 2
op _>>_ : Nat Nat -> Nat [prec 35 gather (E e) special (...)] .
*** left shift -- multiplication by power of 2
op _<<_ : Nat Nat -> Nat [prec 35 gather (E e) special (...)] .
Here are some examples using the bitwise operators.
Maude> red in NAT : 5 xor 7 . result NzNat: 2
Maude> red 5 xor 2 . result NzNat: 7
Maude> red 5 xor 5 . result Zero: 0
Maude> red 5 & 7 . result NzNat: 5
Maude> red 5 & 2 . result Zero: 0
Maude> red 5 | 7 . result NzNat: 7
Maude> red 5 | 2 . result NzNat: 7
Maude> red 5 >> 2 . result NzNat: 1
Maude> red 5 << 2 . result NzNat: 20
The operators _<_, _<=_, _>_, and _>=_ denote the
usual operations for comparing numbers: less than, less than or equal, greater
than, and greater than or equal, respectively. The operator divides returns
true if and only if its second argument is a multiple of the first one.
*** TESTS
*** n less than m
op _<_ : Nat Nat -> Bool [prec 37 special (...)] .
*** n less than or equal to m
op _<=_ : Nat Nat -> Bool [prec 37 special (...)] .
*** n greater than m
op _>_ : Nat Nat -> Bool [prec 37 special (...)] .
*** n greater than or equal to m
op _>=_ : Nat Nat -> Bool [prec 37 special (...)] .
*** n divides m
op _divides_ : NzNat Nat -> Bool [prec 51 special (...)] .
endfm
Note that, to avoid producing negative numbers, subtraction and bitwise not are not provided. The symmetric difference can be used in place of subtraction.
The operational semantics for most of the built-in operators is such that you only get built-in behavior when all the arguments are actually natural numbers. The exception is associative and commutative built-in operators which will compute as much as possible on natural number arguments and leave the remaining arguments unchanged; for example,
Maude> red in NAT : gcd(gcd(12, X:Nat), 15) . result Nat: gcd(X:Nat, 3)
If the built-in operator does not disappear using the built-in semantics, then user equations are tried.
Advisory. It is easy to overload your machine's memory by generating huge natural numbers. There is a limit on exponentiation in that built-in behavior will not occur if the first argument is greater than 1 and the second argument is too large. Similarly, leftshift does not work if the first argument is greater than or equal to 1 and the second argument is too large. Currently ``too large'' means greater than 1000000 but this may change. Modular exponentiation has no such limits as its built-in semantics takes advantage of the fact that the result cannot be larger than the modulus. This is likely to be useful for cryptographic algorithms.