A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata

Klaus Aehlig

doi:10.2168/LMCS-3(3:1)2007

Klaus Aehlig - A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of<br> Automata

lmcs:1232 - Logical Methods in Computer Science, July 4, 2007, Volume 3, Issue 3 - https://doi.org/10.2168/LMCS-3(3:1)2007

A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of<br> AutomataArticle

Authors: Klaus Aehlig

Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type hierarchy upon this interpretation of the base type gives a finite semantics for simply-typed lambda-trees. A calculus based on this semantics is proven sound and complete. In particular, for regular infinite lambda-trees it is decidable whether a given automaton has a run or not. As regular lambda-trees are precisely recursion schemes, this decidability result holds for arbitrary recursion schemes of arbitrary level, without any syntactical restriction.

https://doi.org/10.2168/LMCS-3(3:1)2007

Source: arXiv.org:0706.2076

Volume: Volume 3, Issue 3

Published on: July 4, 2007

Imported on: November 24, 2006

Keywords: Computer Science - Logic in Computer Science,F.3.2

Licence: arXiv.org - Assumed non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Abstract Measures of Low-Level Computational Complexity; Funder: UK Research and Innovation; Code: EP/D03809X/1

Classifications

Mathematics Subject Classification 2020¹

68Q60 - Specification and verification (program logics, model checking, etc.)

Sources:

[1] zbMATH Open.

Bibliographic References

27 Documents citing this article

Igor Walukiewicz, Lambda Y-Calculus With Priorities, pp. 1-13, 2019, Vancouver, BC, Canada, 10.1109/lics.2019.8785674, https://hal.archives-ouvertes.fr/hal-02100196.

Naoki Kobayashi;Étienne Lozes;Florian Bruse, 2017, On the relationship between higher-order recursion schemes and higher-order fixpoint logic, 52, 1, pp. 246-259, 10.1145/3093333.3009854, https://hal.archives-ouvertes.fr/hal-01920615.

Paul-Andre Mellies, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Higher-order parity automata, 2017, Reykjavik, Iceland, 10.1109/lics.2017.8005077.

Pierre Clairambault;Charles Grellois;Andrzej S. Murawski, 2017, Linearity in higher-order recursion schemes, Proceedings of the ACM on Programming Languages, 2, POPL, pp. 1-29, 10.1145/3158127, https://doi.org/10.1145/3158127.

Igor Walukiewicz, 2016, Automata theory and higher-order model-checking, ACM SIGLOG News, 3, 4, pp. 13-31, 10.1145/3026744.3026745, https://doi.org/10.1145/3026744.3026745.

Keiichi Watanabe;Ryosuke Sato;Takeshi Tsukada;Naoki Kobayashi, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, Automatically disproving fair termination of higher-order functional programs, pp. 243-255, 2016, Nara Japan, 10.1145/2951913.2951919.

Keiichi Watanabe;Ryosuke Sato;Takeshi Tsukada;Naoki Kobayashi, 2016, Automatically disproving fair termination of higher-order functional programs, ACM SIGPLAN Notices, 51, 9, pp. 243-255, 10.1145/3022670.2951919.

Naoki Kobayashi;Étienne Lozes;Florian Bruse, On the relationship between higher-order recursion schemes and higher-order fixpoint logic, 2016, Paris France, 10.1145/3009837.3009854, https://hal.science/hal-01920615/file/main-long.pdf.

Xin Li;Naoki Kobayashi, Lecture notes in computer science, Equivalence-Based Abstraction Refinement for $$\mu $$ HORS Model Checking, pp. 304-320, 2016, 10.1007/978-3-319-46520-3_20.

Luke Ong, CiteSeer X (The Pennsylvania State University), Higher-Order Model Checking: An Overview, 2015, Kyoto, Japan, 10.1109/lics.2015.9, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.713.667.

Sylvain Salvati;Igor Walukiewicz, Lecture notes in computer science, Typing Weak MSOL Properties, pp. 343-357, 2015, 10.1007/978-3-662-46678-0_22, https://doi.org/10.1007/978-3-662-46678-0_22.

Taku Terao;Naoki Kobayashi, CiteSeer X (The Pennsylvania State University), A ZDD-Based Efficient Higher-Order Model Checking Algorithm, pp. 354-371, 2014, 10.1007/978-3-319-12736-1_19, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.724.6353.

Luke Ong, Lecture notes in computer science, Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking, pp. 13-41, 2013, 10.1007/978-3-642-37064-9_3.

Naoki Kobayashi, 2013, Model Checking Higher-Order Programs, Journal of the ACM, 60, 3, pp. 1-62, 10.1145/2487241.2487246.

Sylvain Salvati;Igor Walukiewicz, Using Models to Model-Check Recursive Schemes, pp. 189-204, 2013, 10.1007/978-3-642-38946-7_15, https://hal.inria.fr/hal-00741077.

Naoki Kobayashi, Lecture notes in computer science, Program Certification by Higher-Order Model Checking, pp. 9-10, 2012, 10.1007/978-3-642-35308-6_4.

Naoki Kobayashi;C. -H. Luke Ong, 2012, Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus, Logical Methods in Computer Science, Volume 7, Issue 4, 10.2168/lmcs-7(4:9)2011, https://doi.org/10.2168/lmcs-7(4:9)2011.

Robin P. Neatherway;Steven J. Ramsay;Chih-Hao Luke Ong, 2012, A traversal-based algorithm for higher-order model checking, ACM SIGPLAN Notices, 47, 9, pp. 353-364, 10.1145/2398856.2364578.

Naoki Kobayashi, Lecture notes in computer science, A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes, pp. 260-274, 2011, 10.1007/978-3-642-19805-2_18, https://doi.org/10.1007/978-3-642-19805-2_18.

Naoki Kobayashi, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, Higher-Order Model Checking: From Theory to Practice, pp. 219-224, 2011, Toronto, ON, Canada, 10.1109/lics.2011.15.

Naoki Kobayashi;Naoshi Tabuchi;Hiroshi Unno, 2010, Higher-order multi-parameter tree transducers and recursion schemes for program verification, ACM SIGPLAN Notices, 45, 1, pp. 495-508, 10.1145/1707801.1706355.

Jörg Endrullis;Clemens Grabmayer;Dimitri Hendriks;Ariya Isihara;Jan Willem Klop, 2009, Productivity of stream definitions, Theoretical Computer Science, 411, 4-5, pp. 765-782, 10.1016/j.tcs.2009.10.014, https://doi.org/10.1016/j.tcs.2009.10.014.

Naoki Kobayashi, CiteSeer X (The Pennsylvania State University), Model-checking higher-order functions, pp. 25-36, 2009, Coimbra Portugal, 10.1145/1599410.1599415, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.161.3824.

Naoki Kobayashi, 2009, Types and higher-order recursion schemes for verification of higher-order programs, CiteSeer X (The Pennsylvania State University), 44, 1, pp. 416-428, 10.1145/1594834.1480933, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.217.8532.

Naoki Kobayashi, Lecture notes in computer science, Types and Recursion Schemes for Higher-Order Program Verification, pp. 2-3, 2009, 10.1007/978-3-642-10672-9_2.

Naoki Kobayashi;C. -H. Luke Ong, arXiv (Cornell University), Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus, pp. 223-234, 2009, 10.1007/978-3-642-02930-1_19, https://arxiv.org/abs/1109.5267.

Naoki Kobayashi;C.-H. Luke Ong, 2009 24th Annual IEEE Symposium on Logic In Computer Science, A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes, 2009, Los Angeles, California, USA, 10.1109/lics.2009.29.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1546 times.

This article's PDF has been downloaded 334 times.