次の3者の関係が問題 仕様と仕様の記述方法 仕様に基づいて実装する“実装者” 実装が仕様に合致しているかどうかを確認する“テスター” 次のように考える。 仕様は、モノイド生成元と関係で与えられる。関係には観測演算子が使われる。 テストには、テスト式と…

なにがミソかというと、係数（可換）半環Kが総和完備なこと。これによって、K値関数の引き戻しだけではなくて前送りが定義できる。つまり、反変関手だけでなく共変関手も定義できる。反変と共変が同時に定義できると内積と共軛（随伴）っぽい概念が使えるよ…