Rewriting modulo symmetric monoidal structure

被引:26
作者
Bonchi, Filippo [1 ]
Gadducci, Fabio [2 ]
Kissinger, Aleks [3 ]
Sobocinski, Pawel [4 ]
Zanasi, Fabio [3 ]
机构
[1] CNR, ENS Lyon, I-00185 Rome, Italy
[2] Univ Pisa, I-56100 Pisa, Italy
[3] Radboud Univ Nijmegen, Nijmegen, Netherlands
[4] Univ Southampton, Southampton SO9 5NH, Hants, England
来源
PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016) | 2016年
关键词
ALGEBRA; GRAPHS; NETS;
D O I
10.1145/2933575.2935316
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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
引用
收藏
页码:710 / 719
页数:10
相关论文
共 41 条
[1]  
Baez J., 2014, CORR14056881
[2]  
Baez J. C., 2015, ABS150405625 CORR
[3]  
Bonchi Filippo, 2014, CONCUR 2014 - Concurrency Theory. 25th International Conference, CONCUR 2014. Proceedings: LNCS 8704, P435, DOI 10.1007/978-3-662-44584-6_30
[4]  
Bonchi F., 2016, ABS160206771 CORR
[5]  
Bonchi F., 2014, ABS14037048 CORR
[6]  
Bonchi F, 2015, ACM SIGPLAN NOTICES, V50, P515, DOI [10.1145/2775051.2676993, 10.1145/2676726.2676993]
[7]   A basic algebra of stateless connectors [J].
Bruni, Roberto ;
Lanese, Ivan ;
Montanari, Ugo .
THEORETICAL COMPUTER SCIENCE, 2006, 366 (1-2) :98-120
[8]  
Bruni R, 2011, LECT NOTES COMPUT SC, V6901, P312, DOI 10.1007/978-3-642-23217-6_21
[9]   HIGHER-DIMENSIONAL WORD-PROBLEMS WITH APPLICATIONS TO EQUATIONAL LOGIC [J].
BURRONI, A .
THEORETICAL COMPUTER SCIENCE, 1993, 115 (01) :43-62
[10]   MATRICES, RELATIONS, AND GROUP-REPRESENTATIONS [J].
CARBONI, A .
JOURNAL OF ALGEBRA, 1991, 136 (02) :497-529