University of Leicester
Browse
main.pdf (694.34 kB)

The infinitary lambda calculus of the infinite eta Böhm trees

Download (694.34 kB)
journal contribution
posted on 2015-08-24, 14:09 authored by Paula Severi, Fer-Jan de Vries
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.

History

Citation

Mathematical Structures in Computer Science / FirstView Article / August 2015, pp 1 - 53 Available on CJO 2015

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Version

  • AM (Accepted Manuscript)

Published in

Mathematical Structures in Computer Science / FirstView Article / August 2015

Publisher

Cambridge University Press (CUP)

issn

0960-1295

eissn

1469-8072

Copyright date

2015

Available date

2016-02-17

Publisher version

http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9913254&fileId=S096012951500033X

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC