The Complexity of Interaction (Long Version)

TL;DR

This paper analyzes the complexity of functional programs in the interaction-net model, providing a method to certify concrete resource bounds through typed potentials, applicable to both sequential and parallel reductions.

Contribution

It introduces a novel approach using user-defined types and complexity potentials to certify resource bounds in interaction-net programs, applicable to various complexity classes.

Findings

Precise, compositional complexity analysis for interaction-net programs

Applicable to both sequential and parallel reductions

Illustrated on archetypal programming examples

Abstract

In this paper, we analyze the complexity of functional programs written in the interaction-net computation model, an asynchronous, parallel and confluent model that generalizes linear-logic proof nets. Employing user-defined sized and scheduled types, we certify concrete time, space and space-time complexity bounds for both sequential and parallel reductions of interaction-net programs by suitably assigning complexity potentials to typed nodes. The relevance of this approach is illustrated on archetypal programming examples. The provided analysis is precise, compositional and is, in theory, not restricted to particular complexity classes.