Analysis of Bounds for Lengths of Reductions in Typed λ-calculus - Galoyan, Tigran M. (Mathematical Problems of Computer Science, 2021)
We analyze bounds for the lengths of arbitrary reduction sequences of terms in typed ¸-calculus, consider some estimates obtained by the other authors and compare these estimates. The cut elimination and normalization algorithms are also investigated in this paper. Thereafter we re¯ne the estimates achieved in [3] (for pure implicational logic only) by supplement of ´-conversion and then we extend evaluations to ¯rst-order logic.