Paper: A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus (at LICS 2026)

Authors: Thibaut Balabonski

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.9

Abstract

We propose a simple space-cost measure for the λ-calculus, that extends the natural model measuring the size of the terms by also taking into consideration their origin. This new model is able to capture sublinear space complexity and we prove that, in the context of weak reduction, it is reasonable with respect to standard complexity theory. Precisely, the weak λ-calculus and Turing machines can simulate each other with a constant-factor space overhead, for any computation of logarithmic or higher space complexity. This means that the weak λ-calculus equipped with our cost model gives a proper characterization of the classical space complexity classes, including LOGSPACE and PSPACE.

BibTeX

  @InProceedings{Balabonski-AMachineIndependent,
    author = 	 {Thibaut Balabonski},
    title = 	 {A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {9:1--9:26},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.9}
  }