<p>You did not say <em>why</em> you want a formalization, but presumably you want to <em>do</em> 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 <em>mathematical description</em> of dictionaries, or you want a <em>computer formalization</em> of dictionaries.</p>

<p>For a computer formalization have a look at the Coq standard library module <a href="http://www.lix.polytechnique.fr/coq/stdlib/Coq.FSets.FMaps.html">FMaps</a>, and if someone can find something better, please post it in the comments or just edit this question.</p>

<p>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):</p>

<pre><code>d = { 'a' : 1, 'b' : 3, 'c' : 2 }
</code></pre>

<p>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)\}.$$</p>

CC BY-SA 3.0
2015-05-06T01:01:37.170Z
NoSQL database -- glorified hash table:-)
Tegiri Nenashi
CC BY-SA 3.0
2015-04-23T07:59:09.383Z
2015-04-23T07:59:09.383Z
Andrej Bauer
<p>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.  </p>

CC BY-SA 3.0
2015-04-21T12:59:07.553Z
It seems your question is not *research level* and would be better suited for cs.stackexchange.com.
cody
CC BY-SA 3.0
2015-04-22T14:25:00.503Z
Are you saying that you wish formalization that excludes Category Theory?
ouflak
CC BY-SA 3.0
2015-04-22T16:52:28.293Z
@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
CC BY-SA 3.0
2015-04-22T22:36:17.803Z
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) http://smtlib.cs.uiowa.edu/logics.shtml E.g., http://smtlib.cs.uiowa.edu/theories/ArraysEx.smt2
Radu GRIGore
CC BY-SA 3.0
2015-04-23T03:33:52.653Z
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
CC BY-SA 3.0
2015-04-23T22:07:03.750Z
@cody, in the future, if recommending CS.SE, please remind them not to cross-post (as cross-posting is forbidden by site rules).  You can suggest they delete and re-ask or flag for moderator attention and ask the moderators to migrate it.  Thank you!
D.W.
CC BY-SA 3.0
2015-04-24T14:15:50.200Z
@hengxin Thanks for the feedback.I think category theory is too heavy for such kind of storage. I expect from it something like relational data model do for relational database. We all use key-value stores but there is no formal model of it
MainstreamDeveloper00
<ds.data-structures><ct.category-theory><db.databases><set-theory>
How can I formalize key value stores with set theory?
MainstreamDeveloper00
# How can I formalize key value stores with set theory?

(Asked by: username_0 on 2015-04-21)

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.

**Tags:** ds.data-structures, ct.category-theory, db.databases, set-theory

> **Comments:**
> **username_1**: It seems your question is not *research level* and would be better suited for cs.stackexchange.com.  
> **username_2**: Are you saying that you wish formalization that excludes Category Theory?  
> **username_0**: @username_2 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  
> **username_3**: 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) http://smtlib.cs.uiowa.edu/logics.shtml E.g., http://smtlib.cs.uiowa.edu/theories/ArraysEx.smt2  
> **username_4**: 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.)  
> **username_5**: @username_1, in the future, if recommending CS.SE, please remind them not to cross-post (as cross-posting is forbidden by site rules).  You can suggest they delete and re-ask or flag for moderator attention and ask the moderators to migrate it.  Thank you!  
> **username_0**: @username_4 Thanks for the feedback.I think category theory is too heavy for such kind of storage. I expect from it something like relational data model do for relational database. We all use key-value stores but there is no formal model of it  

---

## 1 answers

### Answer by username_6 on 2015-04-23. Score: 6 | Accepted 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)\}.$$

> **Comments:**
> **username_7**: NoSQL database -- glorified hash table:-)  

---

