Hostname: page-component-7b7567c8c-mnklg Total loading time: 0 Render date: 2026-11-13T08:28:36.806Z Has data issue: false hasContentIssue false
  • English
  • Français

The infinitary lambda calculus of the infinite eta Böhm trees

Published online by Cambridge University Press:  17 August 2015

PAULA SEVERI and
FER-JAN DE VRIES
PAULA SEVERI
Affiliation:
Department of Computer Science, University of Leicester, Leicester, U.K. Email: pgs11@le.ac.uk, fdv1@mcs.le.ac.uk
FER-JAN DE VRIES
Affiliation:
Department of Computer Science, University of Leicester, Leicester, U.K. Email: pgs11@le.ac.uk, fdv1@mcs.le.ac.uk
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

In this paper, we introduce a strong form of eta reduction called etabang that we use to construct a confluent and normalising infinitary lambda calculus, of which the normal forms correspond to Barendregt's infinite eta Böhm trees. This new infinitary perspective on the set of infinite eta Böhm trees allows us to prove that the set of infinite eta Böhm trees is a model of the lambda calculus. The model is of interest because it has the same local structure as Scott's D ∞-models, i.e. two finite lambda terms are equal in the infinite eta Böhm model if and only if they have the same interpretation in Scott's D ∞-models.

References

Abramsky, S. and Ong, C.-H.L. (1993). Full abstraction in the lazy lambda calculus. Information and Computation 105 (2) 159–267.Google Scholar
Arnold, A. and Nivat, M. (1980). The metric space of infinite trees. Algebraic and topological properties. Annales Societatis Mathematicae Poloniae Séries IV: Fundamenta Informatica III–4 445–476.Google Scholar
Bakel, S.v., Barbanera, F., Dezani-Ciancaglini, M. and de Vries, F.J. (2002). Intersection types for λ-trees. Theoretical Computer Science 272 (1–2) 3–40.CrossRefGoogle Scholar
Barbanera, F., Dezani-Ciancaglini, M. and de Vries, F.J. (1998). Types for trees. In: PROCOMET'98 (Shelter Island, 1998), Chapman & Hall, London 6–29.Google Scholar
Barendregt, H.P. (1984). The Lambda Calculus: Its Syntax and Semantics, North-Holland, Amsterdam.Google Scholar
Barendregt, H.P. (1992). Lambda calculi with types. In: Abramsky, S., Gabbay, D. M. and Maibaum, T. S. E. (eds.) Handbook of Logic in Computer Science, vol. 2, Oxford University Press, Oxford 117–309.Google Scholar
Berarducci, A. (1996). Infinite λ-calculus and non-sensible models. In: Logic and Algebra (Pontignano, 1994), Dekker, New York 339–377.Google Scholar
Coppo, M., Dezani-Ciancaglini, M. and Zacchi, M. (1987). Type theories, normal forms, and D ∞-lambda-models. Information and Computation 72 (2) 85–116.CrossRefGoogle Scholar
Hyland, J.M.E. (1975). A survey of some useful partial order relations on terms of the lambda calculus. In: Böhm, C. (ed.) Lambda Calculus and Computer Science Theory. vol. 37, Springer-Verlag Lecture Notes in Computer Science 83–93.CrossRefGoogle Scholar
Kennaway, J.R. and de Vries, F.J. (2003). Infinitary rewriting. In: Terese, (ed.) Term Rewriting Systems, vol. 55, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press 668–711.Google Scholar
Kennaway, J.R., Klop, J.W., Sleep, M.R. and de Vries, F.J. (1995a). Infinite lambda calculus and Böhm models. In: Rewriting Techniques and Applications, vol. 914, Lecture Notes in Computer Science, Springer-Verlag 257–270.Google Scholar
Kennaway, J.R., Klop, J.W., Sleep, M.R. and de Vries, F.J. (1995b). Transfinite reductions in orthogonal term rewriting systems. Information and Computation 119 (1) 18–38.CrossRefGoogle Scholar
Kennaway, J.R., Klop, J.W., Sleep, M.R. and de Vries, F.J. (1997). Infinitary lambda calculus. Theoretical Computer Science 175 (1) 93–125.CrossRefGoogle Scholar
Kennaway, J.R., van Oostrom, V. and de Vries, F.J. (1999). Meaningless terms in rewriting. Journal of Functional Logic Programming 1999 (1) 35.Google Scholar
Lévy, J.-J. (1976). An algebraic interpretation of the λβK-calculus, and an application of a labelled λ-calculus. Theoretical Computer Science 2 (1) 97–114.Google Scholar
Longo, G. (1983). Set-theoretical models of λ-calculus: Theories, expansions, isomorphisms. Annals of Pure and Applied Logic 24 (2) 153–188.Google Scholar
Severi, P.G. and de Vries, F.J. (2002). An extensional Böhm model. In: Rewriting Techniques and Applications, vol. 2378, Lecture Notes in Computer Science, Springer-Verlag 159–173.Google Scholar
Severi, P.G. and de Vries, F.J. (2005a). Continuity and discontinuity in lambda calculus. In: Typed Lambda Calculus and Applications, vol. 3461, Lecture Notes in Computer Science, Springer-Verlag 103–116.Google Scholar
Severi, P.G. and de Vries, F.J. (2005b). Order structures for Böhm-like models. In: Computer Science Logic, vol. 3634, Lecture Notes in Computer Science, Springer-Verlag 103–116.CrossRefGoogle Scholar
Severi, P.G. and de Vries, F.J. (2011). Weakening the axiom of overlap in the infinitary lambda calculus. In: Rewriting Techniques and Applications, vol. 10, Leibniz International Proceedings in Informatics (LIPIcs) 313–328.Google Scholar
Simonsen, J.G. (2004). On confluence and residuals in cauchy convergent transfinite rewriting. Information Processing Letters 91 (3) 141–146.CrossRefGoogle Scholar
Wadsworth, C.P. (1976). The relation between computational and denotational properties for Scott's D ∞-models of the lambda-calculus. SIAM Journal on Computing 5 (3) 488–521.CrossRefGoogle Scholar