Harakat algebra - Action algebra

Yilda algebraik mantiq, an harakat algebra bu algebraik tuzilish ikkalasi ham a qoldiq semilattice va a Kleen algebra. U ikkinchisining yulduz yoki refleksiv tranzitiv yopilish operatsiyasini birinchisiga qo'shadi, ikkinchisining chap va o'ng qoldiqlari yoki implikatsiya operatsiyalarini qo'shadi. Aksincha dinamik mantiq Dasturlar va takliflar ikkita alohida turni tashkil etadigan dasturlarning boshqa modal mantiqlari, harakat algebra ikkalasini bitta turga birlashtiradi. Ning varianti sifatida qaralishi mumkin intuitivistik mantiq yulduz bilan va identifikatori yuqori element bo'lmasligi kerak bo'lgan qo'shma birikma bilan. Kleen algebralaridan farqli o'laroq, harakat algebralari a hosil qiladi xilma-xillik, bundan tashqari, bu juda muhim aksiomatizatsiyaga ega a•(a → a)* ≤ a. Kleen algebralarining tenglama nazariyasi modellaridan farqli o'laroq (odatdagi ifoda tenglamalari), harakat algebralarining yulduzcha ishlashi bu tenglamalarning har bir modelida reflektor o'tuvchi yopilishdir.

Ta'rif

An harakat algebra (A, ∨, 0, •, 1, ←, →, *) bu an algebraik tuzilish shu kabi (A, ∨, •, 1, ←, →) a shakllarini hosil qiladi qoldiq semilattice esa (A, ∨, 0, •, 1, *) a hosil qiladi Kleen algebra.[1] Ya'ni, bu algebralarning ikkala sinfining qo'shma nazariyasining har qanday modeli. Endi Kleen algebralari kvazi tenglamalar bilan aksiomatizatsiya qilinadi, ya'ni ikki yoki undan ortiq tenglamalar orasidagi ta'sirlar, shuning uchun to'g'ridan-to'g'ri shu tarzda aksiomatizatsiya qilinganida amal algebralari. Biroq, harakat algebralarining afzalligi shundaki, ular ham ekvivalent aksiomatizatsiyaga ega bo'lib, ular sof tenglamaga ega.[2] Harakat algebralari tili tabiiy ravishda kengayib boradi harakat panjaralari, ya'ni kutib olish operatsiyasini kiritish orqali.[3]

Quyida biz tengsizlikni yozamiz a ≤ b tenglamaning qisqartmasi sifatida a ∨ b = b. Bu bizga tengsizliklar yordamida nazariyani aksiomatizatsiya qilishga imkon beradi, ammo tengsizliklar tengliklarga kengaytirilganda hali ham to'liq tenglama aksiomatizatsiyaga ega.

Aksiomatizatsiya qiluvchi amallar algebrasi tenglamalari qoldiq yarim chiziq uchun tenglamalar va yulduz uchun quyidagi tenglamalar.

1 ∨ a*•a* ∨ a   ≤   a*
a* ≤ (a ∨ b)*
(a → a)*   ≤   a → a

Birinchi tenglamani uchta tenglamaga ajratish mumkin, 1 ≤ a*, a*•a* ≤ a*, va a ≤ a*. Ushbu kuch a* refleksiv, o'tkinchi,[tushuntirish kerak ] va undan katta yoki teng a navbati bilan. Ikkinchi aksioma yulduzning monoton ekanligini ta'kidlaydi. Uchinchi aksiomani ekvivalenti sifatida yozish mumkin a•(a → a)* ≤ a, induktsiya rolini yanada aniqroq ko'rsatadigan shakl. Ushbu ikki aksioma qoldiq yarim chiziq kuchi uchun aksiomalar bilan birgalikda a* ga teng yoki katta yarim chiziqning eng kam refleksiv o'tish elementi bo'lish a. Buni reflektiv o'tish davri yopilishining ta'rifi sifatida qabul qilish a, keyin bizda har bir element uchun shunday bo'ladi a har qanday harakat algebra, a* ning refleksiv o'tish davri yopilishi a.

Ta'sirsiz algebralar bo'linmasining tenglama nazariyasi, → yoki ← ni o'z ichiga olmaydigan tenglamalar Kleen algebralarining tenglama nazariyasiga to'g'ri kelishini ko'rsatishi mumkin. doimiy ifoda tenglamalar. Shu ma'noda yuqoridagi aksiomalar doimiy iboralarning cheklangan aksiomatizatsiyasini tashkil etadi. Redko 1967 yilda ushbu tenglamalarda cheklangan aksiomatizatsiya yo'qligini ko'rsatdi Jon Xorton Konvey 1971 yilda Salomaa ushbu nazariyani aksiomatizatsiya qiladigan tenglama sxemasini keltirdi, keyinchalik Kozen kvaziy tenglamalar yoki tenglamalar orasidagi natijalar yordamida cheklangan aksiomatizatsiya sifatida isloh qildi, agar hal qiluvchi kvazi tenglamalar induktsiyaga tegishli bo'lsa: agar x•a ≤ x keyin x•a* ≤ xva agar bo'lsa a•x ≤ x keyin a*•x ≤ x. Kozen Kleen algebrasini ushbu cheklangan aksiomatizatsiyaning har qanday modeli deb aniqladi.

Konvey shuni ko'rsatdiki, doimiy ifodalarning tenglama nazariyasi qaysi modellarni tan oladi a* ning refleksiv o'tish davri yopilishi emas edi a, to'rt elementli modelni berib 0 ≤ 1 ≤ a ≤ a* unda a•a = a. Konvey modelida, a reflektiv va o'tuvchi, bu erda uning reflektiv o'tish davri yopilishi kerak a. Ammo doimiy iboralar bunga yo'l qo'ymaydi a* dan kattaroq bo'lish a. Bunday g'ayritabiiy xatti-harakatlar harakat algebrasida mumkin emas.

Misollar

Har qanday Heyting algebra (va shuning uchun har qanday Mantiqiy algebra ) amal algebrasini • ni ∧ va ga olish orqali amalga oshiriladi a* = 1. Bu yulduz uchun zarur va etarli, chunki Heyting algebrasining yuqori elementi 1 uning reflektiv elementi bo'lib, tranzitiv, shuningdek algebra har bir elementiga katta yoki tengdir.

To'siq 2Σ * hammasidan rasmiy tillar (cheklangan satrlar to'plami) alifbosi ustida $ 0, $ 1 = {=}, birlashma sifatida ∨, birikma, L ← M barcha satrlar to'plami sifatida x shu kabi xM ⊆ L (va ikkitomonlama uchun M → L) va L* barcha satrlar to'plami sifatida L (Kleenening yopilishi).

To'siq 2X² to'plamdagi barcha ikkilik munosabatlarning X bo'sh algebra sifatida 0, o'zaro bog'liqlik yoki tenglik sifatida 1, birlik sifatida ∨, munosabat tarkibi sifatida, R ← S barcha juftlardan iborat bo'lgan munosabat sifatida (x, y) barchasi uchun z yilda X, ySz nazarda tutadi xRz (va ikkitomonlama uchun S → R) va R * ning reflektiv o'tuvchi yopilishi sifatida R, barcha munosabatlar ustidan birlashma sifatida belgilangan Rn butun sonlar uchun n ≥ 0.

Oldingi ikkita misol - kuch to'plamlari Mantiqiy algebralar odatdagi o'rnatilgan teoretik operatsiyalar bo'yicha birlashma, kesishma va komplement. Bu ularni chaqirishni oqlaydi Mantiqiy harakat algebralari. Aloqaviy misol a tashkil etadi munosabatlar algebra reflektiv o'tuvchi yopilish operatsiyasi bilan jihozlangan. Shuni esda tutingki, har bir mantiqiy algebra Heyting algebrasi va shuning uchun birinchi misolning misoli bo'lish uchun harakat algebrasi.

Shuningdek qarang

Adabiyotlar

  1. ^ Kozen, Dekter (1990), "Kleene algebralari va yopiq semiringi to'g'risida" (PDF), B. Rovanda (tahr.), Kompyuter fanining matematik asoslari (MFCS), LNCS 452, Springer-Verlag, 26-47 betlar
  2. ^ Pratt, Vaughan (1990), "Harakatlar mantig'i va sof induksiya" (PDF), AIda mantiq: JELIA '90 Evropa seminari (tahr. J. van Eyk), LNCS 478, Springer-Verlag, 97-120 betlar.
  3. ^ Kozen, Dekter (1994), "Harakat algebralari to'g'risida" (PDF), Mantiq va axborot oqimi, Topildi. Hisoblash. Ser., MIT Press, Kembrij, MA, 78–88 betlar, JANOB  1295061.
  • Konvey, J.X. (1971). Muntazam algebra va chekli mashinalar. London: Chapman va Xoll. ISBN  0-412-10620-5. Zbl  0231.94041.
  • V.N. Redko, Doimiy hodisalar algebrasi uchun munosabatlarni belgilash to'g'risida (rus), Ukraina. Mat Z., 16:120–126, 1964.