だんだん思い出した：指標＝インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編 Lがrecursion-capable ⇔ ImplLがweakly trace-admissible Lが、構造に対する制約・条件を記述する論理言語（命題言語／証明言語）を備えているとする。このとき、Lの指…

あああああー、そうか。それをjanus〈ヤヌス〉と呼んでいたのだ。 指標＝インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編 双面神Janus プログラミング言語Lを、指標の圏Sigとその上のモナド L = (L, μ, η) と同一視する。つまり、プログラミング…

大局的プログラミング（programming in the large）の話題。ゴグエン先生の論文は "An Implementation-Oriented Semantics for Module Composition" だった。それで、MCLは、Module Composition Language の略でした。しかし、どっかで Connectingも使ってい…

ゴグエン先生が、MCL（Module Connecting Language）と言っていた。なーんか、今さらではあるが、いきなり分かってしまったよ！ 大局的プログラミング（programming in the large）のMCLのなんたるかを。記法を色々使うが、圏論記法、中間記法、実用記法とし…

「一般化フィルターの圏を真面目にやってみればぁ」をかすかに考えた。In-Outコンポネントの圏は、外側にあるコンポネントの圏の部分圏に過ぎない。しかし、一般化フィルター（以下では単にフィルター）の圏は部分圏ではない。特殊なIn-Outコンポネントから…

「In-Outコンポネントとパイプライン」の一般化フィルターの圏は、In-Outコンポネントの圏の部分圏。制限を付けているので、スター（双対）やトレースを定義できない。単にモノイド圏の構造を持つだけ。それでも、まーまー面白い。対象類は、{+, -}から作っ…

http://www.chimaira.org/docs/JanusIntro-2.htm#s4 より： ところで、use、provideのどちらをプラス（もう一方がマイナス）にするかは、まったく恣意的（どっちでもいい）なのだ。必然的、絶対的な理由や根拠なんてなくて、エイヤッと決めればいいことだ。…

http://d.hatena.ne.jp/m-hiyama/20071226/1198629573 年末年始にたいした予定があるわけでもないので、そこらでゴニョゴニョしているかもしれません。 ゴニョゴニュしている。まー、早寝しちゃうんで時間が取れないのだが、、、In-Outコンポネント図絵の描…

本編 http://d.hatena.ne.jp/m-hiyama/20071214/1197598785 に書いたように、JavaのBlocking Queueを使うとスレッドをあまり気にしなくていいようになる。で、パイプラインの幾何学的形状（トポロジ）に集中できるから、パイプラインを表現する式から、動作…

実務作業の8割くらいは雑用、でへこむ。が2割くらいエッセンシャルな部分がある。janusコンポネント概念は、具体的なプログラミング言語を固定して考えると割と具体的。なんだが、複数言語による分散アプリケーションとかを考えると、実装との距離が広がり、…

具体的に遷移変換系を扱うために、記号法／用語法を固定したい。TDを、遷移変換系の圏に対する固有名詞として使う。Σ、Γなどはマルチアルファベット（マルチラベル）で、Σ=(Σ1, ..., Σn)など。書くΣiはアトミック・ラベル（基本記号）の集合。Σの列としての…

全然説明してないが、システムの部屋モデルを考えている。部屋というのが高次圏のセル（高次射）であって、境界セルとして部屋の壁がある。圏の次元は少なくとも3、もっと高いかもしれない。結合以外にモノイド積が入っているから演算の数はやたらに多い。部…

“時間の空間”つうのも変な言葉だが、時間のパラメータ領域となるべき多様体ということ。境界を許す有向コンパクト1次元多様体は、nI+ mCの形をしている。ここでIは有限区間でCは円周S1のこと。nとmは自然数で成分の個数を表す。境界を許す有向コンパクト1次…

振る舞い関手は、加法的TQFT関手なのだろう、たぶん。物理のTQFTは、テンソル積と乗法的トレースを持つベクトル空間の圏を値圏にするが、振る舞い関手は、双積と加法的トレースを持つコゥゼン圏に値を取る。1-in 1-outの入出力仕様がA→Bであるようなコンポネ…

二重圏の定義としては、「“圏の圏Cat”のなかの圏対象（内部圏）」というのが一番スッキリしていると思う。だが、この定義だと、演算法則が露骨に表示されないので、具体性に乏しいし、実際の計算もやりにくい。それに巨大な（小さくない）二重圏の定義には不…

以前、マンダラの話を書いたが、ついつい単純なものを求めたくなる。いかん、いかん。世界はどえらく複雑なのだ！とりあえずコンポネントの圏がどれほどに複雑かを思い出しておこう。出力付きのリグラフ（rigraph）でコンポネントがモデル化されているとする…

「フェース」じゃなくて「フェイス」にした。 フェイス：コンパクト閉圏における域、余域 フロントフェイス：域 バックフェイス：余域 ユーザーサイド： フロントフェイスと同じ クライアントサイド： ユーザーサイドと同じ プラットフォームサイド： バック…

ソフトウェア的な技法 圏論的な解釈 論理計算 ラムダ計算 具体的なモデル ソフトウェア的な技法としては、とりあえずはコンベンションと動的（実行時）演算ライブラリだけを準備して、徒手空拳でも使えることをアピールしよう。もちろん、コンテナ（自動的な…

ポートベース・コンポネントを書くときに、できるだけコーディング量を減らすには： すべてフィールド方式を使う。 それが無理なときは： セッターが必要なポートが少数（1個か2個）なら、そこだけセッターにする。 セッターの使用が多いなら、混乱を避ける…

参考： 対称モノイド圏のシーケント計算 - 檜山正幸のキマイラ飼育記 メモ編 順序ベース多圏と名前ベース多圏、シーケント計算 - 檜山正幸のキマイラ飼育記 メモ編 レコード形式指標に対するセオリーとシーケント - 檜山正幸のキマイラ飼育記 メモ編 janusコ…

ブラックボックス（外から中を見て） ブラックルーム（中から外を見て） ブラックウォール（外と中を対等に考えて）

ボックスはコンポネントの別名として使う。ソリッドボックスとは、機能体と箱が一体のモノ、機能体が箱に作り付け、ハードワイヤされている。融通は効かない。例えば、プロファイルの変更は容易ではない。カスタムボックスは、機能体（ベース圏の射）と箱が…

ベースとなるトレース付き（対称）モノイド圏Cだが、これはセオリーの列(A1, ..., An)またはセオリーのレコード{a1:A1, ..., an:An}を対象とする。射f:A→Bは、ライブラリ／プラットフォームBを使ってサービスAを提供するプログラムになる（「プログラム」っ…