意味じゃなくて、もっぱら記号の話。 定数と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, …

10桁×10行のテキストファイルに、空白文字と星印('*')で描いたアスキーアートを、13バイトのファイルにエンコード／デコードするプログラムを書け。

背景圏としては、Posetoidを使うが、次のような組 (X, p)を考える。 Xはposetoid pはXからΩ={true, false, ⊥}への射 スライス圏を考えるわけではない。射はPosetoidと同じ。ただし、次のような演算を考えることができる。 (X, p) | (Y, q) = (X+Y, [p, q]) (…

JcentricTSのような簡単な型システムでも、型の意味はけっこう複雑で、Uをアンビエント対象＝JSON領域だとして： 台型の表現空間R、これはposetoid 台型の表現空間上で定義された3値述語p、⊥付きbooleanへのposetoid射 台型の値空間V Q(R)と同型だが同じとは…

Setoid, Posetoidもトポスにはならない。部分対象に関して： 充満である -- 埋め込みを関手とみなして充満 推移的である -- x∈D, x〜y ⇒ y∈D 完全である -- 充満かつ推移的 計算可能な述語で定義される部分対象を定義可能と呼べば、定義可能なら完全である。…

provide/require方式だから、requireがあるか・ないかで分類できる。開いたモジュール、閉じたモジュールとでも言えばいいのか。 Mが閉じたモジュール ⇔ モジュールを射とする圏で dom(M) = 1

Jcentric型システムの宣言スタイル・スキーマ構文 - 檜山正幸のキマイラ飼育記 (はてなBlog)の意味論のほうの話。 Posetoidの導入は避けられない。Posetoid自体はデカルト閉っぽい。 Posetoidの圏の変種は、必ずしもデカルト閉にはならない。 category with …

順序を≦、同値関係を〜とすると、条件は： a≦b, a〜a' ⇒ a' ≦ b a≦b, b〜b' ⇒ a ≦ b' くらいかな。Aの商Q(A)にも「≦が落とせる」と言えばいいのか。

集合圏かCPOの圏で考えるとして（デカルト閉圏ならいい）、ωは自然数（順序付き）か似たようなモンだとして、Aは勝手な対象。 in:Aω→A out:A→Aω とすると、ストリームIOの雰囲気がする。inとoutの間には通常はなにかしら関係があるが、特に関係は考えないと…

I = [0, 1] を単位区間とする。Xの柱体Cyl(X)は、X×I として定義される。一方、Yのパス空間Path(Y)は YI として定義される。例えば位相空間の圏Topで考えて、 Top(X×I, Y) = Top(X, YI) という随伴があるんで、Cyl(X)とPath(Y)が相関しているのは明か。だが…

hacker's /* test-inher-3-hacker.js */ // コンストラクタ var Point = function (x, y) { this.x = x; this.y = y; }; var PointPrototype = function () { this.moveTo = function (x, y) { this.x = x; this.y = y; }; this.toString = function () { re…

/* PointWithSecret.js */ var Point = function (x, y, secret_) { this.x = x; this.y = y; var secret = (secret_ || "confidence"); this.getSecret = function() { return secret; }; }; Point.prototype = { moveTo : function (x, y) { this.x = x; t…

集合圏Setに対して、埋め込み（対象上で単射な忠実関手）が指定されているような圏Cを考える。要するに標準的な忘却関手を持っているので、Cは集合・写像ベースの圏と言える。Cの対象の濃度をその台集合（忘却関手の値）の濃度とする。すると、濃度がたかだ…

「Aという性質を持つものに注目し調べましょう」は、「Aという性質を持たないものは意味がない」とか「Aという性質を持たないものを調べる価値がない」とかを含意しない。 Vを固定して、V値関手コボルディズムの圏を作る アロー図で見ると、fとgからf;gを作…

/* test-inher-1.js */ // コンストラクタ function Point(x, y) { this.x = x; this.y = y; } Point.prototype.moveTo = function (x, y) { this.x = x; this.y = y; }; Point.prototype.toString = function () { return "(" + this.x + ", " + this.y + "…

Tが型表現、またはその意味であるインスタンス領域だとして、tags(T) は、Tのインスタンスに付いている可能性のあるタグの集合。次のことを保証したい。 tags(T) は空ではない。 x∈T ならば tag(x) ∈ tags(T) そうなれば、S|T に対して、tags(S)∩tags(T) = 空…

ホーア論理を加群／余加群の枠組みで定式化できないかと考えて、ホーア加群というものをひねり出した。ただし、このままでは現実性がない、やたらに理想的な状況でしか意味を持たない構造。だがそれでも、より先を考えるための道具とはなるはず。いずれ書く…