Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sensible Intersection Type Theories

Mariangiola Dezani-Ciancaglini, Besik Dundua, Paola Giannini, Furio Honsell

TL;DR

This work characterise two classes of intersection type theories which induce sensible filter models and construe intersection type theories as special meet-semilattices and shows that appropriate morphisms, in the opposite category of meet-semilattices, preserve sensibility of the induced lambda-models.

Abstract

Finitary/static semantics in the form of intersection type assignments have become a paradigm for analysing the fine structure of all sorts of lambda-models. The key step is the construction of a filter model isomorphic to a given lambda-model. A property of great interest of filter lambda-models is sensibility, i.e. the interpretation of all unsolvable terms is the least element. The flexibility of intersection type assignments derives from their parametrisation on intersection type theories. We construe intersection type theories as special meet-semilattices and show that appropriate morphisms, in the opposite category of meet-semilattices, preserve sensibility of the induced lambda-models. Interestingly the set of saturated sets together with the set of lambda-terms is such a meet-semilattice, thus showing that arguments based on Tait-Girards's computability amount to the construction of a morphism. We characterise two classes of intersection type theories which induce sensible filter models. The first is non-effective while the second is effective and it amounts to the generalisation of Mendler's criterion to intersection types and head normalising terms. The complete characterisation of sensible filter models however still escapes.

Sensible Intersection Type Theories

TL;DR

This work characterise two classes of intersection type theories which induce sensible filter models and construe intersection type theories as special meet-semilattices and shows that appropriate morphisms, in the opposite category of meet-semilattices, preserve sensibility of the induced lambda-models.

Abstract

Finitary/static semantics in the form of intersection type assignments have become a paradigm for analysing the fine structure of all sorts of lambda-models. The key step is the construction of a filter model isomorphic to a given lambda-model. A property of great interest of filter lambda-models is sensibility, i.e. the interpretation of all unsolvable terms is the least element. The flexibility of intersection type assignments derives from their parametrisation on intersection type theories. We construe intersection type theories as special meet-semilattices and show that appropriate morphisms, in the opposite category of meet-semilattices, preserve sensibility of the induced lambda-models. Interestingly the set of saturated sets together with the set of lambda-terms is such a meet-semilattice, thus showing that arguments based on Tait-Girards's computability amount to the construction of a morphism. We characterise two classes of intersection type theories which induce sensible filter models. The first is non-effective while the second is effective and it amounts to the generalisation of Mendler's criterion to intersection types and head normalising terms. The complete characterisation of sensible filter models however still escapes.
Paper Structure (3 sections, 2 theorems, 1 equation)

This paper contains 3 sections, 2 theorems, 1 equation.

Table of Contents

  1. Introduction
  2. $\lambda$-calculus
  3. Intersection Types and Filter Models

Key Result

Proposition 2.5

Every $\lambda$-term is $\text{either of the form }\lambda \overrightarrow x.x M_1\cdots M_m \text{ or of the form } \lambda \overrightarrow x.(\lambda x.N)P M_1\cdots M_m$ where $m\geq 0$.

Theorems & Definitions (8)

  • Definition 2.1: $\lambda$-terms B85
  • Definition 2.2: $\beta$-rule and $\beta$-reduction B85
  • Definition 2.3: Solvable and unsolvable $\lambda$-terms B85
  • Definition 2.4: Head normal form and head redex B85
  • Proposition 2.5: Shape of $\lambda$-terms B85
  • Definition 2.6: Head reduction B85
  • Theorem 2.7: B85
  • Definition 3.1: Intersection Type Theories