En lógica algebraica , un álgebra de acción es una estructura algebraica que es tanto un semirretículo residido como un álgebra de Kleene . Agrega la operación de cierre transitivo en estrella o reflexiva de la última a la primera, mientras que agrega las operaciones de residuación o implicació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 cuales los programas y las proposiciones forman dos clases distintas, el álgebra de acción combina las dos en una sola clase. Se puede pensar en 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 de ecuaciones de las álgebras de Kleene (las ecuaciones de expresión regular), la operación en estrella de las álgebras de acción es un cierre transitivo reflexivo en cada modelo de las ecuaciones.
Definición
Un álgebra de acción ( A , ∨, 0, •, 1, ←, →, *) es una estructura algebraica tal que ( A , ∨, •, 1, ←, →) forma una semirrejilla residuada mientras que ( A , ∨, 0 , •, 1, *) forma un álgebra de Kleene . [1] 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 ahí que también lo sean las álgebras de acción cuando se axiomatiza 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. [2] El lenguaje de las álgebras de acción se extiende de forma natural al de las redes de acción , es decir, mediante la inclusión de una operación de encuentro. [3]
A continuación, escribimos la desigualdad a ≤ b como abreviatura de la ecuación a ∨ b = b . Esto nos permite axiomatizar la teoría usando desigualdades y aún así tener una axiomatización puramente ecuacional cuando las desigualdades se expanden a igualdades.
Las ecuaciones del álgebra de acción axiomatizadora son las de una semirrejilla residual, junto con las siguientes ecuaciones para la estrella.
- 1 ∨ a * • a * ∨ a ≤ a *
- a * ≤ ( a ∨ b ) *
- ( a → a ) * ≤ a → a
La primera ecuación se puede dividir en tres ecuaciones, 1 ≤ a *, a * • a * ≤ a * y a ≤ a *. Estos obligan a a * a ser reflexivo, transitivo, [ aclaración necesaria ] y mayor o igual a a respectivamente. El segundo axioma afirma que la estrella es monótona. El tercer axioma se puede escribir de forma equivalente como un • ( un → una ) * ≤ una , una forma que hace que su papel como la inducción más evidente. Estos dos axiomas, en conjunción con los axiomas de una semirrejilla residual, fuerzan a * a ser el elemento transitivo menos reflexivo de la semirrejilla mayor o igual a a . Tomando eso como la definición de 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 .
Se puede demostrar que la teoría de ecuaciones del fragmento libre de implicaciones de álgebras de acción, aquellas ecuaciones que no contienen → o ←, coinciden con la teoría de ecuaciones de las álgebras de Kleene, también conocidas como ecuaciones de expresión regular . En ese sentido, los axiomas anteriores constituyen una axiomatización finita de expresiones regulares. Redko demostró en 1967 que estas ecuaciones no tenían axiomatización finita, para lo cual John Horton Conway dio una demostración más corta en 1971. Salomaa dio un esquema de ecuación axiomatizando esta teoría que Kozen posteriormente reformuló como una axiomatización finita usando cuasiecuaciones, o implicaciones entre ecuaciones, la clave fundamental. siendo las cuasiecuaciones 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 el cierre transitivo reflexivo 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 cierre transitivo reflexivo debería ser a . Sin embargo, las expresiones regulares no imponen esto, lo que permite que un * sea estrictamente mayor que un . Tal comportamiento anómalo no es posible en un álgebra de acción.
Ejemplos de
Cualquier álgebra de Heyting (y por lo tanto cualquier álgebra booleana ) se convierte en álgebra de acción tomando • como ∧ y a * = 1. Esto es necesario y suficiente para la estrella porque el elemento superior 1 de un álgebra de Heyting es su único elemento reflexivo, y es tanto transitivo como mayor o igual a todos los elementos 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 conjunto vacío, 1 = {ε}, ∨ como unión, • como concatenación, L ← M como 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 (cierre de Kleene).
El conjunto 2 X ² de todas las relaciones binarias en un conjunto X forma un álgebra de acción con 0 como relación vacía, 1 como relación de identidad o igualdad, ∨ como unión, • como composición de relación, R ← S como la relación que consta de todos 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 de todas las relaciones R n para enteros n ≥ 0.
Los dos ejemplos anteriores son conjuntos de potencias, que son álgebras de Boole bajo las operaciones teóricas de conjuntos habituales de unión, intersección y complemento. Esto justifica llamarlos álgebras de acción booleanas . El ejemplo relacional constituye un álgebra de relaciones equipada con una operación de cierre transitivo reflexivo. Tenga en cuenta que cada á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.
Ver también
Referencias
- ^ Kozen, Dexter (1990), "Sobre álgebras de Kleene y semirrings cerrados" (PDF) , en B. Rovan (ed.), Fundamentos matemáticos de la informática (MFCS) , LNCS 452, Springer-Verlag, págs. 26-47
- ^ Pratt, Vaughan (1990), "Action Logic and Pure Induction" (PDF) , Logics in AI: European Workshop JELIA '90 (ed. J. van Eijck) , LNCS 478, Springer-Verlag, págs. 97-120.
- ^ Kozen, Dexter (1994), "Sobre álgebras de acción" (PDF) , Flujo de información y lógica , Encontrado. Computación. Ser., MIT Press, Cambridge, MA, págs. 78–88, MR 1295061.
- Conway, JH (1971). Álgebra regular y máquinas finitas . Londres: Chapman y Hall. ISBN 0-412-10620-5. Zbl 0231.94041 .
- VN Redko, Sobre la definición de relaciones para el álgebra de eventos regulares (ruso), Ukrain. Estera. Z. , 16: 120-126, 1964.