lambda calculus with co-products

• To: "'types@cis.upenn.edu'" <types@cis.upenn.edu>
• Subject: lambda calculus with co-products
• From: Robert Harper <Robert.Harper@cs.cmu.edu>
• Date: Tue, 20 Nov 2001 18:07:23 -0500

What is known about the decision problem for equality for typed lambda terms
with sum types, taking equality to include the full "co-product" equation
stating that case(M,x.N[inl(x)/u],y.N[inr(y)/u]) = N[M/u]?

This theory is stronger (equates more terms) than the one that takes only
Girard's commuting conversions (described in Proofs and Types, Chapter 10),
which is decidable.  (Girard sketches a proof via a confluence and strong
normalization argument.)

However, we are not familiar with any results covering the more general case
of co-products.  Any pointers or a quick summary would be helpful.

Thanks!
Bob Harper
Karl Crary

• Prev: CFP: 4th International Workshop on Implicit Computational Complexity
• Next: Re: lambda calculus with co-products
• Index(es):
  • Main
  • Thread