Notation for Maps

Mathematical notion of map $f : A \rightharpoonup B$ is a partial function, that is, a function from a subset of $A$ to $B$ .

$\forall x.\forall y_1.\forall y_2.\ (x,y_1) \in f \land (x,y_2) \in f \rightarrow y_1=y_2$

We define $dom(f) = \{ x \mid \exists y. (x,y) \in f \}$

Key operation is function update

$\begin{equation*} f[k:=v] = \{ (x,y) \mid (x=k \land y=v) \lor (x \neq k \land (x,y) \in f) \} \end{equation*}$

If the value was defined before, now we redefine it.

A generalization of update is overriding one map by another:

$\begin{equation*} f \oplus g = \{ (x,y) \mid (x,y) \in g \lor (x \notin dom(g) \land (x,y) \in f \} \end{equation*}$

Sometimes we denote map $\{(k_1,v_1),\ldots,(k_n,v_n)\}$ by $\{k_1 \mapsto v_1,\ldots,k_n \mapsto v_n\}$

Is $f \oplus g = g \oplus f$ ?

$\{x \mapsto b, z \mapsto a \} \oplus \{ x \mapsto c \} = \{ x \mapsto c, z \mapsto a \}$
$\{ x \mapsto c \} \oplus \{x \mapsto b, z \mapsto a \} = \{ x \mapsto b, z \mapsto a \}$