ラムダ式に含まれる全ての部分式に一意かつ列挙可能なタグを付与する方法について考察する。
導入
例として次のラムダ式について考える。
````ABC``DEF`GH
この式を二分木で書くと以下のようになる。
graph TB;
a1((app))---a2((app))
a2((app))---a3((app))
a3((app))---a4((app))
a4((app))---A
a4((app))---B
a3((app))---C
a2((app))---a5((app))
a5((app))---a6((app))
a6((app))---D
a6((app))---E
a5((app))---F
a1((app))---a7((app))
a7((app))---G
a7((app))---H
このラムダ式には全部で15個の部分式が含まれる。
A`ABB``ABCC```ABC``DEFD`DEE``DEFF````ABC``DEF`GHG`GHH
ラムダ式を簡約することを考えるとき、式の中のいずれかのβ基に着目することになる。
β基とはβ簡約可能な部分式のことなので、簡約の過程ではたえず部分式に着目していることになる。
これらの部分式 (元の式も含まれる) を一意に指し示すタグ付けのルールがあると便利だ。
先ほど列挙した部分式は下記のようにタグ付けされる。
| |
部分式 |
タグ |
| 0 |
A |
0 |
| 1 |
`AB |
1 |
| 2 |
B |
1,0 |
| 3 |
``ABC |
2 |
| 4 |
C |
2,0 |
| 5 |
```ABC``DEF |
3 |
| 6 |
D |
3,0 |
| 7 |
`DE |
3,1 |
| 8 |
E |
3,1,0 |
| 9 |
``DEF |
3,2 |
| 10 |
F |
3,2,0 |
| 11 |
````ABC``DEF`GH |
4 |
| 12 |
G |
4,0 |
| 13 |
`GH |
4,1 |
| 14 |
H |
4,1,0 |
はじめに部分式を列挙したときの並び順は、実はタグを辞書順に並べたものだった。
用語の定義
ラムダ式
この記事では一般的な型無しラムダ計算における 変数 と 関数適用 のみからなる式を「ラムダ式」と呼ぶ。
この記事ではラムダ抽象を含む式については取り扱わない。
- 変数はラムダ式である
- ラムダ式をラムダ式に適用したものもまたラムダ式である
- バッククォート
` で適用を表す
A を B に適用したラムダ式を `AB と書く
同じことを バッカス・ナウア記法 で書くと、
<expression> := <variable> | "`" <expression> <expression>
<variable> := "A" | "B" | "C" | ...
となる。
部分式
とある式 expr が別の式 expr0, expr1 を用いて ` expr0 expr1 と書けるとき、expr0 と expr1 を「expr の部分式」と呼ぶ。
さらに別の式 expr2 が expr0 ないしは expr1 の部分式であるとき、expr2 もまた expr の部分式とみなす。
また便宜上 expr 自身も expr の部分式であるとみなす。
``ABC に対して `AC は部分式ではないことに注意。
ラムダ式の列形式
最初に紹介した、
````ABC``DEF`GH
のような形式を「ラムダ式の列形式」と呼ぶ。
列形式はラムダ式を素朴に文字列で書いた形式とみなすことができる。
が、ここでは少し拡張して列形式はラムダ式を トークン の列で書いた形式とみなす。
「トークン」とは列形式の中の最小単位で。上記の例でいうと A, B, ` などがトークンにあたる。
例えば A0 のような複数文字からなる変数を扱う場合、これを「長さ2の文字列」とみなすのではなく、「1つのトークン」とみなす。
また、さきほどこの記事ではラムダ抽象を含む式については取り扱わないと書いたが、ラムダ抽象全体を一つのトークンとみなせば、ラムダ抽象を含む式もこの記事の枠組みで捉えることができる。
ラムダ式の木形式
ラムダ式を二分木で書いた形式を「ラムダ式の木形式」と呼ぶ。
例として `AB を木形式で書くと、
graph TB;
a1((app))---A
a1((app))---B
のようになる。
末端 (葉, Leaf) が変数に対応し、節 (ノード, Node) が関数適用に対応している。
このとき適用する変数を左側に、適用される変数を右側に書くことにする。
列形式と木形式で表現力に差はないが、木形式のほうが部分式の範囲がビジュアルで分かりやすいという利点がある。
木形式において、部分式はそのまま部分木として表現される。
最左項
とあるラムダ式 (またはその部分式) を木形式で書いたとき、最も左に位置する項を「最左項」と呼ぶ。
graph TB;
a1((app))---a2((app))
a2((app))---A
a2((app))---B
a1((app))---C
上記の例では A が最左項にあたる。
木形式おいて最左項を見つけるのは簡単で。ルートから左の枝を辿っていき最後に行き着いた項が最左項になる。
右部分式 (右部分木)
とあるラムダ式 (またはその部分式) を木形式で書いたとき、最左項ではない部分式 (部分木) を「右部分式 (右部分木)」と呼ぶ。
graph TB;
a1((app))---a2((app))
a2((app))---A
a2((app))---B
a1((app))---C
上記の例では B, C はどちらも右部分式である。
右部分式は単一の変数からなる式とは限らない。
graph TB;
a1((app))---a2((app))
a2((app))---A
a2((app))---a3((app))
a3((app))---B0
a3((app))---B1
a1((app))---C
この例では右部分式は `B0 B1 と C となる。
さらに部分式 `B0 B1 に着目しているときには、 B0 が最左項で B1 が右部分式ということになる。
変数のタグ付け
部分式にタグ付けすることを考える前に、ラムダ式の中の変数にタグ付けするルールを考える。
右部分木に番号付けする
右部分木に番号付けするルールを与える。
右部分木に左から 1, 2, ... と連番で付番する。
例えば ``ABC という式に対しては、
graph TB;
a1((app))---a2((app))
a2((app))---A
a2((app))---B[B:index=1]
a1((app))---C[C:index=2]
のように付番される。
右部分木が複数の変数からなる式の場合、式全体に付番されることに注意しよう。
graph TB;
a1((app))---a2((app))
a2((app))---A
a2((app))---a3((app:index=1))
a3((app:index=1))---B0
a3((app:index=1))---B1
a1((app))---C[C:index=2]
この番号付けは再帰的に適用できる。
さきほどの例で `B0 B1 は、 B0 が最左項, B1 が1番目の右部分木となっているので、
graph TB;
a1((app))---a2((app))
a2((app))---A
a2((app))---a3((app:index=1))
a3((app:index=1))---B0
a3((app:index=1))---B1[B1:index=1]
a1((app))---C[C:index=2]
と付番できる。
最左項に番号付けする
右部分木だけでなく最左項にも付番したい。最左項には 0 で付番する。
graph TB;
a1((app))---a2((app))
a2((app))---A[A:index=0]
a2((app))---a3((app:index=1))
a3((app:index=1))---B0[B0:index=0]
a3((app:index=1))---B1[B1:index=1]
a1((app))---C[C:index=2]
一見してこれで全ての変数に付番できたように見えるが、実はまだ付番が完全でない変数がある。
C:index=2 に着目してみよう。index=2 と付番されているため C が2番目の右部分木であることが分かる。
ここで C は単項の部分木だが、部分木である以上 最左項と右部分木に分解できるはずだ。C の最左項は C で、右部分木を持たない。C は最左項でもあるので 0 で付番されるべきだ。
同様に B1 も単項の右部分木であると同時にそれ自体が部分木の最左項でもあるので 0 で付番する。
するとこのようになる。
graph TB;
a1((app))---a2((app))
a2((app))---A[A:index=0]
a2((app))---a3((app:index=1))
a3((app:index=1))---B0[B0:index=0]
a3((app:index=1))---B1[B1:index=1:index=0]
a1((app))---C[C:index=2:index=0]
ルートから変数に至る経路によって変数にタグ付けする
さて全ての最左項と右部分木に付番したので、ようやく各変数にタグ付けできる。
変数へのタグ付けの基本的なアイデアは、ルートから変数に至る経路の番号を全て並べてタグとすることだ。
graph TB;
a1((app))---a2((app))
a2((app))---A[A:index=0]
a2((app))---a3((app:index=1))
a3((app:index=1))---B0[B0:index=0]
a3((app:index=1))---B1[B1:index=1:index=0]
a1((app))---C[C:index=2:index=0]
上記の例で B0 に至るには、まずルートから1番目の右部分木 app:index=1 へと進み、続いて最左項 B0:index=0 へと進めばよい。B0 に至る経路の番号を順に並べて、B0 を 1,0 でタグ付けする。
各変数とタグの関係を表にまとめる。
| 変数 |
タグ |
` |
|
` |
|
A |
0 |
` |
|
B0 |
1,0 |
B1 |
1,1,0 |
C |
2,0 |
タグが「ルートから変数に至る経路」を表現していることを知っていれば、逆にタグから変数への経路を辿ることも容易だ。
関数適用のタグ付け
もう一歩踏み込んで変数だけでなく関数適用にもタグ付けすると便利だ。
木形式において関数適用は節 (ノード, Node) に対応している。右部分木に付番したときと同様に、関数適用にも左から 1, 2, ... と連番で付番する。
graph TB;
a1((app))---a2((app:index=1))
a2((app:index=1))---A
a2((app:index=1))---B
a1((app:index=2))---C
右部分木に現れる関数適用にも同様に付番していく。
さきほど変数にタグ付けする際に右部分木に付番したことと、関数適用に付番することは別の概念として区別する。
graph TB;
a1((app:index=2))---a2((app:index=1))
a2((app:index=1))---A
a2((app:index=1))---a3((app:index=1))
a3((app:index=1))---B0
a3((app:index=1))---B1
a1((app:index=2))---C
関数適用にタグ付けするときの考え方は変数に対するタグ付けの考え方と同様だ。その関数適用に至るまでの経路の番号を並べてタグにする
| 関数適用 |
タグ |
` |
2 |
` |
1 |
A |
|
` |
1,1 |
B0 |
|
B1 |
|
C |
|
変数と関数適用のタグ付けまとめ
各変数に対するタグ付けと各関数適用に対するタグ付けをあわせて表にまとめると以下のようになる
| 変数・関数適用 |
タグ |
` |
2 |
` |
1 |
A |
0 |
` |
1,1 |
B0 |
1,0 |
B1 |
1,1,0 |
C |
2,0 |
変数に対するタグは末尾が 0 になっているのが見て取れる。
それ以外には変数に対するタグと関数に対するタグは形がとても似ている。
タグの性質
ここまででラムダ式のなかの全ての変数と全ての関数適用にタグ付けするルールを定めた。
先ほどよりも複雑な式を例に付番とタグ付けの様子を見てみよう。
````ABC``DEF`GH
最初にも挙げたラムダ式を例とする。
この式の木形式は以下のようになる。
graph TB;
a1((app))---a2((app))
a2((app))---a3((app))
a3((app))---a4((app))
a4((app))---A
a4((app))---B
a3((app))---C
a2((app))---a5((app))
a5((app))---a6((app))
a6((app))---D
a6((app))---E
a5((app))---F
a1((app))---a7((app))
a7((app))---G
a7((app))---H
各変数・各関数適用にタグ付けしたものを列挙すると下記のようになる。
| 変数・関数適用 |
タグ |
` |
4 |
` |
3 |
` |
2 |
` |
1 |
A |
0 |
B |
1,0 |
C |
2,0 |
` |
3,2 |
` |
3,1 |
D |
3,0 |
E |
3,1,0 |
F |
3,2,0 |
` |
4,1 |
G |
4,0 |
H |
4,1,0 |
さてこのタグ付けにはいくつかの有用な性質がある。
一意性
ラムダ式の変数・関数適用にタグ付けしたとき各タグは一意になる。この性質のために、このタグによって特定の変数ないしは関数適用を指し示すことができる。
タグが一意になることの証明は省略するが。直感的には木形式で表現したときの各経路が一意であることから自然に理解できるだろう。
トークンに対する網羅性
これまで "変数・関数適用に対して" タグ付けするルールを定めてきたが。実は列形式で表現したときの "全てのトークンに対して" もタグ付けできている。
列形式の各トークンは変数かバッククォート ` のいずれかであり、バッククォートが関数適用に対応しているため、列形式の各トークンと木形式の変数・関数適用が1対1で対応する。木形式の変数・関数適用に対してタグ付けすることは、同時に列形式の各トークンにタグ付けすることにもなっていた。
部分式 (部分木) に対する網羅性
実は全ての部分式 (部分木) に対してもタグ付けできている。
部分式は単項の変数か関数適用からなっていて、これまでに全ての変数と全ての関数適用にタグ付けしてきたためだ。
先ほど示した変数・関数適用とタグの対応表に、部分式の列を追記してみよう。
| |
変数・関数適用 |
関数適用に対応する部分式 |
タグ |
| 0 |
` |
````ABC``DEF`GH |
4 |
| 1 |
` |
```ABC``DEF |
3 |
| 2 |
` |
``ABC |
2 |
| 3 |
` |
`AB |
1 |
| 4 |
A |
A |
0 |
| 5 |
B |
B |
1,0 |
| 6 |
C |
C |
2,0 |
| 7 |
` |
``DEF |
3,2 |
| 8 |
` |
`DE |
3,1 |
| 9 |
D |
D |
3,0 |
| 10 |
E |
E |
3,1,0 |
| 11 |
F |
F |
3,2,0 |
| 12 |
` |
`GH |
4,1 |
| 13 |
G |
G |
4,0 |
| 14 |
H |
H |
4,1,0 |
列形式に対して指定したタグが示す部分木の範囲を容易に判別可能
さきほどまでで「トークン」「部分式」「タグ」が1対1対1で対応していることを述べた。
与えられたラムダ式に含まれる全ての部分式を列挙するには、列形式 (トークン列) のどこからどこまでが部分式を表現しているか判別する必要がある。全てのタグの列を保持していれば、部分式の範囲を特定することは容易だ。
例としてタグ 3,2 に対応する部分式の範囲について考える。
列挙したタグの一覧から 3,2 で始まるものを探すと。7行目の 3,2 と11行目の 3,2,0 が該当する。そのためタグ 3,2 に対応する部分式の範囲はトークン列の7文字目から11文字目であると分かる。
(ここではトークンを0文字目から数えていることに注意)
````ABC``DEF`GH
^^^^^
タグ 3,2 に対応する部分式の範囲
これによってタグ 3,2 が部分式 ``DEF に対応していることが分かった。
このようにしてタグを指定することで、そのタグに対応する部分木が列形式 (トークン列) の中でどの範囲に対応するのかを知ることができる。
まとめ
この記事で以下のトピックを取り上げてきた
- ラムダ式の列形式と木形式
- 木形式の経路を辿ることによる変数・関数適用へのタグ付け
- タグが一意であり、これによって全ての部分式が網羅的に列挙できること
- 列形式の中のトークン - タグ - 木形式の中の部分木 が1対1対1で対応していること
- タグによって部分木を一意に指し示すことができ、列形式のなかの対応する範囲も分かる
列形式は紙面上でコンパクトである点において優れている一方、部分式の範囲が分かりづらいという欠点もある。列形式のなかの各トークンにタグ付けすることによって、構文解析して木形式に変換することなく即座に部分式の範囲を特定できる。
またタグによって部分式を網羅的に列挙可能なことも、ラムダ式の簡約過程を考える際に有用であると考える。
私からは以上です。
おまけ
この記事におけるタグ付けのルールをプログラムに落とし込んだ参考実装を用意しました。
github.com
TypeScript で実装されていて実際に動作します。
TypeScript をコンパイルすることなく Deno でそのまま動かすのが簡単です。
(JavaScript にコンパイルしたのちに Node.js や Web ブラウザで動かすこともできると思います)
実行イメージ
このあたりが主なロジックの実装です。
