Bunched logic

Bunched logic[1] is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgements Γ |- A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs[2] The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic,[3] and in systems modelling, where it provides a way to decompose the resources used by components of a system.[4][5][6]

Foundations

The deduction theorem of traditional logic relates conjunction and implication

A \wedge B \vdash C \quad \mbox{iff} \quad A \vdash B \Rightarrow C

Bunched logic has two versions of the deduction theorem at once:

A * B \vdash C \quad \mbox{iff} \quad A \vdash B {-\!\!*} C \qquad \mbox{and also} \qquad A \wedge B \vdash C \quad \mbox{iff} \quad A \vdash B \Rightarrow C

A * B and B {-\!\!*} C are forms of conjunction and implication that take resources into account (explained below). In addition to these connectives bunched logic has a formula, sometimes written I or emp, which is the unit of *. In the original version of bunched logic \wedge and \Rightarrow were the connectives from intuitionistic logic, while a boolean variant takes \wedge and \Rightarrow (and \neg ) as from traditional boolean logic. Thus, bunched logic is compatible with constructive principles, but is in no way dependent on them.

Truth Functional Semantics (Resource Semantics)

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. A*B asserts that the resource at hand can be decomposed into resources that satisfy A and B. B {-\!\!*} C says that if we compose the resource at hand with additional resource that satisfies B, then the combined resource satisfies C. \wedge and \Rightarrow have their familiar meanings.

The foundation for this reading of formulae was provided by a forcing semantics r \models A advanced by Pym, where the forcing relation means `A holds of resource r`. The semantics is analogous to Kripke's semantics of intuitionistic or modal logic, but where the elements of the model are regarded as resources which can be composed and decomposed, rather than as possible worlds that are accessible from one another. For example, the forcing semantics for the conjunction is of the form

r \models A * B \quad \mbox{iff} \quad \exists r_Ar_B.\,r_A \models A,\, r_B \models B,\,\mbox{and}\,r_A \bullet r_B \leq r

where r_A \bullet r_B is a way of combining resources and \leq is a relation of approximation.

This semantics of bunched logic draws on prior work in Relevant Logic (especiallly the operational semantics of Routley-Meyer), but differs from it my not requiring r \bullet r \leq r and by accepting the semantics of standard intuitionistic or classical versions of \wedge and \Rightarrow . The property r \bullet r \leq r is justified when thinking about relevance but denied by considerations of resource; having two copies of a resource is not the same as having one, and in some models (e.g., heap models r \bullet r might not even be defined. The standars semantics of \Rightarrow (or of negation) is often rejected by relevantists in their bid to escape the `paradoxes of material implication', which are not a problem from the perspective of modelling resources and so not rejected by bunched logic. The semantics is also related to the 'phase semantics' of linear logic, but again is differentiated by accepting the standard (even boolean) semantics of \wedge and \Rightarrow which in linear logic is rejected in a bid to be constructive. These considerations are discussed in detail in an article on Resource semantics by Pym, O'Hearn and Yang.[7]

Categorical Semantics (Doubly Closed Categories)

The double version of the deduction theorem of bunched logic has a corresponding cartegory theoretic structure. Proofs in intuitionistic logic can be interpreted in cartesian closed categories, that is, categories with finite products satisfying the (natural in A and C) adjunction correpondence relating hom sets:

Hom(A \wedge B, C) \quad \mbox{is isomorphic to} \quad Hom(A, B \Rightarrow C)

Bunched logic can be interpreted in categories possessing two such structures

a categorical model of bunched logic is a single category possessing two closed structures, one symmetric monoidal closed the other cartesian closed.

A host of categorial models can be given using Day's tensor product construction.[8] Additionally, implicational fragment of bunched logic has been given a games semantics.[9]

Algebraic Semantics

The algebraic semantics of bunched logic is a special case of its categorical semantics, but is simple to state and can be more approachable.

an algebraic model of bunched logic is poset which is a Heyting algebra and which carries an additional commutative Residuated lattice structure (for the same lattice as the Heyting algebra): that is, an ordered commuatative monoid with an associated implication satisfying A * B \leq C \quad \mbox{iff} \quad A \leq B {-\!\!*} C.

The boolean version of bunched logic has models as follows.

an algebraic model of bolean bunched logic is poset which is a Boolean algebra and which carries an additional residuated commutative monoid structure.

Proof Theory and Type Theory (Bunches)

The proof theory of bunched logic differs from usual proof calculi in having a tree-like context of hypotheses instead of a flat list-like structure. In its sequent-based proof theories, the context \Delta in an entailment judgement \Delta \vdash A is a tree whose leaves are propositions and whose internal nodes are labelled with modes of composition corresponding to the two conjunctions. The two combining operators, comma and semicolon, are used (for instance) in the introduction rules for the two implications.

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

The difference between the two composition rules comes from additional rules that apply to them.

The structural rules and other operations on bunches are often applied deep within a tree-context, and not only at the top level: it is thus in a sense a calculus of deep inference.

Corresponding to bunched logic is a type theory having two kinds of function type. Following the Curry–Howard correspondence, introduction rules for implications correspond to introduction rules for function types.

\frac{\Gamma,x:A \vdash M:B}{\Gamma \vdash \lambda x.M: A{-\!\!*} B} \qquad \qquad \frac{\Gamma;x:AA \vdash M: B}{\Gamma \vdash \alpha x.M:A{\Rightarrow} B}

Here, there are two distinct binders, $\lambda$ and $\alpha$, one for each kind of function type.

The proof theory of bunched logic has an historical dept to the use of bunches in Relevance logic.[10] But the bunched structure can in a sense be derived from the categorical and algebraic semantics: to formulate an introduction rule for {-\!\!*} we should mimick * on the left in sequents, and to introduce \Rightarrow we should mimick \wedge . This consideration leads to the use of two combining operators.

Brotherston has done further significant work on a unified proof theory for bunched logic and variants,[11] employing Belnap's notion of display logic.[12]

Galmiche, Méry, and Pym have provided a comprehensive treatment of bunched logic, including completeness and other meta-theory, based on labelled tableaux.[13]

Decision Problems

TODO

Modal Extensions

TODO

Applications

Interference Control

In perhaps the first use of substructural type theory to control resources, John C. Reynolds showed how to use an affine type theory to control aliasing and other forms of interference in Algol-like programming languages.[14] O'Hearn used bunched type theory to extend Reynolds system by allowing interference and non-interference to be more flexibly mixed .[2] This resolved open problems concerning recursion and jumps in Reynolds's system.

Separation Logic

Separation logic is an extension of Hoare logic which facilitates reasoning about mutable data structures that use pointers. Following Hoare logic the formulae of separation logic are of the form \{Pre\} program \{Post\}, but the preconditions and postconditions are formulae interpreted in a model of bunched logic. The original version of the logic was based on models as follows:

It is the undefinedness of the composition on overlapping heaps that models the separation idea. This is a model of the boolean variant of bunched logic.

Separation logic was used originally to prove sequential programs, but then was extended to concurrency using a proof rule

\frac{\{P_1\} C_1 \{Q_1\} \quad \{P_2\} C_2 \{Q_2\}}{\{P_1 * P_1\} C_1 \parallel C_2 \{Q_1 * Q_2\}}

that divides the storage accessed by parallel threads.[15]

Later, the greater generality of the resource semantics was utilized: an abstract version of separation logic works for Hoare triples where the preconditions and oostconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model.[16] By suitable choice of commutative monoid, it was surprisingly found that the proofs rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding rely-guarnatee and trace-based reasoning.[17][18]

Separation logic is the basis of a number of tools for automatic and semi-automatic reasoning about programs , and is used in the Infer program analyzer currently deployed at Facebook.[19]

Resources and Processes

Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP[4][5][6] in order to give a (modal) logic which characterizes, in the sense of Hennessey-Milner, the compositional structure of concurrent systems.

SCRP is notable for interpreting A * B in terms of both parallel composition of systems and composition of their associated resources. The semantic clause of SCRP's process logic that corresponds to separation logic's rule for concurrency asserts that a formula A * B is true in resource-process state R , E just in case there are decompositions of the resource R = S \bullet T and process E ~ F \times G, where ~ denotes bisimulation, such that A is true in the resource-process state S , F and B is true in the resource-process state T , G ; that is R , E \models A iff S , F \models A and T , G \models B .

TODO

The system SCRP [4][5][6] is based directly on bunched logic's resource semantics; that is, on ordered monoids of resource elements. While direct and intuitively appealing, this choice leads to a specific technical problem: the Hennessy-Milner completeness theorem holds only for fragments of the modal logic that exclude the multiplicative implication and multiplicative modalities. This problem is solved by basing resource-process calculus on a resource semantics in which resource elements are combined using two combinators, one corresponding to concurrent composition and one corresponding to choice.[20]

Systems Modelling

TODO

Spatial Logics

Cardelli, Caires, Gordon and others have investigated a series of logics of process calculi, where a conjunction is interpreted in terms of parallel composition. [References, to add] Unlike the work of Pym et al in SCRP, they do not distinguish between parallel composition of systems and composition of resources accessed by the systems. Their logics are based on instances of the resource semantics which give rise to models of the boolean variant of bunched logic. Although these logics give rise to instances of boolean bunched logic, they appear to have been arrived at independently, and in any case have significant additional structure in the way of modalities and binders. Related logics have been proposed as well for modelling XML data.

See also

References

  1. ↑ O'Hearn, Peter; Pym, David (1999). "The Logic of Bunched Implications" (PDF). Bulletin of Symbolic Logic 5 (2): 215–244. doi:10.2307/421090.
  2. 1 2 O'Hearn, Peter (2003). "On Bunched Typing" (PDF). Journal of Functional Programming 13 (4): 747–796. doi:10.1017/S0956796802004495.
  3. ↑ Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an assertion language for mutable data structures" (PDF). POPL 28th: 14–26. doi:10.1145/373243.375719.
  4. 1 2 3 Pym, David; Tofts, Chris (2006). "A Calculus and logic of resources and processes" (PDF). Formal Aspects of Computing 8 (4): 495–517.
  5. 1 2 3 Collinson, Matthew; Pym, David (2009). "Algebra and Logic for Resource-based Systems Modelling". Mathematical Structures in Computer Science 19: 959–1027. doi:10.1017/S0960129509990077.
  6. 1 2 3 Collinson, Matthew; Monahan, Brian; Pym, David (2012). A Discipline of Mathematical Systems Modelling. London: College Publications. ISBN 978-1-904987-50-5.
  7. ↑ Pym, David; O'Hearn, Peter; Yang, Hongseok (2004). "Possible worlds and resources: The semantics of BI". Theoretical Computer Science 315 (1): 257–305. doi:10.1016/j.tcs.2003.11.020.
  8. ↑ Day, Brian (1970). "On closed categories of functors" (PDF). Reports of the Midwest Category Seminar IV, Springer Lecture Notes in Mathematics 137: 1–38.
  9. ↑ McCusker, Guy; Pym, David (2007). "A Games Model of Bunched Implications" (PDF). Computer Science Logic, Springer Lecture Notes in Computer Science 4646.
  10. ↑ Read, Stephen (1989). Relevant Logic: A Philosophical Examination of Inference. Wiley-Blackwell.
  11. ↑ Brotherston, James (2012). "Bunched logics displayed" (PDF). Studia Logica 100 (6): 1223–1254.
  12. ↑ Belnap, Nuel (1982). Journal of Philosophical Logic 11 (4): 375–417. Missing or empty |title= (help)
  13. ↑ Galmiche, Didier; Méry, Daniel; Pym, David (2005). "The Semantics of BI and Resource Tableaux". Mathematical Structures in Computer Science 15: 1033–1088.
  14. ↑ Reynolds, John. "Syntactic Control of Interference". Fifth Annual ACM Symposium on Principles of Programming Languages: 39–46. doi:10.1145/512760.512766.
  15. ↑ O'Hearn, Peter (2007). "Resources, Concurrency and Local Reasoning" (PDF). Theoretical Computer Science 375 (1-3): 271–307. doi:10.1016/j.tcs.2006.12.035.
  16. ↑ Calcagno, Cristiano; O'Hearn, Peter; Yang, Hongseok (2007). "Local Action and Abstract Separation Logic" (PDF). 22nd Annual IEEE Symposium on Logic in Computer Science. doi:10.1109/LICS.2007.30.
  17. ↑ Dinsdale-Young, Thomas; Birkedal, Lars; Gardner, Philippa; Parkinson, Matthew; Yang, Hongseok (2013). "Views: Compositional Reasoning for Concurrent Programs" (PDF). Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. doi:10.1145/2480359.2429104.
  18. ↑ Sergey, Ilya; Nanevski, Aleksandar; Banerjee, Anindya (2015). "Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity" (PDF). 24th European Symposium on Programming.
  19. ↑ Calcagno, Cristiano; Distefano, Dino; O'Hearn, Peter. "Open-sourcing Facebook Infer: Identify bugs before you ship".
  20. ↑ Anderson, Gabrielle; Pym, David (2015). "A Calculus and Logic of Bunched Resources and Processes". Theoretical Computer Science. doi:10.1016/j.tcs.2015.11.035.
This article is issued from Wikipedia - version of the Saturday, January 02, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.