Towards the average-case analysis of substitution resolution in λ-calculus
Maciej Bendkowski · Jagiellonian University Repository (Jagiellonian University) · 2019
Substitution resolution supports the computational character ofβ-reduction, complementing itsexecution with a capture-avoiding exchange of terms for bound variables. Alas, the meta-leveldefinition of substitution, masking a non-trivial computation, turnsβ-reduction into an atomicrewriting rule, despite its varying operational complexity. In the current paper we propose asomewhat indirect average-case analysis of substitution resolution in the classicλ-calculus, basedon the quantitative analysis of substitution inλυ, an extension ofλ-calculus internalising theυ-calculus of explicit substitutions. Within this framework, we show that for any fixedn≥0, theprobability that a uniformly random, conditioned on size,λυ-termυ-normalises innnormal-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(Gn)nof regular tree grammars partitioningυ-normalisable terms into classes of terms normalising innnormal-order rewriting steps. The maintechnical ingredient in our construction is an inductive approach to the construction ofGn+1outofGnbased, in turn, on the algorithmic construction of finite intersection partitions, inspired byRobinson’s unification algorithm. Finally, we briefly discuss applications of our approach to otherterm rewriting systems, focusing on two closely related formalisms, i.e. the fullλυ-calculus andcombinatory logic.