Polarized linear logic - Revision history

Olivier Laurent: link to generalized structural rules

2011-10-05T08:28:03Z

link to generalized structural rules

Olivier Laurent: /* Polarization */ link to positive formula

2011-10-05T08:16:40Z

‎Polarization: link to positive formula

Pierre-Marie Pédrot: cr

2011-10-04T22:47:47Z

New page

'''Polarized linear logic''' (LLP) is a logic close to plain linear logic in which structural rules, usually restricted to <math>\wn</math>-formulas, have been extended to the whole class of so called ''negative'' formulae.

== Polarization ==

LLP relies on the notion of ''polarization'', that is, it discriminates between two types of formulae, ''negative'' (noted <math>M, N...</math>) vs. ''positive'' (<math>P, Q...</math>). They are mutually defined as follows:

<math>M, N ::= X \mid M \parr N \mid \bot \mid M \with N \mid \top \mid \wn{P}</math>

<math>P, Q ::= X\orth \mid P \otimes Q \mid 1 \mid P \oplus Q \mid 0 \mid \oc{N}</math>

The dual operation <math>(-)\orth</math> extended to propositions exchanges the roles of connectors and reverses the polarity of formulae.

== Deduction rules ==

They are several design choices for the structure of sequents. In particular, LLP proofs are ''focalized'', i.e. they contain at most one positive formula. We choose to represent this explicitly using sequents of the form <math>\vdash\Gamma\mid\Delta</math>, where <math>\Gamma</math> is a multiset of negative formulae, and <math>\Delta</math> is a ''stoup'' that contains at most one positive formula (though it may be empty).

<math>
\LabelRule{\rulename{ax}}
\NulRule{\vdash P\orth \mid P}
\DisplayProof
\qquad
\AxRule{\vdash \Gamma_1, N \mid \Delta}
\AxRule{\vdash \Gamma_2 \mid N\orth}
\LabelRule{\rulename{cut}}
\BinRule{\vdash\Gamma_1, \Gamma_2 \mid \Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma, N\mid\cdot}
\LabelRule{p}
\UnaRule{\vdash\Gamma\mid \oc{N}}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid P}
\LabelRule{d}
\UnaRule{\vdash\Gamma,\wn{P}\mid \cdot}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma,N,N\mid \Delta}
\LabelRule{c}
\UnaRule{\vdash\Gamma, N\mid\Delta}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid \Delta}
\LabelRule{w}
\UnaRule{\vdash\Gamma,N\mid\Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma_1\mid P}
\AxRule{\vdash\Gamma_2\mid Q}
\LabelRule{\tens}
\BinRule{\vdash\Gamma_1,\Gamma_2\mid P\otimes Q}
\DisplayProof
\qquad
\LabelRule{\one}
\NulRule{\vdash\cdot\mid\one}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma, M, N\mid \Delta}
\LabelRule{\parr}
\UnaRule{\vdash\Gamma, M\parr N\mid \Delta}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid \Delta}
\LabelRule{\bot}
\UnaRule{\vdash\Gamma, \bot\mid\Delta}
\DisplayProof
</math>

<br/>

<math>
\AxRule{\vdash\Gamma\mid P}
\LabelRule{\plus_1}
\UnaRule{\vdash\Gamma\mid P\plus Q}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma\mid Q}
\LabelRule{\plus_2}
\UnaRule{\vdash\Gamma\mid P\plus Q}
\DisplayProof
\qquad
\AxRule{\vdash\Gamma,M\mid \Delta}
\AxRule{\vdash\Gamma,N\mid \Delta}
\LabelRule{\with}
\BinRule{\vdash\Gamma,M\with N\mid \Delta}
\DisplayProof
\qquad
\LabelRule{\top}
\NulRule{\vdash\Gamma,\top\mid \Delta}
\DisplayProof
</math>

← Older revision		Revision as of 08:28, 5 October 2011
Line 1:		Line 1:
−	'''Polarized linear logic''' (LLP) is a logic close to plain linear logic in which structural rules, usually restricted to <math>\wn</math>-formulas, have been extended to the whole class of so called ''negative'' formulae.	+	'''Polarized linear logic''' (LLP) is a logic close to plain linear logic in which structural rules, usually restricted to <math>\wn</math>-formulas, have been [[Positive_formula#Generalized_structural_rules\|extended]] to the whole class of so called ''negative'' formulae.

	== Polarization ==		== Polarization ==

@@ Line 3: / Line 3: @@
 == Polarization ==
-LLP relies on the notion of ''polarization'', that is, it discriminates between two types of formulae, ''negative'' (noted <math>M, N...</math>) vs. ''positive'' (<math>P, Q...</math>). They are mutually defined as follows:
+LLP relies on the notion of ''polarization'', that is, it discriminates between two types of formulae, ''negative'' (noted <math>M, N...</math>) vs. ''[[Positive formula|positive]]'' (<math>P, Q...</math>). They are mutually defined as follows:
 <math>M, N ::= X \mid M \parr N \mid \bot \mid M \with N \mid \top \mid \wn{P}</math>