Deconstructing the Calculus of Relations with Tape Diagrams

2025-05-06 0 0 2.21MB 92 页 10玖币

侵权投诉

Deconstructing the Calculus of Relations with

Tape Diagrams

FILIPPO BONCHI,University of Pisa, Italy

ALESSANDRO DI GIORGIO,University of Pisa, Italy

ALESSIO SANTAMARIA,University of Pisa, Italy and University of Sussex, United Kingdom

Rig categories with nite biproducts are categories with two monoidal products, where one is a biproduct

and the other distributes over it. In this work we present tape diagrams, a sound and complete diagrammatic

language for these categories, that can be intuitively thought as string diagrams of string diagrams. We test

the eectiveness of our approach against the positive fragment of Tarski’s calculus of relations.

CCS Concepts: •Theory of computation →Logic;Categorical semantics.

Additional Key Words and Phrases: calculus of relations, rig categories, string diagrams

1 INTRODUCTION

Diagrammatic notations have been used in computer science since its early stages. A famous

example is the proof of the structured program theorem [

] by Böhm and Jacopini: they rely on a

syntax of ow diagrams and, by means of several transformations preserving the semantics, prove

the existence of a normal form. In physics, diagrams by Feynman [

] and Penrose [

] became

essential linguistic tools: on the one hand they provide intuitive visualisations for otherwise arcane

formulas; on the other, they allow a critical simplication of calculations, pretty much like adding

two Hindu-Arabic numerals is far easier than two Roman ones [26].

In general, well-behaved diagrammatic languages share some desirable features: (a) diagrams can

be composed, like one composes formulas in mathematics, programs in a programming language

or sentences in English; (b) they are equipped with a compositional semantics: the meaning of

a compound diagram is given by the meaning of its components; (c) some basic laws allow us

to transform diagrams into semantically equivalent ones, like the laws of arithmetic allow safe

manipulation of expressions.

Motivated by the interest in dealing with diagrammatic languages that enjoy such features, a

growing number of works [

] exploits string diagrams [

a graphical notation that emerged in the eld of category theory. Formally, string diagrams are

arrows of a strict symmetric monoidal category freely generated by a monoidal signature. A symbol

𝑠

in the signature is represented as a box

𝑠

, and arbitrary string diagrams are depicted by

composing horizontally (;) and vertically

(⊗)

such symbols (plus some wiring technology that we

are going to ignore in this introduction). The following is our rst example of a string diagram:

𝑓1

𝑓2

𝑔1

𝑔2

Observe that it can be regarded as both

(𝑓1

;

𝑔1)⊗(𝑓2

;

𝑔2)

and

(𝑓1⊗𝑓2)

;

(𝑔1⊗𝑔2)

. This ambiguity

is not an issue, since in any monoidal category the law

(𝑓1

;

𝑔1)⊗(𝑓2

;

𝑔2)=(𝑓1⊗𝑓2)

;

(𝑔1⊗𝑔2)

holds for all arrows

𝑓1, 𝑓2, 𝑔1, 𝑔2

. More generally, the main result in [

] states that the diagrammatic

representation identies exactly all and only the laws of strict monoidal categories. This is the key

feature of string diagrams. Indeed, by virtue of this fact, one can safely exploit diagrams to make

proofs, which in this way often amount to suggestive manipulations of diagrams.

2022 Filippo Bonchi, Alessandro Di Giorgio, Alessio Santamaria. This preprint article is available under licence CC-BY 4.0

https://creativecommons.org/licenses/by/4.0/.

arXiv:2210.09950v1 [cs.LO] 18 Oct 2022

Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria

By carefully crafting the monoidal signature, hereafter denoted as

, one obtains the syntaxes of

several languages specifying a large variety of systems: quantum processes [

], linear dynamical

systems [

], Petri nets [

], concurrent connectors [

], digital circuits [

], automata [

], or

conjunctive queries [14]. In these approaches, the semantics are dened by monoidal functors

⟦·⟧

CΣD(1)

going from the category of string diagrams

CΣ

to some monoidal category

representing the

semantic domain. Since

⟦·⟧

is a monoidal functor, it preserves ;and

⊗

, and thus the semantics

is guaranteed to be compositional. Typically, the languages come with a set of axioms, namely

equalities or inequalities between string diagrams, that are sound with respect to the semantics

interpretation. Interestingly, the same algebraic structures seem to appear in many dierent contexts,

e.g. commutative monoids and comonoids, Frobenius algebras, bialgebras, etc.

However, in several occasions the string diagrammatic syntax seems to be too restrictive. For

instance, in the context of the ZX-calculus [

], a well known quantum diagrammatic language,

several works [

] make use of a mixture of diagrammatic and algebraic syntax to represent,

for example, addition of diagrams. Similarly, in [

]

⊔

-props have been introduced in order to enrich

string diagrams with a join operation. Sometimes, the structure of monoidal category is not enough

and one needs to depict arrows of rig categories [

], roughly categories equipped with two

monoidal products:

⊗

and

⊕

. In these cases, the authors often introduce novel kinds of diagrams

[

] to convey the intuition to the reader, but without a soundness and completeness theorem

like in the aforementioned [

] for string diagrams. The main challenge in depicting arrows of a

rig category is given by the possibility of composing them not only with ;(horizontally) and

⊗

(vertically), but also with the novel monoidal product

⊕

. The natural solution consists in exploiting

3 dimensions. This is the approach taken by sheet diagrams [

], certain topological manifolds that,

modulo a notion of isotopy, capture exactly the laws of rig categories.

In this paper, we introduce tape diagrams as a way to depict arrows not of arbitrary rig categories

but only of those where

⊕

is a biproduct [

]. The payo of this restriction in expressiveness

is a better usability: tape diagrams are two dimensional pictures and for this reason they are, in

our opinion, more intuitive and more easily drawable than three dimensional diagrams. A second

important novelty is that we do not need to dene ad-hoc topological structures and transformations,

since tape diagrams are, literally, string diagrams of string diagrams.

Our main result, Theorem 5.11, is analogous to the one of [

]: it states that the category of tape

diagrams, hereafter referred to as

TΣ

, is the rig category with nite biproducts freely generated by

amonoidal signature. Another result, Theorem 4.9, states that for nite biproduct rig categories

considering only monoidal signatures, rather than the more general rig signatures, does not aect

the expressivity, in the sense that for every rig signature

one can nd a monoidal signature

Σ𝑀

such that the nite biproduct rig category generated by

is isomorphic to the one generated

Σ𝑀

. So, Theorems 5.11 and 4.9 together allow us to state that tape diagrams form a universal

diagrammatic language for rig categories with nite biproducts (see Remark 5.16).

A useful consequence of Theorem 5.11 is Corollary 5.12, which states that whenever the semantic

domain

of a string diagrammatic language as in

(1)

carries the structure of a nite biproduct rig

category, the semantics map ⟦·⟧ can be extended to tape diagrams as follows.

CΣD

TΣ

⟦·⟧

⟦·⟧♯

Deconstructing the Calculus of Relations with Tape Diagrams

In Example 5.13, we quickly show that applying the above construction to the ZX-calculus [

one can easily express through a tape diagram a quantum Controlled Unitary gate. In Example 6.13,

we show that, with the help of four “adjointness” axioms (in Figure 2),

⊔

-props from [

] can be

comfortably translated into tape diagrams so to obtain a purely graphical calculus that avoids the

use of algebraic operators. Finally, by taping the calculus of graphical conjunctive queries from [

one obtains a complete axiomatisation for the calculus of relations by Tarski [

]. This is our main

application, which we will illustrate in the next section.

Structure of the paper. In Section 3we recall string diagrams and monoidal categories. In particular,

we show that

Rel

, the category of sets and relations, carries two monoidal structures satisfying

distinct algebraic properties:

(Rel,⊕,

)

is a nite biproduct (fb) category, while

(Rel,⊗,

)

is a

cartesian bicategory (cb). In Section 4we recall rig categories and we introduce a novel (to the best

of our knowledge) notion of strictness that is useful to simplify the presentation. We also illustrate

rig signatures, nite biproduct rig categories and Theorem 4.9.

In Section 5we introduce tape diagrams and we prove Theorem 5.11. The key step of its

proof consists in showing that tapes form a rig category (Theorem 5.10): this is carefully done

by inductively dening left and right whiskerings (Denition 5.7) that enjoy beautiful algebraic

properties (Table 5). Dierently from

⊕

, the representation of the product

⊗

of two tapes involves

some computations. However, a further result, Theorem 5.15, allows us to avoid this issue: in

diagrammatic proofs one can safely forget about ⊗of tapes.

In Section 6we investigate the matrix calculus for

TΣ

that is provided by its nite biproduct

structure. Corollary 6.6 characterises tape diagrams as matrices of multisets of string diagrams.

Interestingly enough

⊕

of tapes corresponds to direct sum of matrices, while

⊗

to their Kro-

necker product. Such correspondence is then extended to a poset enriched setting: the category

of tapes resulting from the four aforementioned adjointness axioms is isomorphic to matrices of

downsets of string diagrams (Theorem 6.9). From this follows a characterisation of the induced

poset (Corollary 6.10) that is fundamental for the completeness result in Section 7: Theorem 7.5.

This result is analogous to Theorem 2.2 in [

] stating that nite dimensional Hilbert spaces are

complete for dagger compact closed categories. Theorem 7.5 shows that

Rel

is complete for fb-cb

rig categories (Denition 7.1), namely rig categories where

⊗

forms a cartesian bicategory and

⊕

nite biproduct category enjoying the aforementioned adjointness axioms. From the completeness

theorem, one can easily show (Corollary 7.8) that the laws of fb-cb categories provide a sound and

complete axiomatisation for the positive fragment of Tarski’s calculus of relations.

This article comes with a series of appendixes. All the coherence conditions are in Appendix A.

Appendix Bcontains some optional gures which may interest the curious reader. Indeed, apart

from Figures 1,2and 3which display all the tape axioms relevant to this paper, all the remaining

gures are in Appendixes Aor B. Finally, every technical section comes with its own appendix

providing additional results and detailed proofs (those in the main text are just sketches).

2 LEADING EXAMPLE: THE CALCULUS OF RELATIONS

In order to provide a preliminary intuition about tape diagrams and, meanwhile, explain their main

application investigated in this paper, we recall now the positive fragment of the calculus of binary

relations by Tarski [60]. Its syntax is specied by the following context free grammar

𝐸::=𝑅|1|𝐸;𝐸| ⊥ | 𝐸∪𝐸| ⊤ | 𝐸∩𝐸|𝐸†(CRΣ)

where

𝑅

is taken from a given set

of generating symbols. The expression 1denotes the identity

relation, ;relational composition,

·†

the opposite relation and the remaining expressions are the

usual set-theoretic union

∪

and intersection

∩

, together with their units

⊥

and

⊤

being, respectively,

Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria

the empty relation and the total relation. Formally, the semantics of

CRΣ

is dened w.r.t. a relational

interpretation I, that is, a set 𝑋together with a binary relation 𝜌(𝑅) ⊆ 𝑋×𝑋for each 𝑅∈Σ.

⟨⟨𝑅⟩⟩I=𝜌(𝑅) ⟨⟨𝐸†⟩⟩I={(𝑦, 𝑥)|(𝑥, 𝑦) ∈ ⟨⟨𝐸⟩⟩I}

⟨⟨⊥⟩⟩I={ } ⟨⟨𝐸1∪𝐸2⟩⟩I=⟨⟨𝐸1⟩⟩I∪ ⟨⟨𝐸2⟩⟩I

⟨⟨⊤⟩⟩I={(𝑥, 𝑦) | 𝑥, 𝑦 ∈𝑋} ⟨⟨𝐸1∩𝐸2⟩⟩I=⟨⟨𝐸1⟩⟩I∩ ⟨⟨𝐸2⟩⟩I

⟨⟨1⟩⟩I=𝑖𝑑𝑋={(𝑥, 𝑥) | 𝑥∈𝑋} ⟨⟨𝐸1;𝐸2⟩⟩I={(𝑥, 𝑧) | ∃𝑦. (𝑥, 𝑦) ∈ ⟨⟨𝐸1⟩⟩I∧ (𝑦, 𝑧) ∈ ⟨⟨𝐸2⟩⟩I}

(2)

Two expressions

𝐸1

𝐸2

are said to be equivalent, written

𝐸1≡CR 𝐸2

, if and only if

⟨⟨𝐸1⟩⟩I=⟨⟨𝐸2⟩⟩I

for all interpretations

. Inclusion, denoted by

≤CR

, is dened analogously by replacing

with

⊆

For instance, the following two laws assert that ;distributes over ∪but only laxly over ∩.

𝑅;(𝑆∪𝑇) ≡CR (𝑅;𝑆)∪(𝑅;𝑇)𝑅;(𝑆∩𝑇) ≤CR (𝑅;𝑆)∩(𝑅;𝑇)(3)

The question left open by Tarski is whether or not

≡CR

can be axiomatised: is there a basic set of

laws from which one can prove all the valid equivalences? Unfortunately, many negative results

show that there are no nite complete axiomatisations for the whole calculus [

], for the positive

fragment [36] and several other fragments, e.g. [10,29,53]. See [52] for a recent overview.

In this paper we propose a solution to the same problem, but from a radically dierent perspective:

we encode the calculus of relations into a novel calculus that is based on, in our opinion, more

primitive linguistic constructions. Our language, named

TCBΣ

, is strictly more expressive than

CRΣ

but allows to obtain a complete axiomatisation of equivalence and inclusion.

The syntax of

TCBΣ

is based on circuits and tapes. Circuits are obtained by composing horizontally

and vertically the following set of basic gates, where 𝑅is a symbol in Σ.

𝑅

To abbreviate, we will denote

, ,

and respectively as

◀,!,¡

and

▶

. Intuitively,

◀

acts as

acopier: it receives a signal (i.e. a value from some set

𝑋

) on its left wire and sends it to both its

wires on the right. Instead,

is a discharger: it throws away the signal coming from its only wire on

the left. Formally,

◀

is the pairing function

⟨𝑖𝑑𝑋, 𝑖𝑑𝑋⟩

going from

𝑋

𝑋×𝑋

, namely the cartesian

product of

𝑋

with itself, while

is the only function going from a set

𝑋

to a singleton set 1. The

gates

▶

and

are interpreted as the opposite relations of

◀

and

, respectively. Finally

𝑅

simply

denotes an arbitrary binary relation 𝑅on 𝑋.

It is worth emphasising here that signal ows through circuits as a wave, i.e. it passes through

all the vertical components at the same time. For instance, the circuit

𝑆

𝑅

denotes the relation

𝑅∩𝑆, i.e. the set of all pairs of signals (𝑥, 𝑦)such that, at the same time, 𝑥 𝑅 𝑦 and 𝑥 𝑆 𝑦.

Tapes are obtained by composing horizontally and vertically the following generators

𝑐

where the middle one represents a circuit

𝑐

wrapped inside a tape. To abbreviate, we will denote the

rst two generators on the left as

◁

and

⊸

and the last two on the right as



and

▷

. Intuitively,

▷

lets pass to the right the signal coming from either the top or the bottom branch on the left, while



simply closes a branch. Formally,

▷

is the coparing function

[𝑖𝑑𝑋, 𝑖𝑑𝑋]

going from

𝑋+𝑋

, i.e. the

disjoint union of

𝑋

with itself, to

𝑋

, while



is the only function going from the the empty set 0to

𝑋. The generators ◁and

⊸

are interpreted as the opposite relations of ▷and



, respectively.

Dierently from circuits, a signal ows through a tape as a particle, i.e. it passes through only

one of the vertical components at a time. For instance, the tape in

(4)

denotes the relation

𝑅∪𝑆

, i.e.

the set of all pairs (𝑥, 𝑦)such that either 𝑥 𝑅 𝑦 or 𝑥 𝑆 𝑦.

Deconstructing the Calculus of Relations with Tape Diagrams

𝑅

𝑆

(4)

𝑅

𝑆

𝑇

(5)

Since circuits can be nested inside tapes, an expression such as

𝑅∪ (𝑆∩𝑇)

can be represented

as the tape in

(5)

. A formal semantics of

TCBΣ

, as well as an encoding of

CRΣ

into

TCBΣ

, will be

given in Section 7. Moreover, Theorem 7.5 will state that the axioms in Figures 1,2and 3are

complete. Figure 1features the axioms for “plain” tape diagrams and Figure 2for their partial order

enrichment (discussed in Sections 6.2 and 7); Figure 3lists axioms to be used specically for

TCBΣ

Our axiomatisation is far from those proposed in more traditional approaches to

, but it

elegantly features some well-known algebraic structures that occur frequently in various elds

[

–

]. The second group of axioms in Figures 1and 3state that

(◁,

⊸

)

and

(◀,!)

are cocommutative comonoids while

(▷,



)

and

(▶,¡)

are commutative monoids. The third group

expresses the facts that

(◁,

⊸

,▷,



)

form a bialgebra and

(◀,!,▶,¡)

a special Frobenius bimonoid.

The axioms in Figure 2assert that the monoid

(▷,



)

is left adjoint to the comonoid

(◁,

⊸

)

, while

those in the last group in Figure 3state the the monoid

(▶,¡)

is right adjoint to the monoid

(◀,!)

The formal justication to these axioms will be claried through the paper but it is worth

establishing now a preliminary intuition: consider the axioms

(▷◁)

and

(▶◀)

. In the leftmost tape

(▷◁)

, the signal ows either in the top branch or in the bottom one, while in the rightmost tape,

the signal coming from any of the two branches on the left may go through any of the branches on

the right. In the two tapes of

(▶◀)

the signal ows, at the same time, through the top and bottom

wires: in the leftmost such signals must be equal, in the rightmost they may be dierent.

The remaining axioms are those in the rst and fourth groups in Figures 1and 3. The laws in

the rst group assert that crossings of tapes and wires behave like symmetries. The axioms in the

fourth group force naturality for

◁,

⊸

,▷

and



, while for

◀

and

naturality only holds laxly (and

from these one can easily derive that

▶

and

are colax natural). With these naturality axioms one

can immediately derive the laws in (3) as follows:

𝑆

𝑇

𝑅

(◁-nat)

𝑆

𝑇𝑅

𝑅

𝑆

𝑇

𝑅

(◀-nat)

≤𝑆

𝑇

𝑅

By means of simple graphical manipulations prescribed by the laws in Figures 1,2and 3, one can

prove all the valid equivalences in

. The curious reader may have a look to Figure 9illustrating

a graphical derivation for

𝑅∪ (𝑅∩𝑆) ≡CR 𝑅

. We conclude this preliminary section by remarking

that the discussed axiomatisation has some redundancies, e.g.

(



⊸

)

evidently follows from

(bo)

. We

have however chosen this presentation to emphasise the various elegant dualities.

3 STRING DIAGRAMS AND MONOIDAL CATEGORIES

We begin our exposition by regarding string diagrams [

] as terms of a typed language. Given

a set

of basic sorts, hereafter denoted by

𝐴, 𝐵 . . .

, types are elements of

S★

, i.e. words over

Terms are dened by the following context free grammar

𝑓::=𝑖𝑑𝐴|𝑖𝑑𝐼|𝑠|𝜎⊙

𝐴,𝐵 |𝑓;𝑓|𝑓⊙𝑓(6)

where

𝑠

belongs to a xed set

of generators and

𝐼

is the empty word. Each

𝑠∈Σ

comes with

two types: arity

ar (𝑠)

and coarity

coar (𝑠)

. The tuple

(S,Σ,ar,coar)

for short, forms a monoidal

signature. Amongst the terms generated by

(6)

we consider only those that can be typed according

to the inference rules in Table 1. String diagrams are such terms modulo the axioms in Table 1

where, for any

𝑋, 𝑌 ∈ S★

𝑖𝑑𝑋

and

𝜎⊙

𝑋,𝑌

can be easily built using

𝑖𝑑𝐼

𝑖𝑑𝐴

𝜎⊙

𝐴,𝐵

⊙

and ;(see e.g. [

]).

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

DeconstructingtheCalculusofRelationswithTapeDiagramsFILIPPOBONCHI,UniversityofPisa,ItalyALESSANDRODIGIORGIO,UniversityofPisa,ItalyALESSIOSANTAMARIA,UniversityofPisa,ItalyandUniversityofSussex,UnitedKingdomRigcategorieswithfinitebiproductsarecategorieswithtwomonoidalproducts,whereoneisabiproductandth...

收起<<

Deconstructing the Calculus of Relations with Tape Diagrams.pdf

共92页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Deconstructing the Calculus of Relations with Tape Diagrams

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: