Paper Info
Title
The infinitary lambda calculus of the infinite eta Böhm trees.
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 Bohm trees. This new infinitary perspective on the set of infinite eta Bohm trees allows us to prove that the set of infinite eta Bohm trees is a model of the lambda calculus. The model is of interest because it has the same local structure as Scott's D-infinity-models, i.e. two finite lambda terms are equal in the infinite eta Bohm model if and only if they have the same interpretation in Scott's D-infinity-models.
Year
DOI
Venue
2017
10.1017/S096012951500033X
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
Field
DocType
Volume
Discrete mathematics,Lambda calculus,Binary lambda calculus,Local structure,If and only if,Mathematics,Lambda
Journal
27
Issue
ISSN
Citations 
SP5
0960-1295
0
PageRank 
References 
Authors
0.34
9
2
Name
Order
Citations
PageRank
Paula Severi112216.19
Fer-Jan de Vries224421.67