UC, Categorically: Rigorous Diagrammatic Proofs

• URL: http://arxiv.org/abs/2608.04521v1
• Date: Wed, 05 Aug 2026 06:54:24 GMT
• Title: UC, Categorically: Rigorous Diagrammatic Proofs
• Abstract summary: Category theory is a mathematical theory of composition, widely used in logic, computing, and physics.<n>We provide a categorical treatment of Canetti's Universal Composability framework for systems with a static number of parties and sessions.<n>We present our results graphically yet retain rigor by applying a standard categorical technique known as string diagrams.
• Score: 2.857713591500304
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Does Syntax Matter? A Graph-Augmented Variational Topic Model for Computational Social Sciences [51.56484100374058]
  This paper introduces the Structural Contextual Probabilistic Topic Model ( SCPTM), an architecture that incorporates syntactic dependency relations into topic inference.<n>We evaluate seven topic modeling techniques across four corpora differing in register and discourse structure.<n>Results show that SCPTM's neural architecture yields substantial gains in document-topic alignment over generative baselines.
  arXiv  Detail & Related papers  (2026-09-07T17:39:06Z)
• PAGR: Proof-Carrying Algebraic-Geometric Retrieval: A Quiver-, Provenance-, and Sheaf-Theoretic Framework for Grounded LLM Retrieval [7.3040623979718475]
  Three distinct questions tend to be conflated: which statements are certified as knowledge, which latent representations are useful for retrieval, and which multi-hop compositions are semantically admissible.<n>We propose Proof-Carrying Algebraic-Geometric Retrieval (PAGR), a framework that separates these questions mathematically.
  arXiv  Detail & Related papers  (2026-09-05T14:51:32Z)
• String Diagrams for Quantum Foundations, Computing and Natural Language Processing [0.38073142980733005]
  We use string diagrams to investigate topics in the areas of quantum foundations, computing, and natural language processing.<n>We develop a formalism for wave-based logic circuits with phase encoding.<n>We investigate the elimination of inter-language grammatical bureaucracy in the distributional compositional circuits.
  arXiv  Detail & Related papers  (2026-05-12T02:11:44Z)
• On Improving Neurosymbolic Learning by Exploiting the Representation Space [54.16389421332958]
  We study the problem of learning neural classifiers in a neurosymbolic setting where the hidden gold labels of input instances must satisfy a logical formula.<n>One challenge is that the space of label combinations can grow exponentially, making learning difficult.<n>We propose a technique that prunes this space by exploiting the intuition that instances with similar latent representations are likely to share the same label.
  arXiv  Detail & Related papers  (2026-02-08T13:56:47Z)
• A Simple Trace Semantics for Asynchronous Sequence Diagrams [0.0]
  Sequence diagrams are a popular technique for describing interactions between software entities.<n>It is impossible to deduce a single interpretation for the notation's semantics.<n>In this work we describe a simple semantics based on the theory of regular languages.
  arXiv  Detail & Related papers  (2025-01-19T08:09:38Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  We propose a hybrid system capable of solving arithmetic problems that require compositional and systematic reasoning over sequences of symbols. We show that the proposed system can accurately solve nested arithmetical expressions even when trained only on a subset including the simplest cases.
  arXiv  Detail & Related papers  (2023-06-29T18:35:41Z)
• Lattice-preserving $\mathcal{ALC}$ ontology embeddings with saturation [50.05281461410368]
  An order-preserving embedding method is proposed to generate embeddings of OWL representations. We show that our method outperforms state-the-art theory-of-the-art embedding methods in several knowledge base completion tasks.
  arXiv  Detail & Related papers  (2023-05-11T22:27:51Z)
• Mathematical Foundations for a Compositional Account of the Bayesian Brain [0.0]
  We use the tools of contemporary applied category theory to supply functorial semantics for approximate inference. We define fibrations of statistical games and classify various problems of statistical inference as corresponding sections. We construct functors which explain the compositional structure of predictive coding neural circuits under the free energy principle.
  arXiv  Detail & Related papers  (2022-12-23T18:58:17Z)
• Equivariance with Learned Canonicalization Functions [77.32483958400282]
  We show that learning a small neural network to perform canonicalization is better than using predefineds. Our experiments show that learning the canonicalization function is competitive with existing techniques for learning equivariant functions across many tasks.
  arXiv  Detail & Related papers  (2022-11-11T21:58:15Z)
• Frame Averaging for Invariant and Equivariant Network Design [50.87023773850824]
  We introduce Frame Averaging (FA), a framework for adapting known (backbone) architectures to become invariant or equivariant to new symmetry types. We show that FA-based models have maximal expressive power in a broad setting. We propose a new class of universal Graph Neural Networks (GNNs), universal Euclidean motion invariant point cloud networks, and Euclidean motion invariant Message Passing (MP) GNNs.
  arXiv  Detail & Related papers  (2021-10-07T11:05:23Z)
• Can We Learn Heuristics For Graphical Model Inference Using Reinforcement Learning? [114.24881214319048]
  We show that we can learn programs, i.e., policies, for solving inference in higher order Conditional Random Fields (CRFs) using reinforcement learning. Our method solves inference tasks efficiently without imposing any constraints on the form of the potentials.
  arXiv  Detail & Related papers  (2020-04-27T19:24:04Z)
• Tensor Network Rewriting Strategies for Satisfiability and Counting [0.0]
  Instances of #SAT can be represented as tensor networks in a standard way. For classes known to be NP-complete, such as 3SAT, or #P-complete, such as #2SAT, the corresponding rewrite rules introduce hyperedges to the diagrams.
  arXiv  Detail & Related papers  (2020-04-14T12:50:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.