Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Three Subtyping Algorithms for Binary Session Types and their Complexity Analyses (full version)

Thien Udomsrirungruang, Nobuko Yoshida

TL;DR

Addressing subtyping for synchronous binary session types, the paper analyzes three algorithms and introduces a quadratic, $XYZW$-simulation-based approach. It shows the original Gay2005 inductive algorithm runs in $O(n^{n^3})$ time, while a memoized variant reduces to $2^{O(n^2)}$, and the new quadratic algorithm achieves $O(n^2)$ time through a graph-based reachability check on a type LTS. The quadratic method encodes types as a labeled transition system and reduces subtyping to a $XYZW$-simulation, providing a provably efficient solution. The work contextualizes these results with respect to prior automata-based and modal-calculus approaches and outlines potential applicability to broader session-type systems.

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 $\mathcal{XYZW}$-simulation, recently introduced by Silva et al.

Three Subtyping Algorithms for Binary Session Types and their Complexity Analyses (full version)

TL;DR

Addressing subtyping for synchronous binary session types, the paper analyzes three algorithms and introduces a quadratic, -simulation-based approach. It shows the original Gay2005 inductive algorithm runs in time, while a memoized variant reduces to , and the new quadratic algorithm achieves time through a graph-based reachability check on a type LTS. The quadratic method encodes types as a labeled transition system and reduces subtyping to a -simulation, providing a provably efficient solution. The work contextualizes these results with respect to prior automata-based and modal-calculus approaches and outlines potential applicability to broader session-type systems.

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 -simulation, recently introduced by Silva et al.
Paper Structure (10 sections, 15 theorems, 9 equations, 5 figures, 1 table)

This paper contains 10 sections, 15 theorems, 9 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Inductive subtyping algorithms
  4. Number of subterms.
  5. An inductive algorithm Gay2005
  6. An algorithm with memoization
  7. Quadratic subtyping algorithm
  8. Related work
  9. Acknowledgements.
  10. Appendix

Key Result

Lemma 3.1

$|\text{Sub}(T)| \leq |T|$.

Figures (5)

  • Figure 1: Algorithmic rules for subtyping, taken from Gay2005.
  • Figure 2: A memoized subtyping algorithm.
  • Figure 3: Rules for the type LTS.
  • Figure 4: Graph for $(T^\mathsf{interface}_2, T^\mathsf{interface}_3)$.
  • Figure A.1: The algorithm in Theorem \ref{['thm:quadratic_binary_subtyping']} written in procedural form.

Theorems & Definitions (46)

  • Definition 2.1: Session Types
  • Definition 2.2: Unfolding
  • Definition 2.3: Coinductive subtyping
  • Definition 2.4: Coinductive equality
  • Example 2.5: Interface
  • Definition 2.6: Size
  • Definition 2.7: Bottom-up subterms
  • Definition 2.8: Top-down subterms
  • Lemma 3.1
  • proof
  • ...and 36 more