あ、これはcircKleisli構成と関係するかもヨー！http://www.iti.cs.tu-bs.de/~adamek/AAV.ps title: Iteration Monad AczelとAdamekが著者に入っている。 Elgotへの言及がある。 18ページ

http://www.cs.nott.ac.uk/~gmh/appsem-papers/uustalu.pdf title: Generalized Iteration and Coiteration for Higher-Order Nested Datatypes Tarmo Uustaluが著者に入っている。 16ページ Mendler-Style (Co)Iteration for (Co)Inductive Types

状況証拠で結ばれた複数のことが、完全には繋がらないで中途半端な感じ。繋ぎたい、繋ぎたい、繋ぎたい。 時系列にはしばられずに、その状況を総括しておく。人名はなるべくカタカナ書きする。でも、今日はダルイから、途中までで止めるけど。マーク W. ホプ…

（二者の）対話における因果性を、僕は一種の「慣性の法則」として理解している。つまり、「何も働きかけなければ何も起きない」と。自分または相手が非因果的であるとは、勝手に変化することだが、実際には隠れた原因があり、そこまで考慮すれば因果的なは…

そうか、自発性（非因果性）はε遷移で記述できるか。εを空語のみからなる言語だとして、 when (R) sending{ε} changes you(R') causes your{E}. 「私は何もしてないのに、あんたが勝手に変わったんでしょう。」「それが悪いか？」

Cond+(Σ) = Form(Obs(Σ+))（内部条件；直接制御可能）、Cond-(Σ) = Form(Obs(Σ-))（外部条件；直接制御不可能、コマンド経由）だとする。P∈Cond(Σ), Q∈Cond+(Σ), R∈Cond-(Σ), F∈Cmd(Σ), E∈Evt(Σ)に対して、次の形を持つ。メッセージは中括弧にする。 when(P)…

“クアドラプル”は言いにくいから、対話（的）ホーア式にする。極性付きでアメナブルな多ソートprefixed隠蔽指標を対話（的）指標と呼ぶことにする。Σがアメナブルなとき、Obs(Σ)は観測子（observer）の集合、Mut(Σ)が変更子（mutator）の集合。対話指標ΣはΣ=…

トリプルじゃなくてクアドラプル（quadruple）。(P, E; Q, F)なんだが、構文じゃなくて意味を使って説明する； コンポネントの（内部＋外部）状態空間をX、コンポネントのプラス（積極的、送り側）アルファベットをA、マイナス（消極的、受け側）アルファベ…

これもスライドPDF版→ http://www.cs.bath.ac.uk/~cf/GoI_London.pdfキーワード： Geometry of Interaction (GoI) dualizing object symmetric liniarly (weekly) distributive category polygraph Dummett category claasical category GoI construction = …

生体を例に刺激反応系と環境を説明 生体を、ブラックルームに閉じこめられた人（主体）に喩える。 外部とのインタラクションをポートとメッセージにする。（この段階で極性が入る。） ブラックルームをブラックウォールに変えて、環境を第二の主体と考える。…

スライドPDF版→ http://www.cs.um.edu.mt/~synchrone05/Presentations/08-TarmoUustalu.pdfキーワード： Comonadic Dataflow Programming Freyd Category symmetric premonoidal category Comonad Distributive law (of Monad)

指標が極性付きでΣ=Σ++Σ-でも、指標Σ上の制約やセオリーが、Σ+上の制約とΣ-上の制約に直和分解できるわけじゃない。そうじゃなくて、Sen(Σ++Σ-)のなかで考えることになる。これはコンポネント（双方向）のコンパクト閉圏が、単方向であるトレース付きモノイ…

πPインスティチューションからあらためて見て、“既に動いている実装の正しさ”と“プログラムソースコードの正しさ”は別な概念だな。実装が正しいとは仕様に対する充足性の問題で、たぶんvalidというのだろう。一方プログラムの正しさは、メイヤーの契約のよう…

インスティチューションがあって、Σ∈|Sign|ごとに、証明可能性“|-”が付いているとする。A⊆Sen(Σ)、b∈Sen(Σ)に対して、A|-b は、Aを仮定してbが証明できること。|-を拡張して、A|-Bが定義できる。「A|-B ならば A|⇒B」が健全性。ここで、A|⇒B は、BがAの帰結…

メモ編ネタがあるときは本編ネタがなくなる。まー、そういうもんだな。メモ編ネタ： Programming in the Hugeをやりたい。 仕様証明とプログラム証明は別物だ。ちゃんと区別。仕様証明はπインスティチューションの概念、プログラム証明はπPインスティチュー…

インスティチューションにプログラム（のソースコード）とプログラム証明を入れる準備。Pインスティチューションとは、(Sign, Mod, Sen, Prog, PMod, |=)であり、ProgとPModを除くとインスティチューション、Sign⊆Progであり、iが包含として、i;PMod = Mod。…

対称モノイド圏上のモナドFで、Fによるcirc-Kleisli構成のためにF(A)+F(B)→F(A+B)が必要だと書いたが、実際には、モナド単位B→F(B)と組み合わせて、F(A)+B→F(A)+F(B)→F(A+B)として使う。つまり、ほんとに必要なのはF(A)+B→F(A+B)だった。F(A)+B→F(A+B)は、テ…

今日はメモ編ばっかり書いていたから、そろそろオシマイ。記憶だけや1行メモに比べて、このくらい書いておけば後で読んで分かるだろう。図式計算は文字で描くの辛いから、紙に描いて捨ててしまうけど。図式の代用（記録）になるカルク記法がやっぱ欲しい。

入出力を持つ状態遷移機械を単に機械とか系と呼ぶとして、機械の圏の射α:A→Bは、集合圏でA×X→Pow(B×X)と解釈できるが、カリー化すると、α':X→Pow(B×X)^A、これは関手F(X) = Pow(B×X)^Aの余代数。機械の圏でHom(A, B)を状態空間の適当な写像を射として再び圏…

あれれれ、Cを集合圏として、(×, 1)でモノイダル構造を与える。共変ベキ関手Powと、sigleton埋め込み{-}:I→Powと∪:Pow(Pow)→Pow でモナドを考える。circ-Kleisli構成を考えると、状態遷移も出力も非決定的な順次機械の圏ができる。射は、A×X→Pow(B×X) で、こ…

circ-Kleisli構成をきまじめにかつ一気に定義すると、かなり面倒。circ-Kleisli構成＝Circ構成の後にKleisli構成だと思う。このことを確認できれば、話は単純になる。←勘違い、そんなことではない。現象の観察結果なので、“一気の定義”が先に来てしまった。…

http://d.hatena.ne.jp/m-hiyama/20060119/1137641539の「モゴモゴな話」に書いた件でメモ：少し分かってきた（かな？）。まず、関連するエントリーは： http://d.hatena.ne.jp/m-hiyama/20050716/1121499351 http://d.hatena.ne.jp/m-hiyama/20050719/11217…

http://www.almaden.ibm.com/cs/people/fagin/tcs93.pdf title: Finite-model theory - a personal perspective 著者はRonald Fagin 30ページ

http://d.hatena.ne.jp/m-hiyama-memo/20051226/1135592087に関連、一般化された帰納構造、帰納関数に関する参考： http://citeseer.ist.psu.edu/barthe03typebased.html 44P 長め http://citeseer.ist.psu.edu/gimenez98structural.html 14P http://citesee…

http://www.lang.osaka-u.ac.jp/~ogata/fosema.pdf -- 「フォーマルセマンティクス入門」でかいPDFだ。飽和法あるかな？

ヘンキン（返金じゃなくて、Henkin）が使った方法が飽和法かな？どうも飽和法の資料が少なくて、、、

そういえば、インスティチューションの具体例って書いたことない。お決まりの、フラグ、カウンタ、スタック。代数だと、半群、モノイド、線形空間（または加群）。多項式全体もうまいことインスティチューションになる。あと、なんか面白い例はないかいな。…

堕読（造語、ってシツコイ）ばっかりしていたいから、こっちに書くネタがない。ムー。

課題：カリー化がうまく表現できて、図式追跡と（比較的）対応した運算法。けっちょうムズ。非形式的な運算って、記号の乱用やオーバーロードを無闇と使っているから、切り分けるのが大変。

なくなったは純堕読用本だが、買ってきてまさに読もうとしたらないから、異常に腹がたった。買い直そうか、、、それもまたムチャクチャ悔しいし。この紛失癖、なんとかならんのか、クッソーー。ムカムカムカムカ。