Алгебра действий
В алгебраической логике алгебра действия — это алгебраическая структура , которая одновременно является резидуированной полурешеткой и алгеброй Клини . Он добавляет звездочку или рефлексивное транзитивное замыкание последнего к первому, одновременно добавляя операции левого и правого остатка или импликации первого ко второму. В отличие от динамической логики и других модальных логик программ, для которых программы и предложения образуют два разных сорта, алгебра действий объединяет их в один вид. Ее можно рассматривать как вариант интуиционистской логики со звездой и некоммутативным соединением, тождество которого не обязательно должно быть верхним элементом. В отличие от алгебр Клини, алгебры действия образуют многообразие , которое, кроме того, является конечно аксиоматизируемым, причем ключевой аксиомой является a •( a → a )* ≤ a . В отличие от моделей эквациональной теории алгебр Клини (уравнений регулярных выражений), звездная операция алгебр действия представляет собой рефлексивное транзитивное замыкание в каждой модели уравнений. Алгебры действия были введены Воан Пратт на европейском семинаре JELIA'90. [1]
Определение [ править ]
Алгебра действия ( A , ∨, 0, •, 1, ←, →, *) — это алгебраическая структура такая, что ( A , ∨, •, 1, ←, →) образует оставшуюся полурешетку в смысле Уорда и Дилворта. , [2] в то время как ( A , ∨, 0, •, 1, *) образует алгебру Клини в смысле Декстера Козена . [3] То есть это любая модель совместной теории обоих классов алгебр. Теперь алгебры Клини аксиоматизируются с помощью квазиуравнений, то есть импликаций между двумя или более уравнениями, а следовательно, то же самое происходит и с алгебрами действия, если аксиоматизировать их непосредственно таким способом. Однако алгебры действия имеют то преимущество, что они также имеют эквивалентную аксиоматизацию, которая является чисто эквациональной. Язык алгебр действия естественным образом расширяется до языка решеток действий , а именно за счет включения операции встречи. [4]
Далее мы записываем неравенство a ≤ b как сокращение для уравнения a ∨ b = b . Это позволяет нам аксиоматизировать теорию с помощью неравенств, но при этом иметь чисто эквациональную аксиоматизацию, когда неравенства расширяются до равенств.
Уравнения, аксиоматизирующие алгебру действия, представляют собой уравнения для оставшейся полурешетки вместе со следующими уравнениями для звезды.
- 1 ∨ а *• а * ∨ а ≤ а *
- а * ≤ ( а ∨ б )*
- ( а → а )* ≤ а → а
Первое уравнение можно разбить на три уравнения: 1 ≤ a *, a *• a * ≤ a * и a ≤ a *. Определяя a рефлексивным, когда 1 ≤ a, и транзитивным, когда a • a ≤ a, путем абстракции от бинарных отношений, первые два из этих уравнений вынуждают a * быть рефлексивным и транзитивным, в то время как третье заставляет a * быть больше или равным a. . Следующая аксиома утверждает, что звезда монотонна. Последнюю аксиому можно эквивалентно записать как a •( a → a )* ≤ a , форма, которая делает ее роль индукции более очевидной. Эти две аксиомы в сочетании с аксиомами оставшейся полурешетки заставляют a * быть наименее рефлексивным транзитивным элементом полурешетки из элементов, больших или равных a . Приняв это за определение рефлексивного транзитивного замыкания a , мы тогда получим, что для каждого элемента a любой алгебры действий a * является рефлексивным транзитивным замыканием a .
Свойства [ править ]
Можно показать, что эквациональная теория фрагментов алгебр действия без импликаций, тех уравнений, которые не содержат → или ←, совпадает с эквациональной теорией алгебр Клини, также известной как уравнения регулярных выражений . В этом смысле приведенные выше аксиомы представляют собой конечную аксиоматизацию регулярных выражений. Редко показал в 1967 году, что уравнения регулярных выражений не имеют конечной аксиоматизации, для чего Джон Хортон Конвей дал более короткое доказательство в 1971 году. [5] [6] Арто Саломаа дал схему уравнений, аксиоматизирующую эту теорию, которую Декстер Козен впоследствии переформулировал как конечную аксиоматизацию с использованием квазиуравнений или импликаций между уравнениями, причем решающими квазиуравнениями являются уравнения индукции: если x • a ≤ x , то x • a * ≤ x , и если a • x ≤ x , тогда a *• x ≤ x . Козен определил алгебру Клини как любую модель этой конечной аксиоматизации.
Конвей показал, что эквациональная теория регулярных выражений допускает модели, в которых a * не является рефлексивным транзитивным замыканием a , дав четырехэлементную модель 0 ≤ 1 ≤ a ≤ a *, в которой a • a = a . В модели Конвея a является рефлексивным и транзитивным, поэтому его рефлексивное транзитивное замыкание должно быть a . Однако регулярные выражения не обеспечивают этого, позволяя * быть строго больше, чем . Такое аномальное поведение невозможно в алгебре действий, которая вынуждает a * быть наименее транзитивным рефлексивным элементом.
Примеры [ править ]
Любая алгебра Гейтинга (и, следовательно, любая булева алгебра ) становится алгеброй действия, если принять • равным ∧ и a * = 1. Это необходимо и достаточно для звезды, потому что верхний элемент 1 алгебры Гейтинга является ее единственным рефлексивным элементом, и транзитивно, а также больше или равно каждому элементу алгебры.
Набор 2 С* всех формальных языков (множеств конечных строк) над алфавитом Σ образует алгебру действий, где 0 — пустое множество, 1 = {ε}, ∨ — объединение, • — конкатенация, L ← M — множество всех строк x таких, что что xM ⊆ L (и двойственно для M → L ), и L * как множество всех строк строк в L (замыкание Клини).
Набор 2 Х² всех бинарных отношений на множестве X образует алгебру действий, где 0 — пустое отношение, 1 — тождественное отношение или равенство, ∨ — объединение, • — композиция отношений, R ← S — отношение, состоящее из всех пар ( x,y ) такой, что для всех в X ySz z влечет xRz ( и двойственно для S → R ), а R* как рефлексивное транзитивное замыкание R , определяемое как объединение всех отношений R н для целых чисел n ≥ 0.
Два предыдущих примера представляют собой степенные множества, которые являются булевыми алгебрами относительно обычных теоретико-множественных операций объединения, пересечения и дополнения. Это оправдывает название их булевых алгебр действия . Реляционный пример представляет собой алгебру отношений , оснащенную операцией рефлексивного транзитивного замыкания. Обратите внимание, что каждая булева алгебра является гейтинговой алгеброй и, следовательно, алгеброй действия, поскольку является примером первого примера.
См. также [ править ]
Ссылки [ править ]
- ^ Пратт, Воган (1990), «Логика действия и чистая индукция» (PDF) , Логика в искусственном интеллекте: Европейский семинар JELIA '90 (под ред. Дж. ван Эйка) , LNCS 478, Springer-Verlag, стр. 97–120 .
- ^ Уорд, Морган и Роберт П. Дилворт (1939) «Остаточные решетки», Trans. амер. Математика. Соц. 45 : 335–54. Перепечатано в книгах Богарт К., Фриз Р. и Кунг Дж., ред. (1990) Теоремы Дилворта: Избранные статьи Р. П. Дилворта Базель: Birkhäuser.
- ^ Козен, Декстер (1990), «Об алгебрах Клини и замкнутых полукольцах» (PDF) , в Б. Роване (ред.), Математические основы информатики (MFCS) , LNCS 452, Springer-Verlag, стр. 26–47.
- ^ Козен, Декстер (1994), «Об алгебрах действия» (PDF) , Логика и информационный поток , Найдено. Вычислить. Ser., MIT Press, Кембридж, Массачусетс, стр. 78–88, MR 1295061 .
- ^ Конвей, Дж. Х. (1971). Регулярная алгебра и конечные машины . Лондон: Чепмен и Холл. ISBN 0-412-10620-5 . Збл 0231.94041 .
- ^ В. Н. Редько, Об определяющих соотношениях для алгебры регулярных событий (рус.), Украин. Мат. З. , 16:120–126, 1964.