ウルトラ・マクロな立場の定式化

「『正規（regular）』とは何なんだ」で「マクロな立場」と呼んでいるのは、再帰代入系の全体RAS(F, K)をトレース付きモノイド圏（traced monoidal category）と考える立場です。そして、「ウルトラ・マクロな立場」とは、F, Kを動かして、全体をfibred categoryと考えること。

で、この「ウルトラ・マクロな立場＝a fibred category」がいまいち分からないのです。F, Kは固定したfibreはわかるけど、何をbaseにとったらいいか確定できませんね、いくつか候補はあるのだけど。

まず、変数全体の集合Kをパラメータ（つまり、baseのobjects）と考えるかどうか？ 変数は単なるプレイスホルダーだから、系に本質的には関与・影響しないと考えることもできます。Bart Jacobsなんかは明らかにこの立場で、変数は番号にしてしまってスッキリと定式化してます。

が、僕はどうも「変数は単なるプレイスホルダー」というのが納得できないのです、感覚的な問題かもしれないけど。この感覚は、ラムダ式におけるde Bruijn インデックス（[1]の2.3節参照）を「不自然だ」と感じるのと同種のものかもしれません。

仮にFだけをパラメータとするにしても、何を「FからGへの射＝baseの射」と考えるのか？ ranked setの写像ではプア過ぎるし、、、実際に候補にあたって、具体的に調べてみるしかなさそうです。

• [1] 型付きラムダのお勉強ならコレでしょう：（表紙は朱色です）

  プログラミング言語の基礎理論 (情報数学講座)