Document Open Access Logo

Phase Semantics for Linear Logic with Least and Greatest Fixed Points

Authors Abhishek De, Farzad Jafarrahmani, Alexis Saurin

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2022.35.pdf
  • Filesize: 0.89 MB
  • 23 pages

Document Identifiers

Author Details

Abhishek De
  • IRIF, Université Paris Cité, CNRS & INRIA $π.r^2$, France
Farzad Jafarrahmani
  • IRIF, Université Paris Cité, CNRS & INRIA $π.r^2$, France
Alexis Saurin
  • IRIF, CNRS, Université Paris Cité & INRIA $π.r^2$, France

Funding

This research has been partially supported by ANR project RECIPROG, project reference ANR-21-CE48-019-01.
  • De, Abhishek: This author has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 754362.

Acknowledgements

We would like to thank anonymous reviewers for their valuable comments that enhanced the clarity and presentation of this paper. We would like to thank Amina Doumane, Graham Leigh and Rémi Nollet for helpful discussions in the early phase of this work.

Cite As Get BibTex

Abhishek De, Farzad Jafarrahmani, and Alexis Saurin. Phase Semantics for Linear Logic with Least and Greatest Fixed Points. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 35:1-35:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSTTCS.2022.35

Abstract

The truth semantics of linear logic (i.e. phase semantics) is often overlooked despite having a wide range of applications and deep connections with several denotational semantics. In phase semantics, one is concerned about the provability of formulas rather than the contents of their proofs (or refutations). Linear logic equipped with the least and greatest fixpoint operators (μMALL) has been an active field of research for the past one and a half decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. 
In this paper, we extend the phase semantics of multiplicative additive linear logic (a.k.a. MALL) to μMALL with explicit (co)induction (i.e. μMALL^{ind}). We introduce a Tait-style system for μMALL called μMALL_ω where proofs are wellfounded but potentially infinitely branching. We study its phase semantics and prove that it does not have the finite model property.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Proof theory
Keywords
  • Linear logic
  • fixed points
  • phase semantics
  • closure ordinals
  • cut elimination

Metrics

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

References

  1. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier, 1977. Google Scholar
  2. Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30-44, Dagstuhl, Germany, 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.30.
  3. Alfred V. Aho and Jeffrey D. Ullman. Universality of data retrieval languages. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '79, pages 110-119, New York, NY, USA, 1979. Association for Computing Machinery. URL: https://doi.org/10.1145/567752.567763.
  4. Jeremy Avigad. Algebraic proofs of cut elimination. The Journal of Logic and Algebraic Programming, 49(1):15-30, 2001. URL: https://doi.org/10.1016/S1567-8326(01)00009-1.
  5. David Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic, 13(1), January 2012. URL: https://doi.org/10.1145/2071368.2071370.
  6. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In 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: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  7. 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, pages 92-106, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  8. Stefano Berardi and Makoto Tatsuta. Classical system of martin-löf’s inductive definitions is not equivalent to cyclic proof system. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 301-317, 2017. Google Scholar
  9. Stefano Berardi and Makoto Tatsuta. Equivalence of inductive definitions and cyclic proofs under arithmetic. In LICS, pages 1-12. IEEE Computer Society, 2017. Google Scholar
  10. Stefano Berardi and Makoto Tatsuta. Classical system of martin-lof’s inductive definitions is not equivalent to cyclic proofs. Log. Methods Comput. Sci., 15(3), 2019. Google Scholar
  11. James Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, November 2006. Google Scholar
  12. James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 51-62. IEEE, 2007. Google Scholar
  13. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. Google Scholar
  14. Kai Brünnler and Thomas Studer. Syntactic cut-elimination for a fragment of the modal mu-calculus. Annals of Pure and Applied Logic, 163(12):1838-1853, 2012. URL: https://doi.org/10.1016/j.apal.2012.04.006.
  15. Rudolf Carnap. Logical Syntax of Language. Kegan Paul, Trench and Truber, 1937. Google Scholar
  16. Edmund M Clarke, Orna Grumberg, and Doron A. Peled. Model checking for the μ-calculus. In Model checking, chapter 7, pages 97-108. MIT Press, London, Cambridge, 1999. Google Scholar
  17. Patrick Cousot and Radhia Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics, 82(1):43-57, 1979. Google Scholar
  18. Marek Czarnecki. How fast can the fixpoints in modal mu-calculus be reached? In Luigi Santocanale, editor, 7th Workshop on Fixed Points in Computer Science, FICS 2010, Brno, Czech Republic, August 21-22, 2010, pages 35-39. Laboratoire d'Informatique Fondamentale de Marseille, 2010. URL: https://hal.archives-ouvertes.fr/hal-00512377/document#page=36.
  19. Ugo Dal Lago and Simone Martini. Phase semantics and decidability of elementary affine logic. Theoretical Computer Science, 318(3):409-433, 2004. URL: https://doi.org/10.1016/j.tcs.2004.02.037.
  20. Anupam Das, Abhishek De, and Alexis Saurin. Decision problems for linear logic with least and greatest fixed points. In FSCD, volume 228 of LIPIcs, pages 20:1-20:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  21. Anuj Dawar and Yuri Gurevich. Fixed Point Logics. Bulletin of Symbolic Logic, 8(1):65-88, 2002. URL: https://doi.org/10.2178/bsl/1182353853.
  22. Pierre Simon de Fermat. Oeuvres de Fermats, T.2. Gauthier-Villars et Fils, Paris, 1894. Google Scholar
  23. 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.
  24. Thomas Ehrhard and Farzad Jafarrahmani. Categorical models of linear logic with fixed points of formulas. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470664.
  25. Thomas Ehrhard, Farzad Jafarrahmani, and Alexis Saurin. Polarized linear logic with fixpoints (technical report). URL: https://drive.google.com/file/d/1eQd5evwcUXYBT5f-TZbs8o4eIE4PhN9m/view?usp=sharing.
  26. Thomas Ehrhard, Farzad Jafarrahmani, and Alexis Saurin. On relation between totality semantic and syntactic validity. In 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Rome (virtual), Italy, June 2021. URL: https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271408.
  27. Euclid. The Elements of Euclid. Dover Publications Inc., New York, 2nd edition, 1956. URL: https://archive.org/details/euclid_heath_2nd_ed.
  28. 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: https://doi.org/10.4230/LIPIcs.CSL.2013.248.
  29. J. Y. Girard. Une extension de l'interpretation de Godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. Proceedings of the second Scandinavian logic symposium, 63:63-92, 1971. Google Scholar
  30. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  31. Maria João Gouveia and Luigi Santocanale. Aleph1 and the Modal mu-Calculus. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 38:1-38:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.38.
  32. Gerhard Jäger, Mathis Kretz, and Thomas Studer. Canonical completeness of infinitary μ. The Journal of Logic and Algebraic Programming, 76(2):270-292, 2008. Logic and Information: From Logic to Constructive Reasoning. URL: https://doi.org/10.1016/j.jlap.2008.02.005.
  33. Bronisław Knaster and Alfred Tarski. Un théorème sur les fonctions d'ensembles. Annales de la Société Polonaise de Mathématique, 6:133-134, 1927. Google Scholar
  34. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  35. Dexter Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, September 1988. URL: https://doi.org/10.1007/BF00370554.
  36. Yves Lafont. The finite model property for various fragments of linear logic. The Journal of Symbolic Logic, 62(4):1202-1208, 1997. URL: http://www.jstor.org/stable/2275637.
  37. Yves Lafont. Soft linear logic and polynomial time. Theoretical Computer Science, 318(1):163-180, 2004. Implicit Computational Complexity. URL: https://doi.org/10.1016/j.tcs.2003.10.018.
  38. Leonid Libkin. Elements of Finite Model Theory. Springer, August 2004. Google Scholar
  39. Shoji Maehara. Lattice-valued representation of the cut-elimination theorem. Tsukuba journal of mathematics, 15:509-521, 1991. Google Scholar
  40. Per Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 179-216. Elsevier, 1971. URL: https://doi.org/10.1016/S0049-237X(08)70847-4.
  41. Grigori Mints. Finite investigations of transfinite derivations. Journal of Soviet Mathematics, 10:548-596, 1978. Google Scholar
  42. Mitsuhiro Okada. Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic. Theoretical Computer Science, 227(1):333-396, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00058-4.
  43. Ewa Palka. An infinitary sequent system for the equational theory of *-continuous action lattices. Fundam. Inf., 78(2):295-309, April 2007. Google Scholar
  44. 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: https://doi.org/10.1007/3-540-45931-6_25.
  45. Kurt Schütte. Vollständige Systeme modaler und intuitionistischer Logik. Springer Berlin Heidelberg, 1968. URL: https://doi.org/10.1007/978-3-642-88664-5.
  46. Kurt Schütte. Syntactical and semantical properties of simple type theory. The Journal of Symbolic Logic, 25(4):305-326, 1960. URL: http://www.jstor.org/stable/2963525.
  47. Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 283-300, 2017. Google Scholar
  48. William W. Tait. A realizability interpretation of the theory of species. In Rohit Parikh, editor, Logic Colloquium, pages 240-251, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg. Google Scholar
  49. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  50. Igor Walukiewicz. A complete deductive system for the μ-calculus. PhD thesis, Warsaw University, 1994. Google Scholar
  51. Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. In LICS 95, San Diego, California, USA, June 26-29, 1995, pages 14-24, 1995. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact