Order Structures on Böhm-Like Models
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.
KeywordsNormal Form Partial Order Order Structure Reduction Rule Context Operator
Unable to display preview. Download preview PDF.
- 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
- 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.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
- 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.Klop, J.W.: Combinatory Reduction Systems. Mathematical centre tracts, vol. 127. Mathematisch Centrum (1980)Google Scholar
- 15.Severi, P., Vries, F.J.d.: A Lambda Calculus for D∞. Technical report, University of Leicester (2002)Google Scholar