Intersection Types and Lambda Theories

TL;DR

This paper demonstrates how intersection types serve as a semantic tool to analyze the lattice of lambda theories, constructing models that prove the consistency of certain lambda theories and reveal their algebraic structure.

Contribution

It introduces the notion of easy intersection type theory and constructs filter models to study properties of lambda theories, showing their consistency and algebraic implications.

Findings

Constructed filter models for lambda theories

Proved the consistency of a well-known lambda theory

Revealed algebraic structure of the lattice of lambda theories

Abstract

We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of lambda theories. Relying on the notion of easy intersection type theory we successfully build a filter model in which the interpretation of an arbitrary simple easy term is any filter which can be described in an uniform way by a predicate. This allows us to prove the consistency of a well-know lambda theory: this consistency has interesting consequences on the algebraic structure of the lattice of lambda theories.