RelHomog

Some functions special to homogeneous relations, that is, relations with equal domain and codomain. This structure contains some closure functions (reflexive, symmetric, transitive). Parameter contains additional functions to compute data for new elements.

Signature of RelHomog

List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Pair
See Rel
See Seq
See Set
See Triple

SIGNATURE RelHomog[dom, <, data, gen, ~, ++]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

Parameter

SORT dom data
FUN < : dom ** dom -> bool

generate new associated data

FUN gen: dom ** dom -> data

invert associated data (gen(c, d) = ~(gen(d, c)))

FUN ~ : data -> data

combine associated data (gen(c, m) ++ gen(m, d) = gen(c, d))

FUN ++ : data ** data -> data

Imports

IMPORT Rel[dom, <, dom, <, data] ONLY rel
       Set[dom, <] ONLY set
       Nat ONLY nat

Special relations

FUN id: set -> rel

Iterating Relations

FUN iter ^ : rel ** nat -> rel

Symmetry

FUN symmetric? : rel -> bool
FUN symClosure : rel -> rel

Reflexivity

FUN reflexive? : rel -> bool
FUN refClosure : rel -> rel

Transitivity

FUN transitive? : rel -> bool
FUN + transClosure : rel -> rel

FUN * refTransClosure: rel -> rel
FUN RSTClosure: rel -> rel

next node: Rel,
prev node: RelConv,
up to node: Subsystem Binary Relations