Please use this identifier to cite or link to this item:

`http://hdl.handle.net/2381/3444`

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 |

Links: | http://link.springer.com/chapter/10.1007%2F11538363_9 http://hdl.handle.net/2381/3444 |

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.