¿Se han considerado los sistemas de acción/predicado (o similares) en la bibliografía?

Question

Pregunta. ¿Se ha considerado en la literatura el siguiente concepto, o algo similar?

Definición. En acción/predicado consiste en conjuntos $A$ (las acciones) y $X$ (los predicados) tales que se cumpla lo siguiente.

1. $A$ forma un monoide
2. $X$ forma una red booleana
3. Existe una acción monoide $A \times X \rightarrow X$ denotado $ax$ tal que para todo $a \in A$ tenemos que la función $x \in X \mapsto ax \in X$ es un endomorfismo de $X$ . Intuitivamente, $ax$ significa "el predicado que devuelve $\mathtt{True}$ precisamente en los Estados en los que $a$ provoca $x$ ."

4. Existe una función $\sim \,: A \times A \rightarrow X$ sujeto a los siguientes axiomas. Intuitivamente, $a \sim b$ significa "el predicado que devuelve $\mathtt{True}$ precisamente en los Estados en los que $a$ tiene el mismo efecto que $b$ ."

   • Reflexividad. $\forall a \in A : \top \leq (a \sim a)$
   • Simetría. $\forall a,b \in A : (a \sim b) \leq (b \sim a)$
   • Transitividad. $\forall a,b,c \in A : (a \sim b) \wedge (b \sim c) \leq (a \sim c)$
   • Compatibilidad I. $$\forall a,b,c \in A : (a \sim b) \leq (ac \sim bc),\quad \forall a,b,c \in A : (a \sim b) \leq (ca \sim cb)$$
   • Compatibilidad II. $\forall a,b \in A,\;\forall x \in X : (a \sim b) \leq (ax \leftrightarrow bx)$

Reiteración de la pregunta. ¿Se ha tenido esto en cuenta en la bibliografía? En caso afirmativo, ¿cuál es la terminología correcta para este tipo de estructuras y dónde puedo obtener más información?

Intuición. En primer lugar, podemos pensar en las acciones como si fueran "órdenes" en un lenguaje de programación; mueven la máquina a un nuevo estado, en función de su estado actual. La unidad $1 \in A$ es el comando que no hace nada; además, si $a$ y $b$ son comandos, entonces $ab$ es el resultado de realizar primero $a$ entonces $b$ .

En segundo lugar, podemos pensar que los predicados son... bueno, predicados; en el sentido de que devuelven verdadero/falso en función del estado actual de la máquina. Además, si $a$ es una acción y $x$ es un predicado, entonces $ax$ puede considerarse como el predicado que devuelve $\mathtt{true}$ precisamente para los estados en los que la acción $a$ si se lleva a cabo, provocaría $x$ . Así, podemos leer " $ax"$ como " $a$ provoca $x$ ."

En tercer lugar, la estipulación de que dicha acción sea un homomorfismo de álgebras booleanas puede motivarse por la observación de que las siguientes afirmaciones deberían ser equivalentes.

1. Estamos en un estado tal que realizar $a$ provocaría $x \vee y$ .
2. Estamos en un estado tal que o bien realizando $a$ provocaría $x$ , o realizando $a$ provocaría $y$ .

Esto corresponde al axioma $a(x \vee y) = ax \vee ay$ . Un razonamiento lingüístico similar puede motivar el resto de la estipulación de homomorfismo.

En cuarto y último lugar, la función $\sim : A \times A \rightarrow X$ puede interpretarse de la siguiente manera. Si $a,b \in A$ son acciones, entonces $a \sim b$ es el predicado que devuelve $\mathtt{true}$ precisamente para aquellos Estados en los que la promulgación $a$ cambiaría la máquina al mismo estado que lo haría promulgar $b$ . Los axiomas asociados a $\sim$ están motivados por este motivo.

Un poco más de motivación. He aquí algunas cosas básicas que podemos expresar en este lenguaje.

• En cualquier Estado en el que $x$ se cumple, tenemos que $a$ provoca $y$ .

$$x \leq ay$$

• En general, la acción $a$ hace que $x$ implica $y$ .

$$\top \leq a(x \rightarrow y)$$

• En cualquier Estado en el que $x$ retenciones, $a$ tiene el mismo efecto que $b$ .

$$x \leq (a \sim b)$$

Answer 1

Las tres primeras condiciones corresponden efectivamente a la acción de un monoide sobre un álgebra de Boole, pero la cuarta condición es de naturaleza diferente. Permítanme introducir otra función $d: A \times A \to X$ estableciendo $d(a, b) = (a \sim b)'$ . Reescribiendo los cuatro axiomas se obtiene

1. Para todos $a \in A$ , $d(a,a) = 0$ ( $0$ significa $\bot$ pero parece más apropiado en este contexto).
2. Para todos $a,b \in A$ , $d(a,b) = d(b,a)$ .
3. Para todos $a,b, c \in A$ , $d(a,c) \leqslant d(a,b) \vee d(b,c)$
4. Para todos $a,b \in A$ y $x \in X$ , $ax\ \Delta\ bx \leqslant d(a,b)$ donde $x\ \Delta\ y$ es la diferencia simétrica de $x$ y $y$ .

Ahora bien, los tres primeros axiomas recuerdan a la definición de una métrica booleana. El bit que falta es $d(a, b) = 0$ implica $a = b$ pero estamos muy cerca. De hecho, si $d(a, b) = 0$ (4) $ax\ \Delta\ bx = 0$ de donde $ax = bx$ para todos $x$ .

La noción de espacio métrico booleano se remonta al menos a los años cincuenta. Es fácil encontrar referencias en Internet. Yo encontré esta primera, pero desgraciadamente no tengo acceso a este documento.

Blumenthal, L. M. Geometría booleana I. Rend. Circ. Mat. Palermo . 1952, 1, 343-360.

Answer 2

Descargo de responsabilidad: no soy un experto, pero estas son mis ideas.

Con sus definiciones algebraicas, ha descrito esencialmente el mu-cálculo utilizado en la comprobación de modelos de programas. El mu-cálculo se define en términos de acciones y celosías, tal como en su descripción.

Además, la relación de equivalencia que has definido parece análoga al concepto de abstracción de predicados. La abstracción de predicados se utiliza para reducir el espacio de estados de un programa identificando acciones que son equivalentes modulo algún predicado.

Puede comprobar lo siguiente para ver si este es el caso:

http://en.wikipedia.org/wiki/Modal_%CE%BC-calculus http://www.cs.ucla.edu/~todd/investigación/pldi01.pdf