Wiki

Interval

In this section, we describe an interval on a totally ordered set (S,R).

In natural numbers, an interval [m..n] is defined as { x | m ≦ x ≦ n }. For any number x and y, x ≦ y is equivalent to not(x < y), i.e., y [>] x, where [>] is a complement of >.

Based on the notion of interval on natural numners, we can describe the module for declaration of intarvals of on a totally orderd set.

#!python
module INTERVAL
(
  X :: TRIV,
  S :: SET(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T),
  O :: TOTALORDER(X,R,I,A,T,P),
  C :: COMPLEMENT(X,R)
)
{
  signature
  {
    [ Interval < Set ]
    op top : Interval -> Elt
    op bot : Interval -> Elt
    op ord : Interval -> TotalOrder
  }
  axioms
  {
    vars X Y : Elt
    vars I : Interval
    eq deducible((X @ I) |- (top(I) [ord(I)] X)) = true .
    eq deducible((X @ I) |- (X [ord(I)] bot(I))) = true .
    eq deducible((top(I) [ord(I)] X),(X [ord(I)] bot(I)) |- (X @ I)) = true .
    eq deducible((bot(I) [ord(I)] top(I)) |- (I = nil)) = true .
  }
}

By instantiating this module with the module NUMBER, we can obtain a module for declatation of intervals on natural number.

However, we have to declare the comparison relation > on natural numbers as a total order. We need to declare the following modules to describe the module declaring >.

Set of natural numbers
Relation on natural numbers
Irreflexive relation on natural numbers
Asymmetric relation on natural numbers
Transitive relation on natural numbers
Partial orders on natural numbers
Total orders on natural numbers
Complement operation for relations on natural numbers

SET of NATURAL NUMBERS

#!python
make SET/NUMBER
(
  SET(
    NUMBER { sort Elt -> Number }
  ) * {
    sort Set -> Set/Number
  }
)

RELATION on NATURAL NUMBERS

#!python
make RELATION/NUMBER
(
  RELATION(
    NUMBER { sort Elt -> Number }
  ) * {
    sort Relation -> Relation/Number
  }
)

IRREFLEXIVE RELATION on NATURAL NUMBERS

#!python
make IRREFLEXIVE/NUMBER
(
  IRREFLEXIVE(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number }
  ) * {
    sort Irreflexive -> Irreflexive/Number
  }
)

ASYMMETRIC RELATION on NATURAL NUMBERS

#!python
make ASYMMETRIC/NUMBER
(
  ASYMMETRIC(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number }
  ) * {
    sort Asymmetric -> Asymmetric/Number
  }
)

TRANSITIVE RELATION on NATURAL NUMBERS

#!python
make TRANSITIVE/NUMBER
(
  TRANSITIVE(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number }
  ) * {
    sort Transitive -> Transitive/Number
  }
)

PARTIAL ORDERS on NATURAL NUMBERS

#!python
make PARTIALORDER/NUMBER
(
  PARTIALORDER(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number },
    IRREFLEXIVE/NUMBER { sort Irreflexive -> Irreflexive/Number },
    ASYMMETRIC/NUMBER { sort Asymmetric -> Asymmetric/Number },
    TRANSITIVE/NUMBER { sort Transitive -> Transitive/Number }
  ) * {
    sort PartialOrder -> PartialOrder/Number
  }
)

TOTAL ORDERS on NATURAL NUMBERS

#!python
make TOTALORDER/NUMBER
(
  TOTALORDER(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number },
    IRREFLEXIVE/NUMBER { sort Irreflexive -> Irreflexive/Number },
    ASYMMETRIC/NUMBER { sort Asymmetric -> Asymmetric/Number },
    TRANSITIVE/NUMBER { sort Transitive -> Transitive/Number },
    PARTIALORDER/NUMBER { sort PartialOrder -> PartialOrder/Number }
  ) * {
    sort TotalOrder -> TotalOrder/Number
  }
)

COMPLEMENT OPERATION of RELATIONS on NATURAL NUMBERS

#!python
make COMPLEMENT/NUMBER
(
  COMPLEMENT(
    NUMBER { sort Elt -> Number },
    RELATION/NUMBER { sort Relation -> Relation/Number }
  )
)

The comparison relation > is declared as a total order on natural numbers as follows:

#!python
module COMPARISON
{
  imports
  {
    ex(TOTALORDER/NUMBER)
  }
  signature
  {
    op > : -> TotalOrder/Number
  }
  axioms
  {
    vars M N : Number
    eq deducible(M > N |- s(M) > s(N)) = true .
    eq deducible(s(M) > s(N) |- M > N) = true .
  }
}

The following modules is an example to use this comparison relation >.

#!python
module FORMER
(
  X :: TRIV,
  L :: LIST(X),
  R :: RELATION(X)
)
{
  imports
  {
    pr(COMPARISON)
  }
  signature
  {
    op former : List -> Relation
  }
  axioms
  {
    vars L : List
    vars X Y : Elt
    eq (X former(L) Y) = (position(L,Y) > position(L,X)) .
  }
}

For any x,y : Elt and l : List, the proposition (x former(l) y) means that x is older than y in the list l, i,e, x is added into l before y is.

The relation former(l) can be regarded as a partial order. Indeed, this relation is irreflexive, asymmetric and transitive.

#!python
open FORMER .
ops l : -> List .
ops x y z : -> Elt .
red deducible((x former(l) x) |- nil) .
red deducible((x former(l) y),(y former(l) x) |- nil) .
red deducible((x former(l) y),(y former(l) z) |- (x former(l) z)) .
close

The result of the execution is listed below:

#!python
-- opening module FORMER(X, L, R).. done.
%FORMER(X, L, R)> %FORMER(X, L, R)> %FORMER(X, L, R)> _*
-- reduce in %FORMER(X, L, R) : (deducible(((x former(l) x) |- nil))):Prop
(true):Bool
(0.000 sec for parse, 2 rewrites(0.000 sec), 23 matches)
%FORMER(X, L, R)> -- reduce in %FORMER(X, L, R) : (deducible((((x former(l) y) , (y former(l) x)) |- nil))):Prop
(true):Bool
(0.000 sec for parse, 3 rewrites(0.000 sec), 47 matches)
%FORMER(X, L, R)> -- reduce in %FORMER(X, L, R) : (deducible((((x former(l) y) , (y former(l) z)) |- (x former(l) z)))):Prop
(true):Bool
(0.000 sec for parse, 4 rewrites(0.000 sec), 63 matches)

So, we can redeclare the relation former(l) as a partial order.

#!python
module FORMER
(
  X :: TRIV,
  L :: LIST(X),
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T)
)
{
  imports
  {
    pr(COMPARISON)
  }
  signature
  {
    op former : List -> PartialOrder
  }
  axioms
  {
    vars L : List
    vars X Y : Elt
    eq (X former(L) Y) = (position(L,Y) > position(L,X)) .
  }
}

Now, we can declare the module declaring intarvals on natural numbers with this comparison relation >.

#!python
module INTERVAL/NUMBER
{
  imports
  {
    pr(COMPARISON)
    ex(INTERVAL(
         NUMBER { sort Elt -> Number },
         SET/NUMBER { sort Set -> Set/Number },
         RELATION/NUMBER { sort Relation -> Relation/Number },
         IRREFLEXIVE/NUMBER { sort Irreflexive -> Irreflexive/Number },
         ASYMMETRIC/NUMBER { sort Asymmetric -> Asymmetric/Number },
         TRANSITIVE/NUMBER { sort Transitive -> Transitive/Number },
         PARTIALORDER/NUMBER { sort PartialOrder -> PartialOrder/Number },
         TOTALORDER/NUMBER { sort TotalOrder -> TotalOrder/Number },
         COMPLEMENT/NUMBER
       ) * {
         sort Interval -> Interval/Number
       }
    )
  }
  signature
  {
    op [_,_] : Number Number -> Interval/Number
  }
  axioms
  {
    vars I : Interval/Number
    vars M N : Number
    eq bot([M,N]) = M .
    eq top([M,N]) = N .
    eq ord([M,N]) = > .
  }
}

Prease notice that [>], i.e., the complement of > is the same as ≧ .