2021/04/28 by Beniamino Accattoli, Accattoli, Beniamino, Ugo Dal Lago +3
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2104.13795
openalex publication_date 2021/04/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.