Wiki

Binary Relations

The purpose of this section is to introduce modules for several kinds of binary relations.

RELATION

First of all, we have to declare a module which declares a sort of binary relations. This module RELATION is a parameterized module which declares a sort of binary relations.

#!python
module RELATION
(
  X :: TRIV
)
{
  imports
  {
    pr(PROP)
    pr(DEDUCIBLE)
  }
  signature
  {
    [ Relation ]
    op ___ : Elt Relation Elt -> Prop
  }
  axioms
  {
    vars X Y Z : Elt
    vars R : Relation
-- substitution
    eq deducible((X = Y),(X R Z) |- (Y R Z)) = true .
    eq deducible((X = Y),(Z R X) |- (Z R Y)) = true .
  }
}

In formal specification languages of model-oriented approach like Z and Event-B, a binary relation R is modelled as a subset of a cartesian product of a domain and a codomain of R. Let x and y be terms of some sort T and R be a binary relation over T. In these specification langeages, the term "x R y" means <x,y>∈R. But the above module does not follow such approach. In the module RELATION, the term "x R y" is treated just an proposition.

IRREFLEXIVE

The module IRREFLEXIVE denotes irreflexive binary relations. Let S be a set and R be a binary relation over S, R is called irreflexive if the following property holds.

∀x∈S・¬（x R x）

#!python
module IRREFLEXIVE
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    [ Irreflexive < Relation ]
  }
  axioms
  {
    vars X : Elt
    vars R : Irreflexive
-- irreflexivity
    eq deducible((X R X) |- nil) = true .
    eq deducible(nil |- (neg X R X)) = true .
  }
}

The above module declares the sort Irreflexive as a subsort of Relation which satisfies the irreflexivity.

ASYMMETRIC

The module ASYMMETRIC denotes asymmetric binary relations. Let S be a set and R be a binary relation over S, R is called asymmetric if the following property holds.

∀x,y∈S・¬（x R y ∧ y R x)

#!python
module ASYMMETRIC
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    [ Asymmetric < Relation ]
  }
  axioms
  {
    vars X Y : Elt
    vars R : Asymmetric
-- asymmetricity
    eq deducible((X R Y),(Y R X) |- nil) = true .
  }
}

The above module declares the sort Asymmetric as a subsort of Relation which satisfies the asymmetricity.

TRANSITIVE

The module TRANSITIVE denotes transitive binary relations. Let S be a set and R be a binary relation over S, R is called transitive if the following property holds.

∀x,y,z∈S・（x R y ∧ y R z）⇒ x R z

#!python
module TRANSITIVE
(
  X :: TRIV,
  R :: RELATION(X)
)
{
  signature
  {
    [ Transitive < Relation ]
  }
  axioms
  {
    vars X Y Z : Elt
    vars R : Transitive
-- transitivity
    eq deducible((X R Y),(Y R Z) |- (X R Z)) = true .
  }
}

The above module declares the sort Transitive as a subsort of Relation which satisfies the transitivity.

PARTIALORDER

The notioon of strict partial order is important because it provides a foundation for verification of the priority-inversion freedom and the deadlock freedom of multitask scheduling systems. A strict partial order is an irreflexive, asymmetric and transitive binary relation.

To tell the truth, irreflexivity and asymmetricity are equivalent to each other under transitivity, i.e.,

Asymmetricity can be derived from irreflexivity and transitivity, and
Irreflexivity can be derived from asymmetricity and transitivity

So, a strict partial order can be defined as:

an irreflexive and transitive binary relation, or
an asymmetric and transitive binary relation

But the module for strict partial orders introduced in this section declares strict partial orders as irreflexive, asymmetric and transitive binary relations.

#!python
module PARTIALORDER
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R)
)
{
  signature
  {
    [ PartialOrder < Irreflexive Asymmetric Transitive ]
  }
}

The module PARTIALORDER declares the sort PartialOrder as a subsort of Irreflexive, Asymmetric and Transitive.

From now on, we denote strict partial orders just by partial orders in this note.

TOTALORDER

We define a total order R on S as a partial order on S with the following totality:

∀x,y∈S・(x R y) ∨ (x = y) ∨ (y R x)

The module TOTALORDER which declares the sort TotalOrder which is a subsort of PartialOrder.

#!python
module TOTALORDER
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  T :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,T)
)
{
  signature
  {
    [ TotalOrder < PartialOrder ]
  }
  axioms
  {
    vars X Y : Elt
    vars R : TotalOrder
--  totality
    eq deducible(nil |- (X R Y),(X = Y),(Y R X)) = true .
  }
}

LEMMA1/TOTALORDER

Let (S,R) be an arbitrary tatally ordered set. Then, for any x,y,z∈S, (x R y) implies (x R z) or (z R y).

This claim can be described as follows:

#!python
module CLAIM1/TOTALORDER
(
  X :: TRIV,
  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)
)
{
  imports
  {
    pr(LK)
  }
  signature
  {
    op r : -> TotalOrder
    ops x y z : -> Elt
    op claim : -> Prop
  }
  axioms
  {
    eq claim = deducible((x r y) |- (x r z),(z r y)) .
  }
}

The following is the proof score to reduce this claim to true.

#!python
open CLAIM1/TOTALORDER .
ops q1 q2 q3 : -> Sequent .
eq q1 = (nil |- (y r z),(y = z),(z r y)) .
eq q2 = ((x r y),(y r z) |- (x r z)) .
eq q3 = ((x r y),(y = z) |- (x r z)) .
ops i : -> Inference .
eq antecedent(i) = (q1,q2,q3) .
eq ((x r y) |- (x r z),(z r y)) = consequent(i) .
red claim .
close

The result of execution of the above proof score is:

#!python
-- reduce in %CLAIM1/TOTALORDER(X, R, I, A, T, P, O) : 
    (claim):Prop

** Found [state 40] (consequent(i)):Set/Sequent
   {}
-- found required number of solutions 1.
(true):Bool
(0.000 sec for parse, 3157 rewrites(0.670 sec), 122743 matches, 1280 memo hits)

Then, we obtain the following lemma.

#!python
module LEMMA1/TOTALORDER
(
  X :: TRIV,
  R :: RELATION(X),
  I :: IRREFLEXIVE(X,R),
  A :: ASYMMETRIC(X,R),
  V :: TRANSITIVE(X,R),
  P :: PARTIALORDER(X,R,I,A,V),
  T :: TOTALORDER(X,R,I,A,V,P)
)
{
  imports
  {
    pr(LK)
  }
  axioms
  {
    vars X Y Z : Elt
    vars R : TotalOrder
    eq deducible((X R Z) |- (X R Y),(Y R Z)) = true .
    eq deducible((neg X R Y),(X R Z) |- (Y R Z)) = true .
    eq deducible((neg Y R Z),(X R Z) |- (X R Y)) = true .
  }
}