I am reading a program analysis book and the author jump right into using some notations without explaining the meaning of them and now I have trouble understand the whole thing. The notations in question are: $\sqsubset$, $\sqsubseteq$, $\sqsupset$, $\sqsupseteq$, $\sqcap$, $\sqcup$, and $\models$. I just wonder if someone could give me some pointers to the definition of these symbols or and references will be greatly appreciated.
Asked
Active
Viewed 8,500 times
8
-
1Not sure about square subset, but square union is sometimes used to denote disjoint union. – aduh Sep 16 '16 at 17:04
-
Related: http://math.stackexchange.com/questions/1569400/does-sqsubset-have-any-special-meaning – JMoravitz Sep 16 '16 at 17:11
-
It's difficult to give an answer without context. While $\subset$ and the like have more or less a fixed and agreed to meaning, the symbols you mention may have greatly different meanings according to the field of research or even to authors. For instance, I sometimes use $\sqcup$ for denoting juxtaposition of one-dimensional arrays and $A\sqsubseteq B$ for denoting that the array $A$ can be obtained from the array $B$ by removing zero or more items. – egreg Sep 16 '16 at 17:14
-
Can you give us the title and author of the book? – Robert Soupe Sep 17 '16 at 01:44
3 Answers
1
The last symbol you included, the double right-facing turnstile $\vDash$, has various uses in some literature in Modal Logic.
On its own (or, perhaps more formally, as a unary symbol), for a proposition $\varphi$, $\vDash \varphi$ signifies that $\varphi$ is valid. Embellishments on the turnstile yield different meanings, e.g. $\vDash^M_w \varphi$ means proposition $\varphi$ is true at world $w$ in model $M$, $\vDash^M \varphi$ means $\vDash^M_w \varphi$ for all $w\in M$, etc.
The symbol can also take two arguments, e.g. for a class of models, frame, or class of frames $X$, $X\vDash \varphi$ means $\varphi$ is valid with respect to $X$.
I believe this symbol has uses in Model Theory and other branches of Logic, but I'm not as aware of those.
Nathan Kruse
- 11
- 2
1
It might be symbols used in domain theory, which in short is about how out-data depends on in-data. For example, a program is always monotonic in the respect that less in-data can not give more out-data.
md2perpe
- 26,770
0
Having a similar question while reading a static analysis book, I was looking for answers. Speaking with my advisor on the subject, I believe I have an answer that at least satisfied me.
In the context of program analysis and static analysis, the square versions of the various relations denote that the relationship between the elements (operands) may no longer be sets, but simply partial orderings. For example, consider the relation $\forall a \in \mathbb{A}$, $\alpha(\gamma(a)) \sqsubseteq a$ , where $\alpha$ is the abstraction function, $\gamma$ is concretization function, and $\mathbb{A}$ is the abstract domain. The value on the left hand side and the right hand side are not necessarily sets, they may simply be ordered elements (according to some lattice) depending on the abstract domain.
kballou
- 1
- 1
- 1
- 2