- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav08:sets_and_relations [2010/02/26 21:56] vkuncak |
sav08:sets_and_relations [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 13: | Line 13: | ||

To denote large or infinite sets we can use set comprehensions: $\{ x.\ P(x) \}$ is set of all objects with property $P$. | To denote large or infinite sets we can use set comprehensions: $\{ x.\ P(x) \}$ is set of all objects with property $P$. | ||

- | \[ | + | \begin{equation*} |

y \in \{ x. P(x) \} \ \leftrightarrow\ P(y) | y \in \{ x. P(x) \} \ \leftrightarrow\ P(y) | ||

- | \] | + | \end{equation*} |

Notation for set comprehension: $\{ f(x)|x. P(x) \} = \{ y. (\exists x. y=f(x) \land P(x)) \}$ | Notation for set comprehension: $\{ f(x)|x. P(x) \} = \{ y. (\exists x. y=f(x) \land P(x)) \}$ | ||

Sometimes the binder $x$ can be inferred from context so we write simply $\{ f(x) | P(x) \}$. In general there is ambiguity in which variables are bound. (Example: what does the $a$ in $f(a,b)$ refer to in the expression: | Sometimes the binder $x$ can be inferred from context so we write simply $\{ f(x) | P(x) \}$. In general there is ambiguity in which variables are bound. (Example: what does the $a$ in $f(a,b)$ refer to in the expression: | ||

- | \[ | + | \begin{equation*} |

\{a \} \cup \{ f(a,b) \mid P(a,b) \} | \{a \} \cup \{ f(a,b) \mid P(a,b) \} | ||

- | \] | + | \end{equation*} |

does it refer to the outerone $a$ as in $\{a\}$ or is it a newly bound variable? The notation with dot and bar resolves this ambiguity. | does it refer to the outerone $a$ as in $\{a\}$ or is it a newly bound variable? The notation with dot and bar resolves this ambiguity. | ||

Subset: $A \subseteq B$ means $\forall x. x \in A \rightarrow x \in B$ | Subset: $A \subseteq B$ means $\forall x. x \in A \rightarrow x \in B$ | ||

- | \[ | + | \begin{equation*} |

A \cup B = \{ x. x \in A \lor x \in B \} | A \cup B = \{ x. x \in A \lor x \in B \} | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

A \cap B = \{ x. x \in A \land x \in B \} | A \cap B = \{ x. x \in A \land x \in B \} | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

A \setminus B = \{ x. x \in A \land x \notin B \} | A \setminus B = \{ x. x \in A \land x \notin B \} | ||

- | \] | + | \end{equation*} |

Boolean algebra of subsets of some set $U$ (we define $A^c = U \setminus A$): | Boolean algebra of subsets of some set $U$ (we define $A^c = U \setminus A$): | ||

Line 55: | Line 55: | ||

Note that sets can be nested. Consider, for example, the following set $S$ | Note that sets can be nested. Consider, for example, the following set $S$ | ||

- | \[ | + | \begin{equation*} |

S = \{ \{ p, \{q, r\} \}, r \} | S = \{ \{ p, \{q, r\} \}, r \} | ||

- | \] | + | \end{equation*} |

This set has two elements. The first element is another set. We have $\{ p, \{q, r\} \} \in S$. Note that it is not the case that | This set has two elements. The first element is another set. We have $\{ p, \{q, r\} \} \in S$. Note that it is not the case that | ||

Suppose that we have a set $B$ that contains other sets. We define union of the sets contained in $B$ as follows: | Suppose that we have a set $B$ that contains other sets. We define union of the sets contained in $B$ as follows: | ||

- | \[ | + | \begin{equation*} |

\bigcup B = \{ x.\ \exists a. a \in B \land x \in a \} | \bigcup B = \{ x.\ \exists a. a \in B \land x \in a \} | ||

- | \] | + | \end{equation*} |

As a special case, we have | As a special case, we have | ||

- | \[ | + | \begin{equation*} |

\bigcup \{ a_1, a_2, a_3 \} = a_1 \cup a_2 \cup a_3 | \bigcup \{ a_1, a_2, a_3 \} = a_1 \cup a_2 \cup a_3 | ||

- | \] | + | \end{equation*} |

Often the elements of the set $B$ are computed by a set comprehension of the form $B = \{ f(i).\ i \in J \}$. | Often the elements of the set $B$ are computed by a set comprehension of the form $B = \{ f(i).\ i \in J \}$. | ||

We then write | We then write | ||

- | \[ | + | \begin{equation*} |

\bigcup_{i \in J} f(i) | \bigcup_{i \in J} f(i) | ||

- | \] | + | \end{equation*} |

and the meaning is | and the meaning is | ||

- | \[ | + | \begin{equation*} |

\bigcup \{ f(i).\ i \in J \} | \bigcup \{ f(i).\ i \in J \} | ||

- | \] | + | \end{equation*} |

Therefore, $x \in \bigcup \{ f(i).\ i \in J \}$ is equivalent to $\exists i.\ i \in J \land x \in f(i)$. | Therefore, $x \in \bigcup \{ f(i).\ i \in J \}$ is equivalent to $\exists i.\ i \in J \land x \in f(i)$. | ||

We analogously define intersection of elements in the set: | We analogously define intersection of elements in the set: | ||

- | \[ | + | \begin{equation*} |

\bigcap B = \{ x. \forall a. a \in B \rightarrow x \in a \} | \bigcap B = \{ x. \forall a. a \in B \rightarrow x \in a \} | ||

- | \] | + | \end{equation*} |

As a special case, we have | As a special case, we have | ||

- | \[ | + | \begin{equation*} |

\bigcap \{ a_1, a_2, a_3 \} = a_1 \cap a_2 \cap a_3 | \bigcap \{ a_1, a_2, a_3 \} = a_1 \cap a_2 \cap a_3 | ||

- | \] | + | \end{equation*} |

We similarly define intersection of an infinite family | We similarly define intersection of an infinite family | ||

- | \[ | + | \begin{equation*} |

\bigcap_{i \in J} f(i) | \bigcap_{i \in J} f(i) | ||

- | \] | + | \end{equation*} |

and the meaning is | and the meaning is | ||

- | \[ | + | \begin{equation*} |

\bigcap \{ f(i).\ i \in J \} | \bigcap \{ f(i).\ i \in J \} | ||

- | \] | + | \end{equation*} |

Therefore, $x \in \bigcap \{ f(i).\ i \in J \}$ is equivalent to $\forall i.\ i \in J \rightarrow x \in f(i)$. | Therefore, $x \in \bigcap \{ f(i).\ i \in J \}$ is equivalent to $\forall i.\ i \in J \rightarrow x \in f(i)$. | ||

Line 101: | Line 101: | ||

Pairs: | Pairs: | ||

- | \[ | + | \begin{equation*} |

(a,b) = (u,v) \iff (a = u \land b = v) | (a,b) = (u,v) \iff (a = u \land b = v) | ||

- | \] | + | \end{equation*} |

Cartesian product: | Cartesian product: | ||

- | \[ | + | \begin{equation*} |

A \times B = \{ (x,y) \mid x \in A \land y \in B \} | A \times B = \{ (x,y) \mid x \in A \land y \in B \} | ||

- | \] | + | \end{equation*} |

Relations $r$ is simply a subset of $A \times B$, that is $r \subseteq A \times B$. | Relations $r$ is simply a subset of $A \times B$, that is $r \subseteq A \times B$. | ||

Note: | Note: | ||

- | \[ | + | \begin{equation*} |

A \times (B \cap C) = (A \times B) \cap (A \times C) | A \times (B \cap C) = (A \times B) \cap (A \times C) | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

A \times (B \cup C) = (A \times B) \cup (A \times C) | A \times (B \cup C) = (A \times B) \cup (A \times C) | ||

- | \] | + | \end{equation*} |

=== Diagonal relation === | === Diagonal relation === | ||

$\Delta_A \subseteq A \times A$, is given by | $\Delta_A \subseteq A \times A$, is given by | ||

- | \[ | + | \begin{equation*} |

\Delta_A = \{(x,x) \mid x \in A\} | \Delta_A = \{(x,x) \mid x \in A\} | ||

- | \] | + | \end{equation*} |

==== Set operations ==== | ==== Set operations ==== | ||

Line 132: | Line 132: | ||

==== Relation Inverse ==== | ==== Relation Inverse ==== | ||

- | \[ | + | \begin{equation*} |

r^{-1} = \{(y,x) \mid (x,y) \in r \} | r^{-1} = \{(y,x) \mid (x,y) \in r \} | ||

- | \] | + | \end{equation*} |

==== Relation Composition ==== | ==== Relation Composition ==== | ||

- | \[ | + | \begin{equation*} |

r_1 \circ r_2 = \{ (x,z) \mid \exists y. (x,y) \in r_1 \land (y,z) \in r_2\} | r_1 \circ r_2 = \{ (x,z) \mid \exists y. (x,y) \in r_1 \land (y,z) \in r_2\} | ||

- | \] | + | \end{equation*} |

Note: relations on a set $A$ together with relation composition and $\Delta_A$ form a //monoid// structure: | Note: relations on a set $A$ together with relation composition and $\Delta_A$ form a //monoid// structure: | ||

- | \[ | + | \begin{equation*} |

\begin{array}{l} | \begin{array}{l} | ||

r_1 \circ (r_2 \circ r_3) = (r_1 \circ r_2) \circ r_3 \\ | r_1 \circ (r_2 \circ r_3) = (r_1 \circ r_2) \circ r_3 \\ | ||

r \circ \Delta_A = r = \Delta_A \circ r | r \circ \Delta_A = r = \Delta_A \circ r | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

Moreover, | Moreover, | ||

- | \[ | + | \begin{equation*} |

\emptyset \circ r = \emptyset = r \circ \emptyset | \emptyset \circ r = \emptyset = r \circ \emptyset | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

r_1 \subseteq r_2 \rightarrow r_1 \circ s \subseteq r_2 \circ s | r_1 \subseteq r_2 \rightarrow r_1 \circ s \subseteq r_2 \circ s | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

r_1 \subseteq r_2 \rightarrow s \circ r_1 \subseteq s \circ r_2 | r_1 \subseteq r_2 \rightarrow s \circ r_1 \subseteq s \circ r_2 | ||

- | \] | + | \end{equation*} |

Line 166: | Line 166: | ||

When $S \subseteq A$ and $r \subseteq A \times A$ we define **image** of a set $S$ under relation $A$ as | When $S \subseteq A$ and $r \subseteq A \times A$ we define **image** of a set $S$ under relation $A$ as | ||

- | \[ | + | \begin{equation*} |

S\bullet r = \{ y.\ \exists x. x \in S \land (x,y) \in r \} | S\bullet r = \{ y.\ \exists x. x \in S \land (x,y) \in r \} | ||

- | \] | + | \end{equation*} |

Line 174: | Line 174: | ||

Iterated composition let $r \subseteq A \times A$. | Iterated composition let $r \subseteq A \times A$. | ||

- | \[ | + | \begin{equation*} |

\begin{array}{l} | \begin{array}{l} | ||

r^0 = \Delta_A \\ | r^0 = \Delta_A \\ | ||

r^{n+1} = r \circ r^n | r^{n+1} = r \circ r^n | ||

\end{array} | \end{array} | ||

- | \] | + | \end{equation*} |

So, $r^n$ is n-fold composition of relation with itself. | So, $r^n$ is n-fold composition of relation with itself. | ||

Transitive closure: | Transitive closure: | ||

- | \[ | + | \begin{equation*} |

r^* = \bigcup_{n \geq 0} r^n | r^* = \bigcup_{n \geq 0} r^n | ||

- | \] | + | \end{equation*} |

Equivalent statement: $r^*$ is equal to the least relation $s$ (with respect to $\subseteq$) that satisfies | Equivalent statement: $r^*$ is equal to the least relation $s$ (with respect to $\subseteq$) that satisfies | ||

- | \[ | + | \begin{equation*} |

\Delta_A\ \cup\ (s \circ r)\ \subseteq\ s | \Delta_A\ \cup\ (s \circ r)\ \subseteq\ s | ||

- | \] | + | \end{equation*} |

or, equivalently, the least relation $s$ (with respect to $\subseteq$) that satisfies | or, equivalently, the least relation $s$ (with respect to $\subseteq$) that satisfies | ||

- | \[ | + | \begin{equation*} |

\Delta_A\ \cup\ (r \circ s)\ \subseteq\ s | \Delta_A\ \cup\ (r \circ s)\ \subseteq\ s | ||

- | \] | + | \end{equation*} |

or, equivalently, the least relation $s$ (with respect to $\subseteq$) that satisfies | or, equivalently, the least relation $s$ (with respect to $\subseteq$) that satisfies | ||

- | \[ | + | \begin{equation*} |

\Delta_A\ \cup\ r \cup (s \circ s)\ \subseteq\ s | \Delta_A\ \cup\ r \cup (s \circ s)\ \subseteq\ s | ||

- | \] | + | \end{equation*} |

==== Some Laws in Algebra of Relations ==== | ==== Some Laws in Algebra of Relations ==== | ||

- | \[ | + | \begin{equation*} |

(r_1 \circ r_2)^{-1} = r_2^{-1} \circ r_1^{-1} | (r_1 \circ r_2)^{-1} = r_2^{-1} \circ r_1^{-1} | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

r_1 \circ (r_2 \cup r_3) = (r_1 \circ r_2) \cup (r_1 \circ r_3) | r_1 \circ (r_2 \cup r_3) = (r_1 \circ r_2) \cup (r_1 \circ r_3) | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

(r^{-1})^{*} = (r^{*})^{-1} | (r^{-1})^{*} = (r^{*})^{-1} | ||

- | \] | + | \end{equation*} |

Binary relation $r \subseteq A\times A$ can be represented as a directed graph $(A,r)$ with nodes $A$ and edges $r$ | Binary relation $r \subseteq A\times A$ can be represented as a directed graph $(A,r)$ with nodes $A$ and edges $r$ | ||

Line 221: | Line 221: | ||

Equivalence classes are defined by | Equivalence classes are defined by | ||

- | \[ | + | \begin{equation*} |

x/r = \{y \mid (x,y) \in r | x/r = \{y \mid (x,y) \in r | ||

- | \] | + | \end{equation*} |

The set $\{ x/r \mid x \in A \}$ is a partition: | The set $\{ x/r \mid x \in A \}$ is a partition: | ||

* each set non-empty | * each set non-empty | ||

Line 229: | Line 229: | ||

* their union is $A$ | * their union is $A$ | ||

Conversely: each collection of sets $P$ that is a partition defines equivalence class by | Conversely: each collection of sets $P$ that is a partition defines equivalence class by | ||

- | \[ | + | \begin{equation*} |

r = \{ (x,y) \mid \exists c \in P. x \in c \land y \in c \} | r = \{ (x,y) \mid \exists c \in P. x \in c \land y \in c \} | ||

- | \] | + | \end{equation*} |

Congruence: equivalence that agrees with some set of operations. | Congruence: equivalence that agrees with some set of operations. | ||

Line 243: | Line 243: | ||

**Example:** an example function $f : A \to B$ for $A = \{a,b,c\}$, $B=\{1,2,3\}$ is | **Example:** an example function $f : A \to B$ for $A = \{a,b,c\}$, $B=\{1,2,3\}$ is | ||

- | \[ | + | \begin{equation*} |

f = \{ (a,3), (b,2), (c,3) \} | f = \{ (a,3), (b,2), (c,3) \} | ||

- | \] | + | \end{equation*} |

Definition of function, injectivity, surjectivity. | Definition of function, injectivity, surjectivity. | ||

Line 265: | Line 265: | ||

Function update operator takes a function $f : A \to B$ and two values $a_0 \in A$, $b_0 \in B$ and creates a new function $f[a_0 \mapsto b_0]$ that behaves like $f$ in all points except at $a_0$, where it has value $b_0$. Formally, | Function update operator takes a function $f : A \to B$ and two values $a_0 \in A$, $b_0 \in B$ and creates a new function $f[a_0 \mapsto b_0]$ that behaves like $f$ in all points except at $a_0$, where it has value $b_0$. Formally, | ||

- | \[ | + | \begin{equation*} |

f[a_0 \mapsto b_0](x) = \left\{\begin{array}{l} | f[a_0 \mapsto b_0](x) = \left\{\begin{array}{l} | ||

b_0, \mbox{ if } x=a_0 \\ | b_0, \mbox{ if } x=a_0 \\ | ||

f(x), \mbox{ if } x \neq a_0 | f(x), \mbox{ if } x \neq a_0 | ||

- | \] | + | \end{equation*} |

==== Domain and Range of Relations and Functions ==== | ==== Domain and Range of Relations and Functions ==== | ||

For relation $r \subseteq A \times B$ we define domain and range of $r$: | For relation $r \subseteq A \times B$ we define domain and range of $r$: | ||

- | \[ | + | \begin{equation*} |

dom(r) = \{ x.\ \exists y. (x,y) \in r \} | dom(r) = \{ x.\ \exists y. (x,y) \in r \} | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

ran(r) = \{ y.\ \exists x. (x,y) \in r \} | ran(r) = \{ y.\ \exists x. (x,y) \in r \} | ||

- | \] | + | \end{equation*} |

Clearly, $dom(r) \subseteq A$ and $ran(r) \subseteq B$. | Clearly, $dom(r) \subseteq A$ and $ran(r) \subseteq B$. | ||

Line 288: | Line 288: | ||

**Partial function** $f : A \hookrightarrow B$ is relation $f \subseteq A \times B$ such that | **Partial function** $f : A \hookrightarrow B$ is relation $f \subseteq A \times B$ such that | ||

- | \[ | + | \begin{equation*} |

\forall x \in A. \exists^{\le 1} y.\ (x,y)\in f | \forall x \in A. \exists^{\le 1} y.\ (x,y)\in f | ||

- | \] | + | \end{equation*} |

Generalization of function update is override of partial functions, $f \oplus g$ | Generalization of function update is override of partial functions, $f \oplus g$ | ||

Line 301: | Line 301: | ||

The following properties follow from the definitions: | The following properties follow from the definitions: | ||

- | \[ | + | \begin{equation*} |

(S \bullet r_1) \bullet r_2 = S \bullet (r_1 \circ r_2) | (S \bullet r_1) \bullet r_2 = S \bullet (r_1 \circ r_2) | ||

- | \] | + | \end{equation*} |

- | \[ | + | \begin{equation*} |

S \bullet r = ran(\Delta_S \circ r) | S \bullet r = ran(\Delta_S \circ r) | ||

- | \] | + | \end{equation*} |

===== Further references ===== | ===== Further references ===== | ||

- | * [[:Gallier Logic Book]], Chapter 2 | ||

* [[sav08:discrete_mathematics_by_rosen|Discrete Mathematics by Rosen]] | * [[sav08:discrete_mathematics_by_rosen|Discrete Mathematics by Rosen]] | ||

+ | * [[:Gallier Logic Book]], Chapter 2 | ||