関数とラムダ計算の話

bugrammer.hateblo.jp

この記事へのツッコミみたいなことを書くつもりだったけど、あんまり関係ない話になったので、サイドストーリーみたいにして読んでください。

分野によって「関数」が違うこともある

前回、数学的な関数の定義の話があったけど、あれは写像の定義であって、個々の分野で「関数」と呼ばれているものと、いつでも一致するとは限らない。まあ普通は関数と言ったらほとんどの場合写像を指すので、少し違う物を指すときは、多価関数とか連続関数みたいに、別の名前を付けていることも多い。

で、プログラミングに関する文脈で「関数」と呼ばれるものが写像と一致するかといえば、もちろん一致しない。ある程度似た部分もあるけど、違う性質を持っている。この違いを、数学的にどうやって説明するかが問題になる。計算の性質を説明するための抽象モデルが抽象書換系で、ラムダ計算の意味も、抽象書換系によって定義できる。この定義の方法は、写像の定義とは大きく異なっている。

写像とラムダ項の間には、具体的にどういう違うがあるのだろうか。

一方で、写像には右一意性\forall a \in A, \forall b_1, b_2 \in B, ((a, b_1) \in G_f \wedge (a, b_2) \in G_f \Rightarrow b_1 = b_2)という性質があるが、ラムダ計算には合流性という性質があり、計算が停止する範囲では、写像とよく似た性質を持っているということが言える。

ラムダ計算の派生

ラムダ計算には、簡約の方法を制限したり、型を付けたりするといった、色々な派生系が存在していて、それぞれの体系が異なる性質を持っている。例えば、単純型付きラムダ計算は、型なしラムダ計算と異なり、計算が必ず停止する。(強停止性を持つ。)

よく知られている関数型言語の多くは、ラムダ計算から派生した体系を使っているが、ラムダ計算以外の体系を使った関数型言語も考えられる。