functional-programming - ラムダの定義可能性とは何ですか？

Question

ラムダ計算について読んでいるときに、ラムダ定義可能性という言葉に出くわしました。良いリソースが見つからなかったので、誰かがそれが何であるかを説明できますか？

ありがとう

Answer 1

より一般的には、幅広いクラスの言語で「ラムダの定義可能性」を特徴づけることを目的とした一連の研究があります。「ラムダ定義可能性」自体は、通常、集合の観点から与えられた言語のセマンティクスに関連しています。私たちの言語の型については、その解釈をセットとしてT記述してください。|T|ここで、の要素を取ります|T|-それを呼び出しますe。私たちの言語に用語があるかどうかを知りたいのですがx : T、| x |のようにそれを（タイプTのx）と呼びます。ですe。そのような用語がある場合、それtはラムダ定義可能であると言います。

さて、私たちの完璧な世界では、言語をセットに解釈するとき、各タイプに関連付けられたセットは、まさにそのタイプのラムダ定義可能要素とラムダ定義可能要素のみを含むセットであると言いたいです（完全性） 。また、セットの要求された要素に関連するラムダ項（決定可能性）があるかどうかを判断するためのアルゴリズムを提供できると言ってもいいでしょう。

現在、多くの場合、集合にモデル化するだけでなく、他の面白い数学的構造にモデル化しています。また、ラムダ計算だけでなく、PlotkinのPCFなどの他の関連システムからもモデル化しています。しかし、調査中のプロパティは、通常、「ラムダ定義可能性」と呼ばれています。

何十年にもわたる研究の後、この点に関してまだ多くの未解決の問題と質問があります-特定の低次の項は決定可能なラムダ定義可能性を持っていることが示されていますが（古典的な結果には2次までの項が含まれます）、多くの項は生成されませんとても簡単に。この論文（ラルフローダーによる「ラムダの決定不能性-定義可能性」）は、重要なそのような決定不可能性の結果を示し、いくつかの結果を特徴づけます： http ://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.6860

Answer 2

ラムダ定義可能な関数（Churchから）が「効果的に計算可能な」関数を提供する関数であるChurch-Turingの論文を参照してください。チューリングは、チューリングマシンに実装可能なプログラムがラムダ定義可能な関数と同等であることを示しました。