Оглавление
Алгебра действий
-
Определение алгебры действия
- Алгебра действия — это алгебраическая структура, объединяющая остаточную полурешетку и алгебру Клини.
- Включает операции звездообразного замыкания, левого и правого остатка.
- Объединяет программы и предложения в один вид.
-
Аксиоматизация алгебры действия
- Аксиоматизируется с помощью квазиусловий и чисто эквациональной аксиоматизации.
- Включает уравнения для остаточной полурешетки и звезды.
- Звезда монотонна и является рефлексивно-транзитивным замыканием.
-
Свойства алгебры действия
- Эквациональная теория свободного от импликаций фрагмента совпадает с теорией алгебр Клини.
- Алгебры действия имеют конечную аксиоматизацию, в отличие от алгебр Клини.
- Примеры включают алгебры Хейтинга, формальные языки и бинарные отношения.
-
Примеры алгебр действия
- Алгебры Хейтинга преобразуются в алгебры действий с помощью операций ∧ и a* = 1.
- Формальные языки образуют алгебру действий с операциями объединения, конкатенации и замыкания Клини.
- Бинарные отношения образуют алгебру действий с операциями объединения, композиции и рефлексивного транзитивного замыкания.
-
Связь с другими логиками
- Алгебры действия связаны с динамической логикой и другими модальными логиками программ.
- Включают операции, аналогичные звездам Клини и обычным выражениям.