モデルの概念と理論 - (保存用) 檜山正幸のキマイラ飼育記メモ編

システム全体もひとつの指標を持つから、それをシステム指標と呼び、Ωで表す。システム指標に含まれる名前はso-called大域名で、いつでもどこからでも自由に参照できる。

システム指標Ωの環境（文脈）下にあるトランスフォーマーtを次のように書く。

なにをシステム指標とみなすかは勝手なので、

   Ω| t:Σ, Σ'→Γ
  --------------------
   Ω, Σ| t':Σ'→Γ


   Ω, Ω'| t:Σ→Γ
  --------------------
   Ω| t':Ω',Σ→Γ

これは重要で、システムをライブラリで拡張したり、カーネル機能をユーザーランドで実装したりに相当する。システムとユーザープログラムの境界は動かしてよい。

トランスフォーマーtに対して、それが定義する置換子をt^←と書く。次の関係がある。



   Ω| t:Σ→Γ

  ---------------

   t^←:Γ→(Ω,Σ)^◇

(-)^◇は、指標＝コンピュータッドから圏を作る演算子。

トランスフォーマーと置換子〈サブスティテューター | substitutor〉の違いは：

よって、次のように考えればよい。

ここで、「同義語・類義語・多義語」の問題を述べる。

システム指標は次のように言っても同じ。

システムとは、システム指標Ωと ω:Ω→Set（厳密には、忘却関手で移したSet）として定義したいが、ωのことは、

などなど、山のような同義語・類義語。組み合わせも考えると

{ | 抽象 | 仮想 | 概念}{ | ランタイム | 実行 | 実行時}{システム | 系 | 実装 | エンジン | 機械 | コンピュータ | ハードウェア | 環境 | 仕様 | アーキテクチャ}

ここでは「モデル」を使用する。システム指標とシステムモデルがシステム（プログラムの実行環境）を定義する。モデルに域・余域の概念は入っているから、「システム＝Ωが域であるモデル」。

構文的なインスタンスとは、引数指標を持たない（空である）トランスフォーマーt

tは、Σのインスタンス（instance of Σ）と呼ぶ。tの置換子は、

置換子は、コンピュータッド圏に働くクリーネ／ストリート・スターのクライスリ射と考える。システム指標Ωにはシステムモデル ω:Ω→Setがあったから、インスタンスの置換子とシステムモデルを結合すると、指標Σ上のモデル ω':Σ→Set が出来る。

これは、システムをΣ-インスタンス（基礎ライブラリ）で拡張〈enhance〉したものになる。

別な見方として：

この見方から、

とも言える。しかし、インスタンスがモデルそのものではなくて、インスタンス（というトランスフォーマー）の置換子を通じて、システムモデル（決っている）が引き戻される。

ここで、システムモデルを色々と動かしてみると、インスタンスtは、

この事実により、Standard MLではトランスフォーマーを関手と呼ぶ。

次のモノの相互関係を調べることが大事。

指標と置換子／トランスフォーマーの理論は、(0,1)-論理のような気がしている。