式Eの計算が、すべての部分式の計算も含めて安全に行われる（と予測できる）とき、《E》 と書く。式Eのすべての部分式とパイプ記号には、番号（一意的ならなんでもいい）が振ってあるとする。異なる番号が同じ場所を指す可能性がある。（[追記]そんなにイッ…

これは、あくまで構文的であり、決して意味的ではないことに注意。意味的な議論は解釈を決めないとできないし、解釈は色々あり、解釈ごとに定義は変わる。基底：コマンド呼び出しと定数 Dom(f::S -> T) = S Dom(c) = null Cod(f::S -> T) = T Cod(c) = sing(…

「文字列（名前）の集合と非負整数値」の組をシグニチャと呼ぶ。次の形で書く； {"foo", "bar"; 2}, {; 3}, {"baz"; 0}, {;0}。シグニチャパターンはオプションシグニチャパターンと引数シグニチャパターンの組である。オプションシグニチャパターンは： 文…

カロウビ展開圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)のコピー与えられた圏Cに対して、新しい圏Kを作ります。その作り方を順に述べます。まず、Kの対象は、Cのベキ等射とします； a∈|K| ⇔ aはCのベキ等射 ⇔ a;a = a inc C。Kの射 f:(A,a)→(B, b) は次の…

モノ（値）かコト（事態、動作）か モノとコトの相互変換 soft-nothing と hard-nothing ⊥の追加、厳密射、リフト 結局は、バンドルと層を使うことになるな。 集合圏の始対象／終対象の非対称性 関数と関数型（べき、指数） 特異値と非特異台 外延的記法によ…