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

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I'm interested in knowing if there some work about formalization of key-value stores outside of category theory? I want to use some more simple and lightweight mathematics for the mathematical description of key-value stores. Set theory looks like it might offer some possibilities.

• It seems your question is not research level and would be better suited for cs.stackexchange.com. – cody Apr 21 '15 at 12:59
• Are you saying that you wish formalization that excludes Category Theory? – ouflak Apr 22 '15 at 14:25
• @ouflak Yes, exactly. I want a more simple model without category theory. I feel that set theory will be enough for this, but couldn't find any helpful articles – MainstreamDeveloper00 Apr 22 '15 at 16:52
• Oddly enough, I can't think of a nice introduction to various ways to specify such things. One thing you could do is to start by looking at what SMTLIB does for "arrays" (which are really maps/dictionaries) smtlib.cs.uiowa.edu/logics.shtml E.g., smtlib.cs.uiowa.edu/theories/ArraysEx.smt2 – Radu GRIGore Apr 22 '15 at 22:36
• Key value store is quite simple. Why do you need a formal mathematical model? What would you expect of such a model? Why do you exclude category theory? And are you hinting that there is a formal model for key value store based on category theory? By key-value store, do you include replicated data types, such as set, stack, queue, and so on? (Sorry for so many questions.) – hengxin Apr 23 '15 at 3:33

## 1 Answer

You did not say why you want a formalization, but presumably you want to do things with it, for instance prove properties of dictionaries and operations on them. In fact, your question can be understood in two ways: you want a mathematical description of dictionaries, or you want a computer formalization of dictionaries.

For a computer formalization have a look at the Coq standard library module FMaps, and if someone can find something better, please post it in the comments or just edit this question.

For a mathematical description all you have to note is that a dictionary is the same thing as a mapping with a finite domain. That is, if we have a dictionary (using Python style syntax):

d = { 'a' : 1, 'b' : 3, 'c' : 2 }


that is the same thing as a map $d$ whose domain of definition is the set $\{a, b, c\}$ and is defined as: $$d(a) = 1, \quad d(b) = 3, \quad d(c) = 2.$$ So now you can take any mathematical description of a map and use that. In set theory we would say that $d$ is the set of ordered pairs $$\{(a,1), (b,3), (c,2)\}.$$

• NoSQL database -- glorified hash table:-) – Tegiri Nenashi May 6 '15 at 1:01