ハイパーインスティチューションのパラメータ化

プログラミングとの対応

プログラミング	ハイパーインスティチューション
インターフェイス	指標
インターフェイスのハード実装	モデル
インターフェイスのソフト実装	指標への射
インターフェイス上のプログラム	指標からの射
インターフェイスのアダプター	一般の射

インターフェイスのソフト実装は、「インターフェイス下の」のプログラミングと言える。

指標射は、置換または代入ともいうが、あまりに普通の言葉なので、少し変えて 置換子／代入子〈substitutor〉と呼ぶ。代入子は、指標のあいだの射である。一方、仕様のあいだの射は変換子と呼ぶ。変換子は代入子〈置換子〉の上に作られる。

さて、パラメータ化〈parameterization〉だが、パラメータ化ヘッダを次の形に書く。

• param(β:Π→Π', ι:Π'→Δ)

Π, Π', Δはすべて指標で、それぞれ、実パラメータ指標、仮パラメータ指標、本体指標と呼ぶ。βとιは代入子〈置換子〉で、βはパラメータ束縛、ιはパラメータ埋め込みと呼ぶ。βは可逆で、β;ι は単射（モノ代入子）となる。モノ代入子は、相対指標とも呼ばれる。したがって、パラメータ化は相対指標を作っていることになる。

ψ:Δ→Ψ が置換子〈代入子 | substitutor〉のとき、パラメータ化は param(β:Π→Π', ι:Π'→Δ){ψ} と書く。パラメータ化によるプロファイルの影響は、

         ψ:Δ→Ψ
 ------------------------------------
  param(β, ι){ψ}:Δ|(β, ι)→Ψ

これはプロファイリングの導出規則になる。このプロファイリングを許すには、プロファイルの左辺は、Δ|π₁| ... |π_n のような形、各π_iはパラメータ化のヘッダ。ただし、パラメータ束縛とパラメータ埋め込みを一緒にしてしまい、それをπのように書くとする。

パラメータ化ヘッダπは、指標のあいだの単射 π:Π→Δ なので、ヘッダを複合合成しても単射、パラメータ化を繰り返すと、最終的に複合合成パラメータ化ヘッダは双射になる。それがフルパラメータ化。

• パラメータ化ヘッダは、実パラメータ指標から本体指標への単射を定義する。

となると、プロファイルの左辺は、パラメータヘッダが複合合成された形をしてなくてはならない。それは、プロファイリングされた名前の集合体をzインデックス付きで重ね合わせた構造をしている。入れ子というより、レイヤー化指標（layerd signature）と言えばよさそう。レイヤー番号〈レイヤーレベル〉を、0, 1, 2, ... としてzインデックスとして使う。レイヤーは他で使うからレベル化指標〈leveled signature〉がいいか。

具体化とは、プロファイリングされた名前に実体（意味、モデル）を与えること。名前の意味は指定されたプロファイルを持つ意味圏のk-射（kはディヴィジョニングで与えられた次元）。レベル化指標＝レイヤー化指標＝マルチレベル・パラメータ化指標に意味を与えるには、環境具体化〈文脈具体化〉とパラメータ具体化がある。パラメータ具体化は内側（右側）からされて、環境具体化は外側（左側）からされる。

いかなる置換子（項の名前付きコレクション）であっても、環境を必要とする。環境の具体化とは、環境指標のモデルを与えること。一方で、パラメータ具体化とは仮パラメータ指標のモデルを与えること。どちらも、置換子の要求指標〈requirement signature〉の部分具体化＝部分モデルを与える。

となると、重要なことは、指標の部分モデル＝部分実装＝部分割り当て＝部分意味論 という概念。置換子の要求指標＝本体指標が、どのように環境指標に埋め込まれるのか？ パラメータ指標がどのように本体指標に埋め込まれるのか？ その記述が、環境、置換子、パラメータの厳密な定義を与え、モデル＝具体化の伝搬現象も記述する。

パラメータを持つ変換子は実は非常に複雑な構造を持っている。特にパラメータのレベル化構造＝ブロック構造が複雑。したがって、パラメータ付き変換子に対するコンビネータ／マニピュレータも複雑になる。

指標はファイブレーションの構造も持てるので、ファイバー付き指標とパラメータ付き指標がどういう関係かも調べないといけない。パラメータ付きファイバー付き指標が完全に分かれば、ハイパーインスティチューションの分析は捗る。