定理の記述Cがトレース付きデカルト圏として、Cにおけるf:A×X→B×YのトレースTr(f)は、次のように分解した形で書ける。 fの第一射影f1をfout（出力関数）、fの第二射影f2をftran（遷移関数）とすると、Tr(f)は、ftranの不動点であるfloopとfoutの和（に近い形…

「繰り返しx*と強い繰り返しx+、長谷川の不動点補題」で言及した定理をトレース分解定理と呼ぶことにする。かなり一般的／周知の事実なので、個人名を冠するのはふさわしくない、と思い直した。さて、このトレース分解定理によれば、デカルト圏のトレースは…