量子群は、ホップ代数の最近の名称。であるなら、対蹠を落とした双代数は量子モノイドってことになる。コンピュータにとっては、群よりモノイドが自然な状況が多い。つまり、量子モノイド＝双代数によるモデルを考えるべきだろう。

メモ編にも書くべき事も山盛りあるんだけどなあ、、、 あー手が間に合わない。しかし、記録しないとドンドン忘却するし、、、うーむ。とりあえず、モノイド圏上に、3項または4項のhomを定義して、それで圏の集まり（indexed family of categories）みたいな…

ルーリエ（Jacob Lurie）は、やっぱり21世紀の（少なくとも21世紀前半）のグロタンディークだと思う。分野横断的な遠大で包括的な構想力、神がかりというか天の啓示みたいにスルスルと新しい概念とアイディアを出してくるし。そして、千ページ単位の書き物を…

MeadowはWindowsなので、改行コードを表す記号が： 記号 改行 (Mac) CR (Unix) LF \ CR+LF それと： キー コマンド C-x RET f set-buffer-file-coding-system C-x RET c universal-coding-system-argument C-x C-v RET find-alternate-file

次のような項目： 名前とラムダ束縛：対角Δ、終射!が名前によって実現される。 関数とメソッドの相互トランスレーション 関数、クラスメソッド、インスタンスメソッドの定式化 継承、委譲、DI などが、射影、indexed category、スタンピング関手で定式化でき…

http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?of=60&word=%a5%c8%a5%ec%a1%bc%a5%b9%c9%d5%a4%ad ビックリするくらいイッパイ書いている。

たしか、Subject-Property-Value図とか、そんなんがあったな。 Subject 丸印 Property 名札が付いた矢印 Value 四角とか、あるいは再帰的にSPV スカラー（基本データ）は四角か楕円とか。細長い四角形で配列を表せばJSONの図示となる。[1, 2] は次の図。 +--…

本編に書くべきなんだが、面倒でなー。 {ただのHTMLファイル} ⊆ {HTMLテンプレートファイル} （一般には {静的コンテンツ} ⊆ {動的コンテンツ}） {JSONデータリテラル} ⊆ {Catyスクリプト} {HTTPリクエスト} ⊆ {Catyコマンドライン} これの左側だけを取ると…

dirname, basename, ext, trunk の定義 ノード概念、ノードの種別 パス名の接頭辞順序 ツリー領域、またはツリー形状の定義 ツリー形状の上で定義された関数としてツリー ノード属性と関数値 パスの存在確認 パスの実体の生成 パスの属性を読む パスの属性を…

when {number => "this is number", string => "this is string"} function output(x) { alert("output: " + x); }if (typeof input === 'number') { output("this is number") } else if (typeof input === 'string') { output ("this is string") }

スコットブラケットとゲーデルの記号（あの記号そのものはなんていうんだ？）は知っておいて損はない。つうか、知っておくべきだし日常的に使うといいと思う。しかーし、手書きじゃないと書けないのが困る！ スコットブラケットを強いて書けば、【…】 ゲーデ…

集合の直積を考えたモノイド圏では、右自明（左自明）モノイドを作れる。集合の直和について同じことをしようと思うとうまくいかない。射を部分写像にすると、右自明積の類似を定義できる。A+A→A を左成分では未定義、右成分では恒等とすればいい。ところが…

Catyのモデルとなる圏って、分配圏をイッパイ含んだ分配圏か？ スタンピングでモナド、コモナドを作るときに使う演算と、JSONデータを細工するときの演算は明らかにレベルが違うのだけど、どっちも分配代数の構造を持つ。なんか、やっぱりマトリョーシカつう…

Prologの意味論で、閉世界仮説とかいうのがあったけど、アリャいったい何だったんだろう。いまだにわからん、つうか、一度も考えた事ないからわからんで当たり前だが。「Aの証明が失敗する」と「Aが証明できない」と「¬Aが真]を同一視するような話だったと思…

The comprehension principle 「包括原理」 The axiom of comprehension (CA) 「包括の公理」かな specification とか separation とも呼ばれる。 The axiom of separation は「分出公理」。 The axiom of specification 訳？ restricted, relative, bounded…

分配代数の圏バージョンである分配圏。2つのモノイド積を持つ。とりあえず、分配法則と結合法則のあいだの結び付きは次の可換図式で表現されるだろう。 a[(b + c) + d] → a[b + (c + d)] ↓ ↓ a(b + c) + ad ab + a(c + d) ↓ ↓ (ab + ac) + ad → ab + (ac + a…

意味じゃなくて、もっぱら記号の話。 定数とarity 0の関数 関数と演算子 fooとfoo()の区別 関数の引数渡しのバリエーション：可変引数、省略とデフォルト値、名前付き引数 関数記号と関係記号の区別 ソートを入れるか、特に真偽値のソート 真偽値のソートが…

JSONの意味論を展開するときの外の圏＝背景圏（background category）は、次のような圏がよかろう。 対象はセットイドである。 射は部分的セットイド写像。 直和、直積は集合ベースで考える。圏論的な直和・直積にならなくてもいい。 直和と直積で分配圏、で…

意味論のときに使う太い括弧を the "Scott-brackets" notation というらしい。Scottって、どのスコットだろう？ ダナ・スコット (Dana Stewart Scott) だな。

u = undefined として、記号の乱用で u = {u}。ブラケット内の数値はランクが減少する量。 ●opt-right A ⊆ B+u [u!∈A] -----------[-1] A ⊆ B●opt-both A+u ⊆ B+u [u!∈A, u!∈B] -----------[-2] A ⊆ B●object object {pi: Ai} ⊆ object {pi: Bi} -----------…

Catyの型推論のために、分解還元法というのを考えた。シーケント計算とタブローの中間のような感じのもの。推論は逆向きに（結論から仮定へと）行われるので、次の用語を導入する。 分解図 -- 推論図（1ステップ）の逆 還元図 -- 証明図（nステップ）の逆 シ…

最小元を持つ順序集合の圏を考える。射は任意の単調写像で、最小元を保存することは要求しない。集合直積が圏論的直積、単元集合が終対象を与え、単調写像の集合が再び最小元を持つ順序集合になる。この圏では、evと(-)^が定義できてデカルト閉になるが、始…

A?? → A? (A?|B) → (A|B)? など A? & B → A & B など A? & B? → (A & B)? bag [A?] → bag [A] (ハテナ定理には不要) @name A? → @name A (ハテナ定理には不要) ハテナ定理に必要なのは、演算子?, |, & に関する正規化だけ。

制限の追加ではなくて、領域（型の意味）の構成となっている演算は7種。 配列構成 オブジェクト構成 バッグ構成 （追加） ?演算 オプショナル構成 |演算 ユニオン構成 @演算 タギング構成 （追加） &演算 インターセクション構成 （追加） 配列、オブジェク…

たいした内容ではないけど、名前を付けておこう。 タグ排他性の原理：α≠β ⇒ (@α A)∩(@β B) = 0 単調性の原理：S ⊆T ⇒ tags(S)⊆tags(T) ハテナ定理：正規形の式なら、一番外側の'?'で確定型か不確定型か判断できる。 ν（nu）定理：ν(T) ≧ 1、ν(T) = n なら、T…

タグの基本はラベル（マーカー）。型情報としての利用は付随的／二次的であり、ラベルをインスタンス型情報として流用しているに過ぎない。利用可能な範囲も限定的である。バリデータをvalidateとすると： 基本は、validate(x, T) Tは型表現 validate(x) → v…

module public provides [person]; // personは公開型名となるtype person = @person object { "name" : string, "age" : integer(minimum=0), * : any } & // インターセクション演算子 personExt // 拡張ポイント ;// 拡張ポイントの実体を外部参照にする …

partialの訳語に「偏」を使う。「部分」だとsubと区別がつかないので。集合Aとその上の二項演算 +, * の組(A, +, *)が次を満たすなら分配代数。 (a + b) + c = a + (b + c) a + b = b + a (a*b)*c = a*(b*c) a*(b + c) = a*b + a*c (a + b)*c = a*c + b*c 0…

∩の定義は、XとYの共通アンビエント領域への埋め込みを使って定義する。 そりゃそうなんだが、共通アンビエント領域を探すのが難しい。∩という絶対的な演算はどうも無理で、∩Zのような演算しか有効じゃない気がする。

Tが型表現のとき T? はオプショナル型だが、この意味がわからない。モナドはもとより関手にさえならない。値空間が表現空間の外にあるときに、T? が何をすることなのか、サッパリわからない。embedded objectsの圏EO(C, A)の中なら解釈できるのか？CとEO(C, …