13

単純なロジック ソルバーのプログラミングに 1 ～ 2 週間を費やしました。それを構築した後、私はそれが解決する言語がチューリング完全であるかどうか疑問に思っていました。そこで、SKI コンビネーター計算で有効な式をすべて受け入れ、その式の正規形を含む結果セットを生成する小さな一連の方程式をコード化しました。SKIはチューリング完全であるため、私の言語が SKI を実行できることを証明することは、そのチューリング完全性を実証することになります。

ただし、不具合があります。ソルバーは通常の順序で式を縮約しません。実際に行うことは、考えられるすべての削減順序を試すことです。これは、ソリューション セットが通常巨大であることを意味します。正規形があればどこかにあるのですが、どこにあるのかわかりにくいです。

これは私に2つの質問をもたらします:

  • 私の言語はチューリング完全ですか? それとも、より良い証拠を見つける必要がありますか?

  • 解の数は入力の計算可能な関数ですか?

(最初は、解集合のサイズは入力サイズの指数または階乗であると想定していました。しかし、よく調べてみると、これは正しくありません。すでに正規形になっている巨大な式と、終了しない小さな式を書くことができます。解集合のサイズを決定することは、停止問題を解くことと同等かもしれないと感じていますが、完全にはわかりません...)

4

2 に答える 2

5

A）オーガストが言うように、あなたのシステムは明らかに完全にチューリングしています。

B）ソリューションのサイズを決定することは、停止性問題と同じです。シーケンスが終了しない場合は、無限の解集合が得られます。したがって、セットが無限であるかどうかを判断するには、リダクションシーケンスが終了するかどうかを判断する必要があります。しかし、それはまさに停止性問題です！

C）私が覚えているように、チューリングマシンに一連の指示を与えると、終了するために必要なステップ数（つまり、ソリューションセットのカーディナリティ）を示すだけのシステム、または指示があった場合に終了しないシステムそれ自体が終了に失敗することは、それ自体が完全なチューリングです。だから、それはここでの直感に役立つはずです。

于 2012-06-04T18:26:32.297 に答える
2

私自身の質問への回答として... ソースコードを微調整することで、入力 SKI 式に正規形がある場合、その正規形が常に解決策 #1 になるようにできることがわかりました。したがって、それ以上の解決策を無視すると、プログラムは SKI 式を通常の形式に縮小します。

これは「より良い証拠」を構成すると思います。;-)

于 2012-06-07T10:45:17.567 に答える