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.2019.7
URN: urn:nbn:de:0030-drops-105144
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10514/
Go to the corresponding LIPIcs Volume Portal

Bendkowski, Maciej

Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus

pdf-format:
LIPIcs-FSCD-2019-7.pdf (0.6 MB)

Abstract

Substitution resolution supports the computational character of beta-reduction, complementing its execution with a capture-avoiding exchange of terms for bound variables. Alas, the meta-level definition of substitution, masking a non-trivial computation, turns beta-reduction into an atomic rewriting rule, despite its varying operational complexity. In the current paper we propose a somewhat indirect average-case analysis of substitution resolution in the classic lambda-calculus, based on the quantitative analysis of substitution in lambda-upsilon, an extension of lambda-calculus internalising the upsilon-calculus of explicit substitutions. Within this framework, we show that for any fixed n >= 0, the probability that a uniformly random, conditioned on size, lambda-upsilon-term upsilon-normalises in n normal-order (i.e. leftmost-outermost) reduction steps tends to a computable limit as the term size tends to infinity. For that purpose, we establish an effective hierarchy (G_n)_n of regular tree grammars partitioning upsilon-normalisable terms into classes of terms normalising in n normal-order rewriting steps. The main technical ingredient in our construction is an inductive approach to the construction of G_{n+1} out of G_n based, in turn, on the algorithmic construction of finite intersection partitions, inspired by Robinson's unification algorithm. Finally, we briefly discuss applications of our approach to other term rewriting systems, focusing on two closely related formalisms, i.e. the full lambda-upsilon-calculus and combinatory logic.

BibTeX - Entry

@InProceedings{bendkowski:LIPIcs:2019:10514,
  author =	{Maciej Bendkowski},
  title =	{{Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{7:1--7:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10514},
  URN =		{urn:nbn:de:0030-drops-105144},
  doi =		{10.4230/LIPIcs.FSCD.2019.7},
  annote =	{Keywords: lambda calculus, explicit substitutions, complexity, combinatorics}
}

Keywords: lambda calculus, explicit substitutions, complexity, combinatorics
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019

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