Please use this identifier to cite or link to this item:
Title: Order Structures on Böhm-like Models
Authors: Severi, Paula
de Vries, Fer-Jan
First Published: 2005
Citation: Computer Science Logic: 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK. August 22-25, 2005. Lecture Notes in Computer Science, 2005, 3634, pp. 103-118
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 ⊥. 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 ⊥ 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.
DOI Link: 10.1007/11538363_9
ISBN: 3540282319
Type: Conference paper
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
There are no files associated with this item.

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.