Multi Types and Reasonable Space (Long Version)

2022/07/18 by Accattoli, Beniamino, Lago, Ugo Dal, Vanoni, Gabriele
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2207.08795

Abstract

Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system.

Related

• Reasonable Space for the λ-Calculus, Logarithmically
• The Space of Interaction (long version)
• Execution Time of lambda-Terms via Denotational Semantics and Intersection Types
• Semantic Bound and Multi Types, Revisited
• Types by Need (Extended Version)