Mathematical formal notation of a dictionary

I was wondering how to express a dictionary or associative array (as known in programming) formally in mathematical notation. A dictionary is basically a set of ordered pairs of keys and values, but each key must appear only once.

Now, if $K$ is the set of all possible keys and $V$ the set of all possible values, my first idea of how to express a dictionary over $(K,V)$ was: $$D \subseteq \{(k,v)\mid k \in K \land v \in V\}$$

The problem is that this allows for repeated keys. So my second idea was this:

$$D \subseteq \{(k,v)\mid k \in K \land v \in V \land \forall (q, w) \in D: k=q \to v=w \}$$

Is this a sensible definition of a dictionary or am I missing something crucial?

• This is sensible, although strictly speaking it is incorrect to use $D$ after the $|$ in the definition of $D$. What you want to say is that $D \subseteq K \times V$ and $\forall (k_1,v_1) \in D \ \forall (k_2,v_2) \in D \ (k_1=k_2 \to v_1=v_2)$. – Dan Shved Feb 28 '13 at 5:26
• Thanks Dan. Could you post this as an answer please. – Hyperboreus Feb 28 '13 at 5:34
• Re "each key must appear only once." If you mean exactly once, then the map is a function, but if some keys don't appear then the map is only a partial function. So by restricting the domain to the keys that in fact do appear in the dictionary, it's a function. – alancalvitti Feb 28 '13 at 6:38
• @Hyperboreus I don't think I should. The answer by Ittay Weiss seems perfectly fine, and comments there dot all the i's. – Dan Shved Feb 28 '13 at 9:04

Yes, it's sensible and it amount precisely to a function $f:K\to V$. That is what a dictionary is, it's a function from the set of keys to the set of values.
• Thank you very much. So to make it short, it can be defined as $D \in V^K$. Or did I get something wrong? – Hyperboreus Feb 28 '13 at 5:20
• @Hyperboreus, Ittay: A dictionary/associative array is usually a partial function from keys to values, which is not an element of $V^K$. – Rahul Feb 28 '13 at 5:28
• You can either model it as some universal set of keys and a $\bot$ value or let $K$ just represent the actual set of keys. For me, using the actual keys (ie, an element of $K \to V$) is closer to actual implementations. – copper.hat Feb 28 '13 at 5:39
• As both approaches are fine, I would recommend $D : K \to V^\bot$ where $V^\bot = V \uplus \{\bot\}$. Dictionaries are very common in formal semantics, and $(V^\bot)^K$ is usually what is being used. Also, useful notation if you want to change your dictionary: $D[k \to v]$, and you can define it as $$D[k\to v](x) = \begin{cases}v & \text{for }x = k \\ D(x) & \text{otherwise}\end{cases}$$ – dtldarek Feb 28 '13 at 6:23