图解推理

图解逻辑于2002年被引入，重点在于规范和模型的概念。在本文中，我们改进了推理过程的描述，该过程被视为分数双范畴上的Yoneda函子。图解逻辑由极限速写（称为传播子）的态射定义，该态射产生一个伴随，进而确定一个分数双范畴。传播子、伴随和分数双范畴分别提供了该逻辑的语法、模型和推理过程。随后，将图解逻辑及其态射应用于计算机语言中副作用的语义。