This is a tutorial text giving an advanced introduction to the diagrammatic syntax of monoidal (and Cartesian) closed categories in the style of "functorial boxes". This syntax can be efficiently represented as a data structure which we call hierarchical hypergraphs, the systematic rewriting of which represents a way of deriving abstract machines for higher-order programming languages directly from their operational semantics. To arrive at this main intended application we pay attention in particular to the diagrammatic language of adjunctions and explicit strictifications. Finally, we present new proof techniques made possible by a quasi-canonical presentation of terms in monoidal closed categories called foliations which are useful in the case of complicated program transformations such as automatic differentiation and closure conversion.

翻译：这是一篇教程性文本，以"函子箱"风格对幺半（及笛卡尔）闭范畴的图解语法进行高级导引。该语法可高效表示为一种称为分层超图的数据结构，其系统性重写代表了一种直接从高阶编程语言的操作语义推导抽象机器的方法。为达到这一主要应用目标，我们特别关注伴随函子的图解语言及显式严格化。最后，我们提出一种新的证明技巧——通过一种称为叶理结构的准典范表示方法，该技巧在处理自动微分与闭包转换等复杂程序变换时尤为有效。