背景圏としては、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 …