Bunched logic

The easiest way to understand these formulae is in terms of its truth-functional semantics. In this semantics a formula is true or false with respect to given resources. ${\displaystyle A*B}$ asserts that the resource at hand can be decomposed into resources that satisfy ${\displaystyle A}$ and ${\displaystyle B}$. ${\displaystyle B{-\!\!*}C}$ says that if we compose the resource at hand with additional resource that satisfies ${\displaystyle B}$, then the combined resource satisfies ${\displaystyle C}$. ${\displaystyle \wedge }$ and ${\displaystyle \Rightarrow }$ have their familiar meanings.

The foundation for this reading of formulae was provided by a forcing semantics ${\displaystyle r\models A}$طوّر بيم هذا المفهوم، حيث تعني علاقة الإجبار أن " أ يمتلك المورد ر " . يشابه هذا المفهوم دلالات كريپكي للمنطق الحدسي أو الموجه ، ولكن حيث تُعتبر عناصر النموذج موارد قابلة للتركيب والتفكيك، بدلاً من كونها عوالم ممكنة يمكن الوصول إليها من بعضها البعض. على سبيل المثال، تكون دلالات الإجبار للاقتران على الشكل التالي:

${\displaystyle r\models A*B\quad {\mbox{iff}}\quad \exists r_{A}r_{B}.\,r_{A}\models A,\,r_{B}\models B,\,{\mbox{and}}\,r_{A}\bullet r_{B}\leq r}$

أين${\displaystyle r_{A}\bullet r_{B}}$هي طريقة لدمج الموارد و${\displaystyle \leq }$هي علاقة تقريبية.

تستند دلالات منطق التجميع هذه إلى أعمال سابقة في منطق الصلة (وخاصة الدلالات التشغيلية لروتلي-ماير)، ولكنها تختلف عنها بعدم اشتراطها ${\displaystyle r\bullet r\leq r}$وذلك بقبول دلالات النسخ الحدسية أو الكلاسيكية القياسية لـ${\displaystyle \wedge }$و${\displaystyle \Rightarrow }$العقار${\displaystyle r\bullet r\leq r}$ يُعتبر ذلك مبرراً عند التفكير في مدى الصلة، ولكنه مرفوض بسبب اعتبارات الموارد؛ فامتلاك نسختين من مورد ما لا يعني بالضرورة امتلاك نسخة واحدة، وفي بعض النماذج (مثل نماذج الكومة ).${\displaystyle r\bullet r}$قد لا يكون لها تعريف محدد. الدلالات القياسية لـ ${\displaystyle \Rightarrow }$(أو النفي) غالبًا ما يرفضه أصحاب المذهب ذي الصلة في محاولتهم للهروب من "مفارقات الاستلزام المادي"، التي لا تُمثل مشكلة من منظور موارد النمذجة، وبالتالي لا يرفضها المنطق المُجمّع. ترتبط الدلالات أيضًا بـ"دلالات الطور" للمنطق الخطي ، ولكنها تتميز مرة أخرى بقبول الدلالات القياسية (حتى المنطقية) لـ${\displaystyle \wedge }$و${\displaystyle \Rightarrow }$وهو ما يُرفض في المنطق الخطي في محاولةٍ للبناء. وقد نُوقشت هذه الاعتبارات بالتفصيل في مقالٍ حول دلالات الموارد من تأليف بيم وأوهيرن ويانغ. ^{[ 7 ]}

للصيغة المزدوجة لنظرية الاستنتاج في المنطق المجمّع بنيةٌ مقابلةٌ في نظرية الفئات. ويمكن تفسير البراهين في المنطق الحدسي في فئات ديكارتية مغلقة ، أي فئات ذات جداءات منتهية تحقق تناظر الاقتران ( الطبيعي في A و C ) الذي يربط بين مجموعات التماثل .

${\displaystyle Hom(A\wedge B,C)\quad {\mbox{متماثل مع}}\quad Hom(A,B\Rightarrow C)}$

يمكن تفسير المنطق المجمع في فئات تمتلك بنيتين من هذا القبيل

النموذج الفئوي للمنطق المجمع هو فئة واحدة تمتلك بنيتين مغلقتين، إحداهما مغلقة أحادية متناظرة والأخرى مغلقة ديكارتية.

يمكن تقديم مجموعة من النماذج التصنيفية باستخدام بناء داي لضرب الموتر . ^{[ 8 ]} بالإضافة إلى ذلك، تم إعطاء الجزء الاستلزامي من المنطق المجمع دلالات لعبة . ^{[ 9 ]}

إن الدلالات الجبرية للمنطق المجمع هي حالة خاصة من دلالاته الفئوية، ولكن من السهل صياغتها ويمكن أن تكون أكثر قابلية للفهم.

النموذج الجبري للمنطق المجمع هو مجموعة مرتبة جزئياً تمثل جبر هيتينغ وتحمل بنية شبكية متبقية تبديلية إضافية (لنفس الشبكة الخاصة بجبر هيتينغ): أي، أحادي تبديلي مرتب مع استلزام مرتبط يحقق${\displaystyle A*B\leq C\quad {\mbox{iff}}\quad A\leq B{-\!\!*}C}$.

يحتوي الإصدار البولياني من المنطق المجمع على نماذج كما يلي.

النموذج الجبري للمنطق المجمع البولياني هو مجموعة مرتبة جزئياً تمثل جبرًا بوليانيًا وتحمل بنية أحادية تبديلية متبقية إضافية.

يختلف حساب البرهان في المنطق المجمّع عن حسابات التسلسل المعتادة في امتلاكه سياقًا شجريًا من الفرضيات بدلًا من بنية مسطحة تشبه القائمة. في نظريات البرهان القائمة على التسلسل، يكون السياق${\displaystyle \Delta }$في حكم يتعلق بالاستلزام${\displaystyle \Delta \vdash A}$ هي شجرة جذرية محدودة، أوراقها عبارة عن قضايا، وعُقدها الداخلية مُصنَّفة بأنماط التركيب التي تُقابل العطفين. يُستخدم عاملا الربط، الفاصلة والفاصلة المنقوطة، (على سبيل المثال) في قواعد الإدخال للاستلزامين.

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

يكمن الفرق بين قاعدتي التركيب في القواعد الإضافية التي تنطبق عليهما.

• التركيب المضاعف${\displaystyle \Delta ,\Gamma }$ينكر القواعد الهيكلية للضعف والانكماش.
• تركيبة مضافة${\displaystyle \Delta$ ;\Gamma } يسمح بإضعاف وانكماش الحزم بأكملها.

غالباً ما يتم تطبيق القواعد الهيكلية والعمليات الأخرى على المجموعات في عمق سياق الشجرة، وليس فقط على المستوى الأعلى: وبالتالي فهي بمعنى ما حساب للاستدلال العميق .

يُقابل منطق التجميع نظرية أنواع تحتوي على نوعين من أنواع الدوال . ووفقًا لتطابق كاري-هوارد ، فإن قواعد إدخال الاستلزام تُقابل قواعد إدخال أنواع الدوال.

${\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 \alpha xM:A{\Rightarrow }B}}}$

يوجد هنا مجلدان مختلفان،${\displaystyle \lambda }$و${\displaystyle \alpha }$واحد لكل نوع من أنواع الوظائف.

تستند نظرية إثبات المنطق التجميعي تاريخيًا إلى استخدام التجميعات في منطق الصلة. ^{[ 10 ]} ولكن يمكن اشتقاق البنية التجميعية، بمعنى ما، من الدلالات الفئوية والجبرية: لصياغة قاعدة إدخال لـ${\displaystyle {-\!\!*}}$ينبغي أن نقلد${\displaystyle *}$على اليسار بالتسلسل، ولتقديم${\displaystyle \Rightarrow }$ينبغي أن نقلد${\displaystyle \wedge }$. هذا الاعتبار يؤدي إلى استخدام عاملين للدمج.

وقد قام جيمس براذرستون بعمل هام آخر على نظرية إثبات موحدة للمنطق المجمع ومتغيراته، ^{[ 11 ]} باستخدام مفهوم بيلناب لمنطق العرض . ^{[ 12 ]}

قدم كل من غالميش وميري وبيم معالجة شاملة للمنطق المجمع، بما في ذلك الاكتمال ونظرية ما وراء النظرية الأخرى، استنادًا إلى الجداول المصنفة . ^{[ 13 ]}

في أول استخدامٍ لنظرية الأنواع البنيوية الفرعية للتحكم في الموارد، بيّن جون سي. رينولدز كيفية استخدام نظرية الأنواع الأفينية للتحكم في التداخل وأنواع أخرى من التداخل في لغات البرمجة الشبيهة بلغة ALGOL . ^{[ 14 ]} استخدم أوهيرن نظرية الأنواع المجمعة لتوسيع نظام رينولدز من خلال السماح بمزج التداخل وعدم التداخل بمرونة أكبر. ^{[ 2 ]} وقد حلّ هذا مشاكل مفتوحة تتعلق بالاستدعاء الذاتي والقفزات في نظام رينولدز.

منطق الفصل هو امتداد لمنطق هوار ، يُسهّل الاستدلال حول هياكل البيانات القابلة للتغيير التي تستخدم المؤشرات . وباتباع منطق هوار، تكون صيغ منطق الفصل على الشكل التالي: ${\displaystyle \{ما قبل\}البرنامج\{ما بعد\}}$لكن الشروط المسبقة واللاحقة عبارة عن صيغ تُفسَّر وفق نموذج منطق التجميع. وقد استندت النسخة الأصلية من هذا المنطق إلى نماذج على النحو التالي:

• ${\displaystyle Heaps=L\rightharpoonup _{f}V\qquad }$( دوال جزئية محدودة من المواقع إلى القيم)
• ${\displaystyle h_{0}\bullet h_{1}=}$اتحاد الأكوام ذات المجالات المنفصلة، ​​غير معرف عندما تتداخل المجالات.

إن عدم تحديد التركيب على الأكوام المتداخلة هو ما يُجسد فكرة الفصل. وهذا نموذج للمتغير البولياني للمنطق المُجمّع.

استُخدم منطق الفصل في الأصل لإثبات خصائص البرامج المتسلسلة، ولكن تم توسيعه لاحقًا ليشمل التزامن باستخدام قاعدة إثبات.

$$$

يقسم ذلك مساحة التخزين التي يتم الوصول إليها بواسطة الخيوط المتوازية. ^{[ 15 ]}

لاحقًا، استُخدمت دلالات الموارد الأكثر عمومية: إذ يعمل إصدار مجرد من منطق الفصل مع ثلاثيات هوار حيث تكون الشروط المسبقة واللاحقة عبارة عن صيغ تُفسَّر على أحادي تبديلي جزئي عشوائي بدلًا من نموذج كومة محدد. ^{[ 16 ]} ومن خلال اختيار مناسب للأحادي التبديلي، وُجد بشكلٍ مفاجئ أنه يمكن استخدام قواعد إثبات الإصدارات المجردة من منطق الفصل المتزامن للاستدلال حول العمليات المتزامنة المتداخلة، على سبيل المثال عن طريق ترميز ضمان الاعتماد والاستدلال القائم على التتبع. ^{[ 17 ] [ 18 ]}

يُعد منطق الفصل أساسًا لعدد من الأدوات المستخدمة في الاستدلال التلقائي وشبه التلقائي حول البرامج، ويُستخدم في محلل البرامج Infer المُستخدم حاليًا في فيسبوك. ^{[ 19 ]}

تم استخدام المنطق المجمع بالاقتران مع حساب الموارد والعمليات (المتزامن) SCRP ^{[ 4 ] [ 5 ] [ 6 ]} من أجل إعطاء منطق (نمطي) يصف، بمعنى هينيسي - ميلنر ، البنية التركيبية للأنظمة المتزامنة.

تشتهر SCRP بقدرتها على تفسير...${\displaystyle A*B}$من حيث كل من التركيب المتوازي للأنظمة وتركيب مواردها المرتبطة بها. يؤكد البند الدلالي لمنطق عملية SCRP، الذي يتوافق مع قاعدة منطق الفصل للتزامن، أن الصيغة${\displaystyle A*B}$هذا صحيح في حالة الموارد والعمليات${\displaystyle R}$،${\displaystyle E}$تحسباً لأي تفكك محتمل للمورد${\displaystyle R=S\bullet T}$والمعالجة ${\displaystyle E}$~${\displaystyle F\times G}$حيث تشير ~ إلى التماثل الثنائي ، بحيث${\displaystyle A}$ينطبق هذا على حالة الموارد والعمليات${\displaystyle S}$،${\displaystyle F}$و${\displaystyle B}$ينطبق هذا على حالة الموارد والعمليات${\displaystyle T}$،${\displaystyle G}$؛ إنه${\displaystyle R,E\models A}$إذا${\displaystyle S,F\models A}$و${\displaystyle T,G\models B}$.

يعتمد نظام SCRP ^{[ 4 ] [ 5 ] [ 6 ]} مباشرةً على دلالات الموارد في المنطق المجمع؛ أي على أحاديات مرتبة لعناصر الموارد. ورغم أن هذا الخيار مباشر وجذاب بديهيًا، إلا أنه يُفضي إلى مشكلة تقنية محددة: إذ لا تنطبق نظرية هينيسي-ميلنر للاكتمال إلا على أجزاء من المنطق الموجه التي تستثني الاستلزام الضربي والطرائق الضربية. وقد حُلّت هذه المشكلة من خلال بناء حساب تفاضلي-عملية الموارد على دلالات موارد تُدمج فيها عناصر الموارد باستخدام مُركِّبين، أحدهما يُقابل التركيب المتزامن والآخر يُقابل الاختيار. ^{[ 20 ]}

قام كارديلي، وكايرز، وغوردون، وآخرون بدراسة سلسلة من منطق حسابات العمليات، حيث يُفسَّر الاقتران من منظور التركيب المتوازي. وخلافًا لعمل بيم وآخرين في SCRP، فإنهم لا يُميّزون بين التركيب المتوازي للأنظمة وتركيب الموارد التي تصل إليها هذه الأنظمة.

تستند منطقاتهم إلى أمثلة من دلالات الموارد التي تُنتج نماذج من النوع البولياني للمنطق المُجمّع. ورغم أن هذه المنطقات تُنتج أمثلة من المنطق البولياني المُجمّع، إلا أنها تبدو وكأنها طُوّرت بشكل مستقل، وعلى أي حال، فهي تتضمن بنية إضافية هامة تتمثل في الوسائط والروابط. وقد اقتُرحت منطقات مشابهة لنمذجة بيانات XML .