Bunched logic

Bunched logic

Bunched logic is a variety of substructural logic that, like linear logic, has classes of multiplicative and additive operators, but differs from usual proof calculi in having a tree-like context of hypotheses instead of a flat list-like structure; it is thus a calculus of deep inference. Sub-trees of the context tree are referred to as "bunches"; hence the name. The internal nodes in the context tree are labelled with the mode of composition — multiplicative or additive, with the following characteristics:

*Multiplicative composition denies the structural rules of weakening and contraction.
*Additive composition admits weakening and contraction of entire bunches.

Correpsonding to each of these bunch combinators is conjunction, and each conjunction has an associated implication; hence the name, the logic of bunched implications.

The semantics of bunched logic can be given in terms of Kripke models in which the set of worlds carries not only a preorder but also a monoidal product. Categorical models of bunched logic are given by doubly-closed categories, which are both cartesian closed and symmetric monoidal closed. Day's tensor product construction can be used to generate categorical models corresponding to the Kripke semantics.

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

Bunched logic extended with a semantic model of locations and store is known as separation logic. It has been used to define the logic of pointer-analysis in languages like ALGOL or C.

The implicational fragment of bunched logic has been given a games semantics.

ee also

* Linear logic

References

* (*)Matthew Collinson, David Pym, and Chris Tofts. "Errata for Formal Aspects of Computing (2006) 18:495-517 and their consequences".
* Peter O'Hearn and David Pym. "The Logic of Bunched Implications". Bulletin of Symbolic Logic 5(2)(1999) 215-244.
* O'Hearn P, [http://www.dcs.qmw.ac.uk/~ohearn/papers/BunchedTyping.ps On bunched typing] , "Journal of Functional Programming", 13(4), 747—796, 2003. ( [http://www.dcs.qmw.ac.uk/~ohearn/papers/BunchedTyping.pdf PDF] )
* Guy McCusker and David Pym. "A Games Model of Bunched Implications". Proc. CSL 2007, LNCS.
*Peter O'Hearn. "Resources, Concurrency, and Local Reasoning". Theoretical Computer Science 357(1-3) 271-307, 2007.
*David Pym, Peter O'Hearn, and Hongseok Yang. "Possible Worlds and Resources: The Semantics of BI". Theoretical Computer Science 315 (2004) 257-305.
*David Pym and Chris Tofts. "A calculus and logic of resources and processes". Formal Aspects of Computing (2006) 18:495-517. Errata in (*).
*David Pym and Chris Tofts. "Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic". In: Cardelli, L. Fiore M, Winskel, G (eds) Electronic Notes in Theoretical Computer Science (Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin) 107, 545-587. Errata in (*).
*David Pym. "The Semantics and Proof Theory of the Logic of Bunched Implications". Kluwer Academic Publishers, 2002. Errata and Remarks at: www.cs.bath.ac.uk/~pym/BI-monograph-errata.pdf.


Wikimedia Foundation. 2010.

Игры ⚽ Нужно решить контрольную?

Look at other dictionaries:

  • Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… …   Wikipedia

  • Outline of logic — The following outline is provided as an overview of and topical guide to logic: Logic – formal science of using reason, considered a branch of both philosophy and mathematics. Logic investigates and classifies the structure of statements and… …   Wikipedia

  • List of mathematics articles (B) — NOTOC B B spline B* algebra B* search algorithm B,C,K,W system BA model Ba space Babuška Lax Milgram theorem Baby Monster group Baby step giant step Babylonian mathematics Babylonian numerals Bach tensor Bach s algorithm Bachmann–Howard ordinal… …   Wikipedia

  • LF (logical framework) — In type theory, the LF logical framework provides a means to define (or present) logics. It is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus. Syntax is treated in a style similar to, but… …   Wikipedia

  • Proof calculus — In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules. The specific inference rules of a member of such a family characterize the theory of a… …   Wikipedia

  • Europe, history of — Introduction       history of European peoples and cultures from prehistoric times to the present. Europe is a more ambiguous term than most geographic expressions. Its etymology is doubtful, as is the physical extent of the area it designates.… …   Universalium

  • Monotonicity of entailment — is a property of many logical systems that states that the hypotheses of any derived fact may be freely extended with additional assumptions. In sequent calculi this property can be captured by an inference rule called weakening, or sometimes… …   Wikipedia

  • Mathematics of Sudoku — The class of Sudoku puzzles consists of a partially completed row column grid of cells partitioned into N regions each of size N cells, to be filled in using a prescribed set of N distinct symbols (typically the numbers {1, ..., N}), so that each …   Wikipedia

  • literature — /lit euhr euh cheuhr, choor , li treuh /, n. 1. writings in which expression and form, in connection with ideas of permanent and universal interest, are characteristic or essential features, as poetry, novels, history, biography, and essays. 2.… …   Universalium

  • Computer cooling — An OEM AMD heatsink mounted onto a motherboard. Computer cooling is required to remove the waste heat produced by computer components, to keep components within their safe operating temperature limits. Various cooling methods help to improve… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”