Towards the average-case analysis of substitution resolution in \lambda-calculus

DOI10.4230/LIPICS.FSCD.2019.7MaRDI QIDQ6311025arXivFDO

Authors Maciej Bendkowski

Publication date 11 December 2018

Published in arXiv

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2019.7

Mathematics Subject Classification ID

Exact enumeration problems, generating functions (05A15) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

arXiv classification

cs.LOmath.CO

Abstract: Substitution resolution supports the computational character of $$-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 $$-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 $lambdaupsilon$, an extension of $lambda$-calculus internalising the $upsilon$-calculus of explicit substitutions. Within this framework, we show that for any fixed $ngeq0$, the probability that a uniformly random, conditioned on size, $lambdaupsilon$-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 $left(mathscr{G}_{n}ight{)}_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 $mathscr{G}_{n+1}$ out of $mathscr{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 $lambdaupsilon$-calculus and combinatory logic.

This page was built for publication: Towards the average-case analysis of substitution resolution in $\lambda$-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6311025)