• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Rewriting modulo symmetric monoidal structure
【24h】

Rewriting modulo symmetric monoidal structure

机译：重写模对称单曲面结构

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. This paper lays a comprehensive foundation for this form of rewriting. We interpret diagrams combinatorially as typed hypergraphs and establish the precise correspondence between diagram rewriting modulo the laws of SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs, subject to a soundness condition called convexity, on the other. This result rests on a more general characterisation theorem in which we show that typed hypergraph DPO rewriting amounts to diagram rewriting modulo the laws of SMCs with a chosen special Frobenius structure. We illustrate our approach with a proof of termination for the theory of non-commutative bimonoids.
机译：字符串图是对称单项类别（SMC）术语的强大而直观的图形语法。他们在计算机科学中找到了许多应用，并且在物理和控制理论等其他领域也变得越来越重要。图的方程式理论在许多此类方法中起着重要作用，这些方程式通常以定向和定向的方式应用于重写规则。本文为这种重写形式奠定了全面的基础。我们将图组合地解释为类型化的超图，并一方面建立以SMC的模模为模的图重写与超图的双推（DPO）重写之间的精确对应关系，另一方面还要遵循称为凸性的健全性条件。该结果基于更一般的特征定理，在该定理中，我们证明了类型化的超图DPO重写等于具有选择的特殊Frobenius结构的SMC律模的图重写。我们用非交换双峰理论的终止证明来说明我们的方法。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号