Normalization by evaluation for typed lambda calculus with coproducts

Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as "normalization by evaluation", and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.

1 Introduction

In this paper we solve the decision problem for simply typed lambda calculus with categorical coproduct (strong disjoint sum) types. While this calculus is both natural and simple, the decision problem is a long-standing thorny issue in the subject. Our solution is based on normalization by evaluation (NBE) (also called “reduction-free normalisation”) introduced by Martin-Löf [22] for weak typed lambda calculus, and by Berger and Schwichtenberg [6] for typed lambda calculus with -conversion. The technique has been further refined by the authors and coworkers using category-theoretic methods [7], [1], [8]. It has also been extended to other systems, such as System F [2]. As shown by Berger, Eberl, Schwichtenberg, and Danvy [5], [9], NBE techniques yield fast normalization algorithms, with applications in interactive proof systems [4] and type-directed partial evaluation [9], [10], [14].