Behavioural inverse limit \(\lambda\)-models (Q1434350)

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.