DROPS

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 Strong Call-By-Need Calculus

Abstract

Cite as

Axiomatic Sharing-via-Labelling

Abstract

Cite as

Thanks for your feedback!

Could not send message