Deriving SN from PSN: a general proof technique

TL;DR

This paper introduces a general proof technique that derives strong normalization (SN) from preservation of strong normalization (PSN) in explicit substitution calculi, simplifying proofs of termination.

Contribution

It formalizes a novel method to establish SN from PSN by expanding substitutions into pure lambda-terms, applicable to various calculi with explicit substitutions.

Findings

Successfully applied to multiple calculi with explicit substitutions

Allows tracing SN failure back to PSN failure

Simplifies proving termination properties in lambda calculus

Abstract

In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easily proved, only one of them is usually established (and sometimes none). We propose here a connection between them which helps to get SN when one already has PSN. For this purpose, we formalize a general proof technique of SN which consists in expanding substitutions into "pure" lambda-terms and to inherit SN of the whole calculus by SN of the "pure" calculus and by PSN. We apply it successfully to a large set of calculi with explicit substitutions, allowing us to establish SN, or, at least, to trace back the failure of SN to that of PSN.