以下、https://arxiv.org/pdf/0706.1033.pdf （「コック達論文」として言及）のズーム複体を見ていて、思ったこと； ゲンツェンのNK証明図とLK証明図の関係がストリング図とメタストリング図の関係として説明できるだろう、ということ。
まず、コック達論文用語とストリング図用語の対応。
| コック達 | ストリング図 |
|---|---|
| エッジ | ワイヤー |
| ドット | ノード |
| 球、円周 | キャンバス境界 |
| (なし) | キャンバスの穴＝スロット |
コック達は、ノードと穴〈スロット | プレースホルダー〉を区別せずに、状況に応じて解釈し分ける。が、ここでは最初からノードと穴を区別する。
キャンバスとキャンバス境界を明示的に描いた図をストリング図テンプレートと呼ぶ。
「テンプレート・ストリング図」でもいいが、C++ では関数テンプレートやクラス・テンプレートが正式らしい。
与えられたストリング図テンプレートから、次のようにしてストリング図を作る。
- ストリング図テンプレート{と名前}? → ノード{とノード名ラベル}?
- 穴（キャンバス境界）{と名前}とプロファイル → 入力ワイヤー{と名前}と型ラベル
- 外側境界{と名前}とプロファイル → 出力ワイヤー{と名前}と型ラベル
k個のスロットを持つストリング図テンプレートは、k-入力_1-出力のノードになる。このノードをストリング図テンプレートのメタノードと呼ぶ。全体のキャンバス境界と穴のキャンバス境界はメタワイヤーになり、境界のプロファイルで型ラベルされる。
ストリング図テンプレートの穴（の一部）が埋められた〈fill-inされた〉図を、コック達は星座と呼んでいる。星座は複数のストリング図テンプレートをオペラッド結合〈置換〉した形をしている。星座は置換の状況を描いている。
星座からメタノードとメタワイヤーを描くと、全体としてツリー状のストリング図ができる。これを、もとの星座のメタストリング図と呼ぶ。メタストリング図は：
- ノード〈メタノード〉はテンプレートを表す。
- ノード〈メタノード〉の名前ラベルは（あれば）テンプレートの名前となる。
- ワイヤーはキャンバス境界を表す。
- ワイヤーの型ラベルは境界のプロファイルとなる。
NKの証明図を元のストリング図として、メタストリング図は対応するLKの証明図になる。
- LKノード〈メタノード〉はNK証明図テンプレート＝推論マクロを表す。
- KLノード〈メタノード〉の名前ラベルは（あれば）推論マクロの名前となる。
- LKワイヤーはNK証明図キャンバス境界を表す。
- LKワイヤーの型ラベルは境界のプロファイル＝シーケントとなる。
これで、NK → LK 対応は疑義無く記述できるだろう。
