相対指標と利用法

セオリー論 本編ネタ

基本的道具は：

特に、"3 Inclusive Institutions" 。$`\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\Within}{ \sqsubseteq }
`$

指標の圏 $`\cat{S}`$ は包含圏〈inclusive category〉だとする。包含射からなる部分圏を $`\mrm{Incl}(\cat{S})`$ と書く。指標のあいだの包含射／包含関係は $`\Sigma \Within \Gamma`$ で書く。

$`\quad \mrm{RelSig}_\cat{S}[\Sigma] := {^{\Sigma/}\mrm{Incl}(\cat{S}) }`$

$`\mrm{RelSig}_\cat{S}[\Sigma]`$ の対象を、指標 $`\Sigma`$ 下の〈under $`\Sigma`$〉相対指標と呼ぶ。あるいは、$`\Sigma`$ の拡張〈extension〉。

$`L = (L, \mu, \eta)`$ を $`\cat{S}`$ 上のモナドとして、L-手続きの圏を次のように定義する。

$`\quad L\text{-Proc}_\cat{S} := (\mrm{Kl}(L/\cat{S}) )^\mrm{op}`$

$`L(\Sigma)`$ は次のようにも書く。

  • $`\mrm{Term}_L(\Sigma)`$ （式言語の項の集合）
  • $`\mrm{Th}_L(\Sigma)`$ （論理言語の論理式の集合）
  • $`\mrm{Prog}_L(\Sigma)`$ （プログラミング言語のプログラムコードの集合）
相対指標の解釈

$`\Sigma \Within \Gamma`$ は次のように解釈できる。

  1. インターフェイスのナローイング、情報隠蔽〈ハイディング〉、publicマーカーキーワード、$`\Sigma`$ が可視部。
  2. パラメータ化、paramマーカーキーワード、$`\Sigma`$ がパラメータ部。
  3. 継承、baseマーカーキーワード、$`\Sigma`$ が基底部。
  4. デリゲーション、依存性注入の注入点、ホットスポット、hotマーカーキーワード。$`\Sigma`$ がホットスポットの集まり。
ハード代入とソフト代入

相対指標 $`(\Sigma\Within\Gamma)`$ があるとき：

  • $`(\Sigma\Within\Gamma)[M]`$ は： $`\Sigma`$ をモデル $`M`$ で置き換えた指標。結果は相対指標ではなくて絶対指標。ハード代入。
  • $`(\Sigma\Within\Gamma)\triangleleft p`$ は： $`p`$ はL-手続き $`p:\Delta \to \Sigma`$ 。

$`\Sigma`$ を手続き $`p`$ で置き換えた指標。結果は $`\Delta`$ 下の相対指標。ソフト代入。

セマンティクス

相対指標の圏 $`\mrm{RelSig}[\Sigma]`$ は、ファイバー付き圏の圏 $`{\bf FibCat}[\mrm{Model}(\Sigma)]`$ に意味を取る。

$`\quad \mrm{RelModel}_\Sigma : \mrm{RelSig}[\Sigma] \to {\bf FibCat}[\mrm{Model}(\Sigma)] \text{ in } {\bf CAT}`$

この対応の具体的表示は以下。$`\leadsto`$ はファイバー付き圏の射影とする。射影は忘却関手で与えられる。

$`\quad (\Sigma \Within \Gamma) \mapsto (U_{\Sigma \Within \Gamma}: \mrm{Model}(\Gamma) \leadsto \mrm{Model}(\Sigma))`$

指標多相な関手

相対モデル $`\mrm{RelModel}`$ は次のように書ける。

$`\text{For }\Sigma \in |\cat{S}|\\
\quad \mrm{RelModel}_\Sigma : \mrm{RelSig}[\Sigma] \to {\bf FibCat}[\mrm{Model}(\Sigma)] \text{ in } {\bf CAT}
`$

関手圏を使って書けば（ウハッ、シグマがかぶった）：

$`\quad \mrm{RelModel} \in \Pi\, \Sigma.[\mrm{RelSig}[\Sigma], {\bf FibCat}[\mrm{Model}(\Sigma)]]
`$

関手圏のパイ型を射に対しても拡張して次のように出来ないか？

$`\quad \mrm{RelModel} \in \Pi\, \sigma \in_* L\text{-Proc}_\cat{S}.[\mrm{RelSig}[\sigma], {\bf FibCat}[\mrm{Model}(\sigma)]]
`$