Wiki

Interval on a totally ordered set

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 numbers, we can describe the module for declaration of intervals of on a totally ordered set.

INTERVAL

The module INTERVAL is a parameterized module to declare and manipulate intervals on tatally ordered sets.

#!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 .
  }
}

In the above module, an interval I consists of a top element top(I), a bottom element bot(I) and a total order ord(I). For any element x,

x∈I　⇔ ((top(I) [ord(I)] x) ∧ (x [ord(I)] bot(I)))

To obtain a module for declatation of intervals on natural numbers, we have to declare the inequality > on natural numbers as a total order. Furthermore, to declare >, we need modules for:

sets of natural numbers
relations on natural numbers
irreflexive relations on natural numbers
asymmetric relations on natural numbers
transitive relations on natural numbers
partial orders on natural numbers
total orders on natural numbers
complement operation for relations on natural numbers

SET/NUMBER

A module for sets of natural numbers can be instantiated as follows.

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

RELATION/NUMBER

A module for relations on natural numbers can be instantiated as follows.

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

IRREFLEXIVE/NUMBER

A module for irreflexive relations on natural numbers can be instantiated as follows.

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

ASYMMETRIC/NUMBER

A module for asymmetric relations on natural numbers can be instantiated as follows.

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

TRANSITIVE/NUMBER

A module for transitive relations on natural numbers can be instantiated as follows.

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

PARTIALORDER/NUMBER

A module for partial orders on natural numbers can be instantiated as follows.

#!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
  }
)

TOTALORDER/NUMBER

A module for total orders on natural numbers can be instantiated as follows.

#!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/NUMBER

A module for a complement of a relation on natural numbers can be instantiated as follows.

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

INEQUALITY

The inequality > on natural numbers can be declared as a constant which belongs to the sort TotalOrder/Number.

#!python
module INEQUALITY
{
  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 .
  }
}

FORMER

For any list∈List and any elements x,y∈Elt, the proposition x former(l) y means that x has been added to l earlier than y.

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

In the above module, the operation former returns a relation on Elt. However, for any l∈List, former(l) satisfies irreflexivity, asymmetricity and transitivity.

#!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

#!python
-- reduce in %FORMER(X, L, R, I, A, T, P) : (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, I, A, T, P)> -- reduce in %FORMER(X, L, R, I, A, T, P) : (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, I, A, T, P)> -- reduce in %FORMER(X, L, R, I, A, T, P) : (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 declare the operation former returns a partial order on Elt.

#!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(INEQUALITY)
  }
  signature
  {
    op former : List -> PartialOrder
  }
  axioms
  {
    vars L : List
    vars X Y : Elt
    eq (X former(L) Y) = (position(L,Y) > position(L,X)) .
  }
}

INTERVAL/NUMBER

The module for intarvals on natural numbers can be declared as follows:

#!python
module INTERVAL/NUMBER
{
  imports
  {
    pr(INEQUALITY)
    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]) = > .
  }
}

For any numbers m and n, the term [m,n] represents a closed interval { x∈Number | m≦x≦n }.