ホーア4つ組の定義らしきもの。やっと、しかし、まだ詰めが甘い。Sは状態空間、Aが入力記号の集合で、指標Σのミューテータ記号で与えられる。Bは出力記号の集合で、指標Γのミューテータ記号で与えられる。A*（Aの列）をコマンド、B*（Bの列）をイベントと呼…

とにかく、書けるときはワサワサ書いておくぞー。ちゃんと調べたり確認したりする余裕／気力／能力に欠けるので、激しく山勘を働かせてイイカゲンな作業仮説を書くことにする。まず、「状態空間が存在する」と信じよう。たまに信じられなくなるのだが、信じ…

Int構成でもGoI構成でも、その結合を絵に描くとワイヤーが交差する。バッテン、たすきがけになる。よって、この結合方法を「たすきがけ結合」（crossing composition）と呼ぼう。そう決めた。

C = (C, ×, 1, σ, *, η, ε)がコンパクト閉圏だとして、f:A→Bに対して、fのネーム[f]:1→A×B* が決まる。しかし、[f]と[g]が同型でも、fとgは全然違うケースもある。この状況をJanusコンポネントの圏で考えてみる。Janus profileからinputとoutputの別を取り除…

バート・ジャコブスが"Many-Sorted Coalgebraic Modal Logic: a Model-Theoretic Study"(http://citeseer.ist.psu.edu/jacobs01manysorted.html)のなかで、Ultrafilter Lemma として、「ブール代数Bのプロパーな（最小元を含まない）フィルターは、ウルトラ…

僕のナントナクの理解（いや、理解してないんだけど）では、文の極大無矛盾集合とは、極大フィルターと同等なものであって、極大無矛盾集合を作ってコンパクト性が示せる、と。そして、構成的に極大無矛盾集合を作る方法を飽和法といい、ヘンキンが創始者な…

飽和法が出ている資料を見つけた！ http://www.math.psu.edu/simpson/courses/math563/master.pdf title: Model Theory author: Stephen G. Simpson