Tape diagrams provide a convenient notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $\oplus$ and $\otimes$, where $\otimes$ distributes over $\oplus $. In this work, we extend tape diagrams with traces over $\oplus$ in order to deal with iteration in imperative programming languages. More precisely, we introduce Kleene-Cartesian bicategories, namely rig categories where the monoidal structure provided by $\otimes$ is a cartesian bicategory, while the one provided by $\oplus$ is what we name a Kleene bicategory. We show that the associated language of tape diagrams is expressive enough to deal with imperative programs and the corresponding laws provide a proof system that is at least as powerful as the one of Hoare logic.

翻译：磁带图为装备两个幺半积$\oplus$和$\otimes$（其中$\otimes$对$\oplus$满足分配律）的rig范畴中的箭头提供了一种便捷的表示法。在本工作中，我们通过引入$\oplus$上的迹来扩展磁带图，以处理命令式编程语言中的迭代。更精确地说，我们引入了Kleene-Cartesian双范畴，即这样的rig范畴：其中由$\otimes$提供的幺半结构是一个笛卡尔双范畴，而由$\oplus$提供的幺半结构则是我们称之为Kleene双范畴的结构。我们证明，相关联的磁带图语言足以表达命令式程序，且相应的定律提供了一个至少与Hoare逻辑的证明系统同等强大的证明系统。