13

我花了一两个星期编写一个简单的逻辑求解器。构建它之后，我发现自己想知道它所解决的语言是否是图灵完备的。所以我编写了一小组方程，它们接受 SKI 组合子演算中的任何有效表达式，并生成一个包含该表达式的正常形式的结果集。由于 SKI是图灵完备的，证明我的语言可以执行 SKI 将证明其图灵完备。

但是，有一个小故障。求解器不会按正常顺序减少表达式。实际上它所做的是尝试所有可能的减少顺序。这意味着解决方案集通常是巨大的。如果一个范式存在，它会在某个地方，但很难说在哪里。

这给我带来了两个问题：

  • 我的语言图灵完备吗？还是我需要找到更好的证据？

  • 解决方案的数量是输入的可计算函数吗？

（起初我假设解决方案集的大小是输入大小的指数或阶乘。但仔细观察，这是不正确的。你可以编写已经是正常形式的巨大表达式，以及不会终止的微小表达式.我有一种感觉，确定解决方案集的大小可能等同于解决停止问题，但我不完全确定......）

4

2 回答 2

5

A）正如augustss所说，您的系统显然已经完成了。

B）你是对的，确定解决方案的大小与停止问题相同。如果一个序列没有终止，那么你会得到一个无限的解决方案集。因此，要确定集合是否无限，您需要确定归约序列是否终止。但这正是停机问题！

C）我记得，一个系统，给定一组图灵机指令，只说明他们需要多少步骤才能终止（我想，你的解决方案集的基数）或者如果指令无法终止他们自己未能终止本身就是图灵完备的。所以这应该有助于这里的直觉。

于 2012-06-04T18:26:32.297 回答
2

在回答我自己的问题时......我发现通过调整源代码，我可以做到如果输入的 SKI 表达式具有范式，那么范式将始终是解决方案#1。因此，如果您只是忽略任何进一步的解决方案，程序会将任何 SKI 表达式简化为正常形式。

我相信这构成了一个“更好的证明”。;-)

于 2012-06-07T10:45:17.567 回答