Confluent terminating extensional lambda-calculi with surjective pairing and terminal type

TL;DR

This paper proves the strong normalization of a confluent rewriting system for lambda-calculi with surjective pairing and terminal types, extending previous work by Curien and Di Cosmo.

Contribution

It introduces a relativized reducibility method to prove strong normalization for the system, including its polymorphic extension.

Findings

Proves SN of Curien-Di Cosmo's rewriting system.

Establishes SN for the polymorphic extension.

Introduces a relativized reducibility method for SN proof.

Abstract

For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo were inspired by Knuth-Bendix completion, and introduced a confluent rewriting system that (1) extends the naive rewriting system, and (2) is stable under contexts. The rewriting system has (i) a rule that rewrites term of a terminal type rewrites to a term constant *, unless the term is not *, (ii) rewrite rules for the extensionality of function types and product types, and rewrite rules mediating the rewrite rules (i) and (ii). Curien and Di Cosmo supposed that because of (iii), any reducibility method cannot prove the strong normalization (SN) of Curien-Di Cosmo's rewriting system, and they left the SN open. By relativizing Girard's reducibility method to the *-free terms, we prove SN of their rewriting, and SN of the extension by polymorphism. The relativization works because: for any SN term t, and for any variable z of terminal type not occurring in $t$, t with all the occurrences of * of terminal type replaced by the variable z is SN.