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

Логика транзакций была впервые предложена в 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].

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