In the first part, we develop layered monoidal theories - a generalisation of monoidal theories combining descriptions of a system at several levels. Via their representation as string diagrams, monoidal theories provide a graphical syntax with a visually intuitive notions of information flow and composition. Layered monoidal theories allow mixing several monoidal theories (together with translations between them) within the same string diagram, while retaining mathematical precision and semantic interpretability. We define three flavours of layered monoidal theories, provide a recursively generated syntax for each, and construct a free-forgetful adjunction with respect to three closely related semantics: opfibrations, fibrations and deflations. We motivate the general theory by providing several examples from existing literature. In the second part, we develop a formal approach to retrosynthesis - the process of backwards reaction search in synthetic chemistry. Chemical processes are treated at three levels of abstraction: (1) (formal) reactions encode all chemically feasible combinatorial rearrangements of molecules, (2) reaction schemes encode transformations applicable to 'patches' of molecules (including the functional groups), and (3) disconnection rules encode local chemical rewrite rules applicable to a single bond or atom at a time. We show that the three levels are tightly linked: the reactions are generated by the reaction schemes, while there is a functorial translation from the disconnection rules to the reactions. Moreover, the translation from the disconnection rules to the reactions is shown to be sound, complete and universal - allowing one to treat the disconnection rules as a formal syntax with the semantics provided by the reactions. We tie together the two parts by providing a formalisation of retrosynthesis within a certain layered monoidal theory.
翻译:在第一部分中,我们发展了分层幺半理论——这是幺半理论的一种推广,结合了对系统在多个层次上的描述。通过其弦图表示,幺半理论提供了一种图形语法,具有视觉直观的信息流与复合概念。分层幺半理论允许在同一弦图中混合多个幺半理论(以及它们之间的转换),同时保持数学精确性与语义可解释性。我们定义了三种分层幺半理论的变体,为每种变体提供了递归生成的语法,并构建了关于三种紧密相关的语义(opfibration、fibration 与 deflation)的自由-遗忘伴随。我们通过提供现有文献中的多个示例来阐述该一般理论。在第二部分中,我们发展了一种逆合成分析的形式化方法——逆合成分析是合成化学中逆向反应搜索的过程。化学过程在三个抽象层次上处理:(1)(形式)反应编码了分子所有化学上可行的组合重排,(2) 反应方案编码了适用于分子“片段”(包括官能团)的变换,(3) 断键规则编码了适用于单键或单个原子的局部化学重写规则。我们证明了这三个层次紧密关联:反应由反应方案生成,同时存在从断键规则到反应的函子性转换。此外,从断键规则到反应的转换被证明是可靠、完备且普适的——允许将断键规则视为一种形式语法,其语义由反应提供。我们通过在某一分层幺半理论中对逆合成分析进行形式化,将两部分内容联系起来。