ラムダ計算の概要

ウィキペディア小見出し辞書

ラムダ計算の概要

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/10 14:50 UTC 版)

「コンビネータ論理」の記事における「ラムダ計算の概要」の解説

詳細は「ラムダ計算」を参照 ラムダ計算は、ラムダ項と呼ばれる以下のような形の記号の列に関係している。 v λv.E1 (E1 E2) vは予め定義された変数の名前の無限集合から引き出された変数名で、E1とE2はラムダ項である。λv.E1の形の項は「抽象」と呼ばれる。vはその抽象の仮引数、E1は本体と呼ばれる。λv.E1という項は、引数に適用されるとvをその値に束縛し、E1の結果の値を評価する。つまり、E1の中にあるvをその引数で置き換えたものを返す。(E1 E2)の形の項は適用と呼ばれる。適用は関数の呼び出しもしくは実行を作る:E1という関数が、E2という引数で呼び出されると、その結果が計算される。もしE1(ときどきapplicandと呼ばれる)がラムダ抽象なら、その項は簡約されるかもしれない: 引数E2は、E1の仮引数の場所に置き換えられ、同値な新しい項が結果になる。もし、ラムダ項が((λv.E1) E2)の形の項を含まないのならば、それは簡約されず、β正規形と呼ばれる。E[v := a]は、Eのvの自由変数としての出現をすべてaで置き換えた結果を表現する。したがって、 ((λv.E)a) => E[v := a] 伝統的に、(a b c d ... z)を(...(((a b) c) d) ... z)の省略として表記する。(i.e. 適用は左結合である)このような定義をするのは、すべての数学的の根本的な振る舞いを捉えているからである。例えば、ある数の平方を求める関数を考えて欲しい。英語ならこのように書くかもしれない。 The square of x is x*x (「*」を乗算の表記に用いている。) xは関数の仮引数である。特定の引数の平方を求めるために、3をあてると、仮引数の場所に3を入れる: The square of 3 is 3*3 3*3の結果を求めるためには、乗算と3という数の知識に頼らなければならない。あらゆる計算は、単に適切な関数と適切な原始的な引数の評価の合成だから、この単純な置き換えの原理は、計算の本質的なメカニズムを捉えるには十分である。さらに、ラムダ計算では3や*は外部の演算子や定数をまったく使わずに表現されうる。ラムダ計算では、適切に解釈された時3や乗算演算子のように振る舞う項を識別することが可能である。(チャーチエンコーディングを参照)ラムダ計算は、計算としてほかのもっともらしい計算のモデル(チューリングマシンを含む)と同等の力があることが分かっている。つまり、あらゆる計算を行える他のモデルはラムダ計算で表現でき、逆もそうである。チャーチ・チューリングのテーゼによれば、両方のモデルはあらゆる可能な計算を表現できる。すべての計算が、ラムダ抽象と適用を基本とした変数の置き換えのシンプルな概念で表現できることは、おそらく驚くべきことである。しかし、さらに目覚ましいのは、ラムダ抽象も必要がないことである。コンビネータ論理はラムダ計算と同等のモデルだが、ラムダ抽象は存在しない。ラムダ計算での式の評価は非常に複雑である(置換の意味論は変数を捉えるのを避けるためのかなりの気配りと共に決めなければならない)。対照的に、コンビネータ論理の式の評価は置換という概念が存在しないため、はるかに簡単である。