Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia Likavec. Behavioural inverse limit lambda-models. Electronic Notes in Theoretical Computer Science, 2004. To appear.

We construct two inverse limit lambda-models which completely characterise sets of terms with similar computational behaviours: the sets of normalising, head normalising, weak head normalising lambda-terms, those corresponding to the persistent versions of these notions, and the sets of closable, closable normalising, and closable head normalising lambda-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: Lambda calculus, intersection types, models of lambda calculus, Stone dualities, reducibility method

Back