[Prev][Next][Index][Thread]
Re: lambda calculus with co-products
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
> >
> >
>