デ・ブリュイン記法

数理論理学において、デ・ブリュイン記法は、オランダの数学者ニコラス・ゴバート・デ・ブリュインによって発明されたλ計算の項の構文である。^[1]これは、λ計算の通常の構文を逆にしたものと見なすことができ、そこでは適用時の引数が関数の本体の後ではなく、 対応する関数バインダーの隣に配置される。

De Bruijn 表記法の項 ( ) は、変数 ( ) であるか、2 つのワゴン接頭辞のいずれかを持ちます。と表記される抽象化ワゴンは、 λ 計算の通常の λ バインダーに対応し、 と表記される適用ワゴンは、λ 計算の適用における引数に対応します。 ${\displaystyle M,N,\ldots }$${\displaystyle v}$${\displaystyle [v]}$${\displaystyle (M)}$

${\displaystyle M,N,...::=\ v\ |\ [v]\;M\ |\ (M)\;N}$

従来の構文の項は、次のような帰納的関数を定義することで De Bruijn 表記法に変換できます。 ${\displaystyle {\mathcal {I}}}$

${\displaystyle {\begin{aligned}{\mathcal {I}}(v)&=v\\{\mathcal {I}}(\lambda v.\ M)&=[v]\;{\mathcal {I}}(M)\\{\mathcal {I}}(M\;N)&=({\mathcal {I}}(N)){\mathcal {I}}(M).\end{aligned}}}$

λ項に対するすべての演算は、変換に関して可換である。例えば、通常のβ-還元は、 ${\displaystyle {\mathcal {I}}}$

${\displaystyle (\lambda v.\ M)\;N\ \ \longrightarrow _{\beta }\ \ M[v:=N]}$

De Bruijn 記譜法では、予想通り、

${\displaystyle (N)\;[v]\;M\ \ \longrightarrow _{\beta }\ \ M[v:=N].}$

この表記法の特徴は、β-還元体の抽象化ワゴンと適用化ワゴンが括弧のように対になっていることである。例えば、項 のβ-還元の段階を考えてみよう。ここで、還元体は下線が引かれている。^[2]${\displaystyle (M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z}$

${\displaystyle {\begin{aligned}(M)\;{\underline {(N)\;[u]}}\;(P)\;[v]\;[w]\;(Q)\;z&{\ \longrightarrow _{\beta }\ }(M)\;{\underline {(P[u:=N])\;[v]}}\;[w]\;(Q[u:=N])\;z\\&{\ \longrightarrow _{\beta }\ }{\underline {(M)\;[w]}}\;(Q[u:=N,v:=P[u:=N]])\;z\\&{\ \longrightarrow _{\beta }\ }(Q[u:=N,v:=P[u:=N],w:=M])\;z.\end{aligned}}}$

したがって、アプリケータを開き括弧 (' (')、抽象子を閉じ括弧 (' ]') と見なすと、上記の用語のパターンは ' ((](]]' になります。De Bruijn は、この解釈でアプリケータとそれに対応する抽象子をパートナーと呼び、パートナーのないワゴンを独身者と呼びました。彼がセグメントと呼んだワゴンのシーケンスは、そのすべてのワゴンがパートナーになっている場合に バランスが取れています。

バランスの取れたセグメントでは、パートナーのワゴンを任意に移動することができ、パリティが破壊されない限り、項の意味は同じままです。たとえば、上記の例では、アプリケータをその抽象化子に移動したり、抽象化子をアプリケータに移動したりできます。実際、ラムダ項のすべての可換および順列変換は、パートナーのワゴンのパリティ保存並べ替えという単純な用語で記述できます。このようにして、 De Bruijn 表記法で λ 項の 一般化された変換プリミティブが得られます。${\displaystyle (M)}$${\displaystyle [w]}$

λ項のいくつかの特性は、従来の表記法では記述や証明が難しいが、De Bruijn表記法では簡単に表現できる。例えば、型理論的な設定では、型付けコンテキスト内の項の型の標準クラスを簡単に計算でき、型チェックの問題を、チェックされた型がこのクラスのメンバーであることを確認する問題に言い換えることができる。^{[3] De Bruijn表記法は}、純粋な型システムでの明示的な置換の計算にも役立つことがわかっている。^[4]

• 数学表記