Unsolvable Terms in Filter Models (Invited Talk)

Dezani-Ciancaglini, Mariangiola; Giannini, Paola; Honsell, Furio

doi:10.4230/LIPIcs.FSCD.2025.3

Unsolvable Terms in Filter Models

Mariangiola Dezani-Ciancaglini

Dipartimento di Informatica, Università di Torino, Italy Paola Giannini

DiSSTE, Università del Piemonte Orientale, Vercelli, Italy Furio Honsell

Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Università di Udine, Italy

Abstract

Intersection type theories (itt’s) and filter models, i.e. $\lambda$ -calculus models generated by itt’s, are reviewed in full generality. In this framework, which subsumes most $\lambda$ -calculus models in the literature based on Scott-continuous functions, we discuss the interpretation of unsolvable terms. We give a necessary, but not sufficient, condition on an itt for the interpretation of some unsolvable term to be non-trivial in the filter model it generates. This result is obtained building on a type theoretic characterisation of the fine structure of unsolvables.

Keywords and phrases:

\lambda

-calculus, Intersection Types, Unsolvable Terms, Filter Models

DOI:

10.4230/LIPIcs.FSCD.2025.3

Category:

Invited Talk

Funding:

Paola Giannini: This original research has the financial support of the Università del Piemonte Orientale.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Type theory

Event:

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Editors:

Maribel Fernández

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

The present paper has a remote companion in [19], a paper written by two of the present authors more than 40 years ago, which first generalised the momentous idea of filter model and finitary intersection type assignment system introduced in [12]. In almost half a century of research on $\lambda$ -calculus huge developments of these ideas have been carried out by the scientific community. Numberless papers have been published capturing many different kinds of properties of $\lambda$ -terms by means of intersection types, see e.g. [13, Section 17.2]. Most notably, Abramsky [1] fully clarified and further generalised the connections between $\lambda$ -models and intersection types in terms of Stone Duality. Finitary/static semantics in the form of a type-assignments have become a paradigm for analysing the fine structure of all sorts of $\lambda$ -models, e.g. qualitative $\lambda$ -models [38], quantitative $\lambda$ -models [20, 31], game $\lambda$ -models [28]. Finally, quite a few papers have been also devoted to exploring the limits of this very paradigm, e.g. [37].

Filter models are useful since the interpretation of a $\lambda$ -term is determined by all the types which can be statically assigned to it, see Definition 32. This finitary approximation of the interpretation of $\lambda$ -terms then permits to fully exploit all the machinery of proof theory in semantics, thus providing powerful technical results on type assignment systems such as Inversion, Lemma 19, or Subject Reduction, Theorem 21. The latter is at the root of the well known ditto “Typed programs cannot go wrong”. Filter models are also very flexible, since they capture many different semantic understandings of $\lambda$ -calculus. There are filter models for lazy $\lambda$ -calculus, filter models isomorphic to graph models and to inverse limit models [13, Chapter 16]. Clearly, the paramount theoretical importance of $\lambda$ -calculus lies in that it models recursive functions [11, Theorem 8.4.13]. Very few people still challenge Church’s Thesis, although Gödel himself, in one of his last published works [33, page 306] raises an intriguing doubt. What is the need, therefore, of yet another paper on such a topic?

There are two distinguished classes of pure $\lambda$ -terms: solvable terms and its complement, the unsolvable terms [11, Definition 2.2.10]. Solvable terms have many features which derive from their computational behaviour [11, Chapter 8]. They are the largest recursively enumerable set closed under $\beta$ -conversion, while the set of unsolvable terms is computationally as intractable as it can possibly be. $\lambda$ -calculus is considered the paradigm of functional programming essentially via solvable terms.

The reason for yet anther paper on filter models and intersection type assignment systems lies in that, as a matter of fact, unsolvable terms have been largely disregarded in the literature. Actually only a dozen or so of families of unsolvable terms have been explicitly considered. So, slightly perturbing the title of a well know work of Girolamo Saccheri, we could call the present paper “Insolvabilia ab omni nævo vindicati”.

The property of an unsolvable term which has been traditionally studied is whether it can be consistently equated to an arbitrary closed $\lambda$ -term [40], i.e. if it is easy. Other interesting subsets of unsolvable terms are zero terms, i.e. terms which do not reduce to an abstraction, and mute terms, i.e. those zero terms which do not reduce to the application of a zero term to another $\lambda$ -term [15]. None of these properties is obviously r.e..

The structure of solvable terms is well represented by Böhm trees [11, Chapter 10], which permit to study syntactic properties of $\lambda$ -terms such as separability [11, Sections 10.4 and 10.5] and invertibility [11, Section 21.2]. In such trees an unsolvable term is represented by a leaf labelled $\bot$ . Lévy-Longo trees [43, 44] refine Böhm trees in that only zero terms are represented by leaves labelled $\bot$ . In turn Berarducci trees [15] refine Lévy-Longo trees in that only mute terms are represented by leaves labelled $\bot$ .

Characterisations of unsolvable terms traditionally refer to their observational behaviour. The only characterisation, to our knowledge, that tries to analyse the internal structure of an unsolvable term was proposed by Kerth in [41]. He conjectured that each unsolvable term has an infinite reduction in which some of its subterms in specific key positions are solvable, see Definition 11. This conjecture was generalised and proved by David [23]. Kerth used this property of unsolvable terms for proving that certain graph and stable models are sensible, i.e. they equate all unsolvable terms. Crucial for his analysis is the notion of critical sequence for a graph or stable model [41, Definition 6.2].

In the present paper we discuss filter models by means of the general notion of intersection type theory (itt), see Definition 17. An itt can come with peculiar axioms, rules or may satisfy special conditions. Each itt uniformly induces a type assignment system, see Definition 18, and uniformly generates a filter model, see Definition 32. We tailor the definition of critical sequence to an itt, see Definition 38. We use Kerth/David characterisation of unsolvable terms for showing that, if the interpretation of some unsolvable term in a filter model is different from the bottom element, then the itt which generates the filter model has a critical sequence. Finally, we show some examples of sensible itt’s with critical sequences and we give a condition ensuring the absence of critical sequences in itt’s.

We hope that the present paper will stimulate future research on the still mysterious nature of unsolvable terms, possibly leading to a complementary version to Church’s Thesis as far as non-termination is concerned.

Outline.

In Section 2 we recall the basic notions of $\lambda$ -calculus and Kerth/David characterisation of unsolvable terms. In Section 3 we introduce in full generality filter models over itt’s. Our main contribution deals with the presence/absence of critical sequences in various classes of filter models, see Sections 4 and 5. We conclude with some pointers to the literature and we discuss future work.

2 $\lambda$ -calculus

2.1 Standard Notions and Results

In this subsection we recall some basic notions and properties of untyped $\lambda$ -calculus following Chapters 2, 3, and 8 of [11]. Readers familiar with $\lambda$ -calculus can skip this subsection.

We start by defining $\lambda$ -terms and $\beta$ -reduction.

Definition 1 ( $\lambda$ -terms [11, Definition 2.1.1]).

The set $\mathrm{\Lambda}$ of pure $\lambda$ -terms is defined by:

M::=x\mid\lambda x.M\mid MM.

We write $\lambda$ -terms with the usual notational conventions. In particular we write $\lambda\overrightarrow{x}.M$ as short for $\lambda x_{1}\cdots x_{n}.M$ assuming $\overrightarrow{x}=x_{1}\cdots x_{n}$ for $n\in{\mathbb{N}}$ . Free and bound occurrences of variables are defined in the standard way. In particular we assume Barendregt’s convention, i.e. that different variables have different names [11, Convention 2.1.12]. It is handy and standard to associate names to some closed $\lambda$ -terms (combinators) [11, Definition 2.1.17(ii)]. In the following we will freely use the combinators below.

Definition 2.

We define ${\bf I}=\lambda x.x$ , ${\bf K}=\lambda xy.x$ , ${\bf B}=\lambda xyz.x(yz)$ , ${\boldsymbol{\Omega}_{2}}=\lambda x.xx$ , ${\boldsymbol{\Omega}_{3}}=\lambda x.xxx$ , ${\bf A}=\lambda xy.y(xxy)$ .

Definition 3 ( $\beta$ -rule and $\beta$ -reduction [11, Definitions 2.1.15, 3.1.3 and 3.1.5]).

1.

The $\beta$ -rule replaces $(\lambda x.M)N$ with $M[x:=N]$ , where $M[x:=N]$ denotes the $\lambda$ -term obtained by the (capture free) substitution of $x$ by $N$ in $M$ .
2.

The one step $\beta$ -reduction $\to_{\beta}$ is defined as the contextual closure of the $\beta$ -rule.
3.

The $\beta$ -reduction $\to^{\ast}_{\beta}$ is defined as the reflexive and transitive closure of $\to_{\beta}$ .
4.

The $\beta$ -convertibility is defined as the equivalence relation generated by $\to^{\ast}_{\beta}$ .

Crucial to our development are the notions of solvability and unsolvability of $\lambda$ -terms.

Definition 4 (Solvable and unsolvable $\lambda$ -terms [11, Definition 2.2.10]).

1.

A $\lambda$ -term $M$ is solvable if there are $n$ $\lambda$ -terms $N_{1},\ldots,N_{n}$ such that

$(\lambda\overrightarrow{x}.M)N_{1}\ldots N_{n}\to^{\ast}_{\beta}{\bf I},$

where $\overrightarrow{x}$ are the variables which occur free in $M$ .
2.

A $\lambda$ -term is unsolvable if it is not solvable.

As in [41] our study of unsolvable terms is based on the notion of head reduction.

Definition 5 (Head normal form and head redex [11, Definition 8.3.9]).

1.

If $M=\lambda\overrightarrow{x}.xM_{1}\cdots M_{m}$ , then $M$ is in head normal form and $x$ is the head variable of $M$ .
2.

If $M=\lambda\overrightarrow{x}.(\lambda x.N)PM_{1}\cdots M_{m}$ , then $(\lambda x.N)P$ is the head redex of $M$ .

Every $\lambda$ -term either is in head normal form or has a head redex.

Proposition 6 (Shape of $\lambda$ -terms [11, Corollary 8.3.8]).

Every $\lambda$ -term is either of the form $\lambda\overrightarrow{x}.xM_{1}\cdots M_{m}$ or of the form $\lambda\overrightarrow{x}.(\lambda x.N)PM_{1}\cdots M_{m}$ , where $m\geq 0$ .

Definition 7 (Head reduction [11, Definition 8.3.10]).

We write $M\to_{h}N$ if $N$ is obtained from $M$ by reducing its head redex. The head reduction of $M$ is the finite or infinite sequence of terms $M_{0}$ , $\dots$ , $M_{n}$ , $\dots$ such that $M=M_{0}$ and $M_{n}\to_{h}M_{n+1}$ with $n\in\mathbb{N}$ .

We use $\to^{\ast}_{h}$ to denote the reflexive and transitive closure of $\to_{h}$ .

In our development we take advantage from the characterisation of unsolvability by means of head reduction.

Theorem 8 ([11, Fact 2.2.12]).

A $\lambda$ -term $M$ is unsolvable iff its head reduction is infinite.

2.2 Notions and Results on Unsolvable Terms

This subsection is devoted to the characterisation of unsolvability by means of decorations (Definition 11), first conjectured by Kerth in [41], and then proved by David in [23], see Theorem 13.

Following [41] we start defining the descendants and the arguments of $\lambda$ -terms.

Definition 9 (Descendants of a $\lambda$ -term [41, Definition 5.1]).

1.

Let $R=(\lambda x.N)P$ be a redex in $M$ and $Q$ be a subterm of $M$ without occurrences of the bound $x$ . Let $M^{\prime}$ be obtained by reducing $R$ in $M$ and let $Q_{1},\ldots,Q_{m}$ be the corresponding occurrences of $Q$ in $M^{\prime}$ . Then each $Q_{i}$ for $1\leq i\leq m$ is a child in $M^{\prime}$ of the occurrence of $Q$ in $M$ .
2.

The relation parent is the converse of the relation child.
3.

The relation descendant is the transitive closure of the relation child.
4.

The relation ancestor is the transitive closure of the relation parent.

For example consider the reduction $(\lambda xy.xxy)NP\to_{\beta}(\lambda y.NNy)P\to_{\beta}NNP$ and let $M=(\lambda xy.xxy)NP$ , $M^{\prime}=(\lambda y.NNy)P$ and $M^{\prime\prime}=NNP$ . Then the two concurrences of $N$ in $M^{\prime}$ are the children of the occurrence of $N$ in $M$ , which in turn is the ancestor of each of the two occurrences of $N$ in $M^{\prime\prime}$ , which are therefore its descendants. The occurrence of $P$ in $M^{\prime}$ is the child of the one in $M$ and the occurrence of $P$ in $M^{\prime\prime}$ is the child of the one in $M^{\prime}$ . Neither the term $\lambda xy.xxy$ nor its subterms $\lambda y.xxy$ and $x x y$ in $M$ have a child in $M^{\prime}$ . The subterm $N N$ in $M^{\prime}$ does not have a parent in $M$ , while $N N$ in $M^{\prime}$ is the parent of $N N$ in $M^{\prime\prime}$ .

It is easy to verify that the parent and all its children are identical and that the parent, if any, is unique.

Definition 10 (Arguments [41, Definition 5.2]).

If $M=N_{0}N_{1}\ldots N_{m}$ , then $N_{1},\ldots,N_{m}$ are the arguments of $N_{0}$ in $M$ .

Definition 11 (Decoration of head reduction [41, Definition 5.3]).

A decoration of the head reduction of a $\lambda$ -term $M_{0}$ is a sequence of pairs $\langle M_{n},N^{n}_{0}\rangle$ such that for all $n\in\mathbb{N}$ :

1.

$M_{n}\to^{\ast}_{h}M_{n+1}$ ;
2.

$M_{n}=\lambda\overrightarrow{x}^{n}.N^{n}_{0}N_{1}^{n}\dots N_{m_{n}}^{n}$ ;
3.

$N^{n}_{0}$ is solvable;
4.

$N^{n+1}_{0}$ is a descendant of $N^{n}_{i_{n}}$ for some $i_{n}$ $(1\leq i_{n}\leq m_{n})$ .

Clearly for a decoration to exist the initial term $M_{0}$ in the above definition needs be unsolvable by condition (4). The notion of decoration is quite subtle and requires some discussion, which we do by way of examples.

Example 12.

1.

The $\lambda$ -term ${\bf I}({\bf A}{\bf A}{\bf I})$ is unsolvable since

${\bf I}({\bf A}{\bf A}{\bf I})\to_{h}{\bf A}{\bf A}{\bf I}\to^{\ast}_{h}{\bf I% }({\bf A}{\bf A}{\bf I})\to_{h}{\bf A}{\bf A}{\bf I}\to^{\ast}_{h}\cdots,$

but the $\lambda$ -term itself ${\bf I}({\bf A}{\bf A}{\bf I})$ does not have a decoration, since the only argument of $\bf I$ is ${\bf A}{\bf A}{\bf I}$ , which is unsolvable. However the $\lambda$ -term ${\bf A}{\bf A}{\bf I}$ , appearing in the infinite reduction above, does have a decoration, namely $\langle M_{n},N^{n}_{0}\rangle$ , where $M_{n}={\bf A}{\bf A}{\bf I}$ and $N^{n}_{0}={\bf A}$ for all $n\in\mathbb{N}$ .
2.
In general the head reduction of an unsolvable term can allow for more than one decoration. For example, if ${\bf D}=\lambda xyz.yz(xxyz)$ , then some of the decorations of ${\bf D}{\bf D}{\bf I}{\bf I}$ are:
- $\blacksquare$
  
  $M_{n}={\bf D}{\bf D}{\bf I}{\bf I}$ , $N^{n}_{0}={\bf D}$ , and
- $\blacksquare$
  
  $M_{0}={\bf D}{\bf D}{\bf I}{\bf I}$ , $N^{0}_{0}={\bf D}$ , $M_{n+1}={\bf I}{\bf I}({\bf D}{\bf D}{\bf I}{\bf I})$ , $N^{n+1}_{0}={\bf I}$ , and
- $\blacksquare$
  
  $M_{2n}={\bf D}{\bf D}{\bf I}{\bf I}$ , $N^{2n}_{0}={\bf D}$ , $M_{2n+1}={\bf I}{\bf I}({\bf D}{\bf D}{\bf I}{\bf I})$ , $N^{n+1}_{0}={\bf I}$
for all $n\in\mathbb{N}$ .
3.

The $N^{n}_{0}$ ’s in a decoration are uniquely determined by the first component, however $N^{n+1}_{0}$ is not always the first solvable descendant of an argument of $M^{n}$ to appear in the head position of the infinite reduction. This latter term might even be a descendant of the same ancestor and yet not be it, as in the following case. Let ${\bf G}=\lambda xy.xxyxy$ , then ${\bf IGIG}\to_{h}{\bf GIG}\to^{\ast}_{h}{\bf IIGIG}\to_{h}{\bf IGIG}$ . Consider the decoration $\langle\bf IGIG,\bf I\rangle$ . All ${\bf I}$ in ${\bf IIGIG}$ have the same parent, but the one appearing as the second component in the decoration is not the ${\bf I}$ in head position in ${\bf IIGIG}$ .

Theorem 13 (Characterisation of unsolvability by decorations [23, Theorem 2]).

Let $M$ be an unsolvable term. Then there is $M_{0}$ such that $M\to^{\ast}_{\beta}M_{0}$ and the head reduction of $M_{0}$ has a decoration.

We recall from [41] some properties of the subterms of unsolvable terms in Lemma 15. This lemma uses the following notions of head closed $\lambda$ -term and head order.

Definition 14 (Head closed $\lambda$ -term and head order [41, Definition 6.1]).

1.

A $\lambda$ -term in head normal form is head closed if its head variable is bound.
2.

If $M=\lambda x_{1}\ldots x_{n}.x_{i}N_{1}\ldots N_{m}$ is head closed, then $i$ is the head order of $M$ .

Lemma 15 ([41, Lemma 6.5]).

Let $M=\lambda\overrightarrow{x}.N_{0}N_{1}\dots N_{m}$ be unsolvable.

1.
If $N_{0}$ is solvable, then
1. (a)
  
  the head normal form of $N_{0}$ is head closed and its head order $i$ satisfies $i\leq m$ ;
2. (b)
  
  the first descendant of some $N_{j}$ , $1\leq j\leq m$ , appearing in head position during the head reduction of $M$ is a descendant of $N_{i}$ .
2.

If $N_{0}$ is unsolvable, then no descendant of some $N_{j}$ , $1\leq j\leq m$ , appears in head position during the head reduction of $M$ .

It is also useful to specify $\lambda$ -terms which arise when reducing the terms in the decoration sequence, but which may not appear themselves in the decoration sequence.

Lemma 16.

In a decoration $\langle M_{n},N^{n}_{0}\rangle$ each $N^{n}_{0}$ has a head closed normal form $N_{n}$ and $M_{n}\to^{\ast}_{h}\lambda\overrightarrow{y}.N^{n}_{i_{n}}\overrightarrow{R}$ , where $i_{n}$ is the head order of $N_{n}$ and $N^{n}_{i_{n}}$ has a head closed normal form.

Proof.

By definition of decoration $M_{n}=\lambda\overrightarrow{x}^{n}.N_{0}^{n}N_{1}^{n}\dots N_{m_{n}}^{n}$ and $N^{n}_{0}$ is solvable. By Lemma 15(1a) $N^{n}_{0}$ has a head closed normal form $N_{n}$ . Let $N_{n}=\lambda\overrightarrow{z}^{n}.z_{i_{n}}R_{1}\dots R_{p}$ . By definition of head reduction, if $q$ is the length of $\overrightarrow{z}^{n}$ ,

\begin{array}[]{lll}M_{n}&\to^{\ast}_{h}&\lambda\overrightarrow{x}^{n}.N_{n}N_% {1}^{n}\dots N_{m_{n}}^{n}\\ &\to^{\ast}_{h}&\lambda\overrightarrow{x}^{n}.(\lambda z_{i_{n}+1}\ldots z_{q}% .N^{n}_{i_{n}}R^{\prime}_{1}\dots R^{\prime}_{p})N^{n}_{i_{n}+1}\dots N_{m_{n}% }^{n}\\ &\to^{\ast}_{h}&\lambda\overrightarrow{x}^{n}z_{m_{n}+1}\ldots z_{q}.N^{n}_{i_% {n}}R^{\prime\prime}_{1}\dots R^{\prime\prime}_{p}N^{n}_{q+1}\ldots N_{m_{n}}^% {n},\end{array}

where $R^{\prime}_{i}=R_{i}[z_{j}:=N^{n}_{j}\mid 1\leq j\leq i_{n}]$ , $R^{\prime\prime}_{i}=R_{i}[z_{j}:=N^{n}_{j}\mid 1\leq j\leq min(q,m_{n})]$ . In the final term of the reduction we have used a somewhat not standard notation, whereby if $q\leq m_{n}$ then no $z_{j}$ ’s are abstracted and if $m_{n}\leq q$ then no $N^{n}_{j}$ ’s appear. By Lemma 15(2) and the definition of decoration $N^{n}_{i_{n}}$ is solvable. By Lemma 15(1a) $N^{n}_{i_{n}}$ has a head closed normal form. $\hfill\blacktriangleleft$

For example, consider the decoration $\langle({\bf I}{\bf A})({\bf I}{\bf A})({\bf I}{\bf I}),{\bf I}{\bf A}\rangle$ , we have that the head normal form of ${\bf I}{\bf A}$ is ${\bf A}$ which has head order 2 and $({\bf I}{\bf A})({\bf I}{\bf A})({\bf I}{\bf I})\to^{\ast}_{h}{\bf I}{\bf I}((% {\bf I}{\bf A})({\bf I}{\bf A})({\bf I}{\bf I}))$ , where the term ${\bf I}{\bf I}$ is a descendant of the second argument of ${\bf I}{\bf A}$ and has the obvious normal form ${\bf I}$ . Notice that none of the head normal forms, nor the intermediate term appears in the decoration itself, yet the head order of their head normal form matters.

3 Intersection Types and Filter Models

This section is devoted to the definitions of intersection types, type theories, type assignment systems and filter models.

Up to Definition 18 (included) we essentially follow Sections 13.1 and 13.2 of [13]. The only differences are that, in defining intersection types and subtyping, we require the constant ${\sf U}$ , which is optional in [13], and our subtyping relation has the additional Axiom ( ${\sf U}_{top}$ ).

Definition 17 (Intersection Type Theories).

1.

Given a set of constants $\mathbb{A}$ and a distinguished constant ${\sf U}$ , the set $\mathbb{T}_{\mathbb{A}}$ of intersection types over $\mathbb{A}\cup\{{\sf U}\}$ is generated by the grammar:

$A,B::={\sf c}\mid{\sf U}\mid A\to A\mid A\cap A,$

where ${\sf c}\in\mathbb{A}$ .
2.

A subtyping relation $\leq$ is a binary relation on $\mathbb{T}_{\mathbb{A}}$ closed under the following axioms and rules:
3.

An intersection type theory (itt) ${\cal T}$ is determined by a set of type constants $\mathbb{A}$ and a subtyping relation on the set $\mathbb{T}_{\mathbb{A}}$ , i.e. ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ .

We adopt the convention that $\cap$ has precedence over $\to$ . We write $A\sim_{\cal T}B$ as short for $A\leq_{\cal T}B$ and $A_{\cal T}\!\!\geq B$ . The above rules permit to show that $\cap$ is a congruence w.r.t. $\sim_{\cal T}$ and moreover that it is idempotent, commutative and associative with neutral element ${\sf U}$ . We assume that $\bigcap_{i\in\emptyset}A_{i}={\sf U}$ .

Definition 18 (Type Assignment System).

The intersection type assignment system induced by an itt ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ is a formal system deriving judgements of the shape $\Gamma\vdash_{\cal T}M:A$ , where $A\in\mathbb{T}_{\mathbb{A}}$ and a basis $\Gamma$ is a finite mapping from term variables to types in $\mathbb{T}_{\mathbb{A}}$ :

\Gamma::=\emptyset\mid\Gamma,x:A.

The axioms and rules of the type system are the following

It is easy to verify that the following rules are admissible

where $x\not\in\Gamma$ is short for $x$ does not occur in $\Gamma$ .

The main properties of intersection type assignment systems are the Inversion Lemma and Subject Expansion, which are proved by induction on type derivations.

Lemma 19 (Inversion Lemma [13, Theorem 14.1.1]).

1.

If $\Gamma\vdash_{\cal T}x:A$ and $A\nsim_{\cal T}{\sf U}$ , then $\Gamma(x)\leq_{\cal T}A$ ;
2.

If $\Gamma\vdash_{\cal T}MN:A$ and $A\nsim_{\cal T}{\sf U}$ , then there are $I$ and $B_{i}$ , $C_{i}$ for $i\in I$ such that $\bigcap_{i\in I}C_{i}\leq_{\cal T}A$ and $\Gamma\vdash_{\cal T}M:B_{i}\to C_{i}$ and $\Gamma\vdash_{\cal T}N:B_{i}$ for all $i\in I$ ;
3.

If $\Gamma\vdash_{\cal T}\lambda x.M:A$ , then there are $I$ and $B_{i}$ , $C_{i}$ for $i\in I$ such that $\bigcap_{i\in I}(B_{i}\to C_{i})\leq_{\cal T}A$ and $\Gamma,x:B_{i}\vdash_{\cal T}M:C_{i}$ for all $i\in I$ .

Theorem 20 (Subject Expansion [13, Corollary 14.2.5(ii)]).

$M\to_{\beta}M^{\prime}$ and $\Gamma\vdash_{\cal T}M^{\prime}:A$ imply $\Gamma\vdash_{\cal T}M:A$ .

Crucial is also the property of Subject Reduction, which however holds only with a proviso.

Theorem 21 (Subject Reduction [13, Proposition 14.2.1(ii)]).

M\to_{\beta}M^{\prime}\text{ and }\Gamma\vdash_{\cal T}M:A\text{ imply }\Gamma% \vdash_{\cal T}M^{\prime}:A

if and only if

\Gamma\vdash_{\cal T}\lambda x.N:B\to C\text{ implies }\Gamma,x:B\vdash_{\cal T% }N:C.

In fact, not all type systems induced by itt’s enjoy Subject Reduction. For example let ${\cal T}_{0}=\langle\{{\sf c}_{0},{\sf c}_{1}\},\leq_{{\cal T}_{0}}\rangle$ , where ${\cal T}_{0}$ has only the axiom ${\sf c}_{0}\to{\sf c}_{0}\leq{\sf c}_{1}\to{\sf c}_{0}$ , then $\vdash_{{\cal T}_{0}}\lambda x.x:{\sf c}_{1}\to{\sf c}_{0}$ , but $x:{\sf c}_{1}\not\vdash_{{\cal T}_{0}}x:{\sf c}_{0}$ . Subject Reduction fails since $y:{\sf c}_{1}\vdash_{{\cal T}_{0}}(\lambda x.x)y:{\sf c}_{0}$ , but $y:{\sf c}_{1}\not\vdash_{{\cal T}_{0}}y:{\sf c}_{0}$ .

A necessary but not sufficient condition for Subject Reduction is target soundness.

Definition 22 (Target soundness).

An itt ${\cal T}$ is target sound if when an arrow type is equivalent to ${\sf U}$ then its target is equivalent to ${\sf U}$ , videlicet if ${\sf U}\leq_{\cal T}B\to A$ then ${\sf U}\leq_{\cal T}A$ , or equivalently Rule ( ${\sf U}\leq$ ) in Figure 1 holds in ${\cal T}$ .

Proposition 23.

If the itt ${\cal T}$ satisfies Subject Reduction, then ${\cal T}$ is target sound.

Proof.

Assume by contradiction that ${\sf U}\leq_{\cal T}B\to A$ , but ${\sf U}\not\leq_{\cal T}A$ . Then we have that from the valid judgement $x:B\vdash_{\cal T}\lambda z.y:{\sf U}$ we can derive $x:B\vdash_{\cal T}\lambda z.y:B\to A$ and hence also $x:B\vdash_{\cal T}(\lambda z.y)x:A$ , but if Subject Reduction holds we would then have also that $x:B\vdash_{\cal T}y:A$ , which contradicts Lemma 19(1). $\hfill\blacktriangleleft$

A sufficient but not necessary condition for Subject Reduction is $\beta$ -soundness.

Definition 24 ( $\beta$ -soundness [13, Definition 14.1.4]).

An itt ${\cal T}$ is $\beta$ -sound if $A\nsim_{\cal T}{\sf U}$ and $\bigcap_{i\in I}(B_{i}\to A_{i})\leq_{\cal T}B\to A$ imply that there is $J\subseteq I$ such that $B\leq_{\cal T}\bigcap_{j\in J}B_{j}$ and $\bigcap_{j\in J}A_{j}\leq_{\cal T}A$ .

For example the itt ${\cal T}_{1}=\langle\{{\sf c}_{0},{\sf c}_{1}\},\leq_{{\cal T}_{1}}\rangle$ , where $\leq_{{\cal T}_{1}}$ has no other axioms and rules, is $\beta$ -sound. Instead the itt ${\cal T}_{0}$ defined above is not $\beta$ -sound. The itt ${\cal T}_{0}$ can be made $\beta$ -sound by adding the axiom ${\sf c}_{1}\leq{\sf c}_{0}$ . Two itt’s which are not $\beta$ -sound but still satisfy Subject Reduction are defined in [19, 4].

In the following definitions we introduce some important classes of itt’s.

Definition 25 (Lazy condition).

An itt ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ satisfies the lazy condition if

{\sf U}\nsim_{\cal T}A\to{\sf U}

for all

A\in\mathbb{T}_{\mathbb{A}}

.

Definition 26 (Set condition).

An itt ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ satisfies the set condition if

\bigcap_{i\in I}A_{i}\leq_{\cal T}B_{1}\to\ldots\to B_{n}\to C

with

C\nsim_{\cal T}{\sf U}

implies

A_{j}\sim_{\cal T}B_{1}\to\ldots\to B_{n}\to D

for some $j\in I$ and some $D\nsim_{\cal T}{\sf U}$ such that $C\cap D\sim_{\cal T}C$ .

The motivation behind the introduction of these two conditions, as well as their names, will become apparent in the examples. Lazy filter models are generated by theories satisfying the former condition. On the other hand, all graph models in the literature are isomorphic to filter models satisfying the latter condition. Graph models are set-theoretic, rather than order theoretic, since they arise essentially as powersets of a universal set, which is the least set containing a set of atoms and closed under the operation of forming new elements out of pairs of finite sets of elements and elements. There is no partial order on the elements of the universal set. In the corresponding itt’s atoms are constants and pairs are arrow types, set formation is intersection, and membership is reverse subtyping. The set condition reflects subtyping as reverse membership on arrow types, allowing for a small perturbation on the target of the arrow in order to account for possible intersections on the target arrow types, which Axiom ( $\to^{\sim}$ ) can split.

Figure 1: Some axioms and rules for itt’s.

Definition 27.

Consider axioms and rules in Figure 1.

1.

An itt is lazy if it satisfies the lazy condition and at least Axiom ( $\to\cap$ ) and Rule ( $\to$ ) hold.
2.

An itt is ${\sf U}$ -sound if at least Axiom ( $\to{\sf U}$ ) and Rule ( ${\sf U}\leq$ ) hold.
3.

An itt is set-like if it satisfies the set condition and at least Axioms ( $\to{\sf U}$ ), ( $\to\cap$ ) and Rule ( $\to^{\sim}$ ) hold.
4.

An itt is $\to$ -sound if it satisfies at least Axioms ( $\to{\sf U}$ ), ( $\to\cap$ ), and Rules ( $\to$ ), ( ${\sf U}\leq$ ) hold.

Notice that a lazy or set-like itt ${\cal T}$ satisfies the target condition of Definition 22. Let ${\cal T}$ be lazy. By Rule ( $\to$ ), we have that $B\to A\leq_{\cal T}B\to{\sf U}$ so if ${\sf U}\nsim_{\cal T}B\to{\sf U}$ , also ${\sf U}\leq_{\cal T}B\to A$ is ruled out. Let ${\cal T}$ be set-like. We have that if $B\to A\sim_{\cal T}{\sf U}$ , for $A\nsim_{\cal T}{\sf U}$ , we have also $B\to{\sf U}\leq_{\cal T}B\to A$ , which by the set condition implies ${\sf U}\leq_{\cal T}A$ against the hypothesis. Notice furthermore, that a set-like or $\to$ -sound itt is ${\sf U}$ -sound.

Some comments on the rules in Figure 1 are in order. Rule ( $\to$ ) amounts to the covariant, contravariant behaviour of $\to$ . Notice that it is not the case, that an itt satisfies either the lazy condition or Axiom ( $\to{\sf U}$ ), see Example 35(10). Rule ( $\to^{\sim}$ ) makes $\sim$ a congruence, while Axiom ( $\to\cap$ ) expresses that the glb nature of $\cap$ is preserved covariantly.

The set condition and $\to$ -soundness imply interesting properties for the induced type assignment systems. Clearly the set condition implies $\beta$ -soundness. Theorem 14.2.8 of [13] shows that $\to$ -soundness is a sufficient and necessary condition for ${\cal T}$ in order to have type preservation under $\eta$ -reduction, i.e. that $\Gamma\vdash_{\cal T}\lambda x.Mx:A$ implies $\Gamma\vdash_{\cal T}M:A$ , when $x$ does not occur in $M$ .

In the present paper a key role is played by the following lemma, characterising the types which we can derive in type systems induced by set-like or $\to$ -sound itt’s for the subterms of a given $\lambda$ -term. We use $\overrightarrow{x:A}$ as short for $x_{1}:A_{1},\ldots,x_{n}:A_{n}$ .

Lemma 28.

Let ${\cal T}$ be set-like or $\to$ -sound. If $\Gamma\vdash_{\cal T}\lambda\overrightarrow{x}.MN_{1}\ldots N_{m}:A$ with $A\nsim_{\cal T}U$ , then $\Gamma,\overrightarrow{x:B}\vdash_{\cal T}M:C_{1}\to\ldots\to C_{m}\to D$ and $\Gamma,\overrightarrow{x:B}\vdash_{\cal T}N_{i}:C_{i}$ ( $1\leq i\leq m$ ) for some $\overrightarrow{B}$ , $C_{1}$ , $\ldots$ , $C_{m}$ and $D\nsim_{\cal T}U$ .

Proof.

Lemma 19(3) applied to $\Gamma\vdash_{\cal T}\lambda x_{1}\ldots x_{n}.MN_{1}\ldots N_{m}:A$ with $A\nsim_{\cal T}U$ gives $\Gamma,x_{1}:B_{1}^{j}\vdash_{\cal T}\lambda x_{2}\ldots x_{n}.MN_{1}\ldots N_% {m}:A_{1}^{j}$ for some $J_{1}$ , $B_{1}^{j}$ , $A_{1}^{j}$ with $j\in J_{1}$ such that $\bigcap_{j\in J_{1}}(B_{1}^{j}\to A_{1}^{j})\leq_{\cal T}A$ . Axiom ( $\to{\sf U}$ ) with $\bigcap_{j\in J_{1}}(B_{1}^{j}\to A_{1}^{j})\leq_{\cal T}A\nsim_{\cal T}U$ implies $A_{1}^{j^{\prime}}\nsim_{\cal T}U$ for some $j^{\prime}\in J_{1}$ . We set $B_{1}=B_{1}^{j^{\prime}}$ and $A_{1}=A_{1}^{j^{\prime}}$ . By iterating we get $\Gamma,x_{1}:B_{1},\ldots x_{n}:B_{n}\vdash_{\cal T}MN_{1}\ldots N_{m}:A_{n}$ with $A_{n}\nsim_{\cal T}U$ . Let $\overrightarrow{x:B}=x_{1}:B_{1},\ldots x_{n}:B_{n}$ . Lemma 19(2) applied to $\Gamma,\overrightarrow{x:B}\vdash_{\cal T}MN_{1}\ldots N_{m}:A_{n}$ with $A_{n}\nsim_{\cal T}U$ gives

\Gamma,\overrightarrow{x:B}\vdash_{\cal T}MN_{1}\ldots N_{m-1}:C^{\ell}_{m}\to D% ^{\ell}_{m}

and

\Gamma,\overrightarrow{x:B}\vdash_{\cal T}N_{m}:C^{\ell}_{m}

for some $L_{m}$ , $C_{m}^{\ell}$ , $D_{m}^{\ell}$ with $\ell\in L_{m}$ such that $\bigcap_{\ell\in L_{m}}D_{m}^{\ell}\leq_{\cal T}A_{n}$ . The remaining of the proof runs differently for set-like and $\to$ -sound itt’s.

The itt ${\cal T}$ is set-like.

From $\bigcap_{\ell\in L_{m}}D_{m}^{\ell}\leq_{\cal T}A_{n}$ and $A_{n}\nsim{\sf U}$ we get that at least for one $\ell^{\prime}\in L_{m}$ we have $D_{m}^{\ell^{\prime}}\nsim{\sf U}$ and hence $C_{m}^{\ell^{\prime}}\to D_{m}^{\ell^{\prime}}\nsim{\sf U}$ by the remark above that set-like itt’s satisfy the target condition. We put $C_{m}=C_{m}^{\ell^{\prime}}$ and $D_{m}=D_{m}^{\ell^{\prime}}$ . Lemma 19(2) applied to $\Gamma,\overrightarrow{x:B}\vdash_{\cal T}MN_{1}\ldots N_{m-1}:C_{m}\to D_{m}$ with $C_{m}\to D_{m}\nsim_{\cal T}U$ gives

\Gamma,\overrightarrow{x:B}\vdash_{\cal T}MN_{1}\ldots N_{m-2}:C^{\ell}_{m-1}% \to D^{\ell}_{m-1}

and

\Gamma,\overrightarrow{x:B}\vdash_{\cal T}N_{m-1}:C^{\ell}_{m-1}

for some $L_{m-1}$ , $C_{m-1}^{\ell}$ , $D_{m-1}^{\ell}$ with $\ell\in L_{m-1}$ such that $\bigcap_{\ell\in L_{m-1}}D_{m-1}^{\ell}\leq_{\cal T}C_{m}\to D_{m}$ . The set condition implies $D_{m-1}^{\ell^{\prime\prime}}\sim_{\cal T}C_{m}\to D_{m-1}$ for some $\ell^{\prime\prime}\in L_{m-1}$ and $D_{m-1}\nsim{\sf U}$ such that $D_{m}\cap D_{m-1}\sim_{\cal T}D_{m}$ . Putting $C_{m-1}=C^{\ell^{\prime\prime}}_{m-1}$ we can then derive using the typing Rule ( $\leq$ ) and the subtyping Rule ( $\to^{\sim}$ ):

\text{$\Gamma,\overrightarrow{x:B}\vdash_{\cal T}MN_{1}\ldots N_{m-2}:C_{m-1}% \to C_{m}\to D_{m-1}$ and $\Gamma,\overrightarrow{x:B}\vdash_{\cal T}N_{m-1}:C% _{m-1}$}.

We can iterate this argument applying the set condition progressively on longer and longer sequences of arrows, preserving the $C_{m-i}$ ’s and modifying only the final target $D_{m-i-1}$ , thus getting

\Gamma,\overrightarrow{x:B}\vdash_{\cal T}M:C_{1}\to\ldots\to C_{m}\to D_{1}% \text{ and }\Gamma,\overrightarrow{x:B}\vdash_{\cal T}N_{i}:C_{i}\leavevmode% \nobreak\ (1\leq i\leq m).

We conclude putting $D=D_{1}$ .

The itt ${\cal T}$ is $\to$ -sound.

Let $D=A_{n}$ , then $\bigcap_{\ell\in L_{m}}D_{m}^{\ell}\leq_{\cal T}D$ . Using the typing Rule ( $\cap$ I) we derive

\text{$\Gamma,\overrightarrow{x:B}\vdash_{\cal T}MN_{1}\ldots N_{m-1}:\bigcap_% {\ell\in L_{m}}(C^{\ell}_{m}\to D^{\ell}_{m})$ and $\Gamma,\overrightarrow{x:B% }\vdash_{\cal T}N_{m}:\bigcap_{\ell\in L_{m}}C^{\ell}_{m}$}.

The subtyping Rule ( $\to$ ) and Axiom ( $\to\cap$ ) imply $\bigcap_{\ell\in L_{m}}(C^{\ell}_{m}\to D^{\ell}_{m})\leq_{\cal T}\bigcap_{% \ell\in L_{m}}C^{\ell}_{m}\to D$ . Putting $C_{m}=\bigcap_{\ell\in L_{m}}C^{\ell}_{m}$ we derive, using Rule ( $\leq$ ),

\text{$\Gamma,\overrightarrow{x:B}\vdash_{\cal T}MN_{1}\ldots N_{m-1}:C_{m}\to D% $ and $\Gamma,\overrightarrow{x:B}\vdash_{\cal T}N_{m}:C_{m}$}.

Notice that $D\nsim_{\cal T}{\sf U}$ implies $C_{m}\to D\nsim_{\cal T}{\sf U}$ , since $\to$ -sound itt’s are target sound by definition. Thence we can iterate the argument and conclude

\Gamma,\overrightarrow{x:B}\vdash_{\cal T}M:C_{1}\to\ldots\to C_{m}\to D\text{% and }\Gamma,\overrightarrow{x:B}\vdash_{\cal T}N_{i}:C_{i}\leavevmode\nobreak% \ (1\leq i\leq m).\qquad\qquad\

$\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 29.

In the particular case of $m=1$ , in the proof of the above lemma one can use any of the $\ell^{\prime}$ such that $D^{\ell^{\prime}}\nsim_{\cal T}{\sf U}$ , thus avoiding the need for either the set condition or the subtyping Rule ( $\to$ ) and the subtyping Axiom ( $\to\cap$ ). In this way ${\cal T}$ can be only ${\sf U}$ -sound instead of set-like or $\to$ -sound.

In order to discuss $\lambda$ -models over itt’s we recall the definition of $\lambda$ -model. An environment in the set ${\mathcal{D}}$ is a total mapping from term variables to elements of ${\mathcal{D}}$ . Let $\rho$ range over environments. As usual, we denote by $\rho[x:={\sf d}]$ the environment which returns ${\sf d}$ when applied to $x$ and $\rho(y)$ when applied to $y\not=x$ .

Definition 30 ( $\lambda$ -model [13, Definition 16.1.2]).

A $\lambda$ -model is a triple $\langle{\mathcal{D}},\cdot,\llbracket\leavevmode\nobreak\ \rrbracket^{{% \mathcal{D}}}\rangle$ , where $\cdot$ is a binary operation on ${\mathcal{D}}$ (application), $\llbracket\leavevmode\nobreak\ \rrbracket^{{\mathcal{D}}}$ is a mapping from $\lambda$ -terms and environments in ${\mathcal{D}}$ to elements of ${\mathcal{D}}$ (term interpretation), and $\llbracket\leavevmode\nobreak\ \rrbracket^{{\mathcal{D}}}$ satisfies:

1.

$\llbracket x\rrbracket^{{\mathcal{D}}}_{\rho}=\rho(x)$ ;
2.

$\llbracket MN\rrbracket^{{\mathcal{D}}}_{\rho}=\llbracket M\rrbracket^{{% \mathcal{D}}}_{\rho}\cdot\llbracket N\rrbracket^{{\mathcal{D}}}_{\rho}$ ;
3.

$\llbracket\lambda x.M\rrbracket^{{\mathcal{D}}}_{\rho}=\llbracket\lambda y.M[x% :=y]\rrbracket^{{\mathcal{D}}}_{\rho}$ ;
4.

$\forall{\sf d}\in{\mathcal{D}}.\llbracket M\rrbracket^{{\mathcal{D}}}_{\rho[x:% ={\sf d}]}=\llbracket N\rrbracket^{{\mathcal{D}}}_{\rho[x:={\sf d}]}$ implies $\llbracket\lambda x.M\rrbracket^{{\mathcal{D}}}_{\rho}=\llbracket\lambda x.N% \rrbracket^{{\mathcal{D}}}_{\rho}$ ;
5.

$\rho(x)=\rho^{\prime}(x)$ for all variables $x$ which occur free in $M$ implies $\llbracket M\rrbracket^{{\mathcal{D}}}_{\rho}=\llbracket M\rrbracket^{{% \mathcal{D}}}_{\rho^{\prime}}$ ;
6.

$\llbracket\lambda x.M\rrbracket^{{\mathcal{D}}}_{\rho}\cdot{\sf d}=\llbracket M% \rrbracket^{{\mathcal{D}}}_{\rho[x:={\sf d}]}$ .

This definition of $\lambda$ -model was first formulated by Hindley and Longo [34].

We can build $\lambda$ -models whose domains are sets of filters of types according to the following definition.

Definition 31 (Filter [13, Definition 13.4.1]).

Let ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ be an itt and $\mathit{F}\subseteq\mathbb{T}_{\mathbb{A}}$ . The set $\mathit{F}$ is a ${\cal T}$ -filter if:

$\blacksquare$

${\sf U}\in\mathit{F}$ ;
$\blacksquare$

$A,B\in\mathit{F}$ imply $A\cap B\in\mathit{F}$ ;
$\blacksquare$

$A\in\mathit{F}$ and $A\leq_{\cal T}B$ imply $B\in\mathit{F}$ .

We use $\mathit{F}$ and $\mathit{G}$ as metavariables for filters and $\mathcal{F}_{\cal T}$ to denote the set of ${\cal T}$ -filters. We will drop the reference to ${\cal T}$ when clear from the context or irrelevant. If $X\subseteq\mathbb{T}_{\mathbb{A}}$ we denote by $\uparrow_{\cal T}X$ the smallest ${\cal T}$ -filter which contains $X$ . If $X=\{A\}$ we use $\uparrow_{\cal T}A$ as short for $\uparrow_{\cal T}\{A\}$ .

Filters can be endowed with an applicative structure as follows:

Definition 32 (Filter Structure).

Let $\mathbb{E}_{{\cal T}}$ be the set of environments in $\mathcal{F}_{\cal T}$ . The filter structure over ${\cal T}$ is the triple $\langle\mathcal{F}_{\cal T},\cdot,\llbracket\leavevmode\nobreak\ \rrbracket^{% \mathcal{F}_{\cal T}}\rangle$ where

$\blacksquare$

application, $\cdot:\mathcal{F}_{\cal T}\times\mathcal{F}_{\cal T}\to\mathcal{F}_{\cal T}$ , is defined by

$\mathit{F}\cdot\mathit{G}=\{A\mid\exists B\in\mathit{G}.\ B\to A\in\mathit{F}\};$
$\blacksquare$

term interpretation, $\llbracket\leavevmode\nobreak\ \rrbracket^{\mathcal{F}_{\cal T}}:\mathrm{% \Lambda}\times\mathbb{E}_{{\cal T}}\to\mathcal{F}_{\cal T}$ , is defined by

$\llbracket M\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}=\{A\in\mathbb{T}\mid% \exists\Gamma\models\rho.\ \Gamma\vdash_{\cal T}M:A\},$

where $\rho$ ranges over $\mathbb{E}_{\mathcal{F}}$ and $\Gamma\models\rho$ if and only if $x:A\in\Gamma$ implies $A\in\rho(x)$ .

It is easy to verify that $\llbracket\leavevmode\nobreak\ \rrbracket^{\mathcal{F}_{\cal T}}$ satisfies all conditions required to be a $\lambda$ -model (Definition 30), but the last one, which is essential when ${\sf d}$ is the interpretation of a $\lambda$ -term. We always have $\llbracket(\lambda x.M)N\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}\subseteq% \llbracket M[x:=N]\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}$ , since Subject Expansion always holds by Theorem 20.

Theorem 33 ([13, Proposition 16.2.4]).

The filter structure over ${\cal T}$ is a $\lambda$ -model (dubbed filter model) iff

\llbracket(\lambda x.M)N\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}\supseteq% \llbracket M[x:=N]\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}

for all $\lambda$ -terms $M,N\in\Lambda$ , all variables $x$ and all environments $\rho$ in $\mathcal{F}_{\cal T}$ .

The condition $\llbracket(\lambda x.M)N\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}\supseteq% \llbracket M[x:=N]\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}$ means that all types of $(\lambda x.M)N$ are also types of $M[x:=N]$ , i.e. that the type system $\vdash_{\cal T}$ enjoys Subject Reduction. Then the following theorem follows naturally, being $\beta$ -soundness a sufficient condition for Subject Reduction.

Theorem 34 ([13, Corollary 16.2.9(i)]).

If ${\cal T}$ is a $\beta$ -sound itt, then the filter structure over ${\cal T}$ is a filter model.

All set-like itt’s generate filter models, since the set condition implies $\beta$ -soundness.

As mentioned after Definition 24, in [19, 4] there are filter models over itt’s which are not $\beta$ -sound.

It is interesting to notice that all continuous functions are representable in a filter model over a $\beta$ -sound itt. This generalises Theorem 2.13(iii) in [19].

Blanket Assumption.

Since our focus is on filter models, in the following we will only consider itt’s ${\cal T}$ which satisfy Subject Reduction, namely itt’s for which $\Gamma\vdash_{\cal T}\lambda x.M:B\to A$ implies $\Gamma,x:B\vdash_{\cal T}M:A$ .

To the best of our knowledge all filter models in the literature are generated by itt’s which fall in one of the categories given in Definition 27 or can be characterised by the axioms and rules in Figure 1. In the following list of distinguished itt’s and corresponding filter models we illustrate this point.

Example 35.

1.

Abramsky-Ong’s model [2] is isomorphic to a filter model generated by a lazy itt [13, Theorem 16.4.3];
2.

Engeler’s model [29], Scott’s $\mathcal{P}$ ( $\omega$ ) model [51], and the $\lambda$ -models defined in [44] are isomorphic to filter models generated by set-like itt’s [13, Theorems 16.4.16 and 16.4.21];
3.

the itt ${\cal T}_{\mathcal{B}CD}=\langle\{{\sf d}_{n}\mid n\in\mathbb{N}\},\leq_{{\cal T% }_{\mathcal{B}CD}}\rangle$ , which generates the original filter model [12], is the $\to$ -sound itt without other axioms/rules;
4.

the $\to$ -sound itt ${\cal T}_{\mathcal{P}LO}=\langle\{\iota\},\leq_{{\cal T}_{\mathcal{P}LO}}\rangle$ without other axioms/rules generates Plotkin’s model [47];
5.

all inverse limit models [49] are isomorphic to filter models generated by $\to$ -sound itt’s [13, Theorems 16.3.22];
6.

the filter models generated by the $\to$ -sound itt’s introduced in [19, 4] are not $\beta$ -sound, since not all Scott-continuous functions are represented; e.g. the itt with only two constants $c_{1}$ and $c_{2}$ and only the extra axiom scheme $A\leq A[c_{1}:=c_{2}]$ ;
7.

the minimal itt without constants, axioms and only Rule ( ${\sf U}\leq$ ) generates a filter model;
8.

the minimal ${\sf U}$ -sound itt with only one constant, and no other axioms and rules is neither set-like nor $\to$ -sound, but it generates a filter model;
9.

the minimal set-like itt with only one constant, and no other axioms and rules generates a filter model;
10.

the itt ${\cal T}^{\prime}=\langle\emptyset,\leq_{{\cal T}^{\prime}}\rangle$ with only the axiom ${\sf U}\sim{\sf U}\to{\sf U}$ , and only Rule ( ${\sf U}\leq$ ) does not satisfy the lazy condition nor Axiom ( $\to{\sf U}$ ), but it generates a filter model. Notice that $({\sf U}\to{\sf U})\to{\sf U}\nsim_{{\cal T}^{\prime}}{\sf U}$ .

All the itt’s mentioned in the Example above generate filter models since they can be proved to be $\beta$ -sound, apart from Example 35(6).

In the rest of the paper we will call lazy, ${\sf U}$ -sound, set-like, and $\to$ -sound the filter models over these itt’s, respectively.

Summing up we have the following separation theorem.

Theorem 36.

There are filter models which are:

$\blacksquare$

neither lazy nor ${\sf U}$ -sound;
$\blacksquare$

${\sf U}$ -sound but neither set-like nor $\to$ -sound;
$\blacksquare$

set-like but not $\to$ -sound;
$\blacksquare$

$\to$ -sound but not set-like.

Proof.

Consider the filter models generated by the itt’s in Example 35(10), Example 35(8), Example 35(9), Example 35(3), respectively. $\hfill\blacktriangleleft$

We conclude this section giving a crucial definition in this paper:

Definition 37 (Sensible Itt, Sensible Filter Model).

An itt $\mathcal{T}$ is sensible if all unsolvable terms are typed only by types equivalent to ${\sf U}$ . A filter model $\mathcal{F_{T}}$ is sensible if $\mathcal{T}$ is sensible, i.e. all unsolvable terms are interpreted in the bottom filter, $\uparrow_{\cal T}{\sf U}$ . Otherwise the itt and the filter model are said to be non-sensible.

4 Critical Sequences for Intersection Type Theories

Critical sequences are defined in [41] for graph models and a special kind of stable models. We tailor this notion to itt’s.

Definition 38.

A critical sequence for an itt ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ is a sequence $A_{n}$ with $n\in\mathbb{N}$ of types in $\mathbb{T}_{\mathbb{A}}$ if for all $n\in\mathbb{N}$ :

1.

$A_{n}\nsim_{\cal T}{\sf U}$ , $A_{n}\sim_{\cal T}B_{1}^{n}\to\ldots\to B_{m_{n}}^{n}\to C_{n}$ and $A_{n+1}{{}_{\cal T}\!\!\geq}B_{i_{n}}^{n}$ for some $i_{n}$ ( $1\leq i_{n}\leq m_{n}$ );
2.

there are a head closed term $P_{n+1}$ and a basis $\Gamma_{n+1}$ such that

$\Gamma_{n+1}\vdash P_{n+1}:B_{i_{n}}^{n};$
3.

if $j_{n+1}$ is the head order of $P_{n+1}$ , then $j_{n+1}\leq m_{n+1}$ and there are a head closed term $Q_{n+1}$ and a basis $\Gamma_{n+1}^{\prime}$ such that

$\Gamma_{n+1}^{\prime}\vdash Q_{n+1}:B_{j_{n+1}}^{n+1}.$

We say that a filter model, generated by an itt $\mathcal{T}$ , has a critical sequence if $\mathcal{T}$ has a critical sequence.

for $\Gamma=\{x:{\sf c},y:{\sf d}\to{\sf d}\}$ .

Figure 2: A derivation of

\vdash_{{\cal T}_{2}}\bf AAI:{\sf d}

, see Example 40.

As in [41] we can relate critical sequences to decorations.

Definition 39.

A decoration $\langle\lambda\overrightarrow{x}^{n}.N^{n}_{0}N_{1}^{n}\dots N_{m_{n}}^{n},N^{% n}_{0}\rangle$ is a witness of the critical sequence $A_{n}$ if for all $n\in\mathbb{N}$ :

1.

$N^{n+1}_{0}\to^{\ast}_{h}P_{n+1}$ ;
2.

$N^{n+1}_{j_{n+1}}\to^{\ast}_{h}Q_{n+1}$ , where $j_{n+1}$ is the head order of $P_{n+1}$ .

Example 40.

Let ${\cal T}_{2}$ be the $\to$ -sound itt obtained by taking $\mathbb{A}=\{{\sf c},{\sf d}\}$ and assuming ${\sf c}\sim{\sf c}\to({\sf d}\to{\sf d})\to{\sf d}$ . A critical sequence witnessed by $\langle{\bf A}{\bf A}\bf I,{\bf A}\rangle$ is $A_{n}={\sf c}$ , $i_{n}=1$ , $P_{n+1}={\bf A}$ , $j_{n+1}=2$ and $Q_{n+1}=\bf I$ for all $n\in\mathbb{N}$ . Notice that $B^{n}_{1}={\sf c}$ , $B^{n+1}_{2}={\sf d}\to{\sf d}$ for all $n\in\mathbb{N}$ and Figure 2 contains the derivations of $\vdash_{{\cal T}_{2}}{\bf A}:{\sf c}$ and $\vdash_{{\cal T}_{2}}\bf I:{\sf d}\to{\sf d}$ .

In the following we first discuss critical sequences for lazy itt’s and then for set-like and $\to$ -sound itt’s together, see Definition 27, the latter two being the classes which satisfy Lemma 28. An example of a filter model which does not belong to any of the three classes, but has nonetheless a critical sequence by Theorem 45, is given in Proposition 46.

4.1 Lazy Itt’s

In a type system induced by a lazy itt ${\cal T}$ any $\lambda$ -term of positive order $m$ , namely a $\lambda$ -term which reduces to $m$ $\lambda$ -abstractions [13, Definition 16.4.1], can be typed with the type ${\sf U}^{m}\to{\sf U}$ , where for any type $A$ and $m\in{\mathbb{N}}$ , ${\sf U}^{m}\to A$ is an abbreviation for ${\underbrace{{\sf U}\to\cdots\to{\sf U}\to}_{m}A}$ . We can show that

{\sf U}^{m}\to A\nsim_{\cal T}{\sf U}\quad\text{for all }m\geq 1.

(1)

Indeed, from Axiom ( ${\sf U}_{top}$ ), Rule ( $\to$ ) and ${\sf U}^{m}\to A={\sf U}\to({\sf U}^{m-1}\to A)$ we derive that ${\sf U}^{m}\to A\leq_{\cal T}{\sf U}\to{\sf U}$ . Assuming by contradiction ${\sf U}^{m}\to A\sim_{\cal T}{\sf U}$ from ${\sf U}^{m}\to A\leq_{\cal T}{\sf U}\to{\sf U}$ we get ${\sf U}\leq_{\cal T}{\sf U}\to{\sf U}$ , which falsifies the lazy condition. So we conclude that ${\sf U}^{m}\to A\nsim_{\cal T}{\sf U}$ .
Hence, no matter whether the $\lambda$ -term $M$ is solvable or unsolvable, if $M$ has positive order $m$ , then in the filter model $\mathcal{F}_{\cal T}$ , generated by a lazy itt ${\cal T}$ , we have that $\llbracket M\rrbracket^{\mathcal{F}_{\cal T}}_{\rho}\supseteq\uparrow_{\cal T}% {\sf U}^{m}\to{\sf U}$ for all $\rho$ , which is a filter strictly larger than the filter $\uparrow_{\cal T}{\sf U}$ . An interesting example is $\boldsymbol{\Theta}{\bf K}$ , where $\boldsymbol{\Theta}={\bf A}{\bf A}$ is Turing fixed-point combinator [11, Definition 6.1.4] and ${\bf K}$ , ${\bf A}$ are defined in Definition 2. We can derive $\vdash_{\cal T}\boldsymbol{\Theta}{\bf K}:{\sf U}^{m}\to{\sf U}\nsim_{\cal T}{% \sf U}$ for all $m\geq 1$ .

In lazy filter models there are plenty of critical sequences whose types are

A^{i}_{n}={\sf U}^{i-1}\to({\sf U}^{i}\to{\sf U})\to{\sf U}

for a fixed $i\geq 1$ . From Equation 1 we get ${\sf U}^{i-1}\to({\sf U}^{i}\to{\sf U})\to{\sf U}\nsim_{\cal T}{\sf U}$ , moreover Axiom ( ${\sf U}_{top}$ ) and Rule ( $\to$ ) imply ${\sf U}^{i-1}\to({\sf U}^{i}\to{\sf U})\to{\sf U}_{\cal T}\!\!\geq{\sf U}^{i}% \to{\sf U},$ so the first condition of Definition 38 is satisfied. These critical sequences are witnessed by decorations $\langle M_{n},N^{n}_{o}\rangle$ in which all $N^{n}_{o}$ have head order $i$ and all $N^{n}_{i}$ have positive order $i$ for all $n\in\mathbb{N}$ , see Theorem 41 below. We call $i$ -lazy such critical sequences and such decorations.
Examples of $1$ -lazy decorations are $\langle\lambda x.{\bf\Omega}_{m}{\bf\Omega}_{m},{\bf\Omega}_{m}\rangle$ where ${\bf\Omega}_{m}=\lambda y.\underbrace{y\ldots y}_{m}$ with $m\geq 2$ . A 1-lazy critical sequence witnessed by this decoration is $A_{n}^{1}=({\sf U}\to{\sf U})\to{\sf U}$ , $i_{n}=j_{n+1}=1$ and $P_{n+1}=Q_{n+1}={\bf\Omega}_{m}$ for all $n\in\mathbb{N}$ .
An interesting example of a $2$ -lazy decoration arising from the head reduction of $\Theta{\bf K}\to^{\ast}_{h}\lambda x.{\bf A}{\bf A}{\bf K}$ is $\langle\lambda xx_{1}\ldots x_{n}.{\bf A}{\bf A}{\bf K},{{\bf A}}\rangle$ for all $n\in\mathbb{N}$ . A 2-lazy critical sequence witnessed by this decoration is $A_{n}^{2}={\sf U}\to({\sf U}\to{\sf U})\to{\sf U}$ , $i_{n}=j_{n+1}=2$ , $P_{n+1}={\bf A}$ , and $Q_{n+1}={\bf K}$ for all $n\in\mathbb{N}$ .

The following theorem shows that lazy filter models have $i$ -lazy critical sequences witnessed by $i$ -lazy decorations.

Theorem 41.

Any $i$ -lazy decoration in a lazy filter model witnesses an $i$ -lazy critical sequence.

Proof.

Let $\langle\lambda\overrightarrow{x}^{n}.N^{n}_{0}N_{1}^{n}\dots N_{m_{n}}^{n},N^{% n}_{0}\rangle$ be an $i$ -lazy decoration for $n\in\mathbb{N}$ . By Lemma 16 $N^{n+1}_{0}$ and $N^{n+1}_{i}$ are solvable and they can be both typed by ${\sf U}^{i}\to{\sf U}$ , since they are of positive order $i$ . Then this decoration witnesses the $i$ -lazy critical sequence $A^{i}_{n}={\sf U}^{i-1}\to({\sf U}^{i}\to{\sf U})\to{\sf U}$ by taking $i_{n}=j_{n}=i$ and $P_{n+1}$ and $Q_{n+1}$ as the head normal forms of $N^{n+1}_{0}$ and $N^{n+1}_{i}$ , respectively. $\hfill\blacktriangleleft$

Two remarks are in order.

1.

Not all decorations can witness $i$ -lazy critical sequences for some $i$ . Examples are the last two decorations in Example 12(2). We conjecture however, that Theorem 41 can be generalised. Namely, given a decoration in a lazy filter model, one can find a critical sequence which it witnesses, and whose types involve only the type symbol ${\sf U}$ .
2.

As we pointed out already, the lazy condition is not the negation of Axiom ( $\to{\sf U}$ ). One can introduce weaker conditions than the lazy condition for a type theory $\mathcal{T}$ , which nonetheless allow for decorations to be witnesses of some critical sequence for $\mathcal{T}$ . However all the ones we have considered appear to be rather contrived or ad hoc.

4.2 Set-like and $\to$ -sound Itt’s

Kerth in [41] shows that if an unsolvable term does not have an empty interpretation in a graph or (a special kind of) stable model, then there is a critical sequence in that model, witnessing the decoration of the head reduction of the unsolvable term.

One of the main results of this paper is the extension of Kerth’s result both to set-like filter models and to $\to$ -sound filter models. The former class includes graph models while the latter includes inverse limit models. Our proof relies on Lemma 28, which permits to prove uniformly a property for two radically different classes of itt’s.

The first part of our proof, which is inspired by Kerth’s proof, considers a decoration $\langle M_{n},N_{0}^{n}\rangle$ for $n\in\mathbb{N}$ . The reduction from $M_{n}$ to $M_{n+1}$ is modified by replacing in every $\lambda$ -term the ancestors of $N^{n+1}_{0}$ in $M_{n+1}$ by a fresh variable. In the second part of our proof we use Lemma 28 to find meaningful types for $N^{n}_{i_{n}}$ and $N^{n+1}_{0}$ , where $N^{n+1}_{0}$ is a descendant of $N^{n}_{i_{n}}$ . We conclude by showing the relation between the types of $N^{n}_{i_{n}}$ and $N^{n+1}_{0}$ by means of the modified reduction from $M_{n}$ to $M_{n+1}$ .

Theorem 42.

If a set-like or an $\to$ -sound filter model gives to an unsolvable term a meaning different from $\uparrow_{\cal T}{\sf U}$ , then any decoration of that unsolvable witnesses a critical sequence.

Proof.

Let $M$ be an unsolvable term with a meaning different from $\uparrow_{\cal T}{\sf U}$ in a set-like or an $\to$ -sound filter model over the itt ${\cal T}$ . By definition of term interpretation (Definition 32) we get $\Gamma\vdash_{\cal T}M:A$ for some basis $\Gamma$ and for some type $A$ such that $A\nsim_{\cal T}{\sf U}$ . By Theorem 13 $M\to^{\ast}_{\beta}M_{0}$ such that the head reduction of $M_{0}$ has a decoration, let it be $\langle M_{n},N_{0}^{n}\rangle$ for $n\in\mathbb{N}$ . By Subject Reduction (Theorem 21) $\Gamma\vdash_{\cal T}M_{n}:A$ for $n\in\mathbb{N}$ .

Let $M_{n}=\lambda\overrightarrow{x}^{n}.N^{n}_{0}\cdots N^{n}_{m_{n}}$ and $M_{n+1}=\lambda\overrightarrow{x}^{n+1}.N^{n}_{i_{n}}N^{n+1}_{1}\cdots N^{n+1}% _{m_{n+1}}$ . Consider the reduction

N^{n}_{0}\cdots N^{n}_{m_{n}}=M^{1}\to_{h}M^{2}\to_{h}\cdots\to_{h}M^{k}=% \lambda\overrightarrow{t}.N^{n}_{i_{n}}N^{n+1}_{1}\cdots N^{n+1}_{m_{n+1}},

where $\overrightarrow{x}^{n+1}=\overrightarrow{x}^{n}\overrightarrow{t}$ and let $R_{s}$ be obtained from $M^{s}$ by replacing the unique ancestor in $M^{s}$ of the occurrence of $N^{n}_{i_{n}}$ in head position in $M^{k}$ with a fresh variable $y$ for $1\leq s\leq k$ . Then $R_{s}$ is such that $M^{s}=R_{s}[y:=N^{n}_{i_{n}}]$ and there is a single occurrence of $y$ in $R_{s}$ . For all $s<k$ , $y$ cannot be in head position in $R_{s}$ , since in this case the corresponding occurrences of $N^{n}_{i_{n}}$ in $M^{s}$ would be reduced and then it could not have a descendant in $M^{k}$ . So the head redex of $M^{s}$ is equal to the head redex of $R_{s}$ . Let $R^{\prime}_{s}$ be such that $R_{s}\to_{h}R^{\prime}_{s}$ . Let $R^{\prime\prime}_{s}$ be obtained by replacing with a fresh $z$ the occurrences of $y$ which are children of the occurrence of $y$ in $R^{\prime}_{s}$ , but are not ancestors of the occurrence of $N^{n}_{i_{n}}$ in head position in $M^{k}$ . Then $R_{s+1}=R^{\prime\prime}_{s}[z:=N^{n}_{i_{n}}]$ . We need to proceed in this way because we cannot simply head reduce $N^{n}_{0}\cdots N^{n}_{i_{n}-1}yN^{n}_{i_{n}+1}\cdots N^{n}_{m_{n}}$ , since in this reduction the variable $y$ could go in head position before $k-1$ steps, as shown in Example 12(3) and so we would not produce a critical sequence witnessed precisely by the decoration we started from.
Since $\Gamma\vdash_{\cal T}M_{n}:A$ with $A\nsim_{\cal T}{\sf U}$ and ${\cal T}$ satisfies Lemma 28 we have, for some $\overrightarrow{A}^{n}$ , $B^{n}_{1}$ , $\ldots$ , $B^{n}_{m_{n}}$ , $C^{n}\nsim_{\cal T}{\sf U}$ :

\Gamma,\overrightarrow{x:A}^{n}\vdash_{\cal T}N_{0}^{n}:B^{n}_{1}\to\ldots\to B% ^{n}_{m_{n}}\to C^{n}\text{ and }\Gamma,\overrightarrow{x:A}^{n}\vdash_{\cal T% }N^{n}_{j}:B^{n}_{j}\ \ \ (1\leq j\leq m_{n}).

Then by repeated applications of the typing Rule ( $\to$ E) we get

\Gamma,\overrightarrow{x:A}^{n}\vdash_{\cal T}M^{1}:C^{n},

and since $R_{1}=N_{0}^{n}N_{1}^{n}\ldots N_{i_{n}-1}^{n}yN_{i_{n}+1}^{n}\ldots N_{m_{n}}% ^{n}$ we get also

\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}}\vdash_{\cal T}R_{1}:C^{n}.

By Subject Reduction (Theorem 21), since $R_{1}\to_{h}R^{\prime}_{1}$ :

\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}}\vdash_{\cal T}R_{1}:C^{n}\mbox% {\ \ \ implies\ \ \ }\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}}\vdash_{% \cal T}R^{\prime}_{1}:C^{n}.

In turn being $R^{\prime\prime}_{1}$ obtained from $R^{\prime}_{1}$ by replacing all but one occurrences of $y$ by $z$ :

\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}}\vdash_{\cal T}R^{\prime}_{1}:C% ^{n}\mbox{\ \ \ implies\ \ \ }\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}},% z:B^{n}_{i_{n}}\vdash_{\cal T}R^{\prime\prime}_{1}:C^{n}.

Finally from

\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}},z:B^{n}_{i_{n}}\vdash_{\cal T}% R^{\prime\prime}_{1}:C^{n}\mbox{\ \ \ and \ \ \ }\Gamma,\overrightarrow{x:A}^{% n}\vdash_{\cal T}N^{n}_{i_{n}}:B^{n}_{i_{n}}

we get

\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}}\vdash_{\cal T}R_{2}:C^{n},

since $R_{2}=R^{\prime\prime}_{1}[z:=N_{i_{n}}^{n}]$ . Iterating these steps $k-1$ times, we conclude

\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}}\vdash_{\cal T}R_{k}:C^{n}.

Notice that $R_{k}=\lambda\overrightarrow{t}.yN^{n+1}_{1}\cdots N^{n+1}_{m_{n+1}}$ . Applying again Lemma 28, we have for some $\overrightarrow{D}$ , $B^{n+1}_{1}$ , $\ldots$ , $B^{n+1}_{m_{n+1}}$ , $C^{n+1}\nsim_{\cal T}{\sf U}$ :

\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}},\overrightarrow{t:D}\vdash_{% \cal T}y:B^{n+1}_{1}\to\ldots\to B^{n+1}_{m_{n+1}}\to C^{n+1}

and

\Gamma,\overrightarrow{x:A}^{n},\overrightarrow{t:D}\vdash_{\cal T}N^{n+1}_{j}% :B^{n+1}_{j}\ \ \ (1\leq j\leq m_{n+1}).

We show that the sequence $A_{n}=B^{n}_{1}\to\ldots\to B^{n}_{m_{n}}\to C^{n}$ for $n\in\mathbb{N}$ thus obtained, does indeed produce a critical sequence.
By the target condition if $C^{n}\nsim{\sf U}$ , then also $A_{n}\nsim{\sf U}$ for all $n\in\mathbb{N}$ . Lemma 19(1) applied to $\Gamma,\overrightarrow{x:A}^{n},y:B^{n}_{i_{n}},\overrightarrow{t:D}\vdash_{% \cal T}y:B^{n+1}_{1}\to\ldots\to B^{n+1}_{m_{n+1}}\to C^{n+1}$ implies $A_{n+1}{{}_{\cal T}\!\!\geq}B^{n}_{i_{n}}$ , since $A_{n+1}=B^{n+1}_{1}\to\ldots\to B^{n+1}_{m_{n+1}}\to C^{n+1}$ . So the first condition of Definition 38 is satisfied. By Lemma 16 $N_{i_{n}}^{n}$ has a head closed normal form. We can choose for $P_{n+1}$ the head normal form of $N_{i_{n}}^{n}$ , since in $\vdash_{\cal T}$ it has the type $B^{n}_{i_{n}}$ by Subject Reduction. If $j_{n+1}$ is the head order of $P_{n+1}$ , then $N_{j_{n+1}}^{n+1}$ has a head closed normal form by Lemma 16. We can choose for $Q_{n+1}$ the head normal form of $N_{j_{n+1}}^{n+1}$ , since in $\vdash_{\cal T}$ it has the type $B_{j_{n+1}}^{n+1}$ by Subject Reduction. Therefore also the last two conditions of Definition 38 are satisfied. $\hfill\blacktriangleleft$

Example 43.

Let $\bf I$ , ${\bf A}$ be defined as in Definition 2 and ${\cal T}_{2}$ be defined as in Example 40. It is easy to verify that ${\cal T}_{2}$ is $\beta$ -sound by induction on $\leq_{{\cal T}_{2}}$ . We can derive $\vdash_{{\cal T}_{2}}{\bf A}{\bf A}\bf I:{\sf d}$ , see Figure 2. Then the interpretation of ${\bf A}{\bf A}\bf I$ in the filter model generated by ${\cal T}_{2}$ contains $\uparrow_{{\cal T}_{2}}{\sf d}$ , and the decoration of ${\bf A}{\bf A}\bf I$ , see Example 12(1), witnesses the critical sequence for ${\cal T}_{2}$ given in Example 40.

$\blacktriangleright$ Remark 44.

As pointed out in Remark 29, Lemma 28 holds for merely ${\sf U}$ -sound itt’s, when the unsolvable terms are of the shape $M_{n}=\lambda\overrightarrow{x}^{n}.N^{n}_{0}N^{n}_{1}$ ( $n\in\mathbb{N}$ ). We can then formulate Theorem 42 for ${\sf U}$ -sound itt’s and unsolvable terms of this shape.

5 Critical Sequences in Action

In this section we further discuss the critical notion of critical sequence and give examples both in sensible and non-sensible filter models.

In Subsection 4.1, we remarked that lazy filter models are naturally non-sensible and given several examples of critical sequences and decorations witnessing them. For set-like and $\to$ -sound filter models Theorem 42 gives a necessary condition for them to be non-sensible, namely the existence of a critical sequence witnessing a decoration.

The existence of a critical sequence, however, is not a sufficient condition for a filter model to be non-sensible. In fact, all itt’s satisfying the following subtyping axiom

A\to C\leq A\cap B\to C\ \ \ \ \ \textnormal{(L$\to$)}

have a critical sequence, albeit almost a trivial one.

Theorem 45.

Let ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ . If $\mathbb{A}$ contains at least a constant and Axiom (L $\to$ ) holds for $\leq_{\cal T}$ , then ${\cal T}$ has a critical sequence.

Proof.

Let ${\sf c}\in\mathbb{A}$ . We define $A_{n}=({\sf c}\to{\sf c})\cap(({\sf c}\to{\sf c})\to{\sf c}\to{\sf c})\to{\sf c% }\to{\sf c}$ , $i_{n}=j_{n+1}=1$ and $P_{n+1}=Q_{n+1}={\bf I}$ for all $n\in\mathbb{N}$ . One can easily check that using Axiom (L $\to$ ):

({\sf c}\to{\sf c})\to{\sf c}\to{\sf c}\leq_{\cal T}({\sf c}\to{\sf c})\cap(({% \sf c}\to{\sf c})\to{\sf c}\to{\sf c})\to{\sf c}\to{\sf c}

and hence

({\sf c}\to{\sf c})\cap(({\sf c}\to{\sf c})\to{\sf c}\to{\sf c})\leq_{\cal T}(% {\sf c}\to{\sf c})\cap(({\sf c}\to{\sf c})\to{\sf c}\to{\sf c})\to{\sf c}\to{% \sf c}.\qquad\

$\hfill\blacktriangleleft$ Notice that Rule ( $\to$ ) of Figure 1 implies Axiom (L $\to$ ), hence all $\to$ -sound filter models have critical sequences. In particular the original filter model [12] and all inverse limit models [13, Theorems 16.3.22] have critical sequences. Hence, in view of Theorem 45, the existence of a critical sequence in a $\to$ -sound filter model is not very informative per se. The significance of Theorem 42, for non-sensible $\to$ -sound filter models, resides in that the decoration arising from the reduction of an unsolvable term, by Theorem 13, witnesses a critical sequence.

Clearly Axiom (L $\to$ ) falsifies the set condition, so this axiom does not hold for set-like itt’s. Incidentally, we give the following proposition, which illustrates the flexibility of itt’s in designing special purpose filter models.

Proposition 46.

The minimal (L $\to$ ) itt, ${\cal T}_{\textnormal{(L$\to$)}}$ , consisting of only one constant, the extra Axiom (L $\to$ ), and Rule ( ${\sf U}\leq$ ) generates a filter model which is neither lazy nor ${\sf U}$ -sound.

Proof.

By induction on the subtyping relation of ${\cal T}_{\textnormal{(L$\to$)}}$ one can show that it is $\beta$ -sound and then apply Theorem 34. $\hfill\blacktriangleleft$

For the sake of completeness we also give an example of a sensible set-like filter model which exhibits a critical sequence.

Example 47.

The set-like itt ${\cal T}_{3}$ with constants $\mathbb{A}_{3}=\{{\sf c}\}\cup\{{\sf c}_{n}\mid n\in{\mathbb{N}}\}$ and axioms ${\sf c}_{n}\sim{\sf c}_{n+1}\rightarrow{\sf c}$ for $n\in{\mathbb{N}}$ generates a sensible filter model which has a critical sequence; namely $A_{n}={\sf c}_{n}$ , $i_{n}=j_{n+1}=1$ , $\Gamma_{n+1}=\{y:{\sf c}_{n+3}\}$ , $\Gamma^{\prime}_{n+1}=\{y:{\sf c}_{n+4}\}$ , $P_{n+1}=Q_{n+1}=\lambda x.xy$ for all $n\in\mathbb{N}$ . Indeed ${\Gamma_{n+1}}\vdash_{{\cal T}_{3}}{P_{n+1}}:{{\sf c}_{n+1}}{}$ and ${\Gamma^{\prime}_{n+1}}\vdash_{{\cal T}_{3}}{Q_{n+1}}:{{\sf c}_{n+2}}$ . The sensibility of the filter model generated by ${\cal T}_{3}$ follows from a result proved in [24].

In the following we give examples of critical sequences for most non-sensible filter models appearing in the literature, which are all witnessed by distinguished unsolvable terms. All itt’s considered in this example are assumed to be $\to$ -sound. The models in 48(3b) are isomorphic to set-like filter models. We use combinators defined in Definition 2.

Example 48.

1.

Park inverse limit model [46] is isomorphic to the filter model generated by the itt ${\cal P}=\langle\{{\sf c}\},\leq_{\cal P}\rangle$ , where $\leq_{\cal P}$ is obtained by adding the axiom ${\sf c}\sim{\sf c}\to{\sf c}$ [13, Figure 13.4]. In the filter model isomorphic to Park model all closed $\lambda$ -terms are interpreted by filters containing $\uparrow_{\cal P}{\sf c}$ , as proved in [39]. A critical sequence is $A_{n}={\sf c}$ , $i_{n}=j_{n+1}=1$ , $P_{n+1}=Q_{n+1}={\boldsymbol{\Omega}_{3}}$ for all $n\in\mathbb{N}$ . This critical sequence is witnessed by the decoration, say, $\langle\underbrace{{\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}\ldots{% \boldsymbol{\boldsymbol{\Omega}}}_{3}}_{n+2},{\boldsymbol{\Omega}}_{3}\rangle$ for all $n\in\mathbb{N}$ .
2.

Honsell and Ronchi define in [39] the itt ${\cal HR}=\langle\{{\sf c},{\sf d}\},\leq_{\cal HR}\rangle$ , where $\leq_{\cal HR}$ is obtained by adding the axioms ${\sf c}\sim({\sf c}\to{\sf c})\cap({\sf d}\to{\sf d})$ , ${\sf d}\sim{\sf c}\to{\sf d}$ , ${\sf d}\leq{\sf c}$ [13, Figure 13.4]. They show that the interpretation of $\bf YB$ , where ${\bf Y}=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$ , in the filter model generated by ${\cal HR}$ , contains $\uparrow_{\cal HR}{\sf c}$ . A critical sequence in ${\cal HR}$ is $A_{n}={\sf c}\to{\sf c}$ , $i_{n}=j_{n+1}=1$ , $P_{n+1}=\lambda xyz.xx(yz)$ , $Q_{n+1}=\bf B$ for all $n\in\mathbb{N}$ . Let ${\bf H}=\lambda x.{\bf B}(xx)$ and $M_{n}=\lambda xy_{0}\ldots y_{n}.{\bf H}{\bf H}(xy_{0}\ldots y_{n})$ for all $n\in\texttt{N}$ . Note that ${\bf Y}{\bf B}\to^{\ast}_{h}M_{0}$ and ${\bf H}\to_{h}P_{n+1}$ . A decoration for $M_{0}$ witnessing this critical sequence is $\langle M_{n},\bf H\rangle$ for all $n\in\mathbb{N}$ .
3.
Easy terms, namely $\lambda$ -terms which can be equated to an arbitrary closed $\lambda$ -term obtaining a consistent $\lambda$ -theory [40, 10], are a very intriguing class of, necessarily unsolvable, terms. We present below, various filter models, in which some easy terms are not interpreted by $\uparrow_{\cal T}{\sf U}$ . These models are the intermediary steps for the semantical proofs of easiness of the corresponding terms, in that they permit to force in the interpretation of the easy term, the filter generated by a generic isolated constant, see [6].
1. (a)
  
  Alessi, Dezani and Honsell define in [6] two itt’s. The first itt is ${{\cal ADH}1{=}\langle\{{\sf c},{\sf d}\},\leq_{{\cal ADH}1}\rangle}$ , where $\leq_{{\cal ADH}1}$ is obtained by adding the axiom ${\sf c}\sim{\sf c}\to{\sf d}$ . In the filter model generated by ${\cal ADH}1$ the interpretation of ${\boldsymbol{\Omega}}_{2}{\boldsymbol{\Omega}}_{2}$ contains $\uparrow_{{\cal ADH}1}{\sf d}$ . A critical sequence for ${\cal ADH}1$ is $A_{n}={\sf c}$ , $i_{n}=j_{n+1}=1$ , $P_{n+1}=Q_{n+1}={\boldsymbol{\Omega}}_{2}$ for all $n\in\texttt{N}$ . A decoration for ${\boldsymbol{\Omega}}_{2}{\boldsymbol{\Omega}}_{2}$ witnessing this critical sequence is $\langle{\boldsymbol{\Omega}}_{2}{\boldsymbol{\Omega}}_{2},{\boldsymbol{\Omega}% }_{2}\rangle$ .
2. (b)
  
  In [10], Baeten and Boerboom show how to define graph models in which the interpretation of $\boldsymbol{\Omega_{2}\Omega_{2}}$ coincides with the interpretation of a given closed $\lambda$ -term. In each such model $\boldsymbol{\Omega_{2}\Omega_{2}}$ gives rise to many critical sequences which are all structurally similar to the one defined above for the theory $\mathcal{ADH}1.$
3. (c)
  
  The second itt in [6] is ${\cal ADH}2=\langle\{{\sf c},{\sf d},{\sf e},{\sf f},{\sf g}\},\leq_{{\cal ADH% }2}\rangle$ , where $\leq_{{\cal ADH}2}$ is obtained by adding the axioms ${\sf c}\sim{\sf d}\cap({\sf d}\to({\sf f}\to{\sf f})\to{\sf g})$ , ${\sf d}\sim{\sf e}\to{\sf c}$ , ${\sf e}\sim{\sf e}\to{\sf d}$ , ${\sf c}\leq{\sf d}\leq{\sf e}$ . In the filter model generated by ${\cal ADH}2$ the interpretation of ${\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}{\bf I}$ contains $\uparrow_{{\cal ADH}2}{\sf g}$ . A critical sequence for ${\cal ADH}2$ is $A_{n}={\sf e}$ , $i_{n}=j_{n+1}=1$ , $P_{n+1}=Q_{n+1}={\boldsymbol{\Omega}}_{3}$ for all $n\in\mathbb{N}$ . A decoration for ${\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}{\bf I}$ witnessing this critical sequence is $\langle\underbrace{{\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}\ldots{% \boldsymbol{\Omega}}_{3}}_{n+2}{\bf I},{\boldsymbol{\Omega}}_{3}\rangle$ for all $n\in\mathbb{N}$ .
4. (d)
  
  The easiness of ${\bf EE}$ , where ${\bf E}=\lambda x.x(\lambda y.yx)$ , is shown by Zylberajch in [54, p.58]. This $\lambda$ -term is interpreted by a filter which contains $\uparrow_{{\cal ADH}1}{\sf d}$ in the filter model generated by the itt ${\cal ADH}1$ . Let
  
  $N_{n}=\begin{cases}{\bf E}&\text{if }n\equiv 0\leavevmode\nobreak\ (\text{mod}% \leavevmode\nobreak\ 3)\\ \lambda y.y{\bf E}&\text{if }n\equiv 1\leavevmode\nobreak\ (\text{mod}% \leavevmode\nobreak\ 3)\\ \lambda z.z(\lambda y.y{\bf E})&\text{if }n\equiv 2\leavevmode\nobreak\ (\text% {mod}\leavevmode\nobreak\ 3)\\ \end{cases}$
  
  and $M_{n}=N_{n}N_{n+1}$ , we have that ${\bf EE}\to_{\beta}M_{0}$ . A decoration for $M_{0}$ is $\langle M_{n},N_{n}\rangle$ for all $n\in\texttt{N}$ . A critical sequence witnessed by this decoration is $A_{n}={\sf c}$ , $i_{n}=j_{n+1}=1$ , $P_{n+1}=N_{n+1}$ , $Q_{n+1}=N_{n+2}$ for all $n\in\texttt{N}$ . Notice that, also if the itt is the same, the critical sequence witnessed by the decoration of ${\bf EE}$ is different from the critical sequence witnessed by the decoration of ${\boldsymbol{\Omega}}_{2}{\boldsymbol{\Omega}}_{2}$ .
5. (e)
  
  Berarducci and Intrigila prove that ${\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}{\bf K}$ is easy [16]. Let ${\cal BI}=\langle\{{\sf c},{\sf d},{\sf e},{\sf f},{\sf g}\},\leq_{{\cal BI}}\rangle$ , where $\leq_{{\cal BI}}$ is obtained by adding the axioms ${\sf c}\sim{\sf d}\cap({\sf d}\to({\sf f}\to{\sf U}\to{\sf f})\to{\sf g})$ , ${\sf d}\sim{\sf e}\to{\sf c}$ , ${\sf e}\sim{\sf e}\to{\sf d}$ , ${\sf c}\leq{\sf d}\leq{\sf e}$ . The subtyping $\leq_{{\cal BI}}$ can be proved to be $\beta$ -sound by induction on its definition. In the filter model generated by $\leq_{{\cal BI}}$ the interpretation of ${\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}{\bf K}$ contains $\uparrow_{{\cal BI}}{\sf g}$ . A decoration for ${\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}{\bf K}$ is $\langle\underbrace{{\boldsymbol{\Omega}}_{3}{\boldsymbol{\Omega}}_{3}\ldots{% \boldsymbol{\Omega}}_{3}}_{n+2}{\bf K},{\boldsymbol{\Omega}}_{3}\rangle$ for all $n\in\texttt{N}$ . A critical sequence witnessed by this decoration is $A_{n}={\sf e}$ , $i_{n}=j_{n+1}=1$ , $P_{n+1}=Q_{n+1}={\boldsymbol{\Omega}}_{3}$ for all $n\in\mathbb{N}$ .

The following definition gives us a criterion for establishing the absence of critical sequences.

Definition 49.

The depth of a type in $\mathbb{T}_{\mathbb{A}}$ for the itt ${\cal T}=\langle\mathbb{A},\leq_{\cal T}\rangle$ (notation $d^{\cal T}\!(A)$ ) is defined by

\begin{array}[]{c}d^{\cal T}\!({\sf c})=0\leavevmode\nobreak\ \forall{\sf c}% \in\mathbb{A}\quad d^{\cal T}\!({\sf U})=0\quad d^{\cal T}\!(A\cap B)=max\{d^{% \cal T}\!(A),d^{\cal T}\!(B)\}\\[7.0pt] d^{\cal T}\!(A\to B)=\begin{cases}max\{d^{\cal T}\!(A)+1,d^{\cal T}\!(B)\}&% \text{if }A\to B\nsim_{\cal T}{\sf U}\\ 0&\text{otherwise.}\end{cases}\end{array}

Theorem 50.

If $A\leq_{{\cal T}}B$ implies $d^{\cal T}\!(B)\leq d^{\cal T}\!(A)$ , then ${\cal T}$ and the filter model over ${\cal T}$ , if any, do not have critical sequences.

Proof.

In a critical sequence we have $d^{\cal T}\!(B_{i_{n}}^{n})<d^{\cal T}\!(A_{n})$ by definition of depth and $d^{\cal T}\!(A_{n+1})\leq d^{\cal T}\!(B_{i_{n}}^{n})$ , by the assumption on $d^{\cal T}\!(\ )$ since $A_{n+1}{{}_{\cal T}\!\!\geq}B_{i_{n}}^{n}$ , these imply $d(A_{n+1})<d(A_{n})$ for all $n\in\mathbb{N}$ . By infinite descent this is impossible, since depths are not negative. $\hfill\blacktriangleleft$

Corollary 51.

If ${\cal T}$ is set-like or $\to$ -sound and $A\leq_{{\cal T}}B$ implies $d^{\cal T}\!(B)\leq d^{\cal T}\!(A)$ , then ${\cal T}$ and the filter model generated by ${\cal T}$ , if any, are sensible.

Proof.

Immediate from Theorem 50 and Theorem 42. $\hfill\blacktriangleleft$

From the above theorem we immediately get that the set-like filter model generated by the itt ${\cal E}=\langle\{{\sf c}_{n}\mid n\in\mathbb{N}\},\leq_{\cal E}\rangle$ , without further axioms/rules, does not have a critical sequence. By Corollary 51 this filter model, which is isomorphic to Engeler’s graph model [29], is sensible as is the set-like filter model generated by the itt in Example 35(9). We point out that the absence of critical sequences in Engeler’s graph model is shown in [41] by a slightly longer proof. It is interesting to notice that the above arguments provide conceptually different proofs, that the models are sensible, from the traditional ones based on indexed reductions [43].

By Theorem 50 the filter models over the itt’s in Example 35(7), (8), and (10) do not have critical sequences, but we cannot apply Corollary 51 to show that they are sensible. The itt’s in Example 35(7) and (10) in fact are non-sensible, since we can derive the type $({\sf U}\to{\sf U})\to{\sf U}\nsim{\sf U}$ for all unsolvable terms of positive order. Instead the itt in Example 35(8) can be shown to be sensible using a criterion proved in [24].

6 Related Work and Conclusion

Intersection types originated in Torino in the late 70’s and early 80’s from the work of the first author of the present paper together with Mario Coppo, see e.g. [20, 12] and [13, Part III]. Intersection types allowed for a novel approach to the semantics of functional languages. The traditional way of interpreting a statement of the shape $M\models\phi$ , i.e. “the program $M$ satisfies the property $\phi$ in a semantic domain ${\mathcal{D}}$ ”, was that of viewing $M$ as a point in ${\mathcal{D}}$ , and $\phi$ as a suitable subset $\Phi$ of ${\mathcal{D}}$ . The statement $M\models\phi$ was then interpreted as the membership judgement $\llbracket M\rrbracket^{{\mathcal{D}}}_{\;}\in\Phi$ , where the interpretation function $\llbracket\cdot\rrbracket^{{\mathcal{D}}}_{\;}$ maps programs to elements of ${\mathcal{D}}$ .

Intersection types “reversed” this traditional point of view in the spirit of a Stone Duality, see [19, 1]. Namely, axioms and rules involving intersection types are used in this approach to define a basis for the topology of a pointless space, and points are no more the building blocks of the semantic domains, but are recovered as filters of types. According to this intuition $M\models\phi$ is translated in the “opposite” membership judgement, i.e. $A\in\llbracket M\rrbracket^{\mathcal{F}}_{\;}$ , “the type $A$ (corresponding to the property $\phi$ and interpreted as $\Phi$ ) is a member of the filter (of properties) which gives the whole interpretation of $M$ ”.

This approach allows to reap many pleasing results, because it opens up the study of program semantics to the syntactic methods from proof theory. The interpretation of a program being fully determined only when all the properties it satisfies are known, its interpretation can be approximated statically in a finitary way through a type assignment system. Many syntactic technical results can then be established, such as the Inversion Lemma and Subject Reduction, and many computational properties of $\lambda$ -terms can be naturally characterised statically. The original filter model [12] was introduced for showing the completeness of Scott’s semantics [50] for simple types à la Curry [22, p.317]. But, already in that model some computational properties of $\lambda$ -terms were naturally characterised statically. Since then, many filter models have been proposed for characterising many more computational properties of $\lambda$ -terms [21, 35, 25, 26, 5, 53]. Recently intersection types have been used for giving exact bounds to the number of $\beta$ -reductions needed to reach the normal forms and to the number of symbols in the normal forms [30, 42, 14, 17, 18, 3, 9]. The key move to increase the expressivity of intersection types is to consider non-idempotent intersections in relevant type assignment systems, by means of which the number of occurrences of variables during the reduction process can be quantitatively measured.

Filter models encompass many kinds of $\lambda$ -models. Inverse limit models [13, Section 16.3], graph models [13, pp.722-27] and lazy models [13, Theorem 16.4.3] are all filter models. Filter models, where easy terms are interpreted either as arbitrary $\lambda$ -terms or as arbitrary continuous predicates, are constructed in a series of papers [6, 8, 27, 7].

In the vast literature on intersection types, unsolvable terms have been considered only marginally. Throughout this paper we have referred to most of such papers, however general results are missing. The present paper tries to contribute in filling this gap and possibly to stimulate further research. The present paper was triggered by [41], from which the crucial definitions of decoration and critical sequence are taken. Crucial to this paper is also the proof of Kerth’s conjecture by David [23]. In [41] critical sequences are defined for graph models and for a kind of stable models. We define critical sequence for itt’s which generate filter models. This general notion of critical sequence achieves full significance once it has a decoration witnessing it. Since there are filter models isomorphic to models of the lazy $\lambda$ -calculus, graph models and inverse limit models we discuss critical sequences for all these models both in the sensible case and in the non-sensible case. In the introduction to [41], Kerth conjectures that the results of his paper should apply to inverse limit models too. The present paper provides a clear and articulate answer to that conjecture. However we leave open a complete answer for filter models which are neither lazy, set-like nor $\to$ -sound.

The existence of a critical sequence in an itt does not imply, however, that the generated filter model is non-sensible. In the companion paper [24] we introduce sufficient conditions on itt’s which imply that they generate sensible filter models.

There are many notions and results in the present paper which could be considered in relation to stable models [38, 36, 41, 45], models of call-by-value $\lambda$ -calculus [36, 48, 52], quantitative domains [31], and game models [36, 28, 32].

We conclude this paper addressing again the crucial question of characterising non-sensible itt’s in a conceptually independent way from the existence of an unsolvable which can be typed in the itt. What is missing, in the language of the present paper, is a strengthened notion of critical sequence which implies that it is witnessed by a decoration. This is probably rather difficult as the final remark of the present paper below shows, indicating that part of the mystery of unsolvables is still there for future generations to address.

$\blacktriangleright$ Remark 52.

One could wonder if asking that the $P_{n+1}$ ’s and $Q_{n+1}$ ’s, in the definition of critical sequence, contain the self application of a bound variable would ensure the existence of a witnessing decoration. A counterexample is the $\to$ -sound itt with the axiom ${\sf c}_{n}\sim{\sf c}_{n+1}\to{\sf U}\to{\sf c}_{0}$ for $n\in\mathbb{N}$ . In fact a critical sequence is $A_{n}={\sf c}_{n}$ , $i_{n}=j_{n+1}=1$ , $\Gamma_{n+1}=\{z:{\sf c}_{n+3}\}$ , $\Gamma^{\prime}_{n+1}=\{z:{\sf c}_{n+4}\}$ , $P_{n+1}=Q_{n+1}=\lambda xy.xz(xx)$ for all $n\in\mathbb{N}$ . This itt can be shown to be $\beta$ -sound by induction on subtyping. A result in [24] allows us to prove that the filter model generated by this itt is sensible.

References

[1] Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1-2):1–77, 1991. doi:10.1016/0168-0072(91)90065-T.
[2] Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105(2):159–267, 1993. doi:10.1006/INCO.1993.1044.
[3] Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1–94:30, 2018. doi:10.1145/3236789.
[4] Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Tailoring filter models. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 17–33. Springer, 2003. doi:10.1007/978-3-540-24849-1_2.
[5] Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoretical Computer Science, 355(2):108–126, 2006. doi:10.1016/j.tcs.2006.01.004.
[6] Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Furio Honsell. Filter models and easy terms. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, ICTCS, volume 2202 of LNCS, pages 17–37. Springer, 2001. doi:10.1007/3-540-45446-2_2.
[7] Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Stefania Lusin. Intersection types and domain operators. Theoretical Computer Science, 316(1):25–47, 2004. doi:10.1016/J.TCS.2004.01.022.
[8] Fabio Alessi and Stefania Lusin. Simple easy terms. In Steffen van Bakel, editor, ITRS, volume 70 of ENTCS, pages 1–18. Elsevier, 2002. doi:10.1016/S1571-0661(04)80487-0.
[9] Sandra Alves, Delia Kesner, and Miguel Ramos. Extending the quantitative pattern-matching paradigm. In Oleg Kiselyov, editor, APLAS, volume 15194 of LNCS, pages 84–105. Springer, 2024. doi:10.1007/978-981-97-8943-6_5.
[10] Jos C. M. Baeten and Bas Boerboom. Omega can be anything it should not be. In Indagationes Mathematicae, volume 82(2), pages 111–120, 1979. doi:10.1016/1385-7258(79)90016-7.
[11] Henk Barendregt. The Lambda Calculus - its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, 1985.
[12] Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983. doi:10.2307/2273659.
[13] Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Cambridge University Press, 2013. doi:10.1017/CBO9781139032636.
[14] Erika De Benedetti and Simona Ronchi Della Rocca. Bounding normalization time through intersection types. In ITRS, volume 121 of EPTCS, pages 48–57. Open Publishing Association, 2012. doi:10.4204/EPTCS.121.4.
[15] Alessandro Berarducci. Infinite $\lambda$ -calculus and non-sensible models. In Aldo Ursini, editor, Logic and Algebra, pages 17:1–17:39. Routledge, 1996. doi:10.1201/9780203748671-17.
[16] Alessandro Berarducci and Benedetto Intrigila. Church-Rosser lambda-theories, infinite lambda-terms and consistency problems. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss, editors, Logic: from Foundations to Applications, chapter 2, pages 33–58. Clarendon Press, 1996. URL: https://arpi.unipi.it/handle/11568/46466.
[17] Alexis Bernadet and Stéphane Graham-Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4):1–46, 2013. doi:10.2168/LMCS-9(4:3)2013.
[18] Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25:433–464, 2017. doi:10.1093/jigpal/jzx018.
[19] Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium ’82, volume 112 of Studies in Logic and the Foundations of Mathematics, pages 241–262. Elsevier, 1984. doi:10.1016/S0049-237X(08)71819-6.
[20] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal type schemes and lambda-calculus semantics. In Roger Hindley and Jonathan P. Seldin, editors, To H.B.Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 535–560. Academic Press, 1980. URL: http://www.di.unito.it/˜dezani/papers/CDV80.pdf.
[21] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms and $D_{\infty}$ -lambda-models. Information and Computation, 72(2):85–116, 1987. doi:10.1016/0890-5401(87)90042-3.
[22] Haskell B. Curry and Robert Feys. Combinatory Logic. North-Holland, Amsterdam, 1958.
[23] René David. Every unsolvable lambda term has a decoration. In Jean-Yves Girard, editor, TLCA, volume 1581 of LNCS, pages 98–113. Springer, 1999. doi:10.1007/3-540-48959-2_9.
[24] Mariangiola Dezani-Ciancaglini, Besik Dundua, Paola Giannini, and Furio Honsell. Sensible intersection type theories. 2025. URL: https://people.unipmn.it/giannini/dgh25.pdf.
[25] Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia Likavec. Behavioural inverse limit lambda-models. Theoretical Computer Science, 316(1):49–74, 2004. doi:10.1016/J.TCS.2004.01.023.
[26] Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko Motohama. Compositional characterisations of lambda-terms using intersection types. Theoretical Computer Science, 340(3):459–495, 2005. doi:10.1016/J.TCS.2005.03.011.
[27] Mariangiola Dezani-Ciancaglini and Stefania Lusin. Intersection types and lambda theories. CoRR, cs.LO/0211011, 2002. URL: http://arxiv.org/abs/cs/0211011.
[28] Pietro Di Gianantonio, Furio Honsell, and Marina Lenisa. A type assignment system for game semantics. Theoretical Computer Science, 398(1):150–169, 2008. doi:10.1016/j.tcs.2008.01.023.
[29] Erwin Engeler. Algebras and combinators. Algebra Universalis, 13:389–392, 1981. doi:10.1007/BF02483849.
[30] Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, TACS, volume 789 of LNCS, pages 555–574. Springer, 1994. doi:10.1007/3-540-57887-0_115.
[31] Pietro Di Gianantonio and Furio Honsell. An abstract notion of application. In Marc Bezem and Jan Friso Groote, editors, TLCA, volume 664 of LNCS, pages 124–138. Springer, 1993. doi:10.1007/BFB0037102.
[32] Pietro Di Gianantonio and Marina Lenisa. Innocent game semantics via intersection type assignment systems. In Simona Ronchi Della Rocca, editor, CSL, volume 23 of LIPIcs, pages 231–247. Schloss Dagstuhl, 2013. doi:10.4230/LIPICS.CSL.2013.231.
[33] Kurt Gödel, Solomon Feferman, John Dawson, Stephen Kleene, Gregory Moore, Robert Solovay, and Jean Heijenoort. Collected Works: Volume II Publications 1938-1974. Oxford University Press, June 2001. doi:10.1093/oso/9780195147216.001.0001.
[34] Roger Hindley and Giuseppe Longo. Lambda calculus models and extensionality. Mathematical Logic Quarterly, 26(19-21):289–310, 1980. doi:10.1002/malq.19800261902.
[35] Furio Honsell and Marina Lenisa. Semantical analysis of perpetual strategies in lambda-calculus. Theoretical Computer Science, 212(1-2):183–209, 1999. doi:10.1016/S0304-3975(98)00140-6.
[36] Furio Honsell and Marina Lenisa. “Wave-Style” geometry of interaction models in Rel are graph-like lambda-models. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 242–258. Springer, 2003. doi:10.1007/978-3-540-24849-1_16.
[37] Furio Honsell and Gordon Plotkin. On the completeness of order-theoretic models of the $\lambda$ -calculus. Information and Computation, 207, May 2009. doi:10.1016/j.ic.2008.03.027.
[38] Furio Honsell and Simona Ronchi Della Rocca. Reasoning about interpretations in qualitative $\lambda$ -models. In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods, pages 505–522. North-Holland, 1990. URL: https://people.uniud.it/sites/default/files/HR90.pdf.
[39] Furio Honsell and Simona Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49–75, 1992. doi:10.1016/0022-0000(92)90040-P.
[40] Giuseppe Jacopini. A condition for identifying two elements of whatever model of combinatory logic. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, pages 213–219. Springer, 1975. doi:10.1007/BFB0029527.
[41] Rainer Kerth. The interpretation of unsolvable $\lambda$ -terms in models of untyped $\lambda$ -calculus. Journal of Symbolic Logic, 63(4):1529–1548, 1998. doi:10.2307/2586665.
[42] Assaf J. Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and Computation, 10(3):411–436, 2000. doi:10.1093/LOGCOM/10.3.411.
[43] Jean-Jacques Lévy. An algebraic interpretation of the lambda beta-calculus and a labeled lambda-calculus. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, pages 147–165. Springer, 1975. doi:10.1007/BFB0029523.
[44] Giuseppe Longo. Set-theoretical models of $\lambda$ -calculus: theories, expansions, isomorphisms. Annals of Pure and Applied Logic, 24(2):153–188, 1983. doi:10.1016/0168-0072(83)90030-1.
[45] Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Logical semantics for stability. In Samson Abramsky, Michael W. Mislove, and Catuscia Palamidessi, editors, MFPS, volume 249 of ENTCS, pages 429–449. Elsevier, 2009. doi:10.1016/J.ENTCS.2009.07.101.
[46] David Park. The Y-combinator in Scott’s lambda-calculus models. Theory of Computation Report, University of Warwick. Department of Computer Science, 1976. URL: http://wrap.warwick.ac.uk/46310/.
[47] Gordon D. Plotkin. Set-theoretical and other elementary models of the lambda-calculus. Theoretical Computer Science, 121(1&2):351–409, 1993. doi:10.1016/0304-3975(93)90094-A.
[48] Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. EATCS. Springer, 2004. doi:10.1007/978-3-662-10394-4.
[49] Dana Scott. Continuous lattices. In Francis William Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of LNM, pages 97–136. Springer, 1972. doi:10.1007/BFb0073967.
[50] Dana S. Scott. Open problem n. II 4. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, page 369. Springer, 1975. doi:10.1007/BFb0029538.
[51] Dana S. Scott. Data types as lattices. SIAM Journal on Computing, 5(3):522–587, 1976. doi:10.1137/0205037.
[52] Jeremy G. Siek. Revisiting elementary denotational semantics. CoRR, abs/2312.02359, 2017. doi:10.48550/arXiv.1707.03762.
[53] Makoto Tatsuta and Mariangiola Dezani-Ciancaglini. Normalisation is insensible to lambda-term identity or difference. In LICS, pages 327–338. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.36.
[54] Cécile Zylberajch. Syntaxe et semantique de la facilité en lambda calcul. PhD thesis, Université de Paris VII, 1991. URL: https://theses.fr/1991PA077272.

[bib.bib1] [1] Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1-2):1–77, 1991. doi:10.1016/0168-0072(91)90065-T.

[bib.bib2] [2] Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105(2):159–267, 1993. doi:10.1006/INCO.1993.1044.

[bib.bib3] [3] Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1–94:30, 2018. doi:10.1145/3236789.

[bib.bib4] [4] Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Tailoring filter models. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 17–33. Springer, 2003. doi:10.1007/978-3-540-24849-1_2.

[bib.bib5] [5] Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoretical Computer Science, 355(2):108–126, 2006. doi:10.1016/j.tcs.2006.01.004.

[bib.bib6] [6] Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Furio Honsell. Filter models and easy terms. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, ICTCS, volume 2202 of LNCS, pages 17–37. Springer, 2001. doi:10.1007/3-540-45446-2_2.

[bib.bib7] [7] Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Stefania Lusin. Intersection types and domain operators. Theoretical Computer Science, 316(1):25–47, 2004. doi:10.1016/J.TCS.2004.01.022.

[bib.bib8] [8] Fabio Alessi and Stefania Lusin. Simple easy terms. In Steffen van Bakel, editor, ITRS, volume 70 of ENTCS, pages 1–18. Elsevier, 2002. doi:10.1016/S1571-0661(04)80487-0.

[bib.bib9] [9] Sandra Alves, Delia Kesner, and Miguel Ramos. Extending the quantitative pattern-matching paradigm. In Oleg Kiselyov, editor, APLAS, volume 15194 of LNCS, pages 84–105. Springer, 2024. doi:10.1007/978-981-97-8943-6_5.

[bib.bib10] [10] Jos C. M. Baeten and Bas Boerboom. Omega can be anything it should not be. In Indagationes Mathematicae, volume 82(2), pages 111–120, 1979. doi:10.1016/1385-7258(79)90016-7.

[bib.bib11] [11] Henk Barendregt. The Lambda Calculus - its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, 1985.

[bib.bib12] [12] Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983. doi:10.2307/2273659.

[bib.bib13] [13] Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Cambridge University Press, 2013. doi:10.1017/CBO9781139032636.

[bib.bib14] [14] Erika De Benedetti and Simona Ronchi Della Rocca. Bounding normalization time through intersection types. In ITRS, volume 121 of EPTCS, pages 48–57. Open Publishing Association, 2012. doi:10.4204/EPTCS.121.4.

[bib.bib15] [15] Alessandro Berarducci. Infinite $\lambda$ -calculus and non-sensible models. In Aldo Ursini, editor, Logic and Algebra, pages 17:1–17:39. Routledge, 1996. doi:10.1201/9780203748671-17.

[bib.bib16] [16] Alessandro Berarducci and Benedetto Intrigila. Church-Rosser lambda-theories, infinite lambda-terms and consistency problems. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss, editors, Logic: from Foundations to Applications, chapter 2, pages 33–58. Clarendon Press, 1996. URL: https://arpi.unipi.it/handle/11568/46466.

[bib.bib17] [17] Alexis Bernadet and Stéphane Graham-Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4):1–46, 2013. doi:10.2168/LMCS-9(4:3)2013.

[bib.bib18] [18] Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25:433–464, 2017. doi:10.1093/jigpal/jzx018.

[bib.bib19] [19] Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium ’82, volume 112 of Studies in Logic and the Foundations of Mathematics, pages 241–262. Elsevier, 1984. doi:10.1016/S0049-237X(08)71819-6.

[bib.bib20] [20] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal type schemes and lambda-calculus semantics. In Roger Hindley and Jonathan P. Seldin, editors, To H.B.Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 535–560. Academic Press, 1980. URL: http://www.di.unito.it/˜dezani/papers/CDV80.pdf.

[bib.bib21] [21] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms and $D_{\infty}$ -lambda-models. Information and Computation, 72(2):85–116, 1987. doi:10.1016/0890-5401(87)90042-3.

[bib.bib22] [22] Haskell B. Curry and Robert Feys. Combinatory Logic. North-Holland, Amsterdam, 1958.

[bib.bib23] [23] René David. Every unsolvable lambda term has a decoration. In Jean-Yves Girard, editor, TLCA, volume 1581 of LNCS, pages 98–113. Springer, 1999. doi:10.1007/3-540-48959-2_9.

[bib.bib24] [24] Mariangiola Dezani-Ciancaglini, Besik Dundua, Paola Giannini, and Furio Honsell. Sensible intersection type theories. 2025. URL: https://people.unipmn.it/giannini/dgh25.pdf.

[bib.bib25] [25] Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia Likavec. Behavioural inverse limit lambda-models. Theoretical Computer Science, 316(1):49–74, 2004. doi:10.1016/J.TCS.2004.01.023.

[bib.bib26] [26] Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko Motohama. Compositional characterisations of lambda-terms using intersection types. Theoretical Computer Science, 340(3):459–495, 2005. doi:10.1016/J.TCS.2005.03.011.

[bib.bib27] [27] Mariangiola Dezani-Ciancaglini and Stefania Lusin. Intersection types and lambda theories. CoRR, cs.LO/0211011, 2002. URL: http://arxiv.org/abs/cs/0211011.

[bib.bib28] [28] Pietro Di Gianantonio, Furio Honsell, and Marina Lenisa. A type assignment system for game semantics. Theoretical Computer Science, 398(1):150–169, 2008. doi:10.1016/j.tcs.2008.01.023.

[bib.bib29] [29] Erwin Engeler. Algebras and combinators. Algebra Universalis, 13:389–392, 1981. doi:10.1007/BF02483849.

[bib.bib30] [30] Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, TACS, volume 789 of LNCS, pages 555–574. Springer, 1994. doi:10.1007/3-540-57887-0_115.

[bib.bib31] [31] Pietro Di Gianantonio and Furio Honsell. An abstract notion of application. In Marc Bezem and Jan Friso Groote, editors, TLCA, volume 664 of LNCS, pages 124–138. Springer, 1993. doi:10.1007/BFB0037102.

[bib.bib32] [32] Pietro Di Gianantonio and Marina Lenisa. Innocent game semantics via intersection type assignment systems. In Simona Ronchi Della Rocca, editor, CSL, volume 23 of LIPIcs, pages 231–247. Schloss Dagstuhl, 2013. doi:10.4230/LIPICS.CSL.2013.231.

[bib.bib33] [33] Kurt Gödel, Solomon Feferman, John Dawson, Stephen Kleene, Gregory Moore, Robert Solovay, and Jean Heijenoort. Collected Works: Volume II Publications 1938-1974. Oxford University Press, June 2001. doi:10.1093/oso/9780195147216.001.0001.

[bib.bib34] [34] Roger Hindley and Giuseppe Longo. Lambda calculus models and extensionality. Mathematical Logic Quarterly, 26(19-21):289–310, 1980. doi:10.1002/malq.19800261902.

[bib.bib35] [35] Furio Honsell and Marina Lenisa. Semantical analysis of perpetual strategies in lambda-calculus. Theoretical Computer Science, 212(1-2):183–209, 1999. doi:10.1016/S0304-3975(98)00140-6.

[bib.bib36] [36] Furio Honsell and Marina Lenisa. “Wave-Style” geometry of interaction models in Rel are graph-like lambda-models. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 242–258. Springer, 2003. doi:10.1007/978-3-540-24849-1_16.

[bib.bib37] [37] Furio Honsell and Gordon Plotkin. On the completeness of order-theoretic models of the $\lambda$ -calculus. Information and Computation, 207, May 2009. doi:10.1016/j.ic.2008.03.027.

[bib.bib38] [38] Furio Honsell and Simona Ronchi Della Rocca. Reasoning about interpretations in qualitative $\lambda$ -models. In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods, pages 505–522. North-Holland, 1990. URL: https://people.uniud.it/sites/default/files/HR90.pdf.

[bib.bib39] [39] Furio Honsell and Simona Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49–75, 1992. doi:10.1016/0022-0000(92)90040-P.

[bib.bib40] [40] Giuseppe Jacopini. A condition for identifying two elements of whatever model of combinatory logic. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, pages 213–219. Springer, 1975. doi:10.1007/BFB0029527.

[bib.bib41] [41] Rainer Kerth. The interpretation of unsolvable $\lambda$ -terms in models of untyped $\lambda$ -calculus. Journal of Symbolic Logic, 63(4):1529–1548, 1998. doi:10.2307/2586665.

[bib.bib42] [42] Assaf J. Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and Computation, 10(3):411–436, 2000. doi:10.1093/LOGCOM/10.3.411.

[bib.bib43] [43] Jean-Jacques Lévy. An algebraic interpretation of the lambda beta-calculus and a labeled lambda-calculus. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, pages 147–165. Springer, 1975. doi:10.1007/BFB0029523.

[bib.bib44] [44] Giuseppe Longo. Set-theoretical models of $\lambda$ -calculus: theories, expansions, isomorphisms. Annals of Pure and Applied Logic, 24(2):153–188, 1983. doi:10.1016/0168-0072(83)90030-1.

[bib.bib45] [45] Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Logical semantics for stability. In Samson Abramsky, Michael W. Mislove, and Catuscia Palamidessi, editors, MFPS, volume 249 of ENTCS, pages 429–449. Elsevier, 2009. doi:10.1016/J.ENTCS.2009.07.101.

[bib.bib46] [46] David Park. The Y-combinator in Scott’s lambda-calculus models. Theory of Computation Report, University of Warwick. Department of Computer Science, 1976. URL: http://wrap.warwick.ac.uk/46310/.

[bib.bib47] [47] Gordon D. Plotkin. Set-theoretical and other elementary models of the lambda-calculus. Theoretical Computer Science, 121(1&2):351–409, 1993. doi:10.1016/0304-3975(93)90094-A.

[bib.bib48] [48] Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. EATCS. Springer, 2004. doi:10.1007/978-3-662-10394-4.

[bib.bib49] [49] Dana Scott. Continuous lattices. In Francis William Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of LNM, pages 97–136. Springer, 1972. doi:10.1007/BFb0073967.

[bib.bib50] [50] Dana S. Scott. Open problem n. II 4. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, page 369. Springer, 1975. doi:10.1007/BFb0029538.

[bib.bib51] [51] Dana S. Scott. Data types as lattices. SIAM Journal on Computing, 5(3):522–587, 1976. doi:10.1137/0205037.

[bib.bib52] [52] Jeremy G. Siek. Revisiting elementary denotational semantics. CoRR, abs/2312.02359, 2017. doi:10.48550/arXiv.1707.03762.

[bib.bib53] [53] Makoto Tatsuta and Mariangiola Dezani-Ciancaglini. Normalisation is insensible to lambda-term identity or difference. In LICS, pages 327–338. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.36.

[bib.bib54] [54] Cécile Zylberajch. Syntaxe et semantique de la facilité en lambda calcul. PhD thesis, Université de Paris VII, 1991. URL: https://theses.fr/1991PA077272.

Unsolvable Terms in Filter Models

Abstract

Keywords and phrases:

DOI:

Category:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Event:

Editors:

Series and Publisher:

1 Introduction

Outline.

2 𝝀-calculus

2.1 Standard Notions and Results

Definition 1 (λ-terms [11, Definition 2.1.1]).

Definition 2.

Definition 3 (β-rule and β-reduction [11, Definitions 2.1.15, 3.1.3 and 3.1.5]).

Definition 4 (Solvable and unsolvable λ-terms [11, Definition 2.2.10]).

Definition 5 (Head normal form and head redex [11, Definition 8.3.9]).

Proposition 6 (Shape of λ-terms [11, Corollary 8.3.8]).

Definition 7 (Head reduction [11, Definition 8.3.10]).

Theorem 8 ([11, Fact 2.2.12]).

2.2 Notions and Results on Unsolvable Terms

Definition 9 (Descendants of a λ-term [41, Definition 5.1]).

Definition 10 (Arguments [41, Definition 5.2]).

Definition 11 (Decoration of head reduction [41, Definition 5.3]).

Example 12.

Theorem 13 (Characterisation of unsolvability by decorations [23, Theorem 2]).

Definition 14 (Head closed λ-term and head order [41, Definition 6.1]).

Lemma 15 ([41, Lemma 6.5]).

Lemma 16.

Proof.

3 Intersection Types and Filter Models

Definition 17 (Intersection Type Theories).

Definition 18 (Type Assignment System).

Lemma 19 (Inversion Lemma [13, Theorem 14.1.1]).

Theorem 20 (Subject Expansion [13, Corollary 14.2.5(ii)]).

Theorem 21 (Subject Reduction [13, Proposition 14.2.1(ii)]).

Definition 22 (Target soundness).

Proposition 23.

Proof.

Definition 24 (β-soundness [13, Definition 14.1.4]).

Definition 25 (Lazy condition).

Definition 26 (Set condition).

Definition 27.

Lemma 28.

Proof.

The itt 𝓣 is set-like.

The itt 𝓣 is →-sound.

▶ Remark 29.

Definition 30 (λ-model [13, Definition 16.1.2]).

Definition 31 (Filter [13, Definition 13.4.1]).

Definition 32 (Filter Structure).

Theorem 33 ([13, Proposition 16.2.4]).

Theorem 34 ([13, Corollary 16.2.9(i)]).

Blanket Assumption.

Example 35.

Theorem 36.

Proof.

Definition 37 (Sensible Itt, Sensible Filter Model).

4 Critical Sequences for Intersection Type Theories

Definition 38.

Definition 39.

Example 40.

4.1 Lazy Itt’s

Theorem 41.

Proof.

4.2 Set-like and →-sound Itt’s

Theorem 42.

Proof.

Example 43.

▶ Remark 44.

5 Critical Sequences in Action

Theorem 45.

Proof.

Proposition 46.

Proof.

Example 47.

Example 48.

2 $\lambda$ -calculus

Definition 1 ( $\lambda$ -terms [11, Definition 2.1.1]).

Definition 3 ( $\beta$ -rule and $\beta$ -reduction [11, Definitions 2.1.15, 3.1.3 and 3.1.5]).

Definition 4 (Solvable and unsolvable $\lambda$ -terms [11, Definition 2.2.10]).

Proposition 6 (Shape of $\lambda$ -terms [11, Corollary 8.3.8]).

Definition 9 (Descendants of a $\lambda$ -term [41, Definition 5.1]).

Definition 14 (Head closed $\lambda$ -term and head order [41, Definition 6.1]).

Definition 24 ( $\beta$ -soundness [13, Definition 14.1.4]).

The itt ${\cal T}$ is set-like.

The itt ${\cal T}$ is $\to$ -sound.

$\blacktriangleright$ Remark 29.

Definition 30 ( $\lambda$ -model [13, Definition 16.1.2]).

4.2 Set-like and $\to$ -sound Itt’s

$\blacktriangleright$ Remark 44.

$\blacktriangleright$ Remark 52.