【发布时间】：2012-06-08 09:08:42
【问题描述】：
我花了一两周时间编写一个简单的逻辑求解器。构建它之后，我发现自己想知道它所解决的语言是否是图灵完备的。所以我编写了一小组方程，它们接受 SKI 组合子演算中的任何有效表达式，并生成一个包含该表达式的正常形式的结果集。由于 SKI 是图灵完备的，证明我的语言可以执行 SKI 将证明其图灵完备。
但是有一个小故障。求解器不会按正常顺序减少表达式。实际上，它所做的是尝试所有可能的减少顺序。这意味着解决方案集通常是巨大的。如果一个正常的形式存在，它会在那里某处，但很难告诉在哪里。
这给我带来了两个问题：
我的语言图灵完备吗？还是我需要找到更好的证据？
解的数量是输入的可计算函数吗？
(起初我假设解决方案集的大小是输入大小的指数或阶乘。但仔细观察，这不是真的。你可以写已经是正常形式的巨大表达式，而微小的表达式不要终止。我觉得确定解决方案集的大小可能等同于解决停止问题，但我不完全确定......）
【问题讨论】：
-
如果一个减少订单没有终止而另一个订单终止会发生什么？你得到终结者了吗？
-
哦，你的 SKI 实现就是我需要的所有证明，证明它是图灵完备的。
-
@augustss 我已经仔细安排了代码尝试正常的降序first。因此，如果存在范式，它将位于解集中的有限位置。但是，如果存在非终止归约顺序，则保证 soler 找到它，并产生无限解集。是否产生一个无限集，其中 包含 正确答案 somewhere 足以实现图灵完备性？我的意思是，简单地列举所有可能的 SKI 表达式就可以了……
-
首先，我假设您的解决方案集在呈现时以某种方式排序。 （否则你不会看到任何有趣的东西。）如果是这样，为什么正常的订单减少不是第一个出现的？
-
解决方案按求解器发现它们的顺序编号。整个归约序列出现，而不仅仅是最终结果。在不知道归约序列有多长的情况下，无法判断不可归约的结果将出现在哪里。