Integer numbers

The module INT extends NAT with a unary minus -_ on nonzero natural numbers to construct the negative integers. Integers can be input, and by default are output, in normal decimal notation; however, -42 is just an alternative concrete syntax for - 42, which itself is just an alternative concrete syntax for - s_^ 42(0).

  fmod INT is
    protecting NAT .
    sorts NzInt Int .
    subsorts NzNat < NzInt Nat < Int .

    op -_ : NzNat -> NzInt  [ctor special (...)] .

Unary minus is then extended to Int so that

  - - I:Int = I:Int
  - 0 = 0

The arithmetic operations of NAT are extended to integers. In addition, there are operators for subtraction, _-_, and absolute value, abs.

    *** ARITHMETIC OPERATIONS
    *** unary minus
    op -_ : NzInt -> NzInt [ditto] .
    op -_ : Int -> Int [ditto] .
    *** addition
    op _+_ : Int Int -> Int  [assoc comm prec 33 special (...)] .
    *** subtraction
    op _-_ : Int Int -> Int  [prec 33 gather (E e) special (...)] .
    *** multiplication
    op _*_ : NzInt NzInt -> NzInt [assoc comm prec 31 special (...)] .
    op _*_ : Int Int -> Int [ditto] .
    *** quotient
    op _quo_ : Int NzInt -> Int [prec 31 gather (E e) special (...)] .
    *** remainder
    op _rem_ : Int NzInt -> Int [prec 31 gather (E e) special (...)] .
    *** exponentiation
    op _^_ : Int Nat -> Int [prec 29  gather (E e) special (...)] .
    op _^_ : NzInt Nat -> NzInt [ditto] .
    *** absolute value
    op abs : NzInt -> NzNat [special (...)] .
    op abs : Int -> Nat [ditto] .
    *** greatest common divisor
    op gcd : NzInt NzInt -> NzNat [assoc comm special (...)] .
    op gcd : Int Int -> Nat [ditto] .
    *** least common multiple
    op lcm : NzInt NzInt -> NzNat [assoc comm special (...)] .
    op lcm : Int Int -> Nat [ditto] .
    *** minimum
    op min : NzInt NzInt -> NzInt [assoc comm special (...)] .
    op min : Int Int -> Int [ditto] .
    *** maximum
    op max : NzInt NzInt -> NzInt [assoc comm special (...)] .
    op max : Int Int -> Int [ditto] .
    op max : NzNat Int -> NzNat [ditto] .
    op max : Nat Int -> Nat [ditto] .

The operators _quo_ and _rem_ satisfy the same equation for integer arguments as for natural numbers. The sign of the quotient is the product of the signs of the arguments.

  Maude> red in INT : -11 quo 4 .
  result NzInt: -2

  Maude> red 11 quo -4 .
  result NzInt: -2

  Maude> red  -11 quo -4 .
  result NzNat: 2

  Maude> red 11 rem -4 .
  result NzNat: 3

  Maude> red -11 rem 4 .
  result NzInt: -3

  Maude> red -11 rem -4 .
  result NzInt: -3

Bitwise operations on negative integers use the 2's complement representation and the operator ~_, computing the bitwise not operation, is added.

    *** BITSTRING MANIPULATION (TWO'S COMPLEMENT)
    *** bitwise not
    op ~_ : Int -> Int [special (...)] .
    *** bitwise exclusive or
    op _xor_ : Int Int -> Int [assoc comm prec 55 special (...)] .
    *** bitwise and
    op _&_ : Nat Int -> Nat [assoc comm prec 53 special (...)] .
    op _&_ : Int Int -> Int [ditto] .
    *** bitwise or
    op _|_ : NzInt Int -> NzInt [assoc comm prec 57 special (...)] .
    op _|_ : Int Int -> Int [ditto] .
    *** rightshift
    op _>>_ : Int Nat -> Int [prec 35 gather (E e) special (...)] .
    *** leftshift
    op _<<_ : Int Nat -> Int [prec 35 gather (E e) special (...)] .

Tests on integers extend those on the natural numbers.

    *** TESTS
    *** less than
    op _<_ : Int Int -> Bool [prec 37 special (...)] .
    *** less than or equal
    op _<=_ : Int Int -> Bool [prec 37 special (...)] .
    *** greater than
    op _>_ : Int Int -> Bool [prec 37 special (...)] .
    *** greater than or equal
    op _>=_ : Int Int -> Bool [prec 37 special (...)] .

    op _divides_ : NzInt Int -> Bool [prec 51 special (...)] .
  endfm

Let us show with an example how a predefined module can be reused to define new subsorts that refine the sort structure of the data type. In the following example, we introduce additional subsorts and overload the successor operator s_ (originally coming from the module NAT imported in protecting mode into INT) in order to specify the sort of integers greater than three.

  fmod INT-GT-3 is
    protecting INT .
    sorts One Two Three IntGt3 .
    subsorts One Two Three IntGt3 < NzNat .
    op s_ : Zero -> One [ctor ditto] .
    op s_ : One -> Two [ctor ditto] .
    op s_ : Two -> Three [ctor ditto] .
    op s_ : Three -> IntGt3 [ctor ditto] .
    op s_ : IntGt3 -> IntGt3 [ctor ditto] .
  endfm

We can check the sort of a number by ``reducing'' the corresponding constant, as follows:

  Maude> red -1 .
  result NzInt: -1

  Maude> red 0 .
  result Zero: 0

  Maude> red 1 .
  result One: 1

  Maude> red 2 .
  result Two: 2

  Maude> red 3 .
  result Three: 3

  Maude> red 4 .
  result IntGt3: 4

  Maude> red 12345678901234567890 .
  result IntGt3: 12345678901234567890

In theory, the sort of integers greater than three could also be specified by means of membership axioms (see Sections 4.2 and 4.3). However, memberships are not guaranteed to work correctly with the number hierarchy, because of the special internal representation for iterated towers of s_ symbols.