我花了一两个星期编写一个简单的逻辑求解器。构建它后，我发现自己想知道它解决的语言是否是图灵完备的。因此，我编写了一小组方程，这些方程接受SKI组合器演算中的任何有效表达式，并生成一个包含该表达式的正常形式的结果集。由于SKI是图灵完备的，证明我的语言可以执行SKI将证明它的图灵完备性。
但是，有一个故障。求解器不会按正常顺序减少表达式。实际上，它所做的是尝试所有可能的减少订单。这意味着解决方案集通常很大。如果存在正常形式，它将在某个地方，但很难说在哪里。
这让我想到了两个问题：
-
我的语言是图灵完备的吗？还是我需要找到更好的证据？
-
解的数量是输入的可计算函数吗？
（起初，我假设解决方案集的大小在输入大小中是指数或阶乘的。但仔细观察，事实并非如此。您可以编写已经处于正常形式的大表达式，以及不会终止的微小表达式。我有一种感觉，确定解决方案集的大小可能等同于解决停止问题，但我不完全确定......
A）正如Augustss所说，你的系统显然是图灵完备的。
B） 您说得对，确定解决方案大小与停止问题相同。如果序列没有终止，那么你就会得到一个无限解集。因此，要确定集合是否是无限的，您需要确定约简序列是否终止。但这正是停止的问题！
C） 我记得，一个系统，向图灵机提供一组指令，只是说他们采取了多少步骤来终止（我想，这是你的解决方案集的基数），或者如果指令本身无法终止，则无法终止本身就是图灵完备的。所以这应该有助于这里的直觉。
回答我自己的问题...我发现通过调整源代码，我可以使输入 SKI 表达式具有正常形式，则该正常形式将始终是解决方案 #1。因此，如果您只是忽略任何进一步的解决方案，程序会将任何 SKI 表达式还原为正常形式。
我相信这构成了一个"更好的证据"。