ベータ簡約

ラムダ計算においても関数の適用という概念がある。

つまり式を書き換えて簡単にする規則を定めたものがベータ簡約である。

(λx.M)

は、写像x→Mを表わす。つまり入力xに対しMを返すとことを表現するラムダ項とされる。

(MN)

は、ラムダ項Mにラムダ項Nを渡す、あるいはMにNを適用するということを表現するラムダ項である。このMやNは具体的には(λx.K)や(x+1)などのラムダ項となることもある。

また括弧は適宜省かれる。

次の式は、xにNを入力し、その上でそのxに対しMを返すと言う意味である。

(λx.M)N

さらにいうとA=(λx.M)などとしてANはNをAに適用しAを返すと言うことができる。

このような意味を式の書き換えであらわす。

次の形になっているものをβ-redexと呼ぶ。

((λx.M)N)

この形においてNをxに代入し(xをNに書き換え)て式を簡単にすることができる。これをベータ簡約という。

(λx.x²+1)(y+1)

はβ-redexの形を持っていて(上項目例ならM=x²+1、N=y+1)、

λy.(y+1)²+1

にベータ簡約できる。

この書き換えにおいて式の意味が変わってしまってはいけない。

たとえば

(λx.x²+y)(y+1)

などを考えるとき、

λy.y²+y

としてしまえば、(λx.x²+y)のyは自由変数なのに、書き換え後は束縛変数になってしまい、式の意味が変わってしまう。

よってこのような事態にはならぬよう、適宜アルファ変換を行なってからベータ簡約をする。