Computer-Aided Program Development
Institute of Computer Science
Faculty of Engineering, Christian-Albrechts-University of Kiel
Logo of the Working Group
RelView Base Functions

The following table lists the base functions, which are available in the RelView system. For more high-level functions, see the file start_up.prog.

Base functions for calculating constant relations and domains:

Syntax Description Input Formal Type
TRUE(), true() Universal relation with type 11. TRUE()⊥,⊥ ⇔ true 11
FALSE(), false() Empty relation with type 11. FALSE()⊥,⊥ ⇔ false 11
L(R) Universal relation with the same dimension as R. R : X↔Y L(R)x,y ⇔ true X↔ Y
O(R) Empty relation with the same dimension as R. R : X↔Y O(R)x,y ⇔ false X↔ Y
I(R) Identity relation with the same dimension as R. R : X↔Y I(R)x,y ⇔ x=y X↔ Y
Ln1(R) Universal column vector with the same row number as R. R : X↔Y Ln1(R)x,⊥ ⇔ true X↔ 1
On1(R) Empty column vector with the same row number as R. R : X↔Y On1(R)x,⊥ ⇔ false X↔ 1
L1n(R) Universal row vector with the same column number as R. R : X↔Y L1n(R)⊥,y ⇔ true 1↔ Y
O1n(R) Empty row vector with the same column number as R. R : X↔Y O1n(R)⊥,y ⇔ false 1↔ Y
dom(R) Domain of relation R. R : X↔Y dom(R)x,⊥ ⇔ ∃ y: Rx,y X↔1

Base functions for calculating Boolean operations:

-R Negation (complement) of relation R. R : X↔Y (-R)x,y ⇔ ¬Rx,y X↔ Y
R|S Union (join) of R and S. R, S : X↔Y (R|S)x,y ⇔ Rx,y ∨ Sx,y X↔ Y
R&S Intersection (meet) of R and S. R, S : X↔Y (R&S)x,y ⇔ Rx,y ∧ Sx,y X↔ Y

Base functions for calculating relationalgebraic operations:

R^ Transposition of relation R. R : X↔Y (R^)y,x ⇔ Rx,y Y↔ X
R*S Composition (product) of R and S. R : X↔Y, S : Y↔Z (R*S)x,z ⇔ ∃ y: Rx,y ∧ Sy,z X↔ Z

Base functions for calculating residuals and symmetric quotients:

S/R Left residual of R and S. R : X↔Z, S : Y↔Z (S/R)y,x ⇔ ∀ z: (Rx,z ⇒ Sy,z) Y↔ X
R\S Right residual of R and S. R : X↔Y, S : X↔Z (R\S)y,z ⇔ ∀ x: (Rx,y ⇒ Sx,z) Y↔ Z
syq(R,S) Symmetric quotient of R and S. R : X↔Y, S : X↔Z syq(R,S)y,z ⇔ ∀ x: (Rx,y ⇔ Sx,z) Y↔ Z

Base functions for calculating closures:

trans(R) Transitive closure of R. R : X↔X trans(R) = R+ X↔ X
refl(R) Reflexive closure of R. R : X↔X refl(R)x,y ⇔ Rx,y ∨ x=y X↔ X
symm(R) Symmetric closure of R. R : X↔X symm(R)x,y ⇔ Rx,y ∨ Ry,x X↔ X

Various base functions concerning vectors and points without choice operations:

inj(v) Injection induced by the non-empty vector v. v : X↔1 inj(v)y,x ⇒ y=x Y↔X, Y ⊆ X
init(v) Initial point with the same dimension as the vector v. v : X↔1, X={1,2,...} init(v)x ⇔ x=1 X↔1
next(p) Successor of the point p with the same dimension as p. p : X↔1, X={1,2,...} next(p)x ⇔ px-1 X↔1
succ(v) Homogeneous successor relation with a dimension given by the number of rows of the vector v. v : X↔1, X={1,2,...} succ(v)x,y ⇔ y=x+1 X↔X

Base operations for choices:

point(v) A point included in the non-empty column vector v. v : X↔1 point(v)⊆v, |point(v)|=1 X↔1
atom(R) An atom (a relation consisting of one pair) included in the non-empty relation R. R : X↔Y atom(R)⊆R, |atom(R)|=1 X↔Y

Base operations which generate random relations. In the following, XY stands for two digits between 00 and 99 and denotes the probability that a pair is contained in the result:

randomXY(R) Generation of a random relation with the same dimension as R and probability XY/100, where XY is between 00 and 99. An example is random10(R) with probability 0.1. R : X↔Y X↔Y
randomcfXY(R) Generation of a cyclefree random relation with the same dimension as the homogeneous relation R. R : X↔X X↔X
random(R,S) Generation of a random relation with the same dimension as R and probability |S|/(|A|*|B|). For instance, if S has 10 rows and 2 columns and 5 of the 20=10*2 elements are set, then the probability is 5/20=0.25. Since version 8.1. R : X↔Y, S : A↔B X↔Y
randomperm(v) Generation of a random permutation, where the dimension is given by the number of rows of the vector v. v : X↔1 X↔X

Base functions for certain tests on relations. The result is true (represented by the universal relation on a singleton set) or false (represented by the empty relation on a singleton set):

empty(R) Test whether R is empty. R : X↔Y empty(R)⊥,⊥ ⇔ ∀ x,y: ¬ Rx,y 11
unival(R) Test whether R is univalent. R : X↔Y unival(R)⊥,⊥ ⇔ ∀ x∈X: ∀ y,z∈Y: (Rx,y ∧ Rx,z ⇒ y=z) 11
eq(R,S) Test whether R and S are equal. R, S : X↔Y eq(R,S)⊥,⊥ ⇔ R = S 11
incl(R,S) Test whether R is included in S. R, S : X↔Y incl(R,S)⊥,⊥ ⇔ R ⊆ S 11
cardeq(R,S) Test whether the cardinalities of R and S are equal. R, S : X↔Y cardeq(R,S)⊥,⊥ ⇔ |R|=|S| 11
cardlt(R,S) Test whether the cardinality of R is less than that of S. R, S : X↔Y cardlt(R,S)⊥,⊥ ⇔ |R|<|S| 11
cardleq(R,S) Test whether the cardinality of R is less than or equal to that of S. R, S : X↔Y cardleq(R,S)⊥,⊥ ⇔ |R|≤|S| 11
cardgt(R,S) Test whether the cardinality of R is greater than that of S. R, S : X↔Y cardgt(R,S)⊥,⊥ ⇔ |R|>|S| 11
cardgeq(R,S) Test whether the cardinality of R is greater than or equal to that of S. R, S : X↔Y cardgeq(R,S)⊥,⊥ ⇔ |R|≥|S| 11

Base functions concerning operations on powersets:

epsi(v) Membership relation, where the cardinality of the base set is given by the row number of the vector v. v : X↔1 X↔2X
cardrel(v) Size comparison relation on a powerset, where the cardinality of the base set is given by the row number of the vector v. v : X↔1 cardrel(v)A,B ⇔ |A| ≤ |B| 2X↔2X
cardfilter(v,w) If v is a vector with a powerset 2X as argument set and w is a vector with n ≤ |X| rows, then the operation selects from v all sets A fulfilling |A| < n. v : 2X1, w : Y↔1, |Y|≤|X| cardfilter(v)A,⊥ ⇔ vA ∧ |A|<|Y| 2X1

Base functions concerning relational product and sum domains. Most of these base functions take a domain definition as argument, the result however is always a relation:

1-st(DD) 1st component of domain DD. DD : X+Y or DD : X×Y 1-st(DD)x,y ⇔ false X↔X
2-nd(DD) 2nd component of domain DD. DD : X+Y or DD : X×Y 2-nd(DD)u,v ⇔ false Y↔Y
p-1(PP) Projection onto the 1st component of product domain PP. PP : X×Y X×Y↔X
p-2(PP) Projection onto the 2nd component of product domain PP. PP : X×Y X×Y↔Y
p-ord(PP) Product order of product domain PP with first component R : X↔X and second component S : Y↔Y. Sometimes written as R ⊗ S. Can be defined by R ⊗ S = [πR, ρS] where π and ρ are the projection relations for the domain PP. The operation [...,...] denotes tupling; see below. PP : X×Y p-ord(PP)⟨x,y⟩,⟨a,b⟩ ⇔ Rx,a ∧ Sy,b X×Y↔X×Y
[R,S] Tupling of relations R,S. R : X↔Y, S : X↔Z [R,S]x,⟨y,z⟩ ⇔ Rx,y ∧ Sx,z X↔Y×Z
[R,S|] Right tupling of relations R,S. This is the same as the [R,S]. Since version 8.1. See [R,S].
[|R,S] Left tupling of relations R,S. Since version 8.1. R : X↔Z, S : Y↔Z [|R,S]⟨x,y⟩,z ⇔ Rx,z ∧ Sy,z X×Y↔Z
i-1(SS) Injection into 1st component of sum domain SS. SS : X+Y X↔X+Y
i-2(SS) Injection into 2nd component of sum domain SS. SS : X+Y Y↔X+Y
s-ord(R,S) Sum order for relations R and S. R : X↔X, S : Y↔Y X+Y↔X+Y
R+S Sum of relations R and S. R : X↔Z, S : Y↔Z X+Y↔Z

Base functions concerning function domains:

part-f(R,S) Columnwise representation of partial functions. Functions maps to ⊥ if undefined. Z is not used. R : X↔Z, S : Y↔Z X×Y↔(Y∪{⊥})X
tot-f(R,S) Columnwise representation of total functions. Z is not used. R : X↔Z, S : Y↔Z X×Y↔YX

Base functions for minimal and maximal sets:

minsets(v) Minimal elements in vector v. Since version 8.1. v : 2X1 minsets(v)A ⇔ vA ∧ ¬∃ B⊆X: vB ∧ B⊂A 2X×1
minsets_upset(v) Minimal elements in vector v under the restriction that v represents an up-set. That is the case if for all S,T ⊆ X satisfying vS and S⊆T the fact vT is implied. This version is usually significantly faster than the general version. Since version 8.1. v : 2X1 Same as for minsets. 2X×1
maxsets(v) Maximal elements in vector v. Since version 8.1. v : 2X1 maxsets(v)A ⇔ vA ∧ ¬∃ B⊆X: vB ∧ A⊂B 2X×1
maxsets_downset(v) Maximal elements in vector v under the restriction that v represents a down-set. That is the case if for all S,T ⊆ X satisfying vT and S⊆T the fact vS is implied. This version is usually significantly faster than the general version. Since version 8.1. v : 2X1 Same as for maxsets. 2X×1
 
Rudolf Berghammer - rub@informatik.uni-kiel.de
Last modified: 17-Aug-2012, 11:59:20 CEST