What does square subset and square union symbol mean?

Question

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.

Answer 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.

Answer 2

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.