The Consistency and Complexity of Multiplicative Additive System Virtual

Published in Volume XXV, Issue 2, 2015, pages 245-316, doi: 10.7561/SACS.2015.2.245

Authors: R. Horne

Abstract

This paper investigates the proof theory of multiplicative additive system virtual (MAV). MAV combines two established proof calculi: multiplicative additive linear logic (MALL) and basic system virtual (BV). Due to the presence of the self-dual non-commutative operator from BV, the calculus MAV is defined in the calculus of structures – a generalisation of the sequent calculus where inference rules can be applied in any context. A generalised cut elimination result is proven for MAV, thereby establishing the consistency of linear implication defined in the calculus. The cut elimination proof involves a termination measure based on multisets of multisets of natural numbers to handle subtle interactions between operators of BV and MAV. Proof search in MAV is proven to be a PSPACE-complete decision problem. The study of this calculus is motivated by observations about applications in computer science to the verication of protocols and to querying.

Full Text (PDF)

References

[1] Samson Abramsky. Computational interpretations of linear logic. Theoretical computer science, 111(1):3–57, 1993. doi:10.1016/ 0304-3975(93)90181-R.

[2] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. The Journal of Symbolic Logic, 59(2):543– 574, 1994. doi:10.2307/2275407.

[3] David Baelde. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic (TOCL), 13(1):Article No. 2, 2012. doi:10.1145/2071368.2071370.

[4] Richard Blute, Alessio Guglielmi, Ivan Ivanov, Prakash Panangaden, and Lutz Straßburger. A logical basis for quantum evolution and entanglement. In Categories and Types in Logic, Language, and Physics, volume 8222 of LNCS, pages 90–107. Springer, 2014. doi:10.1007/ 978-3-642-54789-8_6.

[5] Kai Brünnler. Atomic cut elimination for classical logic. In Matthias Baaz and JohannA. Makowsky, editors, Computer Science Logic, volume 2803 of Lecture Notes in Computer Science, pages 86–97. Springer Berlin Heidelberg, 2003. doi:10.1007/978-3-540-45220-1_9.

[6] Paola Bruscoli. A purely logical account of sequentiality in proof search. In PeterJ. Stuckey, editor, Logic Programming, volume 2401 of Lecture Notes in Computer Science, pages 302–316. Springer Berlin Heidelberg, 2002. doi:10.1007/3-540-45619-8_21.

[7] Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic (TOCL), 10(2):Article No. 14, 2009. doi:10.1145/1462179.1462186.

[8] Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28:114–133, 1981. doi:10.1145/322234. 322243.

[9] Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The focused calculus of structures. In Marc Bezem, editor, Computer Science Logic (CSL’11) – 25th International Workshop/20th Annual Conference of the EACSL, volume 12 of Leibniz International Proceedings in Informatics (LIPIcs), pages 159–173, 2011. doi:10.4230/LIPIcs.CSL.2011.159.

[10] Gabriel Ciobanu and Ross Horne. A provenance tracking model for data updates. In Natallia Kokash and António Ravara, editors, Proceedings of 11th International Workshop on Foundations of Coordination Languages and Self Adaptation (FOCLASA’12), volume 91 of Electronic Proceedings in Theoretical Computer Science, pages 31–44, 2012. doi:10.4204/ EPTCS.91.3.

[11] Gabriel Ciobanu and Ross Horne. Behavioural analysis of sessions using the calculus of structures. In Proceedings of 10th International Ershov Informatics Conference, PSI 2015, 25-27 August, Kazan, Russia, 2015. (to appear).

[12] J Robin B Cockett and Robert AG Seely. Weakly distributive categories. Journal of Pure and Applied Algebra, 114(2):133–173, 1997. doi:10. 1016/0022-4049(95)00160-3.

[13] Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979. doi:10.1145/359138.359142.

[14] Alexandre Frey. Satisfying subtype inequalities in polynomial space. Theoretical Computer Science, 277(1-2):105–117, 2002. doi:10.1016/ S0304-3975(00)00314-5.

[15] Simon Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2):191–225, 2005. doi:10.1007/ s00236-005-0177-z.

[16] Gerhard Gentzen. Untersuchungen über das logische Schließen. I. Mathematische zeitschrift, 39(1):176–210, 1935.

[17] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1– 112, 1987. doi:10.1016/0304-3975(87)90045-4.

[18] Jean-Yves Girard. Linear logic: its syntax and semantics. London Mathematical Society Lecture Note Series, pages 1–42, 1995.

[19] Jay L. Gischer. The equational theory of pomsets. Theoretical Computer Science, 61(2-3):199–224, 1988. doi:10.1016/0304-3975(88)90124-7.

[20] Alessio Guglielmi. A system of interaction and structure. ACM Transactions on Compututational Logic, 8(1):Article No. 1, 2007. doi:10.1145/1182613.1182614.

[21] Alessio Guglielmi and Tom Gundersen. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4(1):PAPER 9, 2008. doi:10.2168/LMCS-4(1:9)2008.

[22] Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: The exponentials and splitting. Mathematical Structures in Computer Science, 21(03):563–584, 2011 doi:10.1017/S096012951100003X.

[23] Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene algebra and its foundations. Journal of Logic and Algebraic Programming, 80(6):266–296, 2011. doi:10.1016/j.jlap.2011.04.005.

[24] Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR’93, volume 715 of Lecture Notes in Computer Science, pages 509–523. Springer Berlin Heidelberg, 1993. doi:10.1007/3-540-57208-2_ 35.

[25] Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida. Scribbling interactions with a formal foundation. In Raja Natarajan and Adegboyega Ojo, editors, Distributed Computing and Internet Technology, volume 6536 of Lecture Notes in Computer Science, pages 55–75. Springer Berlin Heidelberg, 2011. doi:10.1007/ 978-3-642-19056-8_4.

[26] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. ACM SIGPLAN Notices, 43(1):273–284, 2008. doi:10.1145/1328897.1328472.

[27] Haruo Hosoya, Jérôme Vouillon, and Benjamin C Pierce. Regular expression types for XML. ACM Transactions on Programming Languages and Systems (TOPLAS), 27(1):46–90, 2005. doi:10.1145/1053468.1053470.

[28] Raymond Hu, Rumyana Neykova, Nobuko Yoshida, Romain Demangeon, and Kohei Honda. Practical interruptible conversations. In Axel Legay and Saddek Bensalem, editors, Runtime Verification, volume 8174 of Lecture Notes in Computer Science, pages 130–148. Springer Berlin Heidelberg, 2013. doi:10.1007/978-3-642-40787-1_8.

[29] Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-based distributed programming in Java. In Jan Vitek, editor, ECOOP 2008 Object-Oriented Programming, volume 5142 of Lecture Notes in Computer Science, pages 516–541. Springer Berlin Heidelberg, 2008. doi:10.1007/978-3-540-70592-5_22.

[30] Ozan Kahramanogullari. System BV is NP-complete. Annals of Pure and Applied Logic, 152(1-3):107–121, 2008. doi:10.1016/j.apal.2007.11.005.

[31] Grigoris Karvounarakis, Zachary G. Ives, and Val Tannen. Querying data provenance. In Proceedings of the 2010 ACM SIGMOD International Conference on Management of Data, pages 951–962. ACM, 2010. doi:10.1145/1807167.1807269.

[32] Yves Lafont and Andre Scedrov. The undecidability of second order multiplicative linear logic. Information and Computation, 125(1):46–51, 1996. doi:10.2307/2275674.

[33] Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56(1-3):239–311, 1992. doi:10.1016/0168-0072(92) 90075-B.

[34] Patrick D Lincoln, J Mitchell, and Andre Scedrov. Stochastic interaction and linear logic. London Mathematical Society Lecture Note Series, pages 147–166, 1995. doi:10.1017/CBO9780511629150.008.

[35] Jan Łukasiewicz. Aristotle’s syllogistic from the standpoint of modern formal logic. Oxford Clarendon Press, 1951.

[36] Roger C Lyndon. An interpolation theorem in the predicate calculus. Pacific Journal of Mathematics, 9(1):129–142, 1959. URL: http://projecteuclid.org/euclid.pjm/1103039458.

[37] Nicholas Ng, Nobuko Yoshida, and Kohei Honda. Multiparty session C: Safe parallel programming with message optimisation. In CarloA. Furia and Sebastian Nanz, editors, Objects, Models, Components, Patterns, volume 7304 of Lecture Notes in Computer Science, pages 202–218. Springer Berlin Heidelberg, 2012. doi:10.1007/978-3-642-30561-0_ 15.

[38] Frank Pfenning. Structural cut elimination in linear logic. Technical Report CMU-CS-94-222, School of Computer Science, Carnegie Mellon University, 1994. URL: http://reports-archive.adm.cs.cmu.edu/anon/1994/CMU-CS-94-222.ps.

[39] Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In Philippe de Groote and J. Roger Hindley, editors, Typed Lambda Calculi and Applications, volume 1210 of Lecture Notes in Computer Science, pages 300–318. Springer Berlin Heidelberg, 1997. doi:10.1007/3-540-62688-3_43.

[40] Luca Roversi. Linear lambda calculus and deep inference. In Luke Ong, editor, Typed Lambda Calculi and Applications, volume 6690 of Lecture Notes in Computer Science, pages 184–197. Springer, 2011. doi:10.1007/978-3-642-21691-6_16.

[41] Paul Ruet. Non-commutative logic II: sequent calculus and phase semantics. Mathematical Structures in Computer Science, 10(02):277– 312, 2000.

[42] Adi Shamir. IP = PSPACE. Journal of the ACM, 39(4):869–877, 1992. doi:10.1145/146585.146609.

[43] Richard Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9(1):67–72, 1979. doi:10. 1016/0304-3975(79)90006-9.

[44] Lutz Straßburger. A local system for linear logic. In Matthias Baaz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 2514 of Lecture Notes in Computer Science, pages 388–402. Springer Berlin Heidelberg, 2002. doi:10.1007/3-540-36078-6_26.

[45] Lutz Straßburger. Linear logic and noncommutativity in the calculus of structures. PhD thesis, TU Dresden, 2003.

[46] Lutz Straßburger. System NEL is undecidable. Electronic Notes in Theoretical Computer Science, 84:166–177, 2003. doi:10.1016/ S1571-0661(04)80853-3.

[47] Lutz Straßburger. From deep inference to proof nets. In Structures and Deduction, 16-17 July, Lisbon, number FI05-08-Juli, pages 2–18. TU Dresden, 2005. ISSN 1430-211X. URL: http://www.ki.inf.tu-dresden.de/~paola/SD05/SD05-Proc.pdf.

[48] Lutz Straßburger. Some observations on the proof theory of second order propositional multiplicative linear logic. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, volume 5608 of Lecture Notes in Computer Science, pages 309–324. Springer Berlin Heidelberg, 2009. doi:10.1007/978-3-642-02273-9_23.

[49] Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: The exponentials and decomposition. ACM Transactions on Computational Logic, 12(4):23, 2011. URL: http://doi.acm.org/ 10.1145/1970398.1970399.

[50] Alwen Tiu. A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science, 2(2):Paper 4, 2006. doi:10.2168/LMCS-2(2:4)2006.

[51] Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors, Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pages 137–146, 1982. doi:10.1145/800070.802186.

[52] David N. Yetter. Quantales and (noncommutative) linear logic. Journal of Symbolic Logic, 55(1):41–64, 1990. doi:10.2307/2274953 .

Bibtex

@article{sacscuza:horne2015tcacomasv,
  title={The Consistency and Complexity of Multiplicative Additive System Virtual},
  author={R. Horne},
  journal={Scientific Annals of Computer Science},
  volume={25},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2015},
  pages={245--316},
  doi={10.7561/SACS.2015.2.245},
  publisher={``A.I. Cuza'' University Press}
}