DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.9

A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus

Authors: Thibaut Balabonski

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

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.

Cite as

Thibaut Balabonski. A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{balabonski:LIPIcs.LICS.2026.9,
  author =	{Balabonski, Thibaut},
  title =	{{A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{9:1--9:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.9},
  URN =		{urn:nbn:de:0030-drops-267961},
  doi =		{10.4230/LIPIcs.LICS.2026.9},
  annote =	{Keywords: Lambda-calculus, Complexity, Space, Logspace, Weak reduction}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2021.9

A Strong Call-By-Need Calculus

Authors: Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract

We present a call-by-need λ-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a λ-term t admits a normal form n in the λ-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design.

Cite as

Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A Strong Call-By-Need Calculus. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{balabonski_et_al:LIPIcs.FSCD.2021.9,
  author =	{Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
  title =	{{A Strong Call-By-Need Calculus}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{9:1--9:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9},
  URN =		{urn:nbn:de:0030-drops-142477},
  doi =		{10.4230/LIPIcs.FSCD.2021.9},
  annote =	{Keywords: strong reduction, call-by-need, evaluation strategy, normalization}
}

Document

DOI: 10.4230/LIPIcs.RTA.2012.85

Axiomatic Sharing-via-Labelling

Authors: Thibaut Balabonski

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract

A judicious use of labelled terms makes it possible to bring together the simplicity of term rewriting and the sharing power of graph rewriting: this has been known for twenty years in the particular case of orthogonal first-order systems. The present paper introduces a concise and easily usable axiomatic presentation of sharing-via-labelling techniques that applies to higher-order term rewriting as well as to non-orthogonal term rewriting. This provides a general framework for the sharing of subterms and keeps the formalism as simple as term rewriting.

Cite as

Thibaut Balabonski. Axiomatic Sharing-via-Labelling. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 85-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{balabonski:LIPIcs.RTA.2012.85,
  author =	{Balabonski, Thibaut},
  title =	{{Axiomatic Sharing-via-Labelling}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{85--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.85},
  URN =		{urn:nbn:de:0030-drops-34868},
  doi =		{10.4230/LIPIcs.RTA.2012.85},
  annote =	{Keywords: Sharing, Abstract term rewriting, Graphs, Higher order, Non-orthogonality}
}

Search Results

Documents authored by Balabonski, Thibaut

A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus

Abstract

Cite as

A Strong Call-By-Need Calculus

Abstract

Cite as

Axiomatic Sharing-via-Labelling

Abstract

Cite as

Thanks for your feedback!

Could not send message