The Space of Interaction (long version)
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

TL;DR
This paper introduces a new intersection type system based on trees to measure the space complexity of Girard's geometry of interaction, providing insights into the space efficiency of the IAM and its relation to lambda calculus and Turing machine encodings.
Contribution
It presents a novel tree-based intersection type system that precisely measures the space consumption of the IAM, advancing understanding of space complexity in functional programs.
Findings
Space consumption of IAM linked to tree intersection types
Tree intersection types offer a finer analysis of space complexity
Encoding Turing machines into lambda calculus cannot prove IAM's space reasonableness
Abstract
The space complexity of functional programs is not well understood. In particular, traditional implementation techniques are tailored to time efficiency, and space efficiency induces time inefficiencies, as it prefers re-computing to saving. Girard's geometry of interaction underlies an alternative approach based on the interaction abstract machine (IAM), claimed as space efficient in the literature. It has also been conjectured to provide a reasonable notion of space for the lambda-calculus, but such an important result seems to be elusive. In this paper we introduce a new intersection type system precisely measuring the space consumption of the IAM on the typed term. Intersection types have been repeatedly used to measure time, which they achieve by dropping idempotency, turning intersections into multisets. Here we show that the space consumption of the IAM is connected to a…
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 · Computability, Logic, AI Algorithms · Parallel Computing and Optimization Techniques
