On the Decision Problem for Typed Lambda Calculus with Coproducts

Martin Hofmann

We consider the decision problem for simply-typed lambda calculus with coproduct (disjoint union) types generated over one base type. Thus one adds to the simply typed lambda calculus over one base type a type former A + B and the following terms:

inl(t) : A + B, when t : A
inr(t) : A + B, when t : B
case(t_{1}, t_{2}, t_{3}) : C, when t_{1} : A + B, t_{2} : A→C, t_{3} : B→C

Two terms are semantically equivalent if they have the same denotation under the obvious set-theoretic interpretation which interprets the base type as an infinite set and coproduct types as disjoint union of sets.

For example, we have the equivalence:

case(x, λx.y, λx.y) = y

and more generally, if t_{1} = t_{2} then

case(x, λx.t_{1}, λx.t_{2}) = t_{1}(= t2)

provided that t_{1}, t_{2} do not contain x.

Dougherty and Subrahmanyam (1995) have shown that semantic equivalence is captured by the natural equational theory (BiCCC) arising from the theory of bicartesian closed categories.

A long-standing problem is to give an effective decision procedure for this theory BiCCC. We report here on a solution based on the technique of normalisation by evaluation (NBE) introduced by Schwichtenberg and Berger (1991) and further refined by the authors using category-theoretic methods.

We use NBE to associate normal forms with terms. The nontrivial equality between normal forms in then decided using a tableau-based proof system. Here the main technical results are admissibility of transitivity (corresponding to cut elimination) and detection of infinite branches.

Finally, the category-theoretic refinement of NBE (using sheaf theory and Grothendieck topologies) is used to establish completeness of the approach with respect to BiCCC. We remark that the relationship between BiCCC and Grothendieck topologies has been used by Fiore and Simpson (1997) to give a syntax-free characterisation of definability of set-theoretic functionals in the calculus above.

While a decision procedure for BiCCC has been announced by Ghani (1994) our method is quite different and we believe conceptually simpler. Our method also encompasses product types and an initial object.

This reports on joint work with

T. Altenkirch, Univ. of Munich, Germany P. Dybjer, Chalmers University, Sweden P. Scott, Univ. of Ottawa, Canada.

Address: LFCS Edinburgh, Mayfield Rd, Edinburgh EH9 3JZ, United Kingdom

E-mail: mxh@dcs.ed.ac.uk