Subtyping for F-Bounded Quantifiers and Equirecursive Types (Extended Version)

TL;DR

This paper introduces a novel model using binding trees for second-order type systems with F-bounded quantifiers and equirecursive types, establishing subtyping and type equality rules with soundness and completeness.

Contribution

It develops a formal framework of regular binding trees for complex type systems, including subtyping, automata-based representations, and decision algorithms.

Findings

Defines binding trees for second-order types

Proves soundness and completeness of subtyping rules

Provides a polynomial-time subtyping decision algorithm

Abstract

This paper defines a notion of binding trees that provide a suitable model for second-order type systems with F-bounded quantifiers and equirecursive types. It defines a notion of regular binding trees that correspond in the right way to notions of regularity in the first-order case. It defines a notion of subtyping on these trees and proves various properties of the subtyping relation. It defines a mapping from types to trees and shows that types produce regular binding trees. It presents a set of type equality and subtyping rules, and proves them sound and complete with respect to the tree interpretation. It defines a notion of binding-tree automata and how these generate regular binding trees. It gives a polynomial-time algorithm for deciding when two automata's trees are in the subtyping relation.