Behavioural inverse limit -models

DOI10.1016/J.TCS.2004.01.023MaRDI QIDQ1434350zbMATH OpenOpenAlexFDO

Authors Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Silvia Likavec

Publication date 4 August 2004

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2004.01.023

zbMATH Keywords

intersection types lambda calculus models of lambda calculus Stone duality

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Review text

This paper studies nine computational properties of \(\lambda\)-terms and the corresponding sets of \(\lambda\)-terms. We recall that a \(\lambda\)-term \(t\) is normalising if \(t\) reduces to a normal form; head normalising if \(t\) reduces to a term of the form \(\lambda x_1\dots x_n.yu_1\dots u_k\); weak head normalising if \(t\) reduces to an abstraction or to a term starting with a free variable; persistently (head, weak head) normalising if \(tu_1\dots u_k\) is (head, weak head) normalising for all terms \(u_1,\dots, u_k\); closable if \(t\) reduces to a closed term; closable (head) normalising if \(t\) reduces to a closed (head) normal form. In the main result of the paper the authors build two inverse limit \(\lambda\)-models which completely characterise the above mentioned properties. More precisely, for each of the nine properties there is a corresponding element in at least one of these inverse limit \(\lambda\)-models such that a term satisfies the property if, and only if, its interpretation (in a suitable environment) is greater than or equal to that element. This result is shown by using a finitary logical description of the two inverse limit \(\lambda\)-models, obtained by defining two intersection type assignment systems. Therefore, the characterization of the above nine properties can be stated equivalently as follows: a term satisfies one of the nine properties if, and only if, it has a certain type in one of the above mentioned type assignment systems. The novelty of the approach consists in the characterization of all nine computational properties of \(\lambda\)-terms by means of only two \(\lambda\)-models or, equivalently, of only two intersection type assignment systems.

Recommendations

Cites work

Cited in

(11)

This page was built for publication: Behavioural inverse limit \(\lambda\)-models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1434350)