¿Qué significa el símbolo del subconjunto cuadrado y la unión cuadrada?

Question

Estoy leyendo un libro de análisis de programas y el autor se lanza a utilizar algunas notaciones sin explicar su significado y ahora tengo problemas para entenderlo todo. Las notaciones en cuestión son: $\sqsubset$ , $\sqsubseteq$ , $\sqsupset$ , $\sqsupseteq$ , $\sqcap$ , $\sqcup$ y $\models$ . Sólo me pregunto si alguien podría darme algunas indicaciones sobre la definición de estos símbolos o y referencias será muy apreciado.

Answer 1

El último símbolo que ha incluido, el torniquete doble a la derecha $\vDash$ tiene varios usos en alguna literatura de Lógica Modal.

Por sí solo (o, quizá más formalmente, como símbolo unario), para una proposición $\varphi$ , $\vDash \varphi$ significa que $\varphi$ es válido. Los adornos en el torniquete tienen diferentes significados, por ejemplo $\vDash^M_w \varphi$ significa proposición $\varphi$ es cierto en el mundo $w$ en el modelo $M$ , $\vDash^M \varphi$ significa $\vDash^M_w \varphi$ para todos $w\in M$ etc.

El símbolo también puede tomar dos argumentos, por ejemplo, para una clase de modelos, marco o clase de marcos $X$ , $X\vDash \varphi$ significa $\varphi$ es válida con respecto a $X$ .

Creo que este símbolo tiene usos en la Teoría de Modelos y otras ramas de la Lógica, pero no estoy tan al tanto de ellas.

Answer 2

Pueden ser símbolos utilizados en teoría de los dominios que, en resumen, trata de cómo los datos de salida dependen de los datos de entrada. Por ejemplo, un programa es siempre monótona en el sentido de que menos datos de entrada no pueden dar más datos de salida.

Answer 3

Al tener una pregunta similar mientras leía un libro de análisis estático, estaba buscando respuestas. Hablando con mi asesor sobre el tema, creo que tengo una respuesta que al menos me satisface.

En el contexto del análisis de programas y del análisis estático, las versiones cuadradas de las distintas relaciones denotan que la relación entre los elementos (operandos) ya no pueden ser conjuntos, sino simplemente ordenaciones parciales. Por ejemplo, consideremos la relación $\forall a \in \mathbb{A}$ , $\alpha(\gamma(a)) \sqsubseteq a$ , donde $\alpha$ es la función de abstracción, $\gamma$ es la función de concreción, y $\mathbb{A}$ es el dominio abstracto. Los valores de la izquierda y de la derecha no son necesariamente conjuntos, pueden ser simplemente elementos ordenados (según algún entramado) en función del dominio abstracto.