[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----] Dear All: I inadvertantly gave some wrong bibliographic information. The first paper to use type environments with constraints is in Dan Dougherty and Ramesh Subrahmanyam, prelim. version in LICS 1995 (pp. 282-291), and URL for full version is: http://ddougherty.web.wesleyan.edu/my_papers/equality_coproducts.ps While I'm on the topic, I should mention the early work of Dan Dougherty on lambda calculi with coproducts (RTA5, SLNCS 690). More bibliography and history of the coproduct problem, at least insofar as we know it, is contained in our paper referred to below. We would of course be happy to know of additional results, overlooked bibliography, etc. Sincerely, Phil Scott On Tue, 20 Nov 2001, P. Scott wrote:
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
Bob: This is proved decidable (at least, officially, without initial object type) in a paper by Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and me in last years' LICS2001. The proof uses categorical techniques (functor categories and sheaves) and is a version of "reduction-free normalization" or "normalization by evaluation (NBE)". This is a categorical souped-up version of a technique due I suppose originally to Martin-Lof, but independently in LICS'91 by Berger and Schwichtenberg. Along the way, we use a more involved calculus, due originally to Riecke and Subrahmanyam, and later Fiore and Simpson, of "typing judgements with constraints". A decidability result for coproduct types is also developed by N. Ghani in his Edinburgh PhD thesis(1995) using very heavy rewriting techniques. An outline of his proof is in his paper "beta-eta-equality for coproducts", SLN902 (TLCA95). Again, without initial object type.
Cheers, Philip Scott
P.S. Our paper is at : ftp://ftp.cs.chalmers.se/pub/clics/peterd/Sheaves.ps
On Tue, 20 Nov 2001, Robert Harper wrote:
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
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