Authors: Dezani-Ciancaglini, Mariangiola
Ghilezan, Silvia 
Likavec, Silvia
Title: Behavioural inverse limit λ-models
Journal: Theoretical Computer Science
Volume: 316
Issue: 1-3
First page: 49
Last page: 74
Issue Date: 28-May-2004
Rank: M22
ISSN: 0304-3975
DOI: 10.1016/j.tcs.2004.01.023
We construct two inverse limit λ-models which completely characterise sets of terms with similar computational behaviours: the sets of normalising, head normalising, weak head normalising λ-terms, those corresponding to the persistent versions of these notions, and the sets of closable, closable normalising, and closable head normalising λ-terms. More precisely, for each of these sets of terms there is a corresponding element in at least one of the two models such that a term belongs to the set if and only if its interpretation (in a suitable environment) is greater than or equal to that element. We use the finitary logical description of the models, obtained by defining suitable intersection type assignment systems, to prove this.
Keywords: Intersection types | Lambda calculus | Models of lambda calculus | Reducibility method | Stone dualities
Publisher: Elsevier
Project: FET-Global Computing initiative, project DART ST-2001-33477
“Representation of proofs with applications, classification of structures and infinite combinatorics” (of the Ministry of Science, Technology, and Development of Serbia), grant 1630

Show full item record


checked on May 17, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




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