lambda-calculus - 双笛卡尔封闭类别的可判定性

Question

自由双笛卡尔封闭范畴（BCCC）的决策问题是否可判定？等效地，对于使用强 n 元乘积和总和扩展的简单类型 lambda 演算，是否可以判定相等？几乎免费的BCCC的决策问题是可判定的：

但是这项工作不包括初始对象或 lambda 演算术语中的空类型，尽管他们推测他们的方法可以扩展到 BCCC。

score 0 · Accepted Answer

我将给出一个部分答案，这将有助于说明为什么要排除初始对象。当初始对象与指数相结合时，事情开始崩溃；或具有协指数的终端对象。当指数和协指数同时存在时，这种坍缩就完成了；在这种情况下，可判定性问题变得微不足道，在逻辑上简化为可证明性，而“范式”简化问题变得更加困难——具有讽刺意味的是。

我在这里发布了更多详细信息。我在这里无法回答，因为 StackOverflow 中的“代码格式不正确”误报错误导致其界面损坏无法修复。（即使是空的显示窗口，我也能理解，而且我的答案中没有计算机编程，因为这甚至不是计算机问题！）

1 回答 1