通用可组合性（UC），从范畴论视角：严谨的图表化证明
UC, Categorically: Rigorous Diagrammatic Proofs
浏览论文内容
中文总结 AI 辅助
本文运用范畴论的字符串图技术，对静态系统的通用可组合性（UC）框架进行严谨的范畴论处理，扩展其适用范围并修正疏漏，同时保持等价性与表达能力。
中文摘要 AI 辅助
范畴论是一种关于组合的数学理论，广泛应用于逻辑学、计算科学和物理学领域。本文将其应用于构建安全组合理论，具体针对Canetti提出的通用可组合性（Universal Composability, UC）框架，针对具有固定数量参与方与会话的系统（常称为静态系统的UC）提供范畴论处理，带来四项优势：其一，采用标准范畴论技术——字符串图（string diagrams），以图形方式呈现结果同时保持严谨性，本文的组合定理表述可通过简短的图表序列进行图形验证，且可转化为方程并适用于形式化验证；其二，范畴论支持泛化，使研究结果可从交互图灵机扩展至其他计算形式，如量子计算或领域特定语言；其三，范畴论有助于去除UC的部分不必要限制，例如本文的敌手可为计算网络而非单一图灵机，且已证明本文变体与常规UC等价，未损失表达能力；其四，范畴论视角帮助识别并修正了简单UC标准表述中的若干次要技术疏漏。
英文摘要
Category theory is a mathematical theory of composition, widely used in logic, computing, and physics. Here we apply it to give a theory of secure composition. In particular, we provide a categorical treatment of Canetti's Universal Composability (UC) framework for systems with a static number of parties and sessions, often termed UC for static systems, yielding four benefits. First, we present our results graphically yet retain rigor by applying a standard categorical technique known as string diagrams. In particular, our formulation of the composition theorem can be graphically verified with a short sequence of diagrams, while remaining translatable to equations and amenable to formal verification. Second, categories let us generalize so that our results extend beyond interactive Turing machines to other forms of computation, such as quantum computation or domain-specific languages. Third, categories help us drop some unnecessary restrictions of UC (e.g., our adversary can be a computational network rather than a single Turing machine); we prove equivalence between our variant and the usual UC, showing no expressiveness is lost. Finally, the categorical perspective leads us to identify and correct some minor technical oversights in the standard formulation of simple UC.
