Алгебра действий - Action algebra

В алгебраическая логика, алгебра действий является алгебраическая структура что является одновременно остаточная полурешетка и Клини алгебра. Он добавляет операцию звездообразного или рефлексивного транзитивного замыкания последнего к первому, одновременно добавляя операции левой и правой вычетов или импликации первого ко второму. В отличие от динамическая логика и другие модальные логики программ, для которых программы и предложения образуют два различных вида, алгебра действий объединяет эти два вида в один. Это можно рассматривать как вариант интуиционистская логика со звездой и с некоммутативным соединением, тождество которого не обязательно должно быть верхним элементом. В отличие от алгебр Клини, алгебры действия образуют разнообразие, который, кроме того, конечно аксиоматизируем, ключевой аксиомой является а•(а → а)* ≤ а. В отличие от моделей эквациональной теории алгебр Клини (уравнений регулярного выражения), звездная операция алгебр действия является рефлексивным транзитивным замыканием в каждой модели уравнений.

Определение

An алгебра действий (А,, 0, •, 1, ←, →, *) является алгебраическая структура такой, что (А, ∨, •, 1, ←, →) образует остаточная полурешетка пока (А, ∨, 0, •, 1, *) образует Клини алгебра.[1] То есть это любая модель совместной теории обоих классов алгебр. Теперь алгебры Клини аксиоматизируются с помощью квазиуравнений, то есть следствий между двумя или более уравнениями, отсюда и алгебры действия при прямой аксиоматизации таким образом. Однако алгебры действий имеют то преимущество, что они также имеют эквивалентную аксиоматизацию, которая является чисто эквациональной.[2] Язык алгебр действия естественным образом расширяется до языка алгебр действия. решетки действий, а именно включением операции встречи.[3]

Далее запишем неравенство а ≤ б как сокращение для уравнения а ∨ б = б. Это позволяет нам аксиоматизировать теорию, используя неравенства, но все же иметь чисто эквациональную аксиоматизацию, когда неравенства расширяются до равенств.

Уравнения, аксиоматизирующие алгебру действия, являются уравнениями для полурешетки с делениями вместе со следующими уравнениями для звезды.

1 ∨ а*•а* ∨ а   ≤   а*
а* ≤ (а ∨ б)*
(а → а)*   ≤   а → а

Первое уравнение можно разбить на три уравнения, 1 ≤ а*, а*•а* ≤ а*, и а ≤ а*. Эти силы а* быть рефлексивным, переходным,[требуется разъяснение ] и больше или равно а соответственно. Вторая аксиома утверждает, что звезда монотонна. Третья аксиома может быть записана эквивалентно как а•(а → а)* ≤ а, форма, которая делает его роль индукции более очевидной. Эти две аксиомы в сочетании с аксиомами вычетов силы полурешетки а* быть наименее рефлексивным транзитивным элементом полурешетки, большим или равным а. Принимая это как определение рефлексивного транзитивного замыкания а, то для каждого элемента а любой алгебры действия, а* - рефлексивное переходное замыкание а.

Можно показать, что эквациональная теория импликационного фрагмента алгебр действия, уравнения, не содержащие → или ←, совпадают с эквациональной теорией алгебр Клини, также известной как регулярное выражение уравнения. В этом смысле указанные выше аксиомы представляют собой конечную аксиоматизацию регулярных выражений. Редько в 1967 г. показал, что эти уравнения не имеют конечной аксиоматизации, для которой Джон Хортон Конвей дал более короткое доказательство в 1971 году. Саломаа привел схему уравнений, аксиоматизирующую эту теорию, которую Козен впоследствии переформулировал как конечную аксиоматизацию с использованием квазиуравнений или следствий между уравнениями, причем важнейшими квазиуравнениями являются уравнения индукции: Икс•а ≤ Икс тогда Икс•а* ≤ Икс, и если а•Икс ≤ Икс тогда а*•Икс ≤ Икс. Козен определил алгебру Клини как любую модель этой конечной аксиоматизации.

Конвей показал, что эквациональная теория регулярных выражений допускает модели, в которых а* не было рефлексивным переходным замыканием а, давая четырехэлементную модель 0 ≤ 1 ≤ а ≤ а* в котором а•а = а. В модели Конвея а является рефлексивным и транзитивным, поэтому его рефлексивное переходное замыкание должно быть а. Однако регулярные выражения не обеспечивают этого, что позволяет а* быть строго больше, чем а. Такое аномальное поведение невозможно в алгебре действий.

Примеры

Любой Алгебра Гейтинга (и, следовательно, любой Булева алгебра ) превращается в алгебру действия, если • взять и а* = 1. Это необходимо и достаточно для star, потому что верхний элемент 1 алгебры Гейтинга является ее единственным рефлексивным элементом и транзитивен, а также больше или равен каждому элементу алгебры.

Набор 2Σ * из всех формальные языки (множества конечных строк) над алфавитом Σ образует алгебру действий с 0 в качестве пустого множества, 1 = {ε}, ∨ в качестве объединения, • в качестве конкатенации, L ← M как набор всех струн Икс такой, что xM ⊆ L (и вдвойне для M → L), и L* как набор всех строк строк в L (Закрытие Клини).

Набор 2Икс² всех бинарных отношений на множестве Икс образует алгебру действий с 0 как пустым отношением, 1 как тождественным отношением или равенством, ∨ как объединением, • как композицией отношений, р ← S как отношение, состоящее из всех пар (х, у) такой, что для всех z в Икс, ySz подразумевает xRz (и вдвойне для S → р), и Р* как рефлексивное переходное замыкание р, определяемый как объединение всех отношений рп для целых чисел п ≥ 0.

Два предыдущих примера - это наборы мощности, которые Булевы алгебры при обычных теоретико-множественных операциях объединения, пересечения и дополнения. Это оправдывает называть их Булевы алгебры действия. Реляционный пример представляет собой алгебра отношений оснащен операцией рефлексивного переходного замыкания. Обратите внимание, что каждая булева алгебра является алгеброй Гейтинга и, следовательно, алгеброй действия в силу того, что она является экземпляром первого примера.

Смотрите также

Рекомендации

  1. ^ Козен, Декстер (1990), «Об алгебрах Клини и замкнутых полукольцах» (PDF), в Б. Рован (ред.), Математические основы информатики (MFCS), LNCS 452, Springer-Verlag, стр. 26–47
  2. ^ Пратт, Воан (1990), «Логика действия и чистая индукция» (PDF), Логика в AI: европейская мастерская JELIA '90 (ред. Дж. ван Эйк), LNCS 478, Springer-Verlag, стр. 97–120.
  3. ^ Козен, Декстер (1994), «Об алгебрах действия» (PDF), Логика и информационный поток, Найденный. Comput. Сер., MIT Press, Кембридж, Массачусетс, стр. 78–88, МИСТЕР  1295061.
  • Конвей, Дж. (1971). Регулярная алгебра и конечные машины. Лондон: Чепмен и Холл. ISBN  0-412-10620-5. Zbl  0231.94041.
  • В.Н. Редько, Об определяющих соотношениях для алгебры регулярных событий, Украина. Мат. Z., 16:120–126, 1964.