←【情報学基礎Ａ】シラバスへ

第１７回講義内容へ→

←講義のツボメニューへ

情報学基礎Ａ

【第１６回】【2000.12.12】

関数モデル
（５）

部分式
あるラムダ式Ｍを構成していく過程で作られるラムダ式のことをＭの部分式という。

ラムダ式Ｍに対し、Ｍの部分式は

1. Ｍが変数xならば、部分式はである。
2. Ｍが(λx.N)ならば、部分式はNの部分式及びＭ。
3. Ｍが(N₁ N₂)ならば、部分式はN₁の部分式、N₂の部分式、及びＭ。

例）
(λx.(λy.x))の部分式は(λx.(λy.x))、(λy.x)、xの３つ。


xの出現が部分式として(λx.N)というラムダ抽象の中に現れるとき 束縛された出現 といい、そうでないときの出現を 自由な出現 という。
ある変数の出現が 束縛された出現 のとき、その変数を 束縛変数 といい、自由に出現している変数を 自由変数 という。

例）赤字は束縛変数、青字は自由変数
(y(λx.(xx)))
(λx.(y(λy.(yx))))



ラムダ計算における「計算」 （ここからがラムダ計算の重要なところ。）
ラムダ計算における「計算」とは、関数適用の形をしたラムダ式に対してβ変換という 書き換え規則を適用することで値を求める。
ラムダ式の中の自由変数xを全てラムダ式Nに置き換える表記法M≡[x:=N]を導入する。

M≡(x (λx.xy)) N≡z のとき M≡[x:=N]≡(x (λx.xy))[x:=z]≡(z (λx.xy))

ラムダ式M、x、Nに対して、β変換を次のように定義する。

1. ((λx.M)N)→_βM[x:=N]
   このとき((λx.M)N)をβ基（βリデックス）という。
2. M→_βNならば
   (λx.M)→_β(λx.N)
   (M P)→_β(N P)
   (P M)→_β(P N)

例）

((λx.(xy))z)→β(xy)[x:=z]≡(zy)
       M   N     M     N

((λx.(xy))(zy))→β(xy)[x:=(zw)]≡((zw)y)

((λx.(xy))(λz.z))→β(xy)[x:=(λz.z)]≡((λz.z)y)
                  →βz[z:=y]≡y

ここで、β基でないものを正規形という。

←【情報学基礎Ａ】シラバスへ

第１７回講義内容へ→