ラムダ項〈ラムダ式〉を、ド・ブラウン・インデックス〈de Bruijn index〉を使って書く方法。
内容:
de Bruijn のカタカナ書き
12年前〈2011年〉の記事「ブランさん」で、人名“de Bruijn”のカタカナ書きは「デュブラン」がよさそうだ、てなことを書きました。最近、Wikipediaをみると、「ド・ブラウン」を使っているんですね。
- Wikipedia: ド・ブラウン・インデックス
「Wikipediaが正しい」と信奉はしてませんが、「ド・ブラウン」表記が多くなりそうなので、僕も「ド・ブラウン」を採用します。
ラムダ項の構文
一番簡単なラムダ項〈lambda term〉の構文を決めましょう。Vは、前もって決められた変数(記号、名前)の集合とします。ξ∈V を変数とします。ξは実際の変数(例えば x, y)ではなくて、変数を表すメタ変数です。E, F などは、これから定義するラムダ項を表すメタ変数とします。
- 変数はラムダ項である。
- E, F がラムダ項ならば、それらを並べて括弧で囲んだ (E F) (適用〈application〉と呼ぶ)はラムダ項である。
- E がラムダ項、ξ が変数のとき、λξ.E (ラムダ抽象〈lambda abstraction〉と呼ぶ)はラムダ項である。
例えば、次の記号表現はラムダ項です。
- x
- (x y)
- λx.x
- (x λx.x)
- λy.(x y)
- λz.λx.(λy.(x y) z)
ラムダ項における変数の出現は、自由な出現〈free occurrence〉と束縛された出現〈bound occurrence〉があります。自由と束縛の違いを正確に説明するのは面倒なので、先の例において、束縛された出現はギリシャ文字に変えてみます。
- x
- (x y)
- λα.α
- (x λα.α)
- λβ.(x β)
- λγ.λα.(λβ.(α β) γ)
今、ラテン文字とギリシャ文字で区別したように、自由変数の集合FVと束縛変数の集合BVを交わりがないよう〈disjoint〉に決めて使うこともあります。しかし、めんどくさいので、通常は出現位置と出現状況(スコープ)で自由か束縛かを判断します。
意図してない束縛
束縛変数は自由に(?)リネームしてかまいません。例えば:
- λα.α -(αをβにリネーム)→ λβ.β
- λβ.(x β) -(βをγにリネーム)→ λγ.(x γ)
- λγ.λα.(λβ.(α β) γ) -(αをβに、βをγにリネーム)→ λγ.λβ.(λγ.(β γ) γ) これは大丈夫
- λγ.λα.(λβ.(α β) γ) -(αをγにリネーム)→ λγ.λγ.(λβ.(γ β) γ) んっ?
最後のリネームは具合が悪いです。内側の λα.(λβ.(α β) γ) だけ見ると、γは自由変数〈自由な出現の変数〉でしたが、λγ.(λβ.(γ β) γ) では、右端のγが束縛変数〈束縛された出現の変数〉になっています。リネームにより、内側での自由変数が束縛変数に変わってしまうことがあります。これはダメです。
我々が実際にリネームを行うときは、無意識に“意図してない束縛”が起きないように配慮しています。が、何も考えないでテキトーにリネームすると“意図してない束縛”が生じるリスクがあります。
“意図してない束縛”が起きないようにリネームする注意事項があるのですが、これはこれでめんどくさいです(述べません)。
ラムダ項の2次元記法
リネームの影響を考えなくてもよくする工夫がド・ブラウン・インデックスです。ド・ブラウン・インデックスの準備として、ラムダ項を、縦横の2次元を使って書く方法を述べます。まず、適用はそのまま横に書きます。
(x y)
丸括弧はなくてもいいです。
x y
ラムダ抽象は、ラムダ束縛部を上に、束縛される項を下に書いて箱に入れます。ただし、箱と言っても、左右に縦棒を描くだけで済ませます。λα.α は:
|λα| |α |
一階に α 、二階に λα が居る感じです。
適用の横並びと、ラムダ抽象の縦並びを組み合わせます。(x λα.α) は:
x |λα| |α |
λβ.(x β) は:
|λβ | |x β|
λγ.λα.(λβ.(α β) γ) ならば:
|λγ | |λα | |λβ | |(α β) γ|
もう少し複雑な例として λψ.(x λα.λβ.( (β α) λγ.(ψ γ) )) ならば:
|λψ | |x |λα | | |λβ | | |β α |λγ | | | |ψ γ|
ド・ブラウン・インデックス
ここで、ド・ブラウン・インデックス〈de Bruijn index〉の登場です。束縛変数に、名前ではなくて番号(自然数)を使います。もちろん、番号付けの規則・方法が必要です。以下に、番号付けの方法を述べます。
前節では、束縛変数はギリシャ文字でした。ギリシャ文字を見たら、目線を上に動かして、そのギリシャ文字を束縛しているラムダ束縛を探します。「ラムダ束縛が何階上にいるか?」を見ます。
例えば、
|λγ | |λα | |λβ | |(α β) γ|
の最下階に居るギリシャ文字αに注目すると、2階上に λα がいます。つまり、「ラムダ束縛が何階上にいるか?」の答は「2」です。この場合、ギリシャ文字αを番号2で置き換えます。
|λγ | |λα | |λβ | |(2 β) γ|
βとγも同様な方法で番号に置き換えると:
|λγ | |λα | |λβ | |(2 1) 3|
ラムダ束縛に付いていた名前 γ, α, β はもはや不要なので取り除きます。
|λ | |λ | |λ | |(2 1) 3|
横一行に1次元化して λ.λ.λ.( (2 1) 3 ) が束縛変数を番号〈ド・ブラウン・インデックス〉に置き換えたラムダ項です。書き換えは:
- λγ.λα.(λβ.(α β) γ) -(束縛変数を番号に)→ λ.λ.λ.( (2 1) 3 )
番号を0から始めたいときは、1引いてください。
- λ.λ.λ.( (2 1) 3 ) -(番号を1引いた数に)→ λ.λ.λ.( (1 0) 2 )
1から始めるか0から始めるかは好みの問題なのでどーでもいいのですが、「ラムダ束縛が何階上にいるか?」の答としては1始まりが自然です。
ド・ブラウン・インデックスを用いたラムダ項の書き方を“ド・ブラウン記法”と呼んでいる例を見かけますが、間違いです。ド・ブラウン記法はまた別な記法ですから注意してください。
- Wikipedia: ド・ブラウン記法
ド・ブラウン・インデックスは、ラムダ項の“形状”から一意的に決まってしまいます。名前のような恣意的自由度がありません。一意的に決まった番号にリネームなんて出来ないので、リネームに関わるゴチャゴチャとも無縁です。
「リネームに関わるゴチャゴチャと無縁」という特徴はとてもありがたいので、ラムダ項を扱うソフトウェアの実装ではド・ブラウン・インデックスがよく使われます。
他の例
x y
これ〈↑〉は束縛変数がないので何も変わりません。
x |λα| |α |
ド・ブラウン・インデックスを使用すると:
x |λ| |1|
1次元にシリアライズすると: x λ.1
|λβ | |x β|
ド・ブラウン・インデックスを使用すると:
|λ | |x 1|
1次元にシリアライズすると: λ.(x 1)
|λψ | |x |λα | | |λβ | | |β α |λγ | | | |ψ γ|
ド・ブラウン・インデックスを使用すると:
|λ | |x |λ | | |λ | | |1 2 |λ | | | |4 1|
1次元にシリアライズすると: λ.(x λ.λ.( (1 2) λ.(4 1) ))