The Exp-Log Normal Form of Types and Canonical Terms for Lambda Calculus with Sums.

In the presence of sum types, the eta-long beta-normal form of terms of lambda calculus is not canonical. Natural deduction systems for intuitionistic logic (with disjunction) suffer the same defect, thanks to the Curry-Howard correspondence. This canonicity problem has been open in Proof Theory since the 1960s, while it has been addressed in Computer Science, since the 1990s, by a number of authors using de- cision procedures: instead of deriving a notion of syntactic canonical normal form, one gives a procedure based on program analysis to de- cide when any two terms of the lambda calculus with sum types are essentially the same one. In this paper, we show the canonicity problem is difficult because it is too specialized: rather then picking a canonical representative out of a class of beta-eta-equal terms of a given type, one should do so for the enlarged class of terms that are of a type isomorphic to the given one. We isolate a type normal form, ENF, generalizing the usual disjunctive normal form to handle exponentials, and we show that the eta-long beta-normal form of terms at ENF type is canonical, when the eta axiom for sums is expressed via evaluation contexts. By coercing terms from a given type to its isomorphic ENF type, our technique gives unique canonical representatives for examples that had previously been handled using program analysis.