Delayed substitutions

Abstract

This paper investigates an approach to substitution alternative to the implicit treatment of the $\lambda$-calculus and the explicit treatment of explicit substitution calculi. In this approach, substitutions are delayed (but not executed) explicitly. We implement this idea with two calculi, one where substitution is a primitive construction of the calculus, the other where substitutions is represented by a $\beta$-redex. For both calculi, confluence and (preservation of) strong normalisation are proved (the latter fails for a related system due to Revesz, as we show). Applications of delayed substitutions are of theoretical nature. The strong normalisation result implies strong normalisation for other calculi, like the computational lambda-calculus, lambda-calculi with generalised applications, or calculi of cut-elimination for sequent calculus. We give an investigation of the computational interpretation of cut-elimination in terms of generation, execution, and delaying of substitutions, paying particular attention to how generalised applications improve such interpretation.