World's most popular travel blog for travel bloggers.

# [Answers] How can I formalize key value stores with set theory?

, ,
Problem Detail:

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I found article about key value formalisation with category theory, but I'm interested are there some works about formalisation of key-value stores except category theory (I know we can use it for all, but...)? I want to use some more simple and lightweight mathematics for mathematical description of key-value stores. And I feel that set theory will be enough for this, but couldn't find any helpful articles.

One simple way to model a key-value store is as a map $f:K \to V$ where $K$ is the set of possible keys and $V$ is the set of possible values.

Often, each value $v \in V$ will itself be a tuple or record. You can represent a tuple as a Cartesian cross-product, e.g., $V = V_1 \times V_2 \times \dots \times V_k$. You can represent a record as either a tuple (if the set of attributes is finite and known in advance), or as a function from attribute names to values.

Modelling languages like Alloy can represent such maps natively. Some modeling languages will use the notation $k.f$ instead of $f(k)$ (i.e., object field access notation instead of function evaluation), but the two are equivalent.

If you don't want to use functions, but want to stick to just sets, that is also feasible. You can model any function $f: K \to V$ as a binary relation, i.e., a set $S \subseteq K \times V$ with the additional property that if $(k_1,v_1) \in S$ and $(k_2,v_2) \in S$ and $k_1=k_2$, then $v_1=v_2$. However this may be less natural.

This gives you a way to model the state of the store. You will then need to model the effect of each operation that can be performed on the store, in these mathematical terms.