Document Open Access Logo

Models of Lambda-Calculus and the Weak MSO Logic

Authors Pawel Parys, Szymon Torunczyk

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.11.pdf
  • Filesize: 1.24 MB
  • 12 pages

Document Identifiers

Author Details

Pawel Parys
Szymon Torunczyk

Cite As Get BibTex

Pawel Parys and Szymon Torunczyk. Models of Lambda-Calculus and the Weak MSO Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.11

Abstract

We study the weak MSO logic in relationship to infinitary lambda-calculus. We show that for every formula phi of weak MSO there exists a finitary model of infinitary lambda-calculus recognizing the set of infinitary lambda-terms whose Böhm tree satisfies phi. The model is effective, in the sense that for every lambda-Y-term we can effectively compute its value in the model. In particular, given a finite lambda-Y-term, one can decide whether the resulting Böhm tree satisfies a given formula of weak MSO, which is a special case of the result of Ong, which concerns unrestricted MSO. The  existence of effective models for weak MSO and MSO was proved earlier by Salvati and Walukiewicz but our proof uses a different method, as it does not involve automata, but works directly with logics.

Subject Classification

Keywords
  • typed lambda-calculus
  • models
  • weak MSO logic

Metrics

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

References

  1. Klaus Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007. URL: http://dx.doi.org/10.2168/LMCS-3(3:1)2007.
  2. H. P. Barendregt. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland, revised edition, 1984. Google Scholar
  3. Mikolaj Bojańczyk and Szymon Toruńczyk. Weak MSO+U over infinite trees. In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 648-660. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2012.648.
  4. Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre. Recursion schemes and logical reflection. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 120-129. IEEE Computer Society, 2010. URL: http://dx.doi.org/10.1109/LICS.2010.40.
  5. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered tree-pushdown systems. In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 163-177. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://www.dagstuhl.de/dagpub/978-3-939897-97-2, URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.163.
  6. Werner Damm. The IO- and OI-hierarchies. Theoretical Computer Science, 20(2):95-207, 1982. URL: http://dx.doi.org/10.1016/0304-3975(82)90009-3.
  7. Charles Grellois and Paul-André Melliès. Finitary semantics of linear logic and higher-order model-checking. In Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors, Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I, volume 9234 of Lecture Notes in Computer Science, pages 256-268. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48057-1_20.
  8. Axel Haddad. Model checking and functional program transformations. In Seth and Vishnoi [22], pages 115-126. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2013.115.
  9. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 452-461. IEEE Computer Society, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.34.
  10. Thomas A. Henzinger and Dale Miller, editors. Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS'14, Vienna, Austria, July 14-18, 2014. ACM, 2014. Google Scholar
  11. Martin Hofmann and Wei Chen. Abstract interpretation from Büchi automata. In Henzinger and Miller [10], pages 51:1-51:10. URL: http://dx.doi.org/10.1145/2603088.2603127.
  12. Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn. Higher-order pushdown trees are easy. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45931-6_15.
  13. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179-188. IEEE Computer Society, 2009. URL: http://dx.doi.org/10.1109/LICS.2009.29.
  14. Giulio Manzonetto. Models and theories of lambda calculus. CoRR, abs/0904.4756, 2009. URL: http://arxiv.org/abs/0904.4756.
  15. Albert R. Meyer. What is a model of the lambda calculus? Information and Control, 52(1):87-122, 1982. URL: http://dx.doi.org/10.1016/S0019-9958(82)80087-9.
  16. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. URL: http://dx.doi.org/10.1109/LICS.2006.38.
  17. Sylvain Salvati and Igor Walukiewicz. Evaluation is MSOL-compatible. In Seth and Vishnoi [22], pages 103-114. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2013.103.
  18. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340-355, 2014. URL: http://dx.doi.org/10.1016/j.ic.2014.07.012.
  19. Sylvain Salvati and Igor Walukiewicz. A model for behavioural properties of higher-order programs. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 229-243. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://www.dagstuhl.de/dagpub/978-3-939897-90-3, URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.229.
  20. Sylvain Salvati and Igor Walukiewicz. Typing weak MSOL properties. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 343-357. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_22.
  21. Sylvain Salvati and Igor Walukiewicz. Using models to model-check recursive schemes. Logical Methods in Computer Science, 11(2), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(2:7)2015.
  22. Anil Seth and Nisheeth K. Vishnoi, editors. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, December 12-14, 2013, Guwahati, India, volume 24 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  23. Takeshi Tsukada and C.-H. Luke Ong. Compositional higher-order model checking via ω-regular games over Böhm trees. In Henzinger and Miller [10], pages 78:1-78:10. URL: http://dx.doi.org/10.1145/2603088.2603133.
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