Linear Depth Increase of Lambda Terms along Leftmost-Outermost Beta-Reduction

TL;DR

This paper demonstrates that, unlike size, the depth of lambda terms along leftmost-outermost beta-reduction sequences increases only linearly with the number of steps, providing insights into computational complexity.

Contribution

It establishes a linear bound on depth increase during leftmost-outermost beta-reduction and extends this result to lambda-lifting transformed term rewriting systems.

Findings

Depth increases linearly with steps in leftmost-outermost reduction

Depth bound applies to lambda-lifting representations

Supports polynomial overhead in reduction sequence implementations

Abstract

Performing $n$ steps of $\beta$-reduction to a given term in the $\lambda$-calculus can lead to an increase in the size of the resulting term that is exponential in $n$. The same is true for the possible depth increase of terms along a $\beta$-reduction sequence. We explain that the situation is different for the leftmost-outermost strategy for $\beta$-reduction: while exponential size increase is still possible, depth increase is bounded linearly in the number of steps. For every $\lambda$-term $M$ with depth $d$, in every step of a leftmost-outermost $\beta$-reduction rewrite sequence starting from $M$ the term depth increases by at most $d$. Hence the depth of the $n$-th reduct of $M$ in such a rewrite sequence is bounded by $d\cdot (n+1)$. We prove the lifting of this result to $\lambda$-term representations as orthogonal first-order term rewriting systems, which can be obtained by the lambda-lifting transformation. For the transfer to lambda-calculus, we rely on correspondence statements via lambda-lifting. We argue that the linear-depth-increase property can be a stepping stone for an alternative proof of, and so can shed new light on, a result by Accattoli and Dal Lago (2015) that states: leftmost-outermost $\beta$-reduction rewrite sequences of length $n$ in the lambda-calculus can be implemented on a reasonable machine with an overhead that is polynomial in $n$ and the size of the initial term.