Birlashtirilgan mantiq - Bunched logic

Birlashtirilgan mantiq^[1] turli xil substruktiv mantiq tomonidan taklif qilingan Piter O'Hirn va Devid Pim. To'plamli mantiq asoslash uchun ibtidoiy fikrlarni beradi resurs tarkibi, bu kompyuter va boshqa tizimlarning kompozitsion tahliliga yordam beradi. Unda kategoriya-nazariy va haqiqat-funktsional semantika mavjud bo'lib, ularni mavhum kontseptsiya tushunchasi nuqtai nazaridan anglash mumkin, va kontekst tarkibidagi an majburiyat hukm Γ ⊢ A - bu ko'pchilikdagi kabi ro'yxatlar yoki (ko'p) to'plamlardan ko'ra daraxtga o'xshash tuzilmalar (shamlardan). toshlar. Bunched mantiq bog'liq tip nazariyasiga ega va uning birinchi qo'llanilishi imperativ dasturlarda taxallusni va boshqa aralashuvlarni boshqarish usulini ta'minlashda edi.^[2]Mantiqiy dastur tasdiqlashda qo'shimcha dasturlarni ko'rdi, bu erda u tasdiqlash tilining asosi hisoblanadi ajratish mantig'i,^[3] va tizimni modellashtirishda, bu erda tizim tarkibiy qismlari foydalanadigan resurslarni parchalash usuli mavjud.^[4][5][6]

Jamg'arma

The chegirma teoremasi ning klassik mantiq birlashma va ma'no bilan bog'liq:

${ displaystyle A wedge B vdash C quad { mbox {iff}} quad A vdash B Rightarrow C}$

Bunched mantig'ida deduktsiya teoremasining ikkita versiyasi mavjud:

${ displaystyle A * B vdash C quad { mbox {iff}} quad A vdash B {- ! ! *} C qquad { mbox {va shuningdek}} qquad A takoz B vdash C quad { mbox {iff}} quad A vdash B Rightarrow C}$

${ displaystyle A * B}$ va ${ displaystyle B {- ! ! *} C}$ manbalarni hisobga oladigan bog'lanish va imlikatsiya shakllari (quyida tushuntirilgan). Ushbu biriktiruvchilardan tashqari birlashtirilgan mantiq formulaga ega, ba'zida I yoki emp yoziladi, bu * ning birligi. To'plamli mantiqning asl nusxasida ${ displaystyle wedge}$ va ${ displaystyle Rightarrow}$ intuitivistik mantiqdan bog'lovchi edi, mantiqiy variant esa ${ displaystyle wedge}$ va ${ displaystyle Rightarrow}$ (va ${ displaystyle neg}$) an'anaviy mantiqiy mantiqdan. Shunday qilib, yig'ma mantiq konstruktiv printsiplarga mos keladi, lekin hech qanday tarzda ularga bog'liq emas.

Haqiqiy funktsional semantika (manba semantikasi)

Ushbu formulalarni tushunishning eng oson usuli uning haqiqat-funktsional semantikasi nuqtai nazaridan. Ushbu semantikada berilgan manbalarga nisbatan formula to'g'ri yoki noto'g'ri. ${ displaystyle A * B}$ mavjud bo'lgan resursni qoniqtiradigan resurslarga ajratish mumkinligini ta'kidlaydi ${ displaystyle A}$ va ${ displaystyle B}$. ${ displaystyle B {- ! ! *} C}$ agar biz qo'limizdagi manbani qoniqtiradigan qo'shimcha resurs bilan tuzsak ${ displaystyle B}$, keyin birlashtirilgan resurs qondiradi ${ displaystyle C}$. ${ displaystyle wedge}$ va ${ displaystyle Rightarrow}$ ularning tanish ma'nolariga ega.

Ushbu formulalarni o'qish uchun asos semantikani majburlash bilan ta'minlangan ${ displaystyle r modellari A}$ Pym tomonidan ilgari surilgan, bu erda majburiy munosabat "r" manbasini ushlab turish degan ma'noni anglatadi. Semantikasi Kripkening semantikasiga o'xshaydi intuitiv yoki modal mantiq, lekin bu erda model elementlari bir-biridan foydalanish mumkin bo'lgan olamlarga emas, balki tuzilishi va parchalanishi mumkin bo'lgan manbalar sifatida qaraladi. Masalan, boglanish uchun majburiy semantik shakl

${ displaystyle r modellari A * B quad { mbox {iff}} quad mavjud r_ {A} r_ {B}. , r_ {A} A, , r_ {B} modellari B , , { mbox {and}} , r_ {A} bullet r_ {B} leq r}$

qayerda ${ displaystyle r_ {A} bullet r_ {B}}$ resurslarni birlashtirishning bir usuli va ${ displaystyle leq}$ yaqinlashish munosabati.

Ushbu mantiqiy semantika, tegishli mantiqdagi (ayniqsa, Rutli-Meyerning operatsion semantikasi) oldingi ishlarga asoslanadi, ammo undan talab qilmaslik bilan farq qiladi ${ displaystyle r bullet r leq r}$ va standart intuitsional yoki klassik versiyalarining semantikasini qabul qilish orqali ${ displaystyle wedge}$ va ${ displaystyle Rightarrow}$. Mulk ${ displaystyle r bullet r leq r}$ dolzarbligi haqida o'ylashda oqlanadi, ammo resurslarni inkor etishi; resursning ikki nusxasiga ega bo'lish bilan bir xil emas va ba'zi modellarda (masalan, yig'ma modellarda) ${ displaystyle r bullet r}$ hatto aniqlanmagan bo'lishi mumkin. Ning standart semantikasi ${ displaystyle Rightarrow}$ (yoki inkor qilish) ko'pincha modellashtirish resurslari nuqtai nazaridan muammo bo'lmagan va shuning uchun mantiqiy rad etilmagan "moddiy implikatsiya paradokslaridan" qochish uchun tegishli shaxslar tomonidan rad etiladi. Semantika, shuningdek, chiziqli mantiqning "fazoviy semantikasi" bilan bog'liq, ammo yana standart (hatto mantiqiy) semantikani qabul qilish bilan farqlanadi ${ displaystyle wedge}$ va ${ displaystyle Rightarrow}$ chiziqli mantiqda konstruktiv bo'lish taklifida rad etilgan. Ushbu fikrlar Pym, O'Hearn va Yangning Resurs semantikasi haqidagi maqolasida batafsil ko'rib chiqilgan.^[7]

Kategorik semantik (ikki marta yopiq toifalar)

Bunched mantiqning deduksiya teoremasining ikki nusxali versiyasi tegishli kategoriya-nazariy tuzilishga ega. Intuitiv mantiqdagi dalillarni izohlash mumkin kartezian yopildi toifalar, ya'ni uy to'plamlari bilan bog'liq bo'lgan (A va C tabiiy) qo'shma yozishmalarini qondiradigan cheklangan mahsulotlarga ega toifalar:

${ displaystyle Hom (A wedge B, C) quad { mbox {izomorfik}} quad Hom (A, B Rightarrow C)}$

Bunched mantiqni ikkita shunday tuzilishga ega bo'lgan toifalarda talqin qilish mumkin

bunched mantiqning kategorik modeli - bu ikkita yopiq tuzilishga ega bo'lgan bitta toifadir, biri nosimmetrik monoidal, ikkinchisi kartezian yopiq.

Day's yordamida ko'plab toifali modellarni berish mumkin tensor mahsuloti qurilish.^[8]Bundan tashqari, to'plam mantig'ining implikatsion qismiga o'yinlarning semantikasi berilgan.^[9]

Algebraik semantika

Bunched mantiqning algebraik semantikasi uning kategorik semantikasining alohida hodisasidir, ammo bayon qilish oddiy va osonroq bo'lishi mumkin.

bunched mantiqning algebraik modeli - bu poset Heyting algebra va qo'shimcha kommutativga ega qoldiq panjarasi tuzilish (Heyting algebrasi bilan bir xil panjara uchun): ya'ni, qoniqtiradigan bog'liqligi bilan tartiblangan komutativ monoid ${ displaystyle A * B leq C quad { mbox {iff}} quad A leq B {- ! ! *} C}$.

Bunched mantiqning mantiqiy versiyasi quyidagi modellarga ega.

mantiqiy mantiqning algebraik modeli - bu poset Mantiqiy algebra va qo'shimcha qoldiq komutativ monoid tuzilishga ega.

Isbot nazariyasi va tur nazariyasi (guruhlar)

The dalil hisobi mantiqiy odatdagidan farq qiladi ketma-ket toshlar ning daraxtga o'xshash kontekstida gipotezalar tekis ro'yxatga o'xshash tuzilish o'rniga. Uning ketma-ket asoslangan isbot nazariyalarida, kontekst ${ displaystyle Delta}$ sud qaroriga binoan ${ displaystyle Delta vdash A}$barglari takliflar va ichki tugunlari ikkita bog'lovchiga mos keladigan kompozitsiya usullari bilan etiketlangan daraxtdir. Ikkala birlashtiruvchi operatorlar - vergul va vergul (masalan), ikkita taassurot uchun kirish qoidalarida qo'llaniladi.

${ displaystyle { frac { Gamma, A vdash B} { Gamma vdash A {- ! ! *} B}} qquad qquad { frac { Gamma; A vdash B} { Gamma vdash A { Rightarrow} B}}}$

Ikkala kompozitsiya qoidalari orasidagi farq ularga tegishli bo'lgan qo'shimcha qoidalardan kelib chiqadi.

• Multiplikatsion kompozitsiya ${ displaystyle Delta, Gamma}$ inkor qiladi tarkibiy qoidalar zaiflashuv va qisqarish.
• Qo'shimchalar tarkibi ${ displaystyle Delta; Gamma}$ butun guruhlarning zaiflashishi va qisqarishini tan oladi.

Tuzilish qoidalari va dastalardagi boshqa operatsiyalar ko'pincha yuqori kontekstda emas, balki daraxt kontekstida juda ko'p qo'llaniladi: bu ma'lum ma'noda chuqur xulosa chiqarish.

Bunched mantiqiga mos keladigan ikki xil funktsiya turiga ega bo'lgan tip nazariyasi. Keyingi Kori-Xovard yozishmalari, natijalar uchun kirish qoidalari funktsiya turlari uchun kirish qoidalariga mos keladi.

${ displaystyle { frac { Gamma, x: A vdash M: B} { Gamma vdash lambda xM: A {- ! ! *} B}} qquad qquad { frac { Gamma ; x: A vdash M: B} { Gamma vdash alfa xM: A { Rightarrow} B}}}$

Mana, ikkita aniq bog'lovchi bor, ${ displaystyle lambda}$ va ${ displaystyle alpha}$, funktsiya turlarining har bir turi uchun bitta.

Bunched mantiqning isbot nazariyasi, dolzarblik mantig'idagi to'plamlardan foydalanishga tarixiy qarzga ega.^[10] Ammo bunker tuzilishi ma'lum ma'noda kategorik va algebraik semantikadan kelib chiqishi mumkin: kirish qoidasini shakllantirish ${ displaystyle {- ! ! *}}$ biz taqlid qilishimiz kerak ${ displaystyle *}$ chap tomonda ketma-ketlikda va tanishtirish uchun ${ displaystyle Rightarrow}$ biz taqlid qilishimiz kerak ${ displaystyle wedge}$. Ushbu mulohaza ikkita birlashtiruvchi operatordan foydalanishga olib keladi.

Jeyms Brotherston bir qator mantiq va variantlar uchun yagona isbot nazariyasi bo'yicha muhim ishlarni amalga oshirdi,^[11] ish bilan ta'minlash Belnap tushunchasi mantiqni ko'rsatish.^[12]

Galmiche, Méry va Pym to'plamlarga asoslangan mantiqni, shu jumladan to'liqlik va boshqa meta-nazariyani kompleks davolashni ta'minladilar. stol.^[13]

Ilovalar

Shovqinlarni boshqarish

Ehtimol, resurslarni boshqarish uchun pastki tuzilish nazariyasining birinchi qo'llanilishida, Jon C. Reynolds Algolga o'xshash dasturlash tillarida chalg'ituvchi va boshqa aralashuv shakllarini boshqarish uchun afine tip nazariyasidan qanday foydalanishni ko'rsatib berdi.^[14] O'Hearn shovqinlarni va aralashmasliklarni yanada moslashuvchan aralashtirishga imkon berib, Reynolds tizimini kengaytirish uchun bunched tip nazariyasini qo'llagan.^[2] Bu Reynolds tizimidagi rekursiya va sakrash bilan bog'liq ochiq muammolarni hal qildi.

Ajratish mantig'i

Ajratish mantig'i - kengaytmasi Mantiqiylik bu ko'rsatgichlardan foydalanadigan o'zgaruvchan ma'lumotlar tuzilmalari haqida fikr yuritishni osonlashtiradi. Hoare mantig'idan keyin ajratish mantig'ining formulalari shaklga ega${ displaystyle {Pre } programmasi {Post }}$, ammo old shartlar va keyingi shartlar to'plamli mantiq modelida talqin qilingan formulalardir.Mantiqning asl nusxasi quyidagi modellarga asoslangan edi:

• ${ displaystyle Heaps = L rightharpoonup _ {f} V qquad}$ (cheklangan qisman funktsiyalar joylardan qiymatgacha)
• ${ displaystyle h_ {0} bullet h_ {1} =}$ domenlar ustma-ust tushganda aniqlanmagan, ajratilgan domenlar bilan uyumlarning birlashishi.

Ajratish g'oyasini modellashtiradigan bir-birining ustiga chiqadigan uyumlardagi kompozitsiyaning aniqlanmaganligi. Bu to'plamli mantiqning mantiqiy variantining modeli.

Dastlab ketma-ketlikdagi dasturlarni isbotlash uchun ajratish mantig'idan foydalanilgan, ammo keyinchalik dalil qoidasi yordamida bir xillikka kengaytirilgan

${ displaystyle { frac { {P_ {1} } C_ {1} {Q_ {1} } quad {P_ {2} } C_ {2} {Q_ {2} }} { {P_ {1} * P_ {2} } C_ {1} parallel C_ {2} {Q_ {1} * Q_ {2} }}}}$

Parallel iplar orqali saqlanadigan joyni ajratuvchi.^[15]

Keyinchalik, manba semantikasining umumiyligi ishlatildi: ajratish mantig'ining mavhum versiyasi Hoare uchun uch baravar ishlaydi, bu erda old shartlar va postkonditsiyalar ma'lum bir uyum modeli o'rniga o'zboshimchalik bilan qisman komutativ monoidga sharhlangan formulalardir.^[16] Kommutativ monoidni tanlagan holda, ajablanarli tarzda bir vaqtning o'zida ajratish mantig'ining mavhum versiyalarining dalil qoidalari aralashayotgan bir vaqtda jarayonlar haqida fikr yuritish uchun ishlatilishi mumkinligi aniqlandi, masalan, ishonchni kafolatlash va izlashga asoslangan fikrlash.^[17][18]

Ajratish mantig'i dasturlar haqida avtomatik va yarim avtomatik mulohaza yuritish uchun bir qator vositalarning asosidir va hozirda Facebook-da joylashgan Infer dastur analizatorida qo'llaniladi.^[19]

Resurslar va jarayonlar

Biriktirilgan mantiq SCRP (sinxron) resurs-jarayon hisobi bilan bog'liq holda ishlatilgan^[4][5][6] xarakterli (modal) mantiqni berish uchun, Xennessi ma'nosida -Milner, bir vaqtda tizimlarning kompozitsion tuzilishi.

SCRP tarjima qilish bilan ajralib turadi ${ displaystyle A * B}$ xususida ikkalasi ham tizimlarning parallel tarkibi va ular bilan bog'liq resurslarning tarkibi. SCRP jarayoni mantig'ining bir xillik uchun ajratish mantig'ining qoidasiga mos keladigan semantik moddasi formulani tasdiqlaydi ${ displaystyle A * B}$ resurs-jarayon holatida to'g'ri keladi ${ displaystyle R}$,${ displaystyle E}$ manba parchalanishi bo'lsa ${ displaystyle R = S bullet T}$ va jarayon ${ displaystyle E}$ ~ ${ displaystyle F times G}$, qaerda ~ bisimulyatsiyani bildiradi, shunda ${ displaystyle A}$ resurs-jarayon holatida to'g'ri keladi ${ displaystyle S}$ , ${ displaystyle F}$ va ${ displaystyle B}$ resurs-jarayon holatida to'g'ri keladi ${ displaystyle T}$ , ${ displaystyle G}$; anavi ${ displaystyle R, E modellari A}$ iff ${ displaystyle S, F modellari A}$ va ${ displaystyle T, G modellari B}$.

SCRP tizimi ^[4][5][6] to'g'ridan-to'g'ri mantiqiy manba semantikasiga asoslangan; ya'ni resurs elementlarining buyurtma qilingan monoidlarida. To'g'ridan-to'g'ri va intuitiv ravishda jozibador bo'lishiga qaramay, ushbu tanlov o'ziga xos texnik muammoga olib keladi: Hennessy-Milner to'liqligi teoremasi faqat multiplikativ implikatsiya va multiplikativ usullarni istisno qiladigan modal mantiqning qismlari uchungina amal qiladi. Ushbu muammo manba jarayonlari hisobini manba semantikasiga asoslanib echiladi, bunda manba elementlari bir vaqtning o'zida tarkibiga va ikkinchisiga mos keladigan ikkita kombinator yordamida birlashtiriladi.^[20]

Mekansal mantiq

Kardelli, Kaires, Gordon va boshqalar kontseptsiya parallel kompozitsiya nuqtai nazaridan talqin qilinadigan jarayon hisoblashlarining bir qator mantiqlarini tadqiq qildilar. [Adabiyotlar, qo'shimcha qilish] Pym va boshqalarning ishidan farqli o'laroq. SCRP-da ular tizimlarning parallel tarkibi va tizimlar kiradigan resurslar tarkibini ajratib ko'rsatmaydi.

Ularning mantiqiyligi mantiqiy mantiqning mantiqiy varianti modellarini keltirib chiqaradigan manba semantikasi misollariga asoslangan. Garchi bu mantiqlar mantiqiy mantiqiy misollarni keltirib chiqarsa-da, ular mustaqil ravishda kelganga o'xshaydi va har qanday holatda ham modalar va bog'lovchilar yo'lida muhim qo'shimcha tuzilishga ega. XML ma'lumotlarini modellashtirish uchun tegishli mantiqlar taklif qilingan.

Shuningdek qarang

• Ajratish mantig'i
• Muvofiqlik mantig'i
• Lineer mantiq

Adabiyotlar