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$.

  • $f \subseteq A \times 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

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

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

A generalization of update is overriding one map by another:

    f \oplus g = \{ (x,y) \mid (x,y) \in g \lor (x \notin dom(g) \land (x,y) \in f \}

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 \}$