酵素公理、一様性原理

f:A×X→B×X, g:A×Y→B×Y がトレースを取ったとき等しくなる、つまり、Tr^X(f) = Tr^Y(g) について考える。u:X→Yがあって、f;(B + u) = (A + u);g がその条件になるときがある。推論規則で書くなら：

 f;(B + u) = (A + u);g : A×X→B×Y

 ------------------------------------

 TrX(f) = TrY(g)

この形式の推論を酵素公理とか一様性原理による推論と呼ぶ。

トレース付きモノイド圏Cと射の属U⊆Cが「酵素公理（一様性原理）を満たす」とは、u∈Uに対して、上の推論が妥当であること。実際には、Cに対してUを探して、推論の妥当性を(C, U)に関する定理として示す必要がある。Uは部分圏である必要はないが、同型射はUに含まれる。Uの射は酵素射とか厳密射／一様射と呼ぶ。→トレース付きモノイド圏の対角、一様性など - 檜山正幸のキマイラ飼育記 メモ編

一方で、既存の定理が酵素公理になっていることもある。オートマトンの最小化（マイヒル／ネロード型の定理）や、振る舞い同値と双模倣などが例になっているようだ。振る舞い関手と振る舞い正規化（notion of behaviour)も関係するだろう。→Notion of Behaviour - 檜山正幸のキマイラ飼育記 メモ編