Please use this identifier to cite or link to this item:
|Title:||Order Structures on Böhm-like Models|
de Vries, Fer-Jan
|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.|
|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.