Tranzaksiya mantig'i - Transaction logic

Tranzaksiya mantig'i ning kengaytmasi mantiq davlatning o'zgarishi hodisasini toza va deklarativ tarzda hisobga oladigan mantiqiy dasturlar va ma'lumotlar bazalari. Ushbu kengaytma oddiy harakatlarni murakkab operatsiyalarga birlashtirish va ularning bajarilishini nazorat qilishni ta'minlash uchun maxsus ishlab chiqarilgan biriktirgichlarni qo'shadi. Mantiq tabiiydir model nazariyasi va tovushli va to'liq isbot nazariyasi. Transaction Logic a ga ega Shox moddasi deklarativ semantikaga ega bo'lgan protsessual va subset. Mantiqning muhim xususiyatlariga faraziy va sodiq yangilanishlar, tranzaktsiyalarni bajarishda dinamik cheklovlar, noaniqlik va ommaviy yangilanishlar kiradi. Shu tarzda, Transaction Logic bir qator mantiqiy bo'lmagan hodisalarni deklarativ ravishda qamrab olishga qodir, shu jumladan protsessual bilim yilda sun'iy intellekt, faol ma'lumotlar bazalari va yon ta'siri bo'lgan usullar ob'ekt ma'lumotlar bazalari.

Transaction Logic dastlab taklif qilingan [1] tomonidan Entoni Bonner va Maykl Kifer va keyinchalik batafsilroq tavsiflangan [2] va.[3] Eng to'liq tavsif paydo bo'ladi.[4]

Keyingi yillarda Transaction Logic turli yo'llar bilan kengaytirildi, shu jumladan bir vaqtda,[5] mag'lub bo'ladigan mulohaza,[6] qisman belgilangan harakatlar,[7] va boshqa xususiyatlar.[8][9]

2013 yilda Transaction Logic bo'yicha asl qog'oz [1] 20 yillik "Vaqt sinovi" mukofotini protsessning eng ta'sirli qog'ozi sifatida qo'lga kiritdi ICLP 1993 konferentsiyasi oldingi 20 yil ichida.[iqtibos kerak ]

Misollar

Grafikni bo'yash. Bu yerda tinsert ning boshlang'ich yangilanishini bildiradi bitim qo'shimchasi. Connect biriktiruvchisi deyiladi ketma-ket birikma.

colorNode <- // bitta tugunni to'g'ri rangga bo'yash (N) ¬ ¬ rangli (N, _) ⊗ rang (C) ⊗ ¬ (qo'shni (N, N2) ∧ rangli (N2, C)) ⊗ tinsert (rangli (N, C)). ColorGraph <- ¬uncoloredNodesLeft.colorGraph <- colorNode ⊗ colorGraph.

Piramidani yig'ish. Boshlang'ich yangilanish tdelete ifodalaydi tranzaktsiyani o'chirish operatsiya.

stack (N, X) <- N> 0 ⊗ move (Y, X) ⊗ stack (N-1, Y) .stack (0, X) .move (X, Y) <- pick (X) ⊗ putdown ( X, Y). Olish (X) <- aniq (X) ⊗ (X, Y)) ⊗ tdelete ((X, Y)) ⊗ tinsert (aniq (Y)). Qo'yish (X, Y) <- kengroq (Y, X) ⊗ tiniq (Y) ⊗ tinsert ((X, Y) da) ⊗ tdelete (aniq (Y)).

Gipotetik ijro. Bu yerda <> imkoniyatning modal operatori: Agar ikkalasi ham bo'lsa harakat1 va harakat2 mumkin, ijro eting harakat1. Aks holda, agar kerak bo'lsa harakat2 mumkin, keyin uni bajaring.

 <- <> action1 ⊗ <> action2 2 action1 ni bajaring. <- ¬ <> action1 ⊗ <> action2 2 action2 ni bajaring.

Ovqatlanish faylasuflari. Mana | Parallel Transaction Logic-ning parallel birikmasining mantiqiy biriktiruvchisi.[5]

diningFilosoflar <- phil (1) | fil (2) | fil (3) | fil (4).

Amaliyotlar

Transaction Logic dasturining bir qator dasturlari mavjud. Dastlabki dastur mavjud Bu yerga. Bir vaqtning o'zida operatsiyalar mantig'ini amalga oshirish mumkin Bu yerga. Tranzaksiya mantig'i yaxshilandi jadvalga kiritish mavjud Bu yerga. Transaction Logic dasturining bir qismi sifatida kiritilgan Flora-2 bilimlarni namoyish etish va fikrlash tizimi. Ushbu dasturlarning barchasi ochiq manba.

Tranzaksiya mantig'i bo'yicha qo'shimcha hujjatlarni quyidagi manzilda topishingiz mumkin Flora-2 veb-sayti.

Adabiyotlar

  1. ^ a b A.J. Bonner va M. Kifer (1993), Tranzaksiyalarni mantiqiy dasturlash, Mantiqiy dasturlash bo'yicha xalqaro konferentsiya (ICLP), 1993 y.
  2. ^ A.J. Bonner va M. Kifer (1994), Tranzaktsiyalar mantig'iga umumiy nuqtai, Nazariy kompyuter fanlari, 133: 2, 1994 y.
  3. ^ A.J. Bonner va M. Kifer (1998), Ma'lumotlar bazasi operatsiyalari uchun mantiqiy dasturlash Ma'lumotlar bazalari va axborot tizimlari uchun mantiq, J. Chomicki va G. Saake (tahr.), Kluwer Academic Publ., 1998.
  4. ^ A.J. Bonner va M. Kifer (1995), Tranzaktsiyalarni mantiqiy dasturlash (yoki deklarativ va protsessual bilimlarning mantiqi). Texnik hisobot CSRI-323, 1995 yil noyabr, Toronto universiteti kompyuter fanlari tadqiqot instituti.
  5. ^ a b A.J. Bonner va M. Kifer (1996), Transaction Logic-da o'zaro bog'liqlik va aloqa, Qo'shma xalqaro. Mantiqiy dasturlash bo'yicha konferentsiya va simpozium, Bonn, Germaniya, 1996 yil sentyabr
  6. ^ P. Fodor va M. Kifer (2011), Standart va argumentatsion nazariyalar bilan operatsiyalar mantig'i. Mantiqiy dasturlash bo'yicha 27-Xalqaro konferentsiyaning (ICLP) Texnik aloqalarida, 2011 yil iyul.
  7. ^ M. Rezk va M. Kifer (2012), Qisman belgilangan harakatlar bilan operatsiya mantig'i. Ma'lumotlar semantikasi jurnali, 2012 yil avgust, vol. 1, yo'q. 2, Springer.
  8. ^ X. Davulcu, M. Kifer va I.V. Ramakrishnan (2004), CTR-S: Semantik veb-xizmatlarda shartnomalarni belgilash uchun mantiq. 13-Butunjahon Internet tarmog'i konferentsiyasi (WWW2004), 2004 yil may.
  9. ^ P. Fodor va M. Kifer (2010), Tranzaksiya mantig'i uchun jadval tuzish. Deklarativ dasturlash printsiplari va amaliyoti (PPDP) bo'yicha 12-xalqaro ACM SIGPLAN simpoziumi materiallarida, 2010 yil iyul.