Local Validity for Circular Proofs in Linear Logic with Fixed Points

Authors Rémi Nollet, Alexis Saurin, Christine Tasson



PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.35.pdf
  • Filesize: 0.63 MB
  • 23 pages

Document Identifiers

Author Details

Rémi Nollet
  • IRIF, Université Paris Diderot and CNRS, Paris, France
Alexis Saurin
  • IRIF, CNRS, Université Paris Diderot and INRIA π r^2, Paris, France
Christine Tasson
  • IRIF, Université Paris Diderot and CNRS, Paris, France

Cite AsGet BibTex

Rémi Nollet, Alexis Saurin, and Christine Tasson. Local Validity for Circular Proofs in Linear Logic with Fixed Points. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 35:1-35:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.35

Abstract

Circular (ie. non-wellfounded but regular) proofs have received increasing interest in recent years with the simultaneous development of their applications and meta-theory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc. In the setting of non-wellfounded proofs, a validity criterion is necessary to distinguish, among all infinite derivation trees (aka. pre-proofs), those which are logically valid proofs. A standard approach is to consider a pre-proof to be valid if every infinite branch is supported by an infinitely progressing thread. The paper focuses on circular proofs for MALL with fixed points. Among all representations of valid circular proofs, a new fragment is described, based on a stronger validity criterion. This new criterion is based on a labelling of formulas and proofs, whose validity is purely local. This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's muMALL finite proofs with (co)inductive invariants: in particular deciding validity and computing a certifying labelling can be done efficiently. Moreover the Brotherston-Simpson conjecture holds for this fragment: every labelled representation of a circular proof in the fragment is translated into a standard finitary proof. Finally we explore how to extend these results to a bigger fragment, by relaxing the labelling discipline while retaining (i) the ability to locally certify the validity and (ii) to some extent, the ability to finitize circular proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
  • Theory of computation → Logic and verification
Keywords
  • sequent calculus
  • non-wellfounded proofs
  • circular proofs
  • induction
  • coinduction
  • fixed points
  • proof-search
  • linear logic
  • muMALL
  • finitization
  • infinite descent

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005088.
  2. David Baelde. On the proof theory of regular fixed points. In Martin Giese and Arild Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings, volume 5607 of Lecture Notes in Computer Science, pages 93-107. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02716-1_8.
  3. David Baelde. Least and greatest fixed points in linear logic. ACM Transactions on Computational Logic (TOCL), 13(1):2, 2012. Google Scholar
  4. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.42.
  5. David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In Nachum Dershowitz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, volume 4790 of Lecture Notes in Computer Science, pages 92-106. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-75560-9_9.
  6. Stefano Berardi and Makoto Tatsuta. Classical system of martin-löf’s inductive definitions is not equivalent to cyclic proof system. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 301-317, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_18.
  7. Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005114.
  8. James Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, 2006. Google Scholar
  9. James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen. A generic cyclic theorem prover. In Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, volume 7705 of Lecture Notes in Computer Science, pages 350-367. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-35182-2_25.
  10. James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 51-62. IEEE Computer Society, 2007. URL: http://dx.doi.org/10.1109/LICS.2007.16.
  11. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput., 21(6):1177-1216, 2011. URL: http://dx.doi.org/10.1093/logcom/exq052.
  12. Pierre Clairambault. Least and greatest fixpoints in game semantics. In FOSSACS, volume 5504 of Lecture Notes in Computer Science, pages 16-31. Springer, 2009. Google Scholar
  13. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Arch. Math. Log., 28(3):181-203, 1989. URL: http://dx.doi.org/10.1007/BF01622878.
  14. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. URL: http://dx.doi.org/10.1007/11944836_26.
  15. Amina Doumane. On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes). PhD thesis, Paris Diderot University, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01676953.
  16. Amina Doumane, David Baelde, Lucca Hirschi, and Alexis Saurin. Towards Completeness via Proof Search in the Linear Time mu-Calculus. Accepted for publication at LICS, 2016. URL: https://hal.archives-ouvertes.fr/hal-01275289.
  17. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 248-262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: http://drops.dagstuhl.de/opus/portals/extern/index.php?semnr=13009.
  18. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  19. Roope Kaivola. A simple decision method for the linear time mu-calculus. In Jörg Desel, editor, Structures in Concurrency Theory, Workshops in Computing, pages 190-204. Springer London, 1995. URL: http://dx.doi.org/10.1007/978-1-4471-3078-9_13.
  20. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: http://dx.doi.org/10.1016/0304-3975(82)90125-6.
  21. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 81-92. ACM, 2001. URL: http://dx.doi.org/10.1145/360204.360210.
  22. David Park. Fixpoint induction and proofs of program properties. Machine intelligence, 5(59-78):5-3, 1969. Google Scholar
  23. Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, volume 2303 of Lecture Notes in Computer Science, pages 357-371. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45931-6_25.
  24. Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283-300, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_17.
  25. Colin Stirling. A tableau proof system with names for modal mu-calculus. In HOWARD-60: A Festschrift on the Occasion of Howard Barringer’s 60th Birthday, volume 42 of EPiC Series in Computing, pages 306-318. EasyChair, 2014. URL: http://www.easychair.org/publications/?page=1932281032.
  26. Igor Walukiewicz. On completeness of the mu-calculus. In LICS, pages 136-146. IEEE Computer Society, 1993. Google Scholar
  27. Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional mu-calculus. In Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 14-24. IEEE Computer Society, 1995. URL: http://dx.doi.org/10.1109/LICS.1995.523240.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail