[Prev][Next][Index][Thread]

Re: lambda calculus with co-products



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
> 
>