License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2012.6
URN: urn:nbn:de:0030-drops-34813
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3481/
Go to the corresponding LIPIcs Volume Portal

Accattoli, Beniamino

An Abstract Factorization Theorem for Explicit Substitutions

pdf-format:
4.pdf (0.5 MB)

Abstract

We study a simple form of standardization, here called factorization, for explicit substitutions calculi, i.e. lambda-calculi where beta-reduction is decomposed in various rules. These calculi, despite being non-terminating and non-orthogonal, have a key feature: each rule terminates when considered separately. It is well-known that the study of rewriting properties simplifies in presence of termination (e.g. confluence reduces to local confluence). This remark is exploited to develop an abstract theorem deducing factorization from some axioms on local diagrams. The axioms are simple and easy to check, in particular they do not mention residuals. The abstract theorem is then applied to some explicit substitution calculi related to Proof-Nets. We show how to recover standardization by levels, we model both call-by-name and call-by-value calculi and we characterize linear head reduction via a factorization theorem for a linear calculus of substitutions.

BibTeX - Entry

@InProceedings{accattoli:LIPIcs:2012:3481,
  author =	{Beniamino Accattoli},
  title =	{{An Abstract Factorization Theorem for Explicit Substitutions}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12) },
  pages =	{6--21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Ashish Tiwari},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3481},
  URN =		{urn:nbn:de:0030-drops-34813},
  doi =		{10.4230/LIPIcs.RTA.2012.6},
  annote =	{Keywords: lambda-calculus, Standardization, Explicit Substitutions, Abstract rewriting, Diagrammatic reasoning}
}

Keywords: lambda-calculus, Standardization, Explicit Substitutions, Abstract rewriting, Diagrammatic reasoning
Collection: 23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Issue Date: 2012
Date of publication: 29.05.2012

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