Order Structures on Böhm-Like Models

  • Paula Severi
  • Fer-Jan de Vries
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


We are interested in the question whether the models induced by the infinitary lambda calculus are orderable, that is whether they have a partial order with a least element making the context operators monotone. The first natural candidate is the prefix relation: a prefix of a term is obtained by replacing some subterms by \(\bot\). We prove that six models induced by the infinitary lambda calculus (which includes Böhm and Lévy-Longo trees) are orderable by the prefix relation. The following two orders we consider are the compositions of the prefix relation with either transfinite η-reduction or transfinite η-expansion. We prove that these orders make the context operators of the η-Böhm trees and the ∞ η-Böhm trees monotone. The model of Berarducci trees is not monotone with respect to the prefix relation. However, somewhat unexpectedly, we found that the Berarducci trees are orderable by a new order related to the prefix relation in which subterms are not replaced by \(\bot\) but by a lambda term O called the ogre which devours all its inputs. The proof of this uses simulation and coinduction. Finally, we show that there are 2 c unorderable models induced by the infinitary lambda calculus where c is the cardinality of the continuum.


Normal Form Partial Order Order Structure Reduction Rule Context Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1984) (revised edition)zbMATHGoogle Scholar
  2. 2.
    Barr, M.: Terminal coalgebras for endofunctors on sets. Theoretical Computer Science 114(2), 299–315 (1999)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Berarducci, A.: Infinite λ-calculus and non-sensible models. In: Logic and algebra (Pontignano, 1994), Pontignano, pp. 339–377. Dekker, New York (1996)Google Scholar
  4. 4.
    Berarducci, A., Dezani-Ciancaglini, M.: Infinite λ-calculus and types. Theoretical Computer Science 212(1-2), 29–75 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Coppo, M., Dezani-Ciancaglini, M., Zacchi, M.: Type theories, normal forms, and D∞-lambda-models. Information and Computation 72(2), 85–116 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Dezani-Ciancaglini, M., Severi, P., de Vries, F.J.: Infinitary lambda calculus and discrimination of Berarducci trees. Theoretical Computer Science 298(2), 275–302 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Kennaway, J., de Vries, F.J.: Infinitary rewriting. In: Terese (ed.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 668–711. Cambridge University Press, Cambridge (2003)Google Scholar
  8. 8.
    Kennaway, J.R., Klop, J.W., Sleep, M.R., de Vries, F.J.: Infinite lambda calculus and Böhm models. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 257–270. Springer, Heidelberg (1995)Google Scholar
  9. 9.
    Kennaway, J.R., Klop, J.W., Sleep, M.R., de Vries, F.J.: Infinitary lambda calculus. Theoretical Computer Science 175(1), 93–125 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Kennaway, J.R., van Oostrom, V., de Vries, F.J.: Meaningless terms in rewriting. J. Funct. Logic Programming 1, 35 (1999)Google Scholar
  11. 11.
    Klop, J.W.: Combinatory Reduction Systems. Mathematical centre tracts, vol. 127. Mathematisch Centrum (1980)Google Scholar
  12. 12.
    Salibra, A.: Topological incompleteness and order incompleteness of the lambda calculus. ACM Transactions on Computational Logic 4(3), 379–401 (2003) (Special Issue LICS 2001)CrossRefMathSciNetGoogle Scholar
  13. 13.
    Severi, P., de Vries, F.J.: An extensional Böhm model. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 159–173. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    Severi, P., de Vries, F.J.: Continuity and discontinuity in lambda calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 369–385. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  15. 15.
    Severi, P., Vries, F.J.d.: A Lambda Calculus for D∞. Technical report, University of Leicester (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Paula Severi
    • 1
  • Fer-Jan de Vries
    • 1
  1. 1.Department of Computer ScienceUniversity of LeicesterUK

Personalised recommendations