АссистентНовый вопросИсторияОбласти знаний
Партнёрские проектыСпецпроектыСтать автором
Сменить язык
О РУВИКИ

Логика транзакций

Логика транзакций — расширение предикатной логики, которое позволяет чисто и декларативно описывать явление изменения состояния в логических программах и базах данных. Это расширение вводит связки, специально предназначенные для объединения простых действий в сложные транзакции и для организации контроля над их выполнением. Логика транзакций обладает естественной модельной семантикой и полнотой по доказательствам. Существует подмножество логики транзакций на роговых формулах, которое имеет как процедурную, так и декларативную семантику. К важным особенностям логики относятся гипотетические и фиксируемые (committed) обновления, динамические ограничения выполнения транзакций, недетерминизм и пакетные обновления. Благодаря этим свойствам логика транзакций позволяет декларативно описывать ряд нелогических явлений, включая процедурные знания в искусственном интеллекте, активные базы данных и методы с побочными эффектами в объектных базах данных.

История

Логика транзакций была впервые предложена в 1993 году Энтони Боннером[1] и Михаилом Кифером, а затем подробно описана в работах «An Overview of Transaction Logic»[2] и «Logic Programming for Database Transactions»[3]. Наиболее полное изложение логики транзакций дано в техническом отчёте Боннера и Кифера 1995 года[4].

В последующие годы логика транзакций была расширена различными возможностями, включая параллелизм[5], опровержимые рассуждения[6], частично определённые действия[7] и другими особенностями[8][9].

В 2013 году оригинальная статья о логике транзакций была удостоена премии «20-летний тест времени» Ассоциации по логическому программированию (англ. Association for Logic Programming) как самая влиятельная статья из материалов конференции ICLP 1993 за предыдущие двадцать лет.

Примеры

Раскраска графа

Здесь tinsert обозначает элементарную операцию транзакционного добавления. Связка ⊗ называется «сериальная конъюнкция». 

colorNode <-  // корректная раскраска одной вершины
    node(N) ⊗ ¬ colored(N,_) ⊗ color(C)
    ⊗ ¬(adjacent(N,N2) ∧ colored(N2,C))
    ⊗ tinsert(colored(N,C)).
colorGraph <- ¬uncoloredNodesLeft.
colorGraph <- colorNode ⊗ colorGraph.

Составление пирамиды

Элементарное обновление tdelete представляет собой операцию транзакционного удаления. 

stack(N,X) <- N>0 ⊗ move(Y,X) ⊗ stack(N-1,Y).
stack(0,X).
move(X,Y) <- pickup(X) ⊗ putdown(X,Y).
pickup(X) <- clear(X) ⊗ on(X,Y) ⊗
             ⊗ tdelete(on(X,Y)) ⊗ tinsert(clear(Y)).
putdown(X,Y) <-  wider(Y,X) ⊗ clear(Y) 
                 ⊗ tinsert(on(X,Y)) ⊗ tdelete(clear(Y)).

Гипотетическое выполнение

Здесь <> — модальный оператор возможности: если возможны обе action1 и action2, выполняется action1. В противном случае, если возможна только action2, выполняется она. 

execute <- <>action1 ⊗ <>action2 ⊗ action1.
execute <- ¬<>action1 ⊗ <>action2 ⊗ action2.

Задача о пиратах

Здесь | — связка параллельной конъюнкции, введённая в конкурентной логике транзакций[5]. 

diningPhilosophers <- phil(1) | phil(2) | phil(3) | phil(4).

Реализации

Существует несколько реализаций логики транзакций:

  • Оригинальная реализация[10].
  • Реализация конкурентной логики транзакций[11].
  • Логика транзакций с поддержкой табличного вычисления (tabling). Одна из реализаций логики транзакций также входит в состав системы представления знаний и вывода Flora-2[12].

Все эти реализации имеют открытую лицензию.

Примечания

  1. ↑ A.J. Bonner, M. Kifer. Transaction Logic Programming. International Conference on Logic Programming (ICLP), 1993.
  2. ↑ A.J. Bonner, M. Kifer. An Overview of Transaction Logic. Theoretical Computer Science, 133:2, 1994.
  3. ↑ A.J. Bonner, M. Kifer. Logic Programming for Database Transactions // Logics for Databases and Information Systems / под ред. J. Chomicki, G. Saake. Kluwer Academic Publishers, 1998. URL: http://www.cs.sunysb.edu/~kifer/TechReports/tr-chomicki.pdf
  4. ↑ A.J. Bonner, M. Kifer. Transaction Logic Programming (or A Logic of Declarative and Procedural Knowledge). Technical Report CSRI-323, November 1995, Computer Science Research Institute, University of Toronto. URL: http://www.cs.sunysb.edu/~kifer/TechReports/transaction-logic.pdf
  5. ↑ 1 2 A.J. Bonner, M. Kifer. Concurrency and communication in Transaction Logic. Joint International Conference and Symposium on Logic Programming, Bonn, Germany, сентябрь 1996. URL: http://www.cs.sunysb.edu/~kifer/TechReports/concurrent-trans-logic.pdf
  6. ↑ P. Fodor, M. Kifer. Transaction Logic with Defaults and Argumentation Theories. Technical communications of the 27th International Conference on Logic Programming (ICLP), июль 2011. URL: http://drops.dagstuhl.de/opus/volltexte/2011/3159/
  7. ↑ M. Rezk, M. Kifer. Transaction Logic with Partially Defined Actions. Journal on Data Semantics, август 2012, том 1, № 2, Springer. URL: https://link.springer.com/article/10.1007%2Fs13740-012-0007-8
  8. ↑ H. Davulcu, M. Kifer, I.V. Ramakrishnan. CTR-S: A Logic for Specifying Contracts in Semantic Web Services. Proceedings of the 13-ой Всемирной конференции по Всемирной паутине (WWW2004), май 2004. URL: http://www.www2004.org/proceedings/docs/2p144.pdf
  9. ↑ P. Fodor, M. Kifer. Tabling for Transaction Logic. В сборнике: Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), июль 2010. URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.184.6968
  10. ↑ Hung, Samuel Transaction Logic Prototype. University of Toronto, Department of Computer Science (1996). Дата обращения: 10 мая 2021. Архивировано 24 марта 2025 года.
  11. ↑ Sleghel, Amalia F. Concurrent Transaction Logic Prototype. University of Toronto, Department of Computer Science (2000). Дата обращения: 10 мая 2021. Архивировано 10 августа 2025 года.
  12. ↑ Knowledge Representation & Reasoning with Flora-2. Sourceforge.net. Дата обращения: 10 мая 2021.

Литература

Ссылки

  • Сайт Flora-2, содержит дополнительные публикации по логике транзакций

Категории