Please use this identifier to cite or link to this item:
Title: The infinitary lambda calculus of the infinite eta Böhm trees
Authors: Severi, Paula
de Vries, Fer-Jan
First Published: 17-Aug-2015
Publisher: Cambridge University Press (CUP)
Citation: Mathematical Structures in Computer Science / FirstView Article / August 2015, pp 1 - 53 Available on CJO 2015
Abstract: In this paper, we introduce a strong form of eta reduction called etabang that we use to construct a confluent and normalising infinitary lambda calculus, of which the normal forms correspond to Barendregt's infinite eta Böhm trees. This new infinitary perspective on the set of infinite eta Böhm trees allows us to prove that the set of infinite eta Böhm trees is a model of the lambda calculus. The model is of interest because it has the same local structure as Scott's D∞-models, i.e. two finite lambda terms are equal in the infinite eta Böhm model if and only if they have the same interpretation in Scott's D∞-models.
DOI Link: 10.1017/S096012951500033X
ISSN: 0960-1295
eISSN: 1469-8072
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: Archived with reference to SHERPA/RoMEO and publisher website. (c) Cambridge University Press 2015 Version of record:
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
main.pdfPre-review (submitted draft)694.34 kBAdobe PDFView/Open

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