The Complexity of Interaction (Long Version)
St\'ephane Gimenez, Georg Moser

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Parallel Computing and Optimization Techniques · Formal Methods in Verification
