Abstract
Substitution resolution supports the computational character of betareduction, complementing its execution with a captureavoiding exchange of terms for bound variables. Alas, the metalevel definition of substitution, masking a nontrivial computation, turns betareduction into an atomic rewriting rule, despite its varying operational complexity. In the current paper we propose a somewhat indirect averagecase analysis of substitution resolution in the classic lambdacalculus, based on the quantitative analysis of substitution in lambdaupsilon, an extension of lambdacalculus internalising the upsiloncalculus of explicit substitutions. Within this framework, we show that for any fixed n >= 0, the probability that a uniformly random, conditioned on size, lambdaupsilonterm upsilonnormalises in n normalorder (i.e. leftmostoutermost) 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 upsilonnormalisable terms into classes of terms normalising in n normalorder 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 lambdaupsiloncalculus and combinatory logic.
BibTeX  Entry
@InProceedings{bendkowski:LIPIcs:2019:10514,
author = {Maciej Bendkowski},
title = {{Towards the AverageCase Analysis of Substitution Resolution in LambdaCalculus}},
booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
pages = {7:17:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771078},
ISSN = {18688969},
year = {2019},
volume = {131},
editor = {Herman Geuvers},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10514},
URN = {urn:nbn:de:0030drops105144},
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 