License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.9
URN: urn:nbn:de:0030-drops-77307
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7730/
Go to the corresponding LIPIcs Volume Portal

Barenbaum, Pablo ; Bonelli, Eduardo

Optimality and the Linear Substitution Calculus

pdf-format:
LIPIcs-FSCD-2017-9.pdf (0.6 MB)

Abstract

We lift the theory of optimal reduction to a decomposition of the lambda calculus known as the Linear Substitution Calculus (LSC). LSC decomposes beta-reduction into finer steps that manipulate substitutions in two distinctive ways: it uses context rules that allow substitutions to act "at a distance" and rewrites modulo a set of equations that allow substitutions to "float" in a term. We propose a notion of redex family obtained by adapting Lévy labels to support these two distinctive features. This is followed by a proof of the finite family developments theorem (FFD). We then apply FFD to prove an optimal reduction theorem for LSC. We also apply FFD to deduce additional novel properties of LSC, namely an algorithm for standardisation by selection and normalisation of a linear call-by-need reduction strategy. All results are proved in the axiomatic setting of Glauert and Khashidashvili's Deterministic Residual Structures.

BibTeX - Entry

@InProceedings{barenbaum_et_al:LIPIcs:2017:7730,
  author =	{Pablo Barenbaum and Eduardo Bonelli},
  title =	{{Optimality and the Linear Substitution Calculus}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7730},
  URN =		{urn:nbn:de:0030-drops-77307},
  doi =		{10.4230/LIPIcs.FSCD.2017.9},
  annote =	{Keywords: Rewriting, Lambda Calculus, Explicit Substitutions, Optimal Reduction}
}

Keywords: Rewriting, Lambda Calculus, Explicit Substitutions, Optimal Reduction
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI