Skip to content
Snippets Groups Projects
Commit bcb84193 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

improve notebook and use Event-B syntax

parent f4629c31
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 314 additions and 150 deletions
sks/2_Relationen.ipynb
+ 314
− 150
View file @ bcb84193
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
# Relationen in B # Relationen in B
Relationen sind ein wichtiger Bestandteil der B Sprache.
Sie bauen auf Paaren auf.
%% Cell type:code id: tags:
``` prob
:language event_b
```
%% Output
Changed language for user input to Event-B (forced)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Paare ## Paare
Geordnete Paare können in B mit dem "Maplet" Operator ↦ (ASCII |->) erstellt werden: Geordnete Paare können in B mit dem "Maplet" Operator ↦ (ASCII |->) erstellt werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{TRUE}↦1+1 {TRUE}↦1+1
``` ```
%% Output %% Output
$(\{\mathit{TRUE}\}\mapsto 2)$ $(\{\mathit{TRUE}\}\mapsto 2)$
({TRUE}↦2) ({TRUE}↦2)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Paare sind geordnet: Paare sind geordnet:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1↦2 = 2↦1 1↦2 = 2↦1
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Paare können verschachtelt werden: Paare können verschachtelt werden:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
1↦2↦3 = (1↦2)↦3 1↦2↦3 = (1↦2)↦3
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Kartesisches Produkt (Kreuzprodukt) ## Kartesisches Produkt (Kreuzprodukt)
Wir können das Kreuzprodukt zweier Mengen als "Set Comprehension" schreiben: 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) ```{a↦b | a:BOOL & b:1..2}``` (in klassischem B muss hier das Komma anstatt ↦ verwendet werden)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{a,b | a:BOOL & b:1..2} {a↦b | a:BOOL & b:1..2}
``` ```
%% Output %% Output
$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$ $\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$
{(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)} {(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{p | ∃(a,b).( a:BOOL ∧ b:1..2 ∧ p=a↦b)} {p | ∃a,b. a:BOOL ∧ b:1..2 ∧ p=a↦b}
``` ```
%% Output %% Output
$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$ $\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$
{(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)} {(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
BOOL × (1..2) BOOL × (1..2)
``` ```
%% Output %% Output
$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$ $\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$
{(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)} {(FALSE↦1),(FALSE↦2),(TRUE↦1),(TRUE↦2)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Relationen ## Relationen
Eine binäre Relation zwischen A und B ist eine Untermenge des Kreuzprodukts A × B. 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: Das Kreuzprodukt selber ist auch eine Relation, die jedes Element von A mit einem Element aus B in Relation setzt:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("rel",BOOL × (1..4)) :language classical_b
``` ```
%% Output %% Output
Changed language for user input to classical B (forced)
<Dot visualization: expr_as_graph [("rel",BOOL*(1..4))]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("rel",(1..3) × (1..3)) :dot expr_as_graph ("rel",(1..3) × (1..3))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("rel",(1..3)*(1..3))]> <Dot visualization: expr_as_graph [("rel",(1..3)*(1..3))]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("rel",{1|->3,3|->2, 2|->3}) :dot expr_as_graph ("rel",(1..3) × (1..3))
```
%% Output
<Dot visualization: expr_as_graph [("rel",(1..3)*(1..3))]>
%% Cell type:code id: tags:
``` prob
:dot expr_as_graph ("rel",{1↦3,3↦2, 2↦3})
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("rel",{(1,3),(3,2),(2,3)})]> <Dot visualization: expr_as_graph [("rel",{(1,3),(3,2),(2,3)})]>
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
(1..3)×(1..3) (1..3)×(1..3)
``` ```
%% Output %% Output
$\{(1\mapsto 1),(1\mapsto 2),(1\mapsto 3),(2\mapsto 1),(2\mapsto 2),(2\mapsto 3),(3\mapsto 1),(3\mapsto 2),(3\mapsto 3)\}$ $\{(1\mapsto 1),(1\mapsto 2),(1\mapsto 3),(2\mapsto 1),(2\mapsto 2),(2\mapsto 3),(3\mapsto 1),(3\mapsto 2),(3\mapsto 3)\}$
{(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3)} {(1↦1),(1↦2),(1↦3),(2↦1),(2↦2),(2↦3),(3↦1),(3↦2),(3↦3)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table POW((1..2)×(1..2)) :table POW((1..2)×(1..2))
``` ```
%% Output
|Elements|
|---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|
|$\{(1\mapsto 1)\}$|
|$\{(1\mapsto 1),(1\mapsto 2)\}$|
|$\{(1\mapsto 1),(2\mapsto 1)\}$|
|$\{(1\mapsto 1),(2\mapsto 2)\}$|
|$\{(1\mapsto 2)\}$|
|$\{(1\mapsto 1),(1\mapsto 2),(2\mapsto 1)\}$|
|$\{(1\mapsto 1),(1\mapsto 2),(2\mapsto 2)\}$|
|$\{(1\mapsto 2),(2\mapsto 1)\}$|
|$\{(1\mapsto 2),(2\mapsto 2)\}$|
|$\{(1\mapsto 1),(1\mapsto 2),(2\mapsto 1),(2\mapsto 2)\}$|
|$\{(2\mapsto 1)\}$|
|$\{(1\mapsto 1),(2\mapsto 1),(2\mapsto 2)\}$|
|$\{(1\mapsto 2),(2\mapsto 1),(2\mapsto 2)\}$|
|$\{(2\mapsto 1),(2\mapsto 2)\}$|
|$\{(2\mapsto 2)\}$|
Elements
{}
{(1|->1)}
{(1|->1),(1|->2)}
{(1|->1),(2|->1)}
{(1|->1),(2|->2)}
{(1|->2)}
{(1|->1),(1|->2),(2|->1)}
{(1|->1),(1|->2),(2|->2)}
{(1|->2),(2|->1)}
{(1|->2),(2|->2)}
{(1|->1),(1|->2),(2|->1),(2|->2)}
{(2|->1)}
{(1|->1),(2|->1),(2|->2)}
{(1|->2),(2|->1),(2|->2)}
{(2|->1),(2|->2)}
{(2|->2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table (BOOL<->(1..2)) :table (BOOL<->(1..2))
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$| |$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|
|$\{(\mathit{FALSE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{TRUE}\mapsto 2)\}$|
Elements Elements
{} {}
{(FALSE|->1)} {(FALSE|->1)}
{(FALSE|->1),(FALSE|->2)} {(FALSE|->1),(FALSE|->2)}
{(FALSE|->1),(TRUE|->1)} {(FALSE|->1),(TRUE|->1)}
{(FALSE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->2)}
{(FALSE|->2)} {(FALSE|->2)}
{(FALSE|->1),(FALSE|->2),(TRUE|->1)} {(FALSE|->1),(FALSE|->2),(TRUE|->1)}
{(FALSE|->1),(FALSE|->2),(TRUE|->2)} {(FALSE|->1),(FALSE|->2),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1)} {(FALSE|->2),(TRUE|->1)}
{(FALSE|->2),(TRUE|->2)} {(FALSE|->2),(TRUE|->2)}
{(FALSE|->1),(FALSE|->2),(TRUE|->1),(TRUE|->2)} {(FALSE|->1),(FALSE|->2),(TRUE|->1),(TRUE|->2)}
{(TRUE|->1)} {(TRUE|->1)}
{(FALSE|->1),(TRUE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->1),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1),(TRUE|->2)} {(FALSE|->2),(TRUE|->1),(TRUE|->2)}
{(TRUE|->1),(TRUE|->2)} {(TRUE|->1),(TRUE|->2)}
{(TRUE|->2)} {(TRUE|->2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1|->3,3|->2, 3|->3} /\ id(1..3) {1↦3,3↦2, 3↦3} /\ id(1..3)
``` ```
%% Output %% Output
$\{(3\mapsto 3)\}$ $\{(3\mapsto 3)\}$
{(3↦3)} {(3↦3)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:dot expr_as_graph ("rel",id(1..3)) :dot expr_as_graph ("rel",id(1..3))
``` ```
%% Output %% Output
<Dot visualization: expr_as_graph [("rel",id(1..3))]> <Dot visualization: expr_as_graph [("rel",id(1..3))]>
%% Cell type:code id: tags:
``` prob
:language event_b
```
%% Output
Changed language for user input to Event-B (forced)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Operatoren auf Relationen ## Operatoren auf Relationen
In B gibt es folgende Operatoren auf Relationen: In B gibt es folgende Operatoren auf Relationen:
Relational Image: Relational Image:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1|->3,3|->2, 3|->3} [ {3} ] {1↦3,3↦2, 3↦3} [ {3} ]
``` ```
%% Output %% Output
$\{2,3\}$ $\{2,3\}$
{2,3} {2,3}
%% Cell type:markdown id: tags:
Das relational image kann man auch so ausdrücken:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
r={1|->3,3|->2, 3|->3} & img3 = {y | 3|->y : r} r={1↦3,3↦2, 3↦3} & img3 = {y | 3↦y : r}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{img3} = \{2,3\}$ * $\mathit{img3} = \{2,3\}$
* $\mathit{r} = \{(1\mapsto 3),(3\mapsto 2),(3\mapsto 3)\}$ * $\mathit{r} = \{(1\mapsto 3),(3\mapsto 2),(3\mapsto 3)\}$
TRUE TRUE
Solution: Solution:
img3 = {2,3} img3 = {2,3}
r = {(1↦3),(3↦2),(3↦3)} r = {(1↦3),(3↦2),(3↦3)}
%% Cell type:markdown id: tags:
Wenn man das Paar umdreht kann man von der Zielmenge rückwärts mögliche Eingaben bestimmen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
r={1|->3,3|->2, 3|->3} & img3 = {y | y|->3 : r} r={1↦3,3↦2, 3↦3} & img3 = {y | y↦3 : r}
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{img3} = \{1,3\}$ * $\mathit{img3} = \{1,3\}$
* $\mathit{r} = \{(1\mapsto 3),(3\mapsto 2),(3\mapsto 3)\}$ * $\mathit{r} = \{(1\mapsto 3),(3\mapsto 2),(3\mapsto 3)\}$
TRUE TRUE
Solution: Solution:
img3 = {1,3} img3 = {1,3}
r = {(1↦3),(3↦2),(3↦3)} r = {(1↦3),(3↦2),(3↦3)}
%% Cell type:markdown id: tags:
Bequemer geht dies mit dem relationalen Abbild und dem Umkehroperator ```~```
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1|->3,3|->2, 3|->3}~[{3}] {1↦3,3↦2, 3↦3}~[{3}]
``` ```
%% Output %% Output
$\{1,3\}$ $\{1,3\}$
{1,3} {1,3}
%% Cell type:markdown id: tags:
Mit dom und ran kann man die Domäne und den Wertebereich einer Relation berrechnen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
dom({1|->3,3|->2, 3|->4}) dom({1↦3,3↦2, 3↦4})
``` ```
%% Output %% Output
$\{1,3\}$ $\{1,3\}$
{1,3} {1,3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ran({1|->3,3|->2, 3|->4}) ran({1↦3,3↦2, 3↦4})
``` ```
%% Output %% Output
$\{2,3,4\}$ $\{2,3,4\}$
{2,3,4} {2,3,4}
%% Cell type:markdown id: tags:
Man kann Relationen mit dem ```;``` Operator verketten:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
({1|->3,3|->2, 3|->4} ; {1|->3,3|->2, 3|->44}) ({1↦3,3↦2, 3↦4} ; {1↦3,3↦2, 3↦44})
``` ```
%% Output %% Output
$\{(1\mapsto 2),(1\mapsto 44)\}$ $\{(1\mapsto 2),(1\mapsto 44)\}$
{(1↦2),(1↦44)} {(1↦2),(1↦44)}
%% Cell type:markdown id: tags:
Mit dem Override Operator ```<+``` kann man eine Relation an bestimmten Stellen überschreiben:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{11 |-> TRUE, 22|->FALSE,22|->TRUE} <+ {22|->TRUE,33|->FALSE} {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE} <+ {22↦TRUE,33↦FALSE}
``` ```
%% Output %% Output
$\{(11\mapsto \mathit{TRUE}),(22\mapsto \mathit{TRUE}),(33\mapsto \mathit{FALSE})\}$ $\{(11\mapsto \mathit{TRUE}),(22\mapsto \mathit{TRUE}),(33\mapsto \mathit{FALSE})\}$
{(11↦TRUE),(22↦TRUE),(33↦FALSE)} {(11↦TRUE),(22↦TRUE),(33↦FALSE)}
%% Cell type:markdown id: tags:
Mit dem Domain Restriction Operator ```<|``` kann man eine Relation auf eine Domäne einschränken. Es gibt insgesamt vier Operatoren um Relationen einzuschränken ```<|```, ```<<|```, ```|>```, ```|>>```.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{22} <| {11 |-> TRUE, 22|->FALSE,22|->TRUE, 33|->FALSE} {22} <| {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE}
``` ```
%% Output %% Output
$\{(22\mapsto \mathit{FALSE}),(22\mapsto \mathit{TRUE})\}$ $\{(22\mapsto \mathit{FALSE}),(22\mapsto \mathit{TRUE})\}$
{(22↦FALSE),(22↦TRUE)} {(22↦FALSE),(22↦TRUE)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{11 |-> TRUE, 22|->FALSE,22|->TRUE, 33|->FALSE} [{22}] {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE} [{22}]
``` ```
%% Output %% Output
$\{\mathit{FALSE},\mathit{TRUE}\}$ $\{\mathit{FALSE},\mathit{TRUE}\}$
{FALSE,TRUE} {FALSE,TRUE}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{11} <| {11 |-> TRUE, 22|->FALSE,22|->TRUE, 33|->FALSE} |> {TRUE} {11} <| {11 ↦ TRUE, 22 ↦ FALSE,22 ↦ TRUE, 33 ↦ FALSE} |> {TRUE}
``` ```
%% Output %% Output
$\{(11\mapsto \mathit{TRUE})\}$ $\{(11\mapsto \mathit{TRUE})\}$
{(11↦TRUE)} {(11↦TRUE)}
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
## Spezialfälle von Relationen ## Spezialfälle von Relationen
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
id(2..3) id(2..3)
``` ```
%% Output %% Output
$\{(2\mapsto 2),(3\mapsto 3)\}$ $\{2,3\}$
{(2↦2),(3↦3)} {2,3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table BOOL <-> 1..2 :table BOOL <-> 1..2
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$| |$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|
|$\{(\mathit{FALSE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{TRUE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{TRUE}\mapsto 2)\}$|
Elements Elements
{} {}
{(FALSE|->1)} {(FALSE|->1)}
{(FALSE|->1),(FALSE|->2)} {(FALSE|->1),(FALSE|->2)}
{(FALSE|->1),(TRUE|->1)} {(FALSE|->1),(TRUE|->1)}
{(FALSE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->2)}
{(FALSE|->2)} {(FALSE|->2)}
{(FALSE|->1),(FALSE|->2),(TRUE|->1)} {(FALSE|->1),(FALSE|->2),(TRUE|->1)}
{(FALSE|->1),(FALSE|->2),(TRUE|->2)} {(FALSE|->1),(FALSE|->2),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1)} {(FALSE|->2),(TRUE|->1)}
{(FALSE|->2),(TRUE|->2)} {(FALSE|->2),(TRUE|->2)}
{(FALSE|->1),(FALSE|->2),(TRUE|->1),(TRUE|->2)} {(FALSE|->1),(FALSE|->2),(TRUE|->1),(TRUE|->2)}
{(TRUE|->1)} {(TRUE|->1)}
{(FALSE|->1),(TRUE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->1),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1),(TRUE|->2)} {(FALSE|->2),(TRUE|->1),(TRUE|->2)}
{(TRUE|->1),(TRUE|->2)} {(TRUE|->1),(TRUE|->2)}
{(TRUE|->2)} {(TRUE|->2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table BOOL --> 1..2 :table BOOL --> 1..2
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$|
Elements Elements
{(FALSE|->1),(TRUE|->1)} {(FALSE|->1),(TRUE|->1)}
{(FALSE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1)} {(FALSE|->2),(TRUE|->1)}
{(FALSE|->2),(TRUE|->2)} {(FALSE|->2),(TRUE|->2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{11|->2800, 22|->3500}[{11}] {11↦2800, 22↦3500}[{11}]
``` ```
%% Output %% Output
$\{2800\}$ $\{2800\}$
{2800} {2800}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
({11|->2800,22|->3500}(11)) ({11↦2800,22↦3500}(11))
``` ```
%% Output %% Output
$2800$ $2800$
2800 2800
%% Cell type:markdown id: tags:
Mit dem Lambda Operator ```%``` kann man Funktionen erstellen:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
%x.(x:0..9|(x+1) mod 10) (%x.x:0..9|(x+1) mod 10)
``` ```
%% Output %% Output
$\{(0\mapsto 1),(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 0)\}$ $\{(0\mapsto 1),(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 0)\}$
{(0↦1),(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦0)} {(0↦1),(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦0)}
%% Cell type:markdown id: tags:
Dies ist äquivalent zu:
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{x,result | x:0..9 & result = (x+1) mod 10} {x↦result | x:0..9 & result = (x+1) mod 10}
``` ```
%% Output %% Output
$\{(0\mapsto 1),(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 0)\}$ $\{(0\mapsto 1),(1\mapsto 2),(2\mapsto 3),(3\mapsto 4),(4\mapsto 5),(5\mapsto 6),(6\mapsto 7),(7\mapsto 8),(8\mapsto 9),(9\mapsto 0)\}$
{(0↦1),(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦0)} {(0↦1),(1↦2),(2↦3),(3↦4),(4↦5),(5↦6),(6↦7),(7↦8),(8↦9),(9↦0)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table BOOL --> 1..2 :table BOOL --> 1..2
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$|
Elements Elements
{(FALSE|->1),(TRUE|->1)} {(FALSE|->1),(TRUE|->1)}
{(FALSE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1)} {(FALSE|->2),(TRUE|->1)}
{(FALSE|->2),(TRUE|->2)} {(FALSE|->2),(TRUE|->2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table BOOL -->> 1..2 :table BOOL -->> 1..2
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
Elements Elements
{(FALSE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1)} {(FALSE|->2),(TRUE|->1)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table BOOL >-> 1..2 :table BOOL >-> 1..2
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
Elements Elements
{(FALSE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->2)}
{(FALSE|->2),(TRUE|->1)} {(FALSE|->2),(TRUE|->1)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:table BOOL +-> 1..2 :table BOOL +-> 1..2
``` ```
%% Output %% Output
|Elements| |Elements|
|---| |---|
|$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$| |$\renewcommand{\emptyset}{\mathord\varnothing}\emptyset$|
|$\{(\mathit{FALSE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 2)\}$|
|$\{(\mathit{TRUE}\mapsto 1)\}$| |$\{(\mathit{TRUE}\mapsto 1)\}$|
|$\{(\mathit{TRUE}\mapsto 2)\}$| |$\{(\mathit{TRUE}\mapsto 2)\}$|
Elements Elements
{} {}
{(FALSE|->1)} {(FALSE|->1)}
{(FALSE|->1),(TRUE|->1)} {(FALSE|->1),(TRUE|->1)}
{(FALSE|->1),(TRUE|->2)} {(FALSE|->1),(TRUE|->2)}
{(FALSE|->2)} {(FALSE|->2)}
{(FALSE|->2),(TRUE|->1)} {(FALSE|->2),(TRUE|->1)}
{(FALSE|->2),(TRUE|->2)} {(FALSE|->2),(TRUE|->2)}
{(TRUE|->1)} {(TRUE|->1)}
{(TRUE|->2)} {(TRUE|->2)}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{f| f:BOOL +-> 1..2 & dom(f)=BOOL & ran(f)=1..2} {f| f:BOOL +-> 1..2 & dom(f)=BOOL & ran(f)=1..2}
``` ```
%% Output %% Output
$\{\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\},\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}\}$ $\{\{(\mathit{FALSE}\mapsto 1),(\mathit{TRUE}\mapsto 2)\},\{(\mathit{FALSE}\mapsto 2),(\mathit{TRUE}\mapsto 1)\}\}$
{{(FALSE↦1),(TRUE↦2)},{(FALSE↦2),(TRUE↦1)}} {{(FALSE↦1),(TRUE↦2)},{(FALSE↦2),(TRUE↦1)}}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1|->22, 2|->33, 3|->22} {1|->22, 2|->33, 3|->22}
``` ```
%% Output %% Output
$[22,33,22]$ $[22,33,22]$
[22,33,22] [22,33,22]
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1|->22, 2|->33, 3|->22} (2) {1|->22, 2|->33, 3|->22} (2)
``` ```
%% Output %% Output
$33$ $33$
33 33
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
{1|->22, 2|->33, 3|->22}~[{22}] {1|->22, 2|->33, 3|->22}~[{22}]
``` ```
%% Output %% Output
$\{1,3\}$ $\{1,3\}$
{1,3} {1,3}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
card({1|->22, 2|->33, 3|->22}) card({1|->22, 2|->33, 3|->22})
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
ran({1|->22, 2|->33, 3|->22}) ran({1|->22, 2|->33, 3|->22})
``` ```
%% Output %% Output
$\{22,33\}$ $\{22,33\}$
{22,33} {22,33}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
``` ```
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment