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: 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 | 1↔1 |
| unival(R) | Test whether R is univalent. | R : X↔Y | unival(R)⊥,⊥ ⇔ ∀ x∈X: ∀ y,z∈Y: (Rx,y ∧ Rx,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↔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 : 2X↔1, w : Y↔1, |Y|≤|X| | cardfilter(v)A,⊥ ⇔ vA ∧ |A|<|Y| | 2X↔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⟩ ⇔ 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. | 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↔YX | |
Base functions for minimal and maximal sets: |
||||
| minsets(v) | Minimal elements in vector v. Since version 8.1. | v : 2X↔1 | 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 : 2X↔1 | Same as for minsets. | 2X×1 |
| maxsets(v) | Maximal elements in vector v. Since version 8.1. | v : 2X↔1 | 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 : 2X↔1 | Same as for maxsets. | 2X×1 |