Relationen in B
Relationen sind ein wichtiger Bestandteil der B Sprache. Sie bauen auf Paaren auf.
B => :language event_b
ha-Ha broken
Paare
Geordnete Paare können in B mit dem "Maplet" Operator ↦ (ASCII |->) erstellt werden:
B => {TRUE}↦1+1
[#{true} -> 2]
Paare sind geordnet:
B => 1↦2 = 2↦1
FALSE
Paare können verschachtelt werden:
B => 1↦2↦3 = (1↦2)↦3
TRUE
Kartesisches Produkt (Kreuzprodukt)
Wir können das Kreuzprodukt zweier Mengen als "Set Comprehension" schreiben:
{a↦b | a:BOOL & b:1..2} (in klassischem B muss hier das Komma anstatt ↦ verwendet werden)
B => {a↦b | a:BOOL & b:1..2}
#{[true -> 1] [false -> 2] [true -> 2] [false -> 1]}
B => {p | ∃a,b. a:BOOL ∧ b:1..2 ∧ p=a↦b}
ha-Ha broken
B => BOOL × (1..2)
#{[true -> 1] [false -> 2] [true -> 2] [false -> 1]}
Relationen
Eine binäre Relation zwischen A und B ist eine Untermenge des Kreuzprodukts A × B. Das Kreuzprodukt selber ist auch eine Relation, die jedes Element von A mit einem Element aus B in Relation setzt:
B => :language classical_b
ha-Ha broken
B => :dot expr_as_graph ("rel",(1..3) × (1..3))
ha-Ha broken
B => :dot expr_as_graph ("rel",(1..3) × (1..3))
ha-Ha broken
B => :dot expr_as_graph ("rel",{1↦3,3↦2, 2↦3})
ha-Ha broken
B => (1..3)×(1..3)
#{[1 -> 2] [3 -> 3] [2 -> 3] [2 -> 1] [3 -> 1] [2 -> 2] [1 -> 3] [1 -> 1] [3 -> 2]}
B => :table POW((1..2)×(1..2))
ha-Ha broken
B => :table (BOOL<->(1..2))
ha-Ha broken
B => {1↦3,3↦2, 3↦3} /\ id(1..3)
lol, broken
B => :dot expr_as_graph ("rel",id(1..3))
ha-Ha broken
B => :language event_b
ha-Ha broken
Operatoren auf Relationen
In B gibt es folgende Operatoren auf Relationen:
Relational Image:
B => {1↦3,3↦2, 3↦3} [ {3} ]
#{3 2}
Das relational image kann man auch so ausdrücken:
B => r={1↦3,3↦2, 3↦3} & img3 = {y | 3↦y : r}
{"img3" #{3 2}, "r" #{[3 -> 3] [3 -> 2] [1 -> 3]}}
Wenn man das Paar umdreht kann man von der Zielmenge rückwärts mögliche Eingaben bestimmen:
B => r={1↦3,3↦2, 3↦3} & img3 = {y | y↦3 : r}
{"img3" #{1 3}, "r" #{[1 -> 3] [3 -> 3] [3 -> 2]}}
Bequemer geht dies mit dem relationalen Abbild und dem Umkehroperator ~
B => {1↦3,3↦2, 3↦3}~[{3}]
#{1 3}
Mit dom und ran kann man die Domäne und den Wertebereich einer Relation berrechnen:
B => dom({1↦3,3↦2, 3↦4})
#{1 3}
B => ran({1↦3,3↦2, 3↦4})
#{4 3 2}
Man kann Relationen mit dem ; Operator verketten:
B => ({1↦3,3↦2, 3↦4} ; {1↦3,3↦2, 3↦44})
#{[1 -> 44] [1 -> 2]}
Mit dem Override Operator <+ kann man eine Relation an bestimmten Stellen überschreiben:
B => {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE} <+ {22↦TRUE,33↦FALSE}
#{[11 -> true] [33 -> false] [22 -> true]}
Mit dem Domain Restriction Operator <| kann man eine Relation auf eine Domäne einschränken. Es gibt insgesamt vier Operatoren um Relationen einzuschränken <|, <<|, |>, |>>.
B => {22} <| {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE}
#{[22 -> true] [22 -> false]}
B => {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE} [{22}]
#{true false}
B => {11} <| {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE} |> {TRUE}
#{[11 -> true]}
Spezialfälle von Relationen
B => id(2..3)
#{3 2}
B => :table BOOL <-> 1..2
ha-Ha broken
B => :table BOOL --> 1..2
ha-Ha broken
B => {11↦2800, 22↦3500}[{11}]
#{2800}
B => ({11↦2800,22↦3500}(11))
2800
Mit dem Lambda Operator % kann man Funktionen erstellen:
B => (%x.x:0..9|(x+1) mod 10)
ha-Ha broken
Dies ist äquivalent zu:
B => {x↦result | x:0..9 & result = (x+1) mod 10}
#{[0 -> 1] [8 -> 9] [4 -> 5] [9 -> 0] [2 -> 3] [5 -> 6] [1 -> 2] [6 -> 7] [7 -> 8] [3 -> 4]}
B => :table BOOL --> 1..2
ha-Ha broken
B => :table BOOL -->> 1..2
ha-Ha broken
B => :table BOOL >-> 1..2
ha-Ha broken
B => :table BOOL +-> 1..2
ha-Ha broken
B => {f| f:BOOL +-> 1..2 & dom(f)=BOOL & ran(f)=1..2}
#{#{[true -> 2] [false -> 1]} #{[true -> 1] [false -> 2]}}
B => {1|->22, 2|->33, 3|->22}
#{[1 -> 22] [3 -> 22] [2 -> 33]}
B => {1|->22, 2|->33, 3|->22} (2)
33
B => {1|->22, 2|->33, 3|->22}~[{22}]
#{1 3}
B => card({1|->22, 2|->33, 3|->22})
3
B => ran({1|->22, 2|->33, 3|->22})
#{33 22}