Transitivity of Subtyping for Intersection Types

TL;DR

This paper introduces a simplified subtyping system for intersection types that omits transitivity, providing a direct proof of transitivity and ensuring the subformula conjunction property, thus improving proof efficiency and clarity.

Contribution

Develops a regular style subtyping system without transitivity, with a direct proof of transitivity, reducing proof complexity and enhancing theoretical understanding.

Findings

The new system is equivalent to the classical Barendregt-Coppo-Dezani system.

It satisfies the subformula conjunction property.

The proof length for transitivity is significantly reduced.

Abstract

The subtyping rules for intersection types traditionally employ a transitivity rule (Barendregt et al. 1983), which means that subtyping does not satisfy the subformula property, making it more difficult to use in filter models for compiler verification. Laurent develops a sequent-style subtyping system, without transitivity, and proves transitivity via a sequence of six lemmas that culminate in cut-elimination (2018). This article develops a subtyping system in regular style that omits transitivity and provides a direct proof of transitivity, significantly reducing the length of the proof, exchanging the six lemmas for just one. Inspired by Laurent's system, the rule for function types is essentially the $\beta$-soundness property. The new system satisfies the "subformula conjunction property": every type occurring in the derivation of $A <: B$ is a subformula of $A$ or $B$, or an intersection of such subformulas. The article proves that the new subtyping system is equivalent to that of Barendregt, Coppo, and Dezani-Ciancaglini.