regex - 実用的な非チューリング完全言語?

Question

使用されるほぼすべてのプログラミング言語はチューリング完全であり、これにより言語は計算可能なアルゴリズムを表すことができますが、独自の問題も伴います。私が書いているアルゴリズムはすべて停止することを意図しているため、停止することを保証する言語でそれらを表現できるようにしたいと考えています。

文字列と有限状態マシンの照合に使用される正規表現は、 lexingのときに使用されますが、チューリングが完全ではない、より一般的で幅広い言語があるかどうか疑問に思っています。

編集：明確にする必要があります。「汎用」により、必ずしもすべての停止アルゴリズムをその言語で記述できるようにしたいわけではありません（そのような言語が存在するとは思いません）が、共通のスレッドがあると思われますすべてのアルゴリズムが停止することが保証されている言語を生成するために一般化できる停止証明。

この問題に取り組む別の方法もあります - 理論的に無限のメモリの必要性を排除します。マシンが許可されるメモリの量を制限すると、マシンが存在する状態の数は有限であり、数えることができるため、アルゴリズムが停止するかどうかを判断できます (マシンが以前の状態に移行することを許可しないことによって)。 ）。

Answer 1

否定論者の言うことを聞かないでください。終了を保証したり、ランタイムエラーの可能性を排除するなどしてコードを単純化したい場合は、一部のコンテキストで非チューリング完全言語を好む理由が非常にあります。時には、物事を無視するだけでは不十分な場合があります。

論文TotalFunctionalProgrammingは、コンパイラの保証が非常に強力であるため、実際にはほとんどの場合、そのような制限された言語を好むべきであると多かれ少なかれ説得力を持って主張しています。プログラムが停止したことを証明できること自体が重要な場合がありますが、実際には、これは、より単純な言語が提供するはるかに簡単な推論の結果です。さまざまな機能を持つ言語の階層の1つのコンポーネントとして、非普遍的な言語の有用性の範囲は非常に広いです。

この階層化の概念にさらに完全に対応するもう1つのシステムは、ヒュームです。ヒュームレポートは、システムと、徐々に完全で安全性の低い言語の5つの層の完全な説明を提供します。

そして最後に、チャリティーを忘れないでください。これは少し抽象的ですが、圏論の概念に直接基づいている、有用ではあるが普遍的ではないプログラミング言語への非常に興味深いアプローチでもあります。

Answer 2

BlooP ( B ounded loopの略) は興味深い非チューリング完全言語です。これは本質的にチューリング完全な言語ですが、1 つの (重要な) 注意点があります。すべてのループには反復回数の制限が含まれている必要があります。無限ループは許可されていません。その結果、BlooP プログラムの停止問題を解決できます。

Answer 3

問題はチューリングマシンではなく、「アルゴリズム」にあります。アルゴリズムが停止するかどうかを予測できない理由は、次の理由によるものです。

function confusion()
{
    if( halts( confusion ) )
    {
        while True:
            no-op
    }
    else
        return;
}

再帰やループを実行できない言語は、実際には「汎用」ではありません。

正規表現と有限状態マシンは同じものです！字句解析と文字列照合は同じものです。FSMが停止する理由は、FSMがループしないためです。入力をcharごとに渡して終了するだけです。

編集：

多くのアルゴリズムでは、それらが停止するかどうかは明らかです。

例えば：

function nonhalting()
{
    while 1:
        no-op
}

この機能は明らかに停止することはありません。

そして、この関数は明らかに停止します：

function simple_halting_function()
{
    return 1;
}

つまり、最終的には、アルゴリズムが停止することを保証できます。停止するように設計するだけです。

アルゴリズムが常に停止するかどうかわからない場合は、そうすれば、おそらく「停止」を保証する言語でそれを実装することはできません。

Answer 4

チャリティーは完全なチューリングではありませんが、理論的、教訓的に興味深い (圏論) だけでなく、実際の問題を解決することもできます (ハノイの塔)。その強さはアッカーマン関数まで表現できるほどです。

Answer 5

完全なチューリングを行うのはかなり簡単であることがわかります。たとえば、8 つの命令 ala BrainF**kだけが必要であり、実際には1 つの命令だけが必要な点まで必要です。

これらの言語の核心はループ構造であり、制限のないループを作成するとすぐに固有の停止問題が発生します。ループはいつ終了しますか? 無限ループをサポートする非チューリング完全言語でも、実際には停止の問題が発生する可能性があります。

すべてのプログラムを終了させたい場合は、コードを注意深く書く必要があります。特定の言語の方が好みやスタイルに合っているかもしれませんが、結果のプログラムが停止することを完全に保証できる言語はないと思います。

Answer 6

これを行う正しい方法は、私見ですが、チューリング完全な言語を使用することですが、プルーフチェッカーによる処理に適したセマンティクスを述べるシステムを提供することです。

次に、終了プログラムを意図的に書いていると仮定すると、停止する理由について適切な議論が頭に浮かびます。この新しい種類の言語を使用すると、その議論を表現し、証明することができます。

余談ですが、実稼働コンパイラの再帰には、特定の入力で停止しないことがわかっている再帰があります..これを停止するには、厄介なハックを使用します。「適切な」制限のあるカウンターです。参考までに、実際のコードは多相コードの単相化に関与しており、多相再帰を使用すると無限展開が発生します。Haskell はこれをキャッチしますが、Felix 用の私のコンパイラはキャッチしません (これは、たまたま修正方法がわからないコンパイラのバグです)。

私の一般的な議論に続いて..宣言された目的に適した注釈の種類を知りたいと思います.言語とコンパイラを制御しているので、何をすべきかを正確に知っていれば、そのようなサポートを簡単に追加できます.追加:)この目的のためにループに「不変」および「変種」句が追加されているのを見てきましたが、言語がその情報を終了の証明に使用するように拡張されたとは思いません(むしろ、で不変条件と変種をチェックしました私の記憶が正しければ実行時間）。

多分それは別の質問に値する..

Answer 7

「理論的に無限のメモリの必要性を排除します。」 - まあ、そうだろう。どの物理コンピュータも、宇宙のエントロピーによって制限されており、それ以前でも光速 (== 情報が伝播できる最大速度) によって制限されています。

さらに簡単に、物理的に実現可能なコンピューターでは、リソースの消費を監視し、それに制限をかけるだけです。(つまり、メモリまたは時間の消費量 > MY_LIMIT の場合、プロセスを強制終了します)。

あなたが求めているのが純粋に数学的/理論的な解決策である場合、「汎用」をどのように定義しますか?

Answer 8

チューリング完全でない言語は、汎用言語としてはあまり役に立ちません。チューリング完全でなくても、汎用言語として自称するものを見つけることができるかもしれませんが、私はそれを見たことがありません。