1,x,+-term equality

• To: types@cs.indiana.edu
• Subject: 1,x,+-term equality
• From: Neil Ghani <N.Ghani@cs.bham.ac.uk>
• Date: Tue, 16 Sep 1997 15:17:37 +0100 (BST)
• Delivery-Date: Tue, 16 Sep 1997 09:18:45 -0500

I wrote a paper on the decidability of the term equlaity of the simply
typed lambda calculus extended with coproducts. But it was horrendously
complicated and so I thought I could explain my arguments if I were to
drop the -> type constructor and simply work with 1,x,+-fragment

My question is whether the decidability of the term equality for the
1,+,x-fragment has been considered in the literature and in particular is
it trivial and rather obvious.

(By term equality, I mean the one that is sound and complete for the usual
categorical models)

Thanks for your help

Neil Ghani

• Prev: JICSLP'98 -- First CFP
• Next: ICCL'98 Call For Papers
• Index(es):
  • Main
  • Thread