ラムダ計算における変換規則の一つ。ラムダ式の中の各ラムダ項同士の関係を定めたものである。

目次 基本理念 概念 表現 例 操作 β-redex 例 注意 正規形

基本理念

概念

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

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

表現

(λ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

次の形になっているものをβ-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は自由変数なのに、書き換え後は束縛変数になってしまい、式の意味が変わってしまう。

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

正規形

ベータ簡約がこれ以上できない、つまりβ-redexと呼ばれる形が式中に存在しないラムダ式を正規形という。

リンク

関連する用語
ラムダ計算
アルファ変換

[再検索] [戻る]