En lógica algebraica , un álgebra de acción es una estructura algebraica que es a la vez una semirretícula residual y un álgebra de Kleene . Añade la operación de cierre transitivo reflexivo o en estrella de la última a la primera, mientras que añade las operaciones de implicación o residuación izquierda y derecha de la primera a la segunda. A diferencia de la lógica dinámica y otras lógicas modales de programas, para las que los programas y las proposiciones forman dos tipos distintos, el álgebra de acción combina los dos en un único tipo. Puede considerarse como una variante de la lógica intuicionista con estrella y con una conjunción no conmutativa cuya identidad no necesita ser el elemento superior. A diferencia de las álgebras de Kleene, las álgebras de acción forman una variedad , que además es finitamente axiomatizable, siendo el axioma crucial a •( a → a )* ≤ a . A diferencia de los modelos de la teoría ecuacional de las álgebras de Kleene (las ecuaciones de expresión regular), la operación estrella de las álgebras de acción es el cierre transitivo reflexivo en cada modelo de las ecuaciones. Las álgebras de acción fueron introducidas por Vaughan Pratt en el Taller Europeo JELIA'90. [1]
Un álgebra de acción ( A , ∨, 0, •, 1, ←, →, *) es una estructura algebraica tal que ( A , ∨, •, 1, ←, →) forma una semirretícula residual en el sentido de Ward y Dilworth, [2] mientras que ( A , ∨, 0, •, 1, *) forma un álgebra de Kleene en el sentido de Dexter Kozen . [3] Es decir, es cualquier modelo de la teoría conjunta de ambas clases de álgebras. Ahora bien, las álgebras de Kleene se axiomatizan con cuasiecuaciones, es decir, implicaciones entre dos o más ecuaciones, de donde también lo son las álgebras de acción cuando se axiomatizan directamente de esta manera. Sin embargo, las álgebras de acción tienen la ventaja de que también tienen una axiomatización equivalente que es puramente ecuacional. El lenguaje de las álgebras de acción se extiende de manera natural al de las redes de acción, es decir, mediante la inclusión de una operación de encuentro. [4]
A continuación, escribimos la desigualdad a ≤ b como abreviatura de la ecuación a ∨ b = b . Esto nos permite axiomatizar la teoría utilizando desigualdades y, aun así, tener una axiomatización puramente ecuacional cuando las desigualdades se expanden a igualdades.
Las ecuaciones que axiomatizan el álgebra de acción son aquellas para una semired residual, junto con las siguientes ecuaciones para la estrella.
La primera ecuación se puede descomponer en tres ecuaciones, 1 ≤ a *, a *• a * ≤ a *, y a ≤ a *. Definiendo a como reflexivo cuando 1 ≤ a y transitivo cuando a • a ≤ a por abstracción de las relaciones binarias, las primeras dos de esas ecuaciones fuerzan a a * a ser reflexivo y transitivo mientras que la tercera fuerza a * a ser mayor o igual a a . El siguiente axioma afirma que la estrella es monótona. El último axioma se puede escribir de manera equivalente como a •( a → a )* ≤ a , una forma que hace más evidente su papel como inducción. Estos dos axiomas en conjunción con los axiomas para un semirretículo residual fuerzan a a * a ser el elemento transitivo menos reflexivo del semirretículo de elementos mayores o iguales a a . Tomando esto como la definición del cierre transitivo reflexivo de a , entonces tenemos que para cada elemento a de cualquier álgebra de acción, a * es el cierre transitivo reflexivo de a .
La teoría ecuacional del fragmento libre de implicaciones de las álgebras de acción, aquellas ecuaciones que no contienen → o ←, puede demostrarse que coincide con la teoría ecuacional de las álgebras de Kleene, también conocidas como ecuaciones de expresiones regulares . En ese sentido, los axiomas anteriores constituyen una axiomatización finita de las expresiones regulares. Redko demostró en 1967 que las ecuaciones de expresiones regulares no tenían axiomatización finita, para lo cual John Horton Conway dio una prueba más corta en 1971. [5] [6] Arto Salomaa dio un esquema de ecuación axiomatizando esta teoría que Dexter Kozen posteriormente reformuló como una axiomatización finita utilizando cuasiecuaciones, o implicaciones entre ecuaciones, siendo las cuasiecuaciones cruciales las de inducción: si x • a ≤ x entonces x • a * ≤ x , y si a • x ≤ x entonces a *• x ≤ x . Kozen definió un álgebra de Kleene como cualquier modelo de esta axiomatización finita.
Conway demostró que la teoría ecuacional de expresiones regulares admite modelos en los que a * no es la clausura transitiva reflexiva de a , dando un modelo de cuatro elementos 0 ≤ 1 ≤ a ≤ a * en el que a • a = a . En el modelo de Conway, a es reflexivo y transitivo, por lo que su clausura transitiva reflexiva debería ser a . Sin embargo, las expresiones regulares no imponen esto, permitiendo que a * sea estrictamente mayor que a . Tal comportamiento anómalo no es posible en un álgebra de acción, que obliga a que a * sea el elemento reflexivo menos transitivo.
Cualquier álgebra de Heyting (y, por lo tanto, cualquier álgebra de Boole ) se convierte en un álgebra de acción al tomar • como ∧ y a * = 1. Esto es necesario y suficiente para star porque el elemento superior 1 de un álgebra de Heyting es su único elemento reflexivo y es transitivo, así como mayor o igual que cada elemento del álgebra.
El conjunto 2 Σ* de todos los lenguajes formales (conjuntos de cadenas finitas) sobre un alfabeto Σ forma un álgebra de acción con 0 como el conjunto vacío, 1 = {ε}, ∨ como unión, • como concatenación, L ← M como el conjunto de todas las cadenas x tales que xM ⊆ L (y dualmente para M → L ), y L * como el conjunto de todas las cadenas de cadenas en L (clausura de Kleene).
El conjunto 2 X ² de todas las relaciones binarias en un conjunto X forma un álgebra de acciones con 0 como la relación vacía, 1 como la relación identidad o igualdad, ∨ como unión, • como composición de relaciones, R ← S como la relación que consiste en todos los pares ( x,y ) tales que para todo z en X , ySz implica xRz (y dualmente para S → R ), y R* como el cierre transitivo reflexivo de R , definido como la unión sobre todas las relaciones R n para números enteros n ≥ 0.
Los dos ejemplos anteriores son conjuntos potencia, que son álgebras de Boole bajo las operaciones habituales de la teoría de conjuntos de unión, intersección y complemento. Esto justifica llamarlas álgebras de acción de Boole . El ejemplo relacional constituye un álgebra relacional dotada de una operación de clausura transitiva reflexiva. Nótese que toda álgebra de Boole es un álgebra de Heyting y, por lo tanto, un álgebra de acción en virtud de ser una instancia del primer ejemplo.