Hereditary Substitution for the \lambda\Delta-Calculus

TL;DR

This paper extends hereditary substitution techniques to the lambda-Delta calculus, a non-constructive logic, demonstrating normalization through a novel application of this method.

Contribution

It introduces a non-trivial extension of hereditary substitution to the lambda-Delta calculus and uses it to prove normalization.

Findings

Hereditary substitution can be extended to the lambda-Delta calculus.

Normalization of the lambda-Delta calculus is proven using hereditary substitution.

Abstract

Hereditary substitution is a form of type-bounded iterated substitution, first made explicit by Watkins et al. and Adams in order to show normalization of proof terms for various constructive logics. This paper is the first to apply hereditary substitution to show normalization of a type theory corresponding to a non-constructive logic, namely the lambda-Delta calculus as formulated by Rehof. We show that there is a non-trivial extension of the hereditary substitution function of the simply-typed lambda calculus to one for the lambda-Delta calculus. Then hereditary substitution is used to prove normalization.