Can someone help me identify this math symbol and its meaning?

Question

From my university notes:

Comment to slide 9

By virtue of the result shown in this slide, we can talk about the least element of a set $D$, if one exists, and we denote it with $\perp$, pronounced "bottom". As an example, given the set $S=\{1,2,3\}$, the pair $(\mathcal{P}(S),\subseteq)$ (where $\mathcal{P}(S)$ denotes the power set of $S$) is a poset and the empty set is its bottom.

Having introduced an ordering on the partial functions, we can now summarize the require-ments for $\mathrm{FIX}\,F$:

• $\mathrm{FIX}\,F$ is a fixed point of $F$, that is $F(\mathrm{FIX}\,F)=\mathrm{FIX}\,F$ and

• $\mathrm{FIX}\,F$ is a least fixed point of $F$, that is if $Fg=g$ then $\mathrm{FIX}\,\color{red}{F\sqsubseteq g}$.

The next task is to ensure that all functionals $F$ that may arise in ${\tt While}$ do indeed have least fixed points.

There is this symbol which looks like a square version of an inclusion symbol but there is also an actual inclusion symbol in this same it of text. Here is another example of it's usage: Fixed point theory

Definition A partially ordered set is a pair $(D,\sqsubseteq_D)$, where $D$ is a set and $\sqsubseteq_D$ is a reflexive, transitive, anti-symmetric relation on $D$.

Example Defined the ordering $\sqsubseteq$ on partial functions of $\mathbf{State}\hookrightarrow\mathbf{State}$: $$g_1\sqsubseteq g_2\ \text{whenever}$$ $$\text{if}\ g_1s=s'\ \text{then}\ g_2s=s'\ \text{for all choices of}\ s\ \text{and}\ s'$$ then $(\mathbf{State}\hookrightarrow\mathbf{State},\sqsubseteq)$ is a poset.

As you can see the symbol can also contain a subscript (in this case $D$). What does this symbol mean? when is is used and what does the subscript stand for?

Both of these examples are in context to Denotational semantics. I tried to google the meaning but couldn't find anything. copy-pasting the symbol in the search bar resulted in pasting a v character

Answer 1

Detexify identifies it as \sqsubseteq. As discussed here, its meaning is highly context-dependent. But @MauroALLEGRANZA has identified the meaning applicable here.

Answer 2

In this CS context, I think $\sqsubseteq$ would be called the refinement relation (see, for example Morgan's Programming from Specifications). The subscript $D$ is just a reminder of the set $\sqsubseteq$ is defined on. Here one partial function $g_1$ is refined by another function $g_2$, if they agree wherever $g_1$ is defined (allowing for the possibility that the domain of $g_2$ strictly includes $g_1$, so that $g_2$ is "more defined" than $g_1$). Typically refinement is about resolving indeterminacy (a.k.a., strengthening the post-condition) and expanding the domain of definition (a.k.a., weakening the pre-condition). Here the relations being refined are deterministic (i.e., partial functions), so only weakening the pre-condition applies.