トレース付きモノイド圏Cに意味を持つような形式的体系の項を考えると、その項はシーケント計算の証明に対応する。証明図の木構造がちょうど項の木構造に対応する。よって、項の変形は証明図の変形になっている。さらに、項の値（意味）は圏Cの射だから、証…

最近、少しだけ多圏の使い方に慣れてきた。多圏はけっこうバリエーションがある。まず、カットの自由度から、シングルカット多圏とマルチカット多圏がある。シングルカットはワイヤー1本に関してカットする。マルチカットは束（たば；リボン）でカットできる…

ステファネスクは酵素（enzymatic）公理／規則を使っているが、これは他の概念と関係する。 酵素公理／規則 一様性原理（uniformity principle; Plotkin） （双）模倣 （bisimulation） 圏の振る舞い正規化（notion of behaviour）→Notion of Behaviour - 檜…

monoid + al で monoidal という形容詞ができる。semiring + al で semiringal。ステファネスクは、semiringal categoryという言葉を使っている。半環圏と訳そう。半環圏は、2つのモノイド構造を持ち。それらが、分配性（distributivity）自然変換で関係して…