The Space of Interaction (long version)

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 further structural modification, turning multisets into trees. Tree intersection types lead to a finer understanding of some space complexity results from the literature. They also shed new light on the conjecture about reasonable space: we show that the usual way of encoding Turing machines into the lambda calculus cannot be used to prove that the space of the IAM is a reasonable cost model.