Three Subtyping Algorithms for Binary Session Types and their Complexity Analyses
Thien Udomsrirungruang, Nobuko Yoshida
TL;DR
The paper addresses the computational challenge of subtyping for synchronous binary session types by analyzing three algorithms: the original inductive Gay2005 method, a memoized optimization, and a new quadratic graph-based approach using XYZW-simulation. It shows that bottom-up and top-down subterm bounds are linear, leading to precise complexity results: the original is bounded by $O(n^{n^3})$ with a matching exponential lower bound, the memoized variant improves to $2^{O(n^2)}$ yet remains exponential, and the quadratic LTS-based approach achieves $O(n^2)$ via a $ ext{XYZW}$-simulation on a linear-size type LTS. This work also connects with prior results on automata-based and model-checking techniques, providing a unified, scalable framework for subtyping checks in binary session types. The methods have practical implications for type checkers and the design of session-type systems, and they offer a blueprint for extending to related session-type regimes.
Abstract
Session types are a type discipline for describing and specifying communication behaviours of concurrent processes. Session subtyping, firstly introduced by Gay and Hole, is widely used for enlarging typability of session programs. This paper gives the complexity analysis of three algorithms for subtyping of synchronous binary session types. First, we analyse the complexity of the algorithm from the original paper, which is based on an inductive tree search. We then introduce its optimised version, which improves the complexity, but is still exponential against the size of the two types. Finally, we propose a new quadratic algorithm based on a graph search using the concept of XYZW-simulation, recently introduced by Silva et al.