このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ラムダ式のド・ブラウン・インデックス

ラムダ項〈ラムダ式〉を、ド・ブラウン・インデックス〈de Bruijn index〉を使って書く方法。

内容:

de Bruijn のカタカナ書き

12年前〈2011年〉の記事「ブランさん」で、人名“de Bruijn”のカタカナ書きは「デュブラン」がよさそうだ、てなことを書きました。最近、Wikipediaをみると、「ド・ブラウン」を使っているんですね。

「Wikipediaが正しい」と信奉はしてませんが、「ド・ブラウン」表記が多くなりそうなので、僕も「ド・ブラウン」を採用します。

ラムダ項の構文

一番簡単なラムダ項〈lambda term〉の構文を決めましょう。Vは、前もって決められた変数(記号、名前)の集合とします。ξ∈V を変数とします。ξは実際の変数(例えば x, y)ではなくて、変数を表すメタ変数です。E, F などは、これから定義するラムダ項を表すメタ変数とします。

  1. 変数はラムダ項である。
  2. E, F がラムダ項ならば、それらを並べて括弧で囲んだ (E F) (適用〈application〉と呼ぶ)はラムダ項である。
  3. E がラムダ項、ξ が変数のとき、λξ.E (ラムダ抽象〈lambda abstraction〉と呼ぶ)はラムダ項である。

例えば、次の記号表現はラムダ項です。

  1. x
  2. (x y)
  3. λx.x
  4. (x λx.x)
  5. λy.(x y)
  6. λz.λx.(λy.(x y) z)

ラムダ項における変数の出現は、自由な出現〈free occurrence〉と束縛された出現〈bound occurrence〉があります。自由と束縛の違いを正確に説明するのは面倒なので、先の例において、束縛された出現はギリシャ文字に変えてみます。

  1. x
  2. (x y)
  3. λα.α
  4. (x λα.α)
  5. λβ.(x β)
  6. λγ.λα.(λβ.(α β) γ)

今、ラテン文字とギリシャ文字で区別したように、自由変数の集合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始まりが自然です。

ド・ブラウン・インデックスを用いたラムダ項の書き方を“ド・ブラウン記法”と呼んでいる例を見かけますが、間違いです。ド・ブラウン記法はまた別な記法ですから注意してください。

ド・ブラウン・インデックスは、ラムダ項の“形状”から一意的に決まってしまいます。名前のような恣意的自由度がありません。一意的に決まった番号にリネームなんて出来ないので、リネームに関わるゴチャゴチャとも無縁です。

「リネームに関わるゴチャゴチャと無縁」という特徴はとてもありがたいので、ラムダ項を扱うソフトウェアの実装ではド・ブラウン・インデックスがよく使われます。

他の例

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) ))