A Finite Model Property for Intersection Types

TL;DR

This paper proves that the relational theory of intersection types called BCD has the finite model property, ensuring completeness for finite models, and demonstrates polynomial time decidability of the preorder <=.

Contribution

It establishes the finite model property for BCD intersection types and introduces rewriting techniques that lead to polynomial time decidability of the preorder.

Findings

BCD has the finite model property.

Rewriting techniques enable polynomial time decidability.

Completeness of BCD for finite models is proven.

Abstract

We show that the relational theory of intersection types known as BCD has the finite model property; that is, BCD is complete for its finite models. Our proof uses rewriting techniques which have as an immediate by-product the polynomial time decidability of the preorder <= (although this also follows from the so called beta soundness of BCD).