[Prev][Next][Index][Thread]
1,x,+-term equality
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