Linear logic question

• To: types
• Subject: Linear logic question
• From: Philip Wadler <wadler@dcs.glasgow.ac.uk>
• Date: Wed, 10 Jun 92 12:15:59 EDT
• Sender: meyer@theory.lcs.mit.edu

Date: Wed, 10 Jun 92 14:56:31 BST

Define the formulae of linear logic as usual:

	atoms			X
	linear formulae		A, B ::=  X | (A -o B) | !A

Define also two subsets of formulae:

	standard formulae	A*, B* ::=  X | (A$ -o B*)
	lax standard formulae	A$     ::=  A* | !A*

Standard form only allows ! to the left of -o, while lax standard form
optionally allows ! at the beginning.  Let Gamma$ range over sequences
of lax standard formulae.

I conjecture that the following is the case:

	If Gamma$ |- A$ and A$ begins with !
	then each formula in Gamma$ begins with !

I'd be grateful if anyone could verify or disprove this conjecture,
or point me to related work.  Thanks,  -- Phil

-----------------------------------------------------------------------
Philip Wadler                                  wadler@dcs.glasgow.ac.uk
Department of Computing Science                    tel: +44 41 330 4966
University of Glasgow                              fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND

• Prev: translations of classical into LL
• Next: Advanced School on LOGIC and ARTIFICIAL INTELLIGENCE
• Index(es):
  • Main
  • Thread