変数xと型記号（ソート）Aに対して、x::A （普通はx:A）を変数の型宣言と呼ぶことにする。型宣言の集合を型環境と呼びΔ、Γなどで表す。型環境には、同じ変数の宣言が2回以上は登場しないとする。型環境に登場する変数の集合をVar(Δ)と書く。Var(Δ)とΔは同じ…

面白いことに気が付いた。Σをアルファベット（アトミック・アクションのラベル集合）とする遷移系Tがあったとする。それに、観測子（オブザーバー）φが付いているとする。φは|S|→V という写像。ここで、|T|はTの内部状態空間、Vは観測値（量）の空間である。…

うーん、随伴相方（adjoint mate）の解釈が間違っていたかも。F:C→D, G:D→Cで、D(F(A), Y)≒C(A, G(Y)) のとき、(f:F(A)→Y in D) と (g:A→G(Y) in C)が対応しているとして、fとgを相方（mate）と呼んでいるようだ。つまり、関手のあいだの関係ではなくて、圏D…