A Theory of Explicit Substitutions with Safe and Full Composition

TL;DR

This paper develops a comprehensive theory of explicit substitutions for the lambda-calculus, achieving properties like full composition, beta-reduction simulation, and preservation of normalization, with implications for higher-order language implementations.

Contribution

It introduces a simple variable-style notation for explicit substitutions that ensures desirable properties like confluence and normalization preservation in lambda-calculus.

Findings

Achieves full composition and simulation of beta-reduction.

Preserves beta-strong normalization in typed terms.

Ensures confluence on metaterms.

Abstract

Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.