このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

世界観

基本的に2つの“世界”がある。構文世界〈syntactic {world | realm}〉と意味世界〈semantic {world | realm}〉。補助的にシステムの世界〈{world | realm} of systems | system {world | realm}〉があるとする。システムの世界に自立性はなく、各システムは、構文的対象と意味的対象に分割されてしまう。

構文世界は、文字とテキストの世界だが、文法による構造化により、リテラル、変数(名)、定数(名)、関数(名)、項、論理式などの区分される。証明もまた構文世界に所属する構文的対象だとする。

意味世界は、データ、型、関数からなる。型はデータの集合と捉える。型と関数の集まりは実際は圏Sをなす。データ(インスタンス)は、格上げにより関数とみなせる。圏Sの構造としてデカルト積とリストモナドが付いている。直和は事後的に構成可能。Sの特徴として、普遍領域Dataを持っている。すべての型は標準亭にDataへの埋め込みを持つ。したがって、Sそのものよりは、D := S/Data というオーバー圏で考えるべきかも知れない。

また、意味世界S or Dは、帰納再帰構造を持つ。これは、領域不動点方程式が、up-to-isoで一意的に解ける(最小不動点の存在)ことが保証されていることだ。帰納再帰構造は非常に重要で、計算可能性は、帰納再帰構造に強く依存する。

構文世界Synと意味世界Semを結ぶ対応として、

  1. デノテーション
  2. ゲーデル符号化

デノテーションはスコット括弧、ゲーデル符号化はゲーデル括弧で表す。デノテーションは関手なので、関手として構成するのがよい。ゲーデル符号化は、関数のソーステキストをコンパイルする操作で、コンパイルされたコードが値を取る集合を符号空間と呼ぶ。符号空間は、チューリング圏のチューリング対象である。

意味世界の計算可能関数=射は、その定義により計算指示書であるソースコードを持つ。ソースコードは構文世界の対象。ソースコードコンパイルして(=ゲーデル符号化して)符号空間の点を得る。この符号点〈エグゼキュータブル〉がもとの計算可能関数を表現している。

符号点から計算可能関数を再現するメカニズムがザ・マシン=普遍コンピュータで、マシンmは、符号点〈エグゼキュータブル〉とデータを引数にとって、符号点が表す関数の値を計算する。

ゲーデル符号化により、構文世界を意味世界の一対象に落とすことが出来て、それにより、2つの世界が居住しているメタ環境も意味世界に引きずり込むことができる。例えば、デノテーションは、ゲーデル符号化を経由して、意味世界内の単純な関数になる。意味世界内のデノテーションを、符号化デノテーション〈coded denotation〉と呼ぶ。

  1. デノテーション 凹レンズ =スコット括弧
  2. ゲーデル符号化 ゲーデル括弧
  3. 符号化デノテーション 凸レンズ
  4. クォーティング アットマークかドルマーク