さまざまな評価戦略に関する記事を読んでいます（wikiで記事をリンクしましたが、英語ではない別の記事を読んでいます）。そしてそれは、戦略とは異なり、call-by-name戦略はチューリング完全ではないと言っています。call-by-needcall-by-value
誰か説明してもらえますか、なぜそうなのですか？可能であれば、plsの例を追加してください。
2 に答える
10
私はあなたが読んでいる記事の主張に異議を唱えます。（私はこれに対して報酬を得ていないので、証拠ではなく、示唆的な議論を提供するつもりです。）
少なくとも通常の次数の削減（別名、名前による呼び出し）では、純粋なラムダ計算がチューリング完全であることはよく知られています。しかし、JohnReynoldsの独創的な論文DefinitionalInterpreters for Higher-Order Programming Languagesを見ると、Reynoldsが名前による呼び出しと値による呼び出しの違いについて詳細に説明していることがわかります。議論の重要な部分は、適切な区別をするために、プログラムを継続渡しスタイルに変換できるということです。CPS変換は、必要性による呼び出しと値による呼び出しで異なりますが、結果の変換された用語はどちらのスタイルでも評価できます。
したがって、ここで議論があります。チューリングマシンをシミュレートするラムダ計算プログラムを作成し、CBN変換を使用してCPS変換すると、CBV削減戦略を使用して結果のコードを評価できます。バン！チューリング完全。
実際には、チューリングマシンをエミュレートするCBVプログラムを作成できると思います。たとえば、Θのような適切な固定小数点コンビネータを選択するだけでおそらく十分です。（より有名なYコンビネータは、名前による呼び出しの削減戦略、つまり通常の順序の削減の下でのみ機能します。）
免責事項：私はラムダ計算を何年も研究していません。上記の議論にはいくつかの詳細が間違っていると確信しています。しかし、私はその内容に自信があります。プログラミング言語理論に関するオンラインリソースで露骨に間違っていることに気付いたのは初めてではありません。
于 2010-05-31T20:26:15.437 に答える
0
あなたの質問は、特定の言語を参照しないとあまり意味がありませんが、型なしラムダ計算に関しては、最善を尽くして答えます。
型指定されていないラムダ計算に対する値による呼び出しの固定小数点コンビネータ（つまり「Yコンビネータ」）の存在は、基本的な主張に反論しているようです（固定小数点コンビネータを参照）。このようなコンビネータの存在は、強力な正規化を破ります。これは、値による呼び出しの評価戦略を使用するチューリング完全な言語が少なくとも1つあることを示しています。
言語のチューリング完全性に影響を与える可能性がはるかに高いのは、型システムの存在（または欠如）です。たとえば、単純型付きラムダ計算は固定小数点コンビネータをエンコードできず、強く正規化されます（つまり、すべての適切に型付けされた項は値に減少します）が、これは採用された評価戦略に関係なく当てはまります。むしろ、それは型システムの結果です。
于 2010-06-01T11:40:39.323 に答える