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 λ-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 λ-calculus cannot be used to prove that the space of the IAM is a reasonable cost model.

Accattoli B., Dal Lago U., Vanoni G. (2021). The Space of Interaction. Institute of Electrical and Electronics Engineers Inc. [10.1109/LICS52264.2021.9470726].

The Space of Interaction

Accattoli B.;Dal Lago U.;Vanoni G.
2021

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 λ-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 λ-calculus cannot be used to prove that the space of the IAM is a reasonable cost model.
2021
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
1
13
Accattoli B., Dal Lago U., Vanoni G. (2021). The Space of Interaction. Institute of Electrical and Electronics Engineers Inc. [10.1109/LICS52264.2021.9470726].
Accattoli B.; Dal Lago U.; Vanoni G.
File in questo prodotto:
File Dimensione Formato  
main.pdf

Open Access dal 08/01/2022

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 703.93 kB
Formato Adobe PDF
703.93 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/834277
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 3
social impact