…数 小ディヴィジョン： 圏名[ベース圏の対象]_次元数 プロファイリングプロファイリングとディヴィジョニングは若干の重複がある。0-射〈対象〉のプロファイリングはディヴィジョニングと一致する。小ディヴィジョニングは、プロファイリングの一種と捉えてもたぶん問題はない。項、環境、クロージャ、評価項〈式〉の定義と、項を環境内で評価すること。項と環境をパッケージしたデータであるクロージャなどを定式化する必要がある。in-the-largeレベル（大局的プログラミング）でも定義が必要。

…としては与えることができない。直和や融合和（プッシュアウト、余ファイバー和）はup-to-isoで作ることができる。up-to-isoのisoを与えているのはリネーミング同型射である。 up-to-iso ＝ up-to-rename これは非常に重要な知見である。up-to-renameはラムダ計算のα変換と同じだし、名前の影響は無視して良いことを示している。大局的プログラミングにおけるモジュール演算は、すべてup-to-renameで構成されるもので、確定的演算ではない！

…が出来る。この貼り合わせが大局的プログラミングに相当する。もとのアンビエント圏、またはベース圏（アンビエント圏と名前から作った圏）における射（＝プログラム）の構成が小局プログラミング。グロタンディーク／エルブラン圏に対して余スライス構成をして作ったインスティチューションをハイパーインスティチューションと呼ぶ。Modの作り方は自明だが、Senがいまいち分からない。 ハイパーインスティチューション＝ハイパードクトリンのグロタンディーク／エルブラン圏上の余スライス・インデキシング。

…で、モジュール計算＝大局的プログラミングと関係する。 仕様記述は仕様モジュールの書き方だろう。 モデル圏が余代数の圏ならば、模倣、双模倣と関係すると思う。 モデル圏のスペクトラムが作れるのでは？ リンデンバウム構成と判断〈judgement〉 高次圏論とストリング論理 ホーア式とホーア論理 コンピュータッド＝生成系＝プレゼンテーション あらためてハイパードクトリンを定義すると：まずドクトリンDがある。値の"圏の圏”としてDを取るインデックス付き圏の全体を IndCat&ltD…

…16 あたりの続き。大局的プログラミング（programming in the large）関係。とある圏がありまする。 この圏の射（対象じゃない）はモジュールである。 この圏の対象は名前の有限集合である。 名前を型名だけに限定しても圏となる。とりあえず、型名だけで考えてもいい。 Lispのフィーチャーシステムと同じようなもの。 モジュール圏と呼びたいがそれはダメ。 この圏の対象は指標（signature）と呼んでよい。（インスティチューションの用語法では。） この圏の射は指…

大局的プログラミング（programming in the large）：手でモジュールの計算をするときの演算記号を決めておこう。キーボードでも書けるようにアスキーベース。 演算記号 意味 + モノイド積、モジュールの集約／マージ |> 圏の結合、普通の結合 :> 閉じた吸収結合 *> 開いた吸収結合 <:> 対称な閉じた吸収結合 <*> 対称な開いた吸収結合 吸収結合（absorbing composition; 檜山造語）は絵を描かないとうまく説明できない。ので、いずれま…

…[/追記]ゴグエンの大局的プログラミング（programming in the large）の発想でモジュール計算をしていたら、GoI構成とコンパクト閉圏が出てきてビックリ。モジュールMとNが提供（provide）している名前をお互いに吸収しあう方法で結合すると、これがGoI構成の8の字結合になる。8の字結合と対角、余対角を組み合わせると、提示する名前を減らさない（privateにしない）結合になる。再帰的な定義（定義の再帰化）がトレースに対応しているから、モジュール集約をモ…

大局的プログラミング（programming in the large）の話題：モジュールの演算5つはもっと簡単になる - 檜山正幸のキマイラ飼育記 メモ編のモジュール演算の件だが：enrichmentってのがイマイチわからん。が、次のようなもんだと思う。 module M = (A+B).((from N import A;) + K) ここで、Aは、Nがprovidesする名前の部分集合（A⊆ cod(N)）、BはKがprovidesする名前の集合（defineする名前の…

大局的プログラミング（programming in the large）の話題。ゴグエン先生の論文は "An Implementation-Oriented Semantics for Module Composition" だった。それで、MCLは、Module Composition Language の略でした。しかし、どっかで Connectingも使っていたと思う。さて、5つのモジュール演算とは、 aggrigation 弱モノイド積 instantiation 結…

…かってしまったよ！ 大局的プログラミング（programming in the large）のMCLのなんたるかを。記法を色々使うが、圏論記法、中間記法、実用記法としよう。対象が名前の有限集合（指標のもっとも簡単な例）、射がモジュールである圏を考える。 ＼ 圏論記法 中間記法 実用記法 結合 M;N N[M] N[M] 制限 M;πA A.M {a, b}M 弱モノイド積 M∨N M, N M, N 改名 ρab (b {a' 中間記法と実用記法がほとんど同じだな。（a, b…

…節と1.6節にモジュールの複合（composition）について書かれている。大局的プログラミング一般については、 http://www-adele.imag.fr/~jmfavre/ENSEIGNEMENT/TRANSPARENTS/ProgrammingInTheLarge/19/ProgrammingInTheLarge-19.pdf ↑のスライドがなかなかいい。スライドなので説明は十分ではないが、絵を眺めながら自分で行間を埋めると、色々な知見やヒントを得られるだろう。

大局的プログラミング（programming in the large）もプログラミングなのだから、当然にプログラミング言語が必要である。が、通常のプログラミング言語に大局的プログラミングが統合された言語は存在しない。仕様記述言語は、GoguenのOBJファミリーをはじめ山のようにあるが、どれも広く使われてはいない。仕様記述専門の言語を使え、というのはどうも無理があるのかもしれない。代替案は： 自然言語による記述 -- 従来型の仕様書 現存するプログラミング言語を使った仕様記…

大局的プログラミング（programming in the large）は必要か？ この問は、設計（デザイン）やアーキテクチャが必要か？ という問と同じだから、答はYESに決まっている。とはいえ、大局的プログラミングの定義や捉え方は人によりかなり異なる。僕自身は、設計と同義ではあるが、通常プログラミング（programming in the small）と同列に、かつ相似的に扱いたい、という意図がある。多くの人が（専門家も含めて）、"large"をシステムや開発チームが大規模…

…きないとき。 さて、大局的プログラミング（programming in the large）とは、モジュールを組み合わせることをプログラミング行為と位置づけたものだが、通常、設計とかアーキテクチャ策定とか呼ばれている行為と同じと考えてよい。同じではあるが、一種のプログラミングなのだ、という立場から大局的“プログラミング”と呼ぶ。大局的プログラミングに関して 言語機能 ライブラリ／開発ツール 手法／規約 によるサポート状況は? というと： import, require, us…