関数とラムダ計算の話
この記事へのツッコミみたいなことを書くつもりだったけど、あんまり関係ない話になったので、サイドストーリーみたいにして読んでください。
分野によって「関数」が違うこともある
前回、数学的な関数の定義の話があったけど、あれは写像の定義であって、個々の分野で「関数」と呼ばれているものと、いつでも一致するとは限らない。まあ普通は関数と言ったらほとんどの場合写像を指すので、少し違う物を指すときは、多価関数とか連続関数みたいに、別の名前を付けていることも多い。
で、プログラミングに関する文脈で「関数」と呼ばれるものが写像と一致するかといえば、もちろん一致しない。ある程度似た部分もあるけど、違う性質を持っている。この違いを、数学的にどうやって説明するかが問題になる。計算の性質を説明するための抽象モデルが抽象書換系で、ラムダ計算の意味も、抽象書換系によって定義できる。この定義の方法は、写像の定義とは大きく異なっている。
写像とラムダ項の間には、具体的にどういう違うがあるのだろうか。
- 写像はドメイン（始域）とコドメイン（終域）が定義されている。一方、ラムダ計算におけるラムダ項に、ドメインやコドメインといった考えはない。
- 写像
は全域性
を持つ。つまり、どのような
に対しても、
は必ず値を持つ。一方、ラムダ計算には正規形を持たない元がある。それは、
一方で、写像には右一意性という性質があるが、ラムダ計算には合流性という性質があり、計算が停止する範囲では、写像とよく似た性質を持っているということが言える。
