双笛卡尔闭范畴的可判定性

Question

自由双笛卡尔闭范畴(BCCC)的决策问题是可判定的吗？等价地，对于具有强n值积和和的简单类型lambda演算，等式可判定吗？对于免费的几乎BCCC的决策问题是可以确定的：

http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf

但这项工作不包括初始对象，也不包括空类型的lambda-calulus术语，尽管他们推测他们的方法可以扩展到BCCCs。

Answer 1

我将给出一个部分的答案，这将有助于说明为什么最初的对象被排除在外。当初始对象与指数组合时，或者终端对象与共指数组合时，事物就开始崩溃。当指数和共指数都存在时，这种崩溃就会完全完成；在这种情况下，可判定性问题变得微不足道，在逻辑上降为可证明性，而“正常形式”约简问题变得更加困难--讽刺的是。

我在这里贴了更多的细节。我不能在这里回答它，因为StackOverflow中的“格式不正确的代码”错误使它的接口无法修复。(即使是在一个空的显示窗口，我的回答中也没有计算机编程，因为这甚至不是一个计算机问题！)

https://math.stackexchange.com/questions/4032422/decidability-of-bi-cartesian-closed-categories