A confluent reduction for the λ—calculus with surjective pairing and terminal object

Abstract

We exhibit confluent and effectively weakly normalizing (thus decidable) rewriting systems for the full equational theory underlying cartesian closed categories, and for polymorphic ex­tensions of it. The λ-calculus extended with surjective pairing has been well-studied in the last two decades. It is not confluent in the untyped case, and confluent in the typed case. But to the best of our knowledge the present work is the first treatment of the lambda calculus extended with surjective pairing and terminal object via a confluent rewriting sytem, and is the first solution to the decidability problem of the full equational theory of Cartesian Closed Categories extended with polymorphic types. Our approach yields conservativity results as well. In separate papers we apply our results to the study of provable type isomorphisms, and to the decidability of equality in a typed λ-calculus with subtyping.