Paper Info
Title
Order structures on böhm-like models
Abstract
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 2c unorderable models induced by the infinitary lambda calculus where c is the cardinality of the continuum.
Year
DOI
Venue
2005
10.1007/11538363_9
CSL
Keywords
Field
DocType
hm trees monotone,prefix relation,order structure,new order,context operators monotone,hm-like model,context operator,hm tree,infinitary lambda calculus,partial order,berarducci tree,lambda term,lambda calculus
Discrete mathematics,Lambda calculus,Combinatorics,Cardinal number,Prefix,Coinduction,Transfinite number,Cardinality of the continuum,Monotone polygon,Partially ordered set,Mathematics
Conference
Volume
ISSN
ISBN
3634
0302-9743
3-540-28231-9
Citations 
PageRank 
References 
3
0.40
9
Authors
2
Name
Order
Citations
PageRank
Paula Severi112216.19
Fer-Jan de Vries224421.67