Computer-Aided Program
Development Institute of Computer Science Faculty of Engineering, Christian-Albrechts-University of Kiel |
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 1↔1. | TRUE()_{⊥,⊥} ⇔ true | 1↔1 | |
FALSE(), false() | Empty relation with type 1↔1. | FALSE()_{⊥,⊥} ⇔ false | 1↔1 | |
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: R_{x,y} | X↔1 |
Base functions for calculating Boolean operations: |
||||
-R | Negation (complement) of relation R. | R : X↔Y | (-R)_{x,y} ⇔ ¬R_{x,y} | X↔ Y |
R|S | Union (join) of R and S. | R, S : X↔Y | (R|S)_{x,y} ⇔ R_{x,y} ∨ S_{x,y} | X↔ Y |
R&S | Intersection (meet) of R and S. | R, S : X↔Y | (R&S)_{x,y} ⇔ R_{x,y} ∧ S_{x,y} | X↔ Y |
Base functions for calculating relationalgebraic operations: |
||||
R^ | Transposition of relation R. | R : X↔Y | (R^)_{y,x} ⇔ R_{x,y} | Y↔ X |
R*S | Composition (product) of R and S. | R : X↔Y, S : Y↔Z | (R*S)_{x,z} ⇔ ∃ y: R_{x,y} ∧ S_{y,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: (R_{x,z} ⇒ S_{y,z}) | Y↔ X |
R\S | Right residual of R and S. | R : X↔Y, S : X↔Z | (R\S)_{y,z} ⇔ ∀ x: (R_{x,y} ⇒ S_{x,z}) | Y↔ Z |
syq(R,S) | Symmetric quotient of R and S. | R : X↔Y, S : X↔Z | syq(R,S)_{y,z} ⇔ ∀ x: (R_{x,y} ⇔ S_{x,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} ⇔ R_{x,y} ∨ x=y | X↔ X |
symm(R) | Symmetric closure of R. | R : X↔X | symm(R)_{x,y} ⇔ R_{x,y} ∨ R_{y,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} ⇔ p_{x-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: ¬ R_{x,y} | 1↔1 |
unival(R) | Test whether R is univalent. | R : X↔Y | unival(R)_{⊥,⊥} ⇔ ∀ x∈X: ∀ y,z∈Y: (R_{x,y} ∧ R_{x,z} ⇒ y=z) | 1↔1 |
eq(R,S) | Test whether R and S are equal. | R, S : X↔Y | eq(R,S)_{⊥,⊥} ⇔ R = S | 1↔1 |
incl(R,S) | Test whether R is included in S. | R, S : X↔Y | incl(R,S)_{⊥,⊥} ⇔ R ⊆ S | 1↔1 |
cardeq(R,S) | Test whether the cardinalities of R and S are equal. | R, S : X↔Y | cardeq(R,S)_{⊥,⊥} ⇔ |R|=|S| | 1↔1 |
cardlt(R,S) | Test whether the cardinality of R is less than that of S. | R, S : X↔Y | cardlt(R,S)_{⊥,⊥} ⇔ |R|<|S| | 1↔1 |
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| | 1↔1 |
cardgt(R,S) | Test whether the cardinality of R is greater than that of S. | R, S : X↔Y | cardgt(R,S)_{⊥,⊥} ⇔ |R|>|S| | 1↔1 |
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| | 1↔1 |
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↔2^{X} | |
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| | 2^{X}↔2^{X} |
cardfilter(v,w) | If v is a vector with a powerset 2^{X} 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 : 2^{X}↔1, w : Y↔1, |Y|≤|X| | cardfilter(v)_{A,⊥} ⇔ v_{A} ∧ |A|<|Y| | 2^{X}↔1 |
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. | 1-st(DD)_{x,y} ⇔ false | X↔X | |
2-nd(DD) | 2nd component of domain DD. | 2-nd(DD)_{u,v} ⇔ false | Y↔Y | |
p-1(PP) | Projection onto the 1st component of product domain PP. | X×Y↔X | ||
p-2(PP) | Projection onto the 2nd component of product domain PP. | 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. | p-ord(PP)_{⟨x,y⟩,⟨a,b⟩} ⇔ R_{x,a} ∧ S_{y,b} | X×Y↔X×Y | |
[R,S] | Tupling of relations R,S. | R : X↔Y, S : X↔Z | [R,S]_{x,⟨y,z⟩} ⇔ R_{x,y} ∧ S_{x,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} ⇔ R_{x,z} ∧ S_{y,z} | X×Y↔Z |
i-1(SS) | Injection into 1st component of sum domain SS. | X↔X+Y | ||
i-2(SS) | Injection into 2nd component of sum domain SS. | 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↔Y^{X} | |
Base functions for minimal and maximal sets: |
||||
minsets(v) | Minimal elements in vector v. Since version 8.1. | v : 2^{X}↔1 | minsets(v)_{A} ⇔ v_{A} ∧ ¬∃ B⊆X: v_{B} ∧ B⊂A | 2^{X}×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 v_{S} and S⊆T the fact v_{T} is implied. This version is usually significantly faster than the general version. Since version 8.1. | v : 2^{X}↔1 | Same as for minsets. | 2^{X}×1 |
maxsets(v) | Maximal elements in vector v. Since version 8.1. | v : 2^{X}↔1 | maxsets(v)_{A} ⇔ v_{A} ∧ ¬∃ B⊆X: v_{B} ∧ A⊂B | 2^{X}×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 v_{T} and S⊆T the fact v_{S} is implied. This version is usually significantly faster than the general version. Since version 8.1. | v : 2^{X}↔1 | Same as for maxsets. | 2^{X}×1 |