Hostname: page-component-848d4c4894-p2v8j Total loading time: 0 Render date: 2024-05-01T14:46:19.229Z Has data issue: false hasContentIssue false
  • English
  • Français

Simply typed fixpoint calculus and collapsible pushdown automata

Published online by Cambridge University Press:  18 March 2015

SYLVAIN SALVATI  and
IGOR WALUKIEWICZ
SYLVAIN SALVATI
Affiliation:
INRIA, CNRS, Université de Bordeaux, France
IGOR WALUKIEWICZ
Affiliation:
INRIA, CNRS, Université de Bordeaux, France
Get access Rights & Permissions [Opens in a new window]

Abstract

Simply typed λ-calculus with fixpoint combinators, λY-calculus, offers an interesting method for approximating program semantics. The Böhm tree of a λY-term represents the meaning of the program up to the meaning of built-in constants. It is much easier to reason about properties of such trees than properties of interpreted programs. Moreover, some interesting properties of programs are already expressible on the level of these trees.

Collapsible pushdown automata (CPDA) give another way of generating the same class of trees as λY-terms. We clarify the relationship between the two models. In particular, we present two relatively simple translations from λY-terms to CPDA using Krivine machines as an intermediate step. The latter are general machines for describing computation of the weak head normal form in the λ-calculus. They provide the notions of closure and environment that facilitate reasoning about computation.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Issue 7 , October 2016 , pp. 1304 - 1350
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aehlig, K., de Miranda, J. G. and Ong, C.-H. L. (2005) The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In: Proceedings of the International Conference on Typed Lambda Calculi and Applications. Springer Lecture Notes in Computer Science 3461 39–54.Google Scholar
Aho, A. (1968) Indexed grammars – an extension of context-free grammars. Journal of the Association of Computing Machinery 15 (4) 647–671.Google Scholar
Barendregt, H. (1977) The type free lambda calculus. In: Barwise, J.(ed.) Handbook of Mathematical Logic, Chapter D.7, North Holland, Amsterdam 1091–1132.Google Scholar
Barendregt, H. (1985) The Lambda Calculus, Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics volume 103, North Holland, Amsterdam.Google Scholar
Barendregt, H. and Klop, J. W. (2009) Applications of infinitary lambda calculus. Information and Computation 207 (5) 559–582.Google Scholar
Blum, W. and Ong, L. (2009) The safe lambda calculus. Logical Methods in Computer Science 5 (1:3) 1–38.Google Scholar
Broadbent, C., Carayol, A., Ong, L. and Serre, O. (2010) Recursion schemes and logical reflection. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 120–129.Google Scholar
Broadbent, C. H., Carayol, A., Hague, M. and Serre, O. (2012) A saturation method for collapsible pushdown systems. In: Proceedings of the International Colloquium on Automata, Languages and Programming Track B. Springer-Verlag Lecture Notes in Computer Science 7392 165–176.Google Scholar
Carayol, A., Hague, M., Meyer, A., Ong, C.-H. L. and Serre, O. (2008) Winning regions of higher-order pushdown games. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 193–204.Google Scholar
Carayol, A. and Serre, O. (2012) Collapsible pushdown automata and labeled recursion schemes equivalence, safety and effective selection. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 165–174.Google Scholar
Carayol, A. and Wöhrle, S. (2003) The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In: Foundations of Software Technology and Theoretical Computer Science. Springer Lecture Notes in Computer Science 2914 112–124.Google Scholar
Caucal, D. (2002) On infinite terms having a decidable monadic theory. In: Proceedings of the International Symposium on Mathematical Foundations of Computer Science. Springer Lecture Notes in Computer Science 2420 165–176.Google Scholar
Damm, W. (1982) The IO– and OI–hierarchies. Theoretical Computer Science 20 (2) 95–208.Google Scholar
Damm, W. and Goerdt, A. (1986) An automata-theoretical characterization of the OI-hierarchy. Information and Control 71 (1–2) 1–32.Google Scholar
Dezani-Ciancaglini, M., Giovannetti, E. and de' Liguoro, U. (1998) Intersection types, Lambda-models and Böhm trees. In: MSJ-Memoir Vol. 2 ‘Theories of Types and Proofs’, volume 2, Mathematical Society of Japan 45–97.Google Scholar
Hague, M., Murawski, A. S., Ong, C.-H. L. and Serre, O. (2008) Collapsible pushdown automata and recursion schemes. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 452–461.Google Scholar
Hyland, J. M. E. and Ong, C.-H. L. (2000) On full abstraction for pcf: I, II, and III. Information and Computation 163 (2) 285–408.Google Scholar
Ianov, Y. (1969) The logical schemes of algorithms. In: Problems of Cybernetics I, Oxford: Pergamon Press, 82–140.Google Scholar
Kfoury, A. and Urzyczyn, P. (1988) Finitely typed functional programs, Part II: Comparisons to imperative languages. Technical report BUCS tech report, 88-012, Boston University.Google Scholar
Knapik, T., Niwinski, D. and Urzyczyn, P. (2002) Higher-order pushdown trees are easy. In: Proceedings of the International Conference on Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science 2303 205–222.Google Scholar
Knapik, T., Niwinski, D., Urzyczyn, P. and Walukiewicz, I. (2005) Unsafe grammars and panic automata. In: Proceedings of the International Colloquium on Automata, Languages and Programming. Springer Lecture Notes in Computer Science 3580 1450–1461.Google Scholar
Kobayashi, N. (2011) A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In: Proceedings of the International Conference on Foundations of Software Science and Computation Structures. Springer Lecture Notes in Computer Science 6604 260–274.Google Scholar
Kobayashi, N. (2013) Model checking higher order programs. Journal of the Association of Computing Machinery 60 (3) Article No. 20. doi: 10.1145/2487241.2487246.Google Scholar
Kobayashi, N. and Ong, L. (2009) A type system equivalent to modal mu-calculus model checking of recursion schemes. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 179–188.Google Scholar
Krivine, J.-L. (2007) A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20 (3) 199–207.Google Scholar
Maslov, A. (1974) The hierarchy of indexed languages of an arbitrary level. Soviet Mathematics Doklady 15 1170–1174.Google Scholar
Maslov, A. (1976) Multilevel stack automata. Problems of Information Transmission 12 38–42.Google Scholar
Milner, R. (1973) Models of LCF. Memo AIM-186, Stanford University.Google Scholar
Miranda, J. G. de (2006) Structures Generated by Higher-Order Grammars and the Safety Constraint, Ph.D. thesis, Oxford University.Google Scholar
Nivat, M. (1972a) Langages algébriques sur le magma libre et sémantique des schémas de programme. In: Proceedings of the International Colloquium on Automata, Languages and Programming 293–308.Google Scholar
Nivat, M. (1972b) On the interpretation of recursive program schemes. In: Symposia Mathematica 15 255–281.Google Scholar
Ong, C.-H. L. (2006) On model-checking trees generated by higher-order recursion schemes. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 81–90.Google Scholar
Parys, P. (2012) On the significance of the collapse operation. In: Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society 521–530.Google Scholar
Plotkin, G. D. (1977) LCF considered as a programming language. Theoretical Computer Science 5 (3) 223–255.Google Scholar
Salvati, S. and Walukiewicz, I. (2011) Krivine machines and higher-order schemes. In: Proceedings of the International Colloquium on Automata, Languages and Programming Track B. Springer Lecture Notes in Computer Science 6756 162–173.Google Scholar
Salvati, S. and Walukiewicz, I. (2012) Recursive schemes, Krivine machines, and collapsible pushdown automata. In: Proceedings of the International Workshop on Reachability Problems. Springer Lecture Notes in Computer Science 7550 6–20.Google Scholar
Salvati, S. and Walukiewicz, I. (2013) Using models to model-check recursive schemes. In: Proceedings of the International Conference on Typed Lambda Calculi and Applications. Springer Lecture Notes in Computer Science 7941 189–204.Google Scholar