Full affine logic is decidable

• To: linear@cs.stanford.edu
• Subject: Full affine logic is decidable
• From: sergei@artemov.mian.su (Sergei N. Artemov)
• Date: Thu, 23 Jun 94 23:03:48 +0300 (MSD)
• Approved: types@dcs.gla.ac.uk

 FULL PROPOSITIONAL AFFINE LOGIC IS DECIDABLE.

	The full propositional Linear Logic is undecidable
(Lincoln, Mitchell, Scedrov, and Shankar). The decidability 
problem for the full propositional Affine Logic LLW, i.e. 
Linear Logic with the Weakening Rule, remained open.
	Now, contrary to what might be expected, Alexey KOPYLOV
(a 3-d year undergraduate student under Artemov at Moscow University) 
proved that the FULL propositional Affine Logic LLW is DECIDABLE.
	His proof is based on
 (a) reduction of full LLW (containing all the multiplicatives,
     additives, exponentials, and constants) to sequents of specific
    'normal forms', and
 (b) a generalization of Kanovich's computational interpretation
     of Linear Logic adapted to these 'normal forms'.
	We have checked the proof, which was delivered in April of 1994.
The corresponding LaTeX paper is expected to be available soon via 
ftp, we'll immediately let you know. 

Best regards, 
Artemov & Kanovich

• Prev: new version: 2nd-order Lambda Calculus Typability Undecidable
• Next: in which models of untyped lambda calculus are terms with no whnf
• Index(es):
  • Main
  • Thread