コンテンツにスキップ

英文维基 | 中文维基 | 日文维基 | 草榴社区

ド・ブラウン記法

出典: フリー百科事典『ウィキペディア(Wikipedia)』
ド・ブラン記法から転送)

ド・ブラウン記法(英:De Bruijn notation)とは、ラムダ計算表記のための構文の一つである。オランダ人数学者ニコラース・ホーヴァート・ド・ブラウンによって発明された。

生成文法

[編集]

ド・ブラウン記法の項は、vを任意の変数名、MとNを任意のド・ブラウン記法の項とするとき、

  1. v
  2. [v] M
  3. (M) N

の形で表されるもの全てである。

通常の記法との対応

[編集]

Iを通常のラムダ計算の記法からド・ブラウン記法への変換とし、vを任意の変数名、MとNを任意のド・ブラウン記法の項とするとき、

  1. I(v) = v
  2. I(λv.M) = [v]I(M)
  3. I(M N) = (I(N))I(M)

となる。

参考文献

[編集]
  • BONELLI E, RIOS A (Univ. Buenos Aires, Buenos Aires, ARG), KESNER D (Univ. Paris-Sud, Orsay, FRA) "A de Bruijn Notation for Higher-Order Rewriting" postscript