Noncommutative logic
Encyclopedia
Noncommutative logic is an extension of linear logic
which combines the commutative connectives of linear logic with the noncommutative multiplicative connectives of the Lambek
calculus (see External links below). Its sequent calculus
relies on the structure of order varieties (a family of cyclic orders which may be viewed as a species of structure
), and the correctness criterion for its proof net
s is given in terms of partial permutations. It also has a denotational semantics
in which formulas are interpreted by modules over some specific Hopf algebra
s.
is inadmissible. The remainder of this article is devoted to a presentation of this acceptance of the term.
The oldest noncommutative logic is the Lambek calculus, which gave rise to the class of logics known as categorial grammars. Since the publication of Jean-Yves Girard
's linear logic
there have been several new noncommutative logics proposed, namely the cyclic linear logic of David Yetter, the pomset logic of Christian Retore, and the noncommutative logics BV and NEL studied in the calculus of structures
.
Noncommutative logic is sometimes called ordered logic, since it is possible with most proposed noncommutative logics to impose a total or partial order on the formulae in sequents. However this is not fully general since some noncommutative logics do not support such an order, such as Yetter's cyclic linear logic. Note also that while most noncommutative logics do not allow weakening or contraction together with noncommutativity, this restriction is not necessary.
proposed the first noncommutative logic in his 1958 paper Mathematics of Sentence Structure to model the combinatory possibilities of the syntax of natural languages. His calculus has thus become one of the fundamental formalisms of computational linguistics
.
; instead the sense of the calculus was established through a denotational semantics.
to accommodate the calculus. The principal novelty of the calculus of structures was its pervasive use of deep inference
, which it was argued is necessary for calculi combining commutative and noncommutative operators; this explanation concurs with the difficulty of designing sequent systems for pomset logic that have cut-elimination.
Lutz Strassburger devised a related system, NEL, also in the calculus of structures in which linear logic with the mix rule appears as a subsystem.
along the lines of Joyal's combinatorial species
, allowing the treatment of more drastically nonstandard logics than those described above, where, for example, the ',' of the sequent calculus is not associative.
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
which combines the commutative connectives of linear logic with the noncommutative multiplicative connectives of the Lambek
Joachim Lambek
Joachim Lambek is Peter Redpath Emeritus Professor of Pure Mathematics at McGill University, where he earned his Ph.D. degree in 1950 with Hans Julius Zassenhaus as advisor. He is called Jim by his friends.- Scholarly work :...
calculus (see External links below). Its sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
relies on the structure of order varieties (a family of cyclic orders which may be viewed as a species of structure
Combinatorial species
In combinatorial mathematics, the theory of combinatorial species is an abstract, systematic method for analysing discrete structures in terms of generating functions. Examples of discrete structures are graphs, permutations, trees, and so on; each of these has an associated generating function...
), and the correctness criterion for its proof net
Proof net
In proof theory, proof nets are a geometrical method of representing proofs thateliminates two forms of bureaucracy that differentiates proofs: irrelevant syntactical features of regular proof calculi such as the natural deduction calculus and the sequent calculus, and the order of rules applied...
s is given in terms of partial permutations. It also has a denotational semantics
Denotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
in which formulas are interpreted by modules over some specific Hopf algebra
Hopf algebra
In mathematics, a Hopf algebra, named after Heinz Hopf, is a structure that is simultaneously an algebra and a coalgebra, with these structures' compatibility making it a bialgebra, and that moreover is equipped with an antiautomorphism satisfying a certain property.Hopf algebras occur naturally...
s.
Noncommutativity in logic
By extension, the term noncommutative logic is also used by a number of authors to refer to a family of substructural logics in which the exchange ruleStructural rule
In proof theory, a structural rule is an inference rule that does not refer to any logical connective, but instead operates on the judgements or sequents directly. Structural rules often mimic intended meta-theoretic properties of the logic...
is inadmissible. The remainder of this article is devoted to a presentation of this acceptance of the term.
The oldest noncommutative logic is the Lambek calculus, which gave rise to the class of logics known as categorial grammars. Since the publication of Jean-Yves Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
's linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
there have been several new noncommutative logics proposed, namely the cyclic linear logic of David Yetter, the pomset logic of Christian Retore, and the noncommutative logics BV and NEL studied in the calculus of structures
Calculus of structures
The calculus of structures is a proof calculus with deep inference for studying the structural proof theory of noncommutative logic. The calculus has since been applied to study linear logic, classical logic, modal logic, and process calculi, and many benefits are claimed to follow in these...
.
Noncommutative logic is sometimes called ordered logic, since it is possible with most proposed noncommutative logics to impose a total or partial order on the formulae in sequents. However this is not fully general since some noncommutative logics do not support such an order, such as Yetter's cyclic linear logic. Note also that while most noncommutative logics do not allow weakening or contraction together with noncommutativity, this restriction is not necessary.
The Lambek calculus
Joachim LambekJoachim Lambek
Joachim Lambek is Peter Redpath Emeritus Professor of Pure Mathematics at McGill University, where he earned his Ph.D. degree in 1950 with Hans Julius Zassenhaus as advisor. He is called Jim by his friends.- Scholarly work :...
proposed the first noncommutative logic in his 1958 paper Mathematics of Sentence Structure to model the combinatory possibilities of the syntax of natural languages. His calculus has thus become one of the fundamental formalisms of computational linguistics
Computational linguistics
Computational linguistics is an interdisciplinary field dealing with the statistical or rule-based modeling of natural language from a computational perspective....
.
Cyclic linear logic
David Yetter proposed a weaker structural rule in place of the exchange rule of linear logic, yielding cyclic linear logic. Sequents of cyclic linear logic form a ring, and so are invariant under rotation, where multipremise rules glue their rings together at the formulae described in the rules. The calculus supports three structural modalities, a self-dual modality allowing exchange, but still linear, and the usual exponentials (? and !) of linear logic, allowing nonlinear structural rules to be used together with exchange.Pomset logic
Pomset logic was proposed by Christian Retore in a semantic formalism with two dual sequential operators existing together with the usual tensor product and par operators of linear logic, the first logic proposed to have both commutative and noncommutative operators. A sequent calculus for the logic was given, but it lacked a cut-elimination theoremCut-elimination theorem
The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively...
; instead the sense of the calculus was established through a denotational semantics.
BV and NEL
Alessio Guglielmi proposed a variation of Retore's calculus, BV, in which the two noncommutative operations are collapsed onto a single, self-dual, operator, and proposed a novel proof calculus, the calculus of structuresCalculus of structures
The calculus of structures is a proof calculus with deep inference for studying the structural proof theory of noncommutative logic. The calculus has since been applied to study linear logic, classical logic, modal logic, and process calculi, and many benefits are claimed to follow in these...
to accommodate the calculus. The principal novelty of the calculus of structures was its pervasive use of deep inference
Deep inference
Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity...
, which it was argued is necessary for calculi combining commutative and noncommutative operators; this explanation concurs with the difficulty of designing sequent systems for pomset logic that have cut-elimination.
Lutz Strassburger devised a related system, NEL, also in the calculus of structures in which linear logic with the mix rule appears as a subsystem.
Structads
Structads are an approach to the semantics of logic that are based upon generalising the notion of sequentSequent
In proof theory, a sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction. In the sequent calculus, the name sequent is used for the construct which can be regarded as a specific kind of judgment, characteristic to this deduction system.-...
along the lines of Joyal's combinatorial species
Combinatorial species
In combinatorial mathematics, the theory of combinatorial species is an abstract, systematic method for analysing discrete structures in terms of generating functions. Examples of discrete structures are graphs, permutations, trees, and so on; each of these has an associated generating function...
, allowing the treatment of more drastically nonstandard logics than those described above, where, for example, the ',' of the sequent calculus is not associative.
External links
- Non-commutative logic I: the multiplicative fragment by V. Michele Abrusci and Paul Ruet, Annals of Pure and Applied Logic 101(1), 2000.
- Logical aspects of computational linguistics (PS) by Patrick Blackburn, Marc Dymetman, Alain Lecomte, Aarne Ranta, Christian Retore and Eric Villemonte de la Clergerie.
- Papers on Commutative/Non-commutative Linear Logic in the calculus of structures: a research homepage from which the papers proposing BV and NEL are available.