I am working on my bachelor's thesis, and I have problem formally specifying constraints on one of the components.

Bachelor's thesis is in the field of Computer Science, and I am expressing one of the components of system I designed as set of ordered pairs ${(name,value),...} $(implemented as hashmap name -> value). I need to define constraint of this component, so that each $name$ is unique - no 2 elements share same $name$. So far I have come up with this: $\forall(n1,v2) \in Values, \nexists(n2,v2) \in Values: n1==n2 $

Also, I am writing several algorithms describing real implementation, and for this purpose I would like to use map notation $arr[n] = v; v = arr[n]$. I have defined it as so:

Let $arr$ be set containing elements, where each element is an ordered pair $(n,v)$. Notation $arr[n] = v$ denotes insertion operation into this set so the resulting set will be $arr = arr ∪ {(n,v)}$. Notation $v = arr[n]$ denotes selection and projection operation $((a,v) ∈ arr ∧ a == n) → v$.

My background in mathematics is pretty slim, but I would like to express these details as formally, and clearly as possible.


For the first part, your example is bad because you didn't specify that $v_1\neq v_2$. In other words, the set $\{(a,b)\}$ does not satisfy your condition because I can set $n_1=n_2=a$ and $v_1=v_2=b$.

I would say the easiest way would be to say $$\forall n\in\text{Names},\forall v_1, v_2\in\text{Names}:(n, v_1)\in\text{Values}\land(n, v_2)\in\text{Values}\implies v_1=v_2$$

For the second part, the operation $arr=arr\cup (n, v)$ does not say what happens when $(n, v')$ is already in $arr$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.