Hassan Kallam
email: hassan.kallam@insa-lyon.fr

Leonardo S Cardoso
email: leonardo.cardoso@insa-lyon.fr

Jean Marie Gorce
email: jean-marie.gorce@insa-lyon.fr

Topological Interference Management: Trade-off Between DoF and SIR for Cellular Systems

Keywords: topological interference management, interference, topology, wireless systems, graph theory, cellular, degrees of freedom

Topological interference management (TIM) allows studying the degrees of freedom (DoF) of partially connected linear interference communication networks, where the channel state information at the transmitters (CSIT) is restricted to the topology of the network, i.e., a knowledge of which interference links are weak and which are strong. In this paper, we consider TIM for an infinite downlink cellular network in the onedimensional (1D) linear and the two-dimensional (2D) hexagonal models. We consider uniformly distributed users in each cellular cell, effectively creating a continuous distribution of users, aiming to study user classes based on different interference profiles rather than on actual individual users' positions. We also consider the construction of the TIM network topology by analyzing different interference thresholds. Unlike previous works, we use TIM at the user class level to find the system's DoF independent of the actual user position. Finally, after proposing a fractional coloring scheme that can achieve the optimal DoF solution, a trade-off between DoF and SIR is given.

I. INTRODUCTION

In spite of all recent advancements concerning wireless communications systems, interference remains one of the most critical "Achilles heels" of multi-user wireless systems, a problem that naturally arises due the broadcast nature of radio transmissions. Traditionally, interference has been dealt with the orthogonalization of resources, essentially avoiding interference [START_REF] Rappaport | Wireless communications: principles and practice[END_REF]. However, the strict structure in the partition of resources is known to provide lackluster performance in many situations. Facing the problem of interference has become all the more important nowadays due the need to extract more and more capacity out of an ever shrinking pool of spectral resources.

Recent techniques, such as interference alignment (IA) [START_REF] Cadambe | Interference Alignment and Degrees of Freedom of the K-User Interference Channel[END_REF], [START_REF] Suh | Interference alignment for cellular networks[END_REF] for dealing with interference rely on channel state information at the transmitter (CSIT) or receiver (CSIR), cooperation between transmitters and receivers and other complicated signaling techniques. While such techniques perform very well in controlled settings, they have proven complicated to implement in real life systems and are not easily scalable to large networks. A clever way of understanding the impact of interference in large wireless systems was proposed in [START_REF] Jafar | Topological interference management through index coding[END_REF], where channel knowledge is not needed beyond the topology of the interference links. This technique, called topological interference management (TIM), bases its analysis on a classification of the interference links into relevant or non-relevant, giving rise to a topology. Based on the topology, graph analysis can be made to characterize the underlying network with respect to its degrees of freedom (DoF).

The analysis of cellular networks through TIM has been the subject of recent works. TIM itself as a technique has been introduced in [START_REF] Jafar | Topological interference management through index coding[END_REF], where the foundations of graph analysis for topological networks is laid out. Analysis for simple cellular network structures (linear, square and hexagonal, with users located in the border of the cells) is addressed therein, with their DoF characterized. The work in [START_REF] Gao | Topological interference management for hexagonal cellular networks[END_REF] extends [START_REF] Jafar | Topological interference management through index coding[END_REF] by adding multi-layer interference as well as asymmetrical user positioning along the border of the cell. The work in [START_REF] Maleki | Optimality of orthogonal access for onedimensional convex cellular networks[END_REF] shows that an orthogonal resource allocation scheme achieves the sum DoF for linear one dimensional (1D) convex networks. This work is later generalized in [START_REF] Yi | Tdma is optimal for allunicast dof region of tim if and only if topology is chordal bipartite[END_REF], where a linear 1D and twodimensional (2D) cellular networks are studied through TIM, and it is shown that, if the resulting TIM network topology is chordal, then an orthogonal resource sharing scheme based on fractional coloring is sufficient to achieve optimal DoF performance. The authors show that one-dimensional convex TIM network topologies are chordal bipartite topologies. A bipartite topology graph is called a chordal bipartite topology graph if and only if any cycle of length 6 or more in this graph has at least one chord. A closed loop of a set of vertices and edges is called a cycle, and the chord is an edge connects two non-adjacent vertices of a cycle.

As stated before, defining a topology is crucial to perform TIM analysis. However, different interference thresholds will yield different topologies. As a matter of fact, even at a given interference threshold, different classifications of interference links may be considered, changing the topology accordingly. In this work, we will focus on defining a unique topology for a wireless network at a given interference threshold. As such the contributions of this work are as follows. First, unlike [START_REF] Jafar | Topological interference management through index coding[END_REF]- [START_REF] Yi | Tdma is optimal for allunicast dof region of tim if and only if topology is chordal bipartite[END_REF], where a discrete distribution of users is considered, we adopt a uniform linear distribution of users, where users that share the same interference profile can be grouped into a user class. We then apply TIM at the user class level to extract DoF information for the system independent of the actual user position. This approach is useful to characterize the average performance of the network. Second, we consider the effect of the interference threshold on the topology and the DoF of the system. By varying the interference threshold, an interesting trade-off arises: either we have a loosely connected graph, hence more DoF, but at the same time a higher interference since nodes contend more to access the medium, or a densely connected graph, hence less DoF, but at the same time a lower interference since nodes will choose a more conservative access to the medium. In this work we look for the best operating point in terms of interference threshold.

The remainder of this paper is organized as follows. Section II describes the infinite 1D (linear) and the infinite 2D (hexagonal) downlink cellular models studied in this work, along with the uniform user distribution adopted in the analysis. Section III presents the different topologies and their link to the interference threshold parameter. Additionally, this section provides the corresponding DoF analysis. Section IV presents the signal to interference ratio (SIR) analysis as well as the results of the DoF-SIR tradeoff study. Finally, section V provides final remarks of this work.

II. SYSTEM MODEL

In this work, we consider two distinct downlink cellular models, namely, infinite 1D and infinite 2D downlink cellular networks, whose characteristics are now presented.

A. Infinite 1D Downlink Linear Cellular Network Model

For the infinite 1D downlink linear cellular network, as shown in Fig. 1, cells of coverage region of length L are placed uniformly along a straight line. We consider one base station (BS) in each cell, with total transmit power P , located at the center of the cell. Each BS has M messages to be sent to its own M mobile users, and each user receives a unique message from its home BS. A total of M users are distributed uniformly in each cell coverage region, with M chosen sufficiently large to be represented by a continuous linear distribution of users in the cells. Such a continuum representation is appropriate to perform a long-term resource allocation. To simplify the analysis, only path loss is considered in the channel gain. It is worth saying that TIM relying on a reduced feedback, cannot manage fading at the BSs. However, the impact of fading could be introduced in the model by replacing the classical rate-SIR relation given in (17), by a modified version such as R = βη • log 2 (1 + ΞSIR (w) ) following [START_REF] Mogensen | Lte capacity compared to the shannon bound[END_REF], where β and Ξ are the spectral efficiency and the SIR efficiency respectively for a given system in some specific conditions. The channel gain between user m and BS i, is

γ i,m = ρ δ α i,m , (1)
where δ i,m is the distance between user m and BS i, α is the path loss factor, and ρ is the reference path loss for δ i,m = 1 meter. Also, in the subsequent analysis, the interference perceived by any user in the network, is as shown in Fig. 1, considered to come from its home BS (when it's serving other users in the home cell) and from all other BSs up to the second layer of interference, i.e., from the BSs in its adjacent cells and the first BSs following the adjacent cells. Hence, the distance above which we consider no link, i.e., γ i,m = 0, for the interfering channels is lower bounded by 5L/2.

… … Interference Cell i Cell i+1 Cell i 1 BS i BS i+1 BS i 1

B. Infinite 2D Downlink Hexagonal Cellular Network Model

The second model considered in this work is an infinite 2D downlink hexagonal cellular network where the cells of radius R are placed according to an hexagonal grid pattern, with the same area A T . We consider that each BS is equipped with an omni-directional antenna located at the center of the hexagonal cell with a total transmit power P . Similar to the 1D case, each BS has M messages to be sent for its own M mobile users, and each user receives a unique message from its home BS. Again, a large number M of users is distributed uniformly in the hexagonal cell area for all cells, and can be approximated by a spatial continuum of users. The channel follows the same considerations as for the 1D case in [START_REF] Rappaport | Wireless communications: principles and practice[END_REF]. We consider interference perceived by any user to come from its home BS (when it's serving other users in the home cell) and from only the first layer of interference, i.e., from the six BSs adjacent to its home cell, in its first surrounding layer given the hexagonal layout.

III. NETWORK TOPOLOGY AND DOF ANALYSIS

As introduced in [START_REF] Jafar | Topological interference management through index coding[END_REF], a topology must be determined to allow the calculation of the DoF via graph analysis. The path loss only model used herein allows a simple distance based interference connectivity threshold to be used for our TIM network topology construction. Therefore, the interference connectivity threshold is defined according to the interference distance D: significant interference links (i.e., connected interference links in the TIM representation) are only those such that δ i,m ≤ D. In other words, in the TIM network topology, the interference links between nodes separated by a distance greater than D are considered disconnected (the corresponding channel coefficient is zero in the TIM representation), and the interference links between nodes separated by a distance D or less are considered connected (the corresponding channel coefficient is set to one in the TIM representation).

A. Infinite 1D Downlink Linear Cellular Network Model

Let us start with the infinite 1D downlink linear network, for which the corresponding TIM network topology is shown in Fig. 2. In our case, the interference connectivity threshold is bounded by D < 5L/2 because of the considered path loss and interference models from section II-A.

Each user m gets two kinds of links: the desired link, from its home BS, and significant interference link, from each BS i where δ i,m ≤ D. The resulting network topology is then convex, as defined in [START_REF] Maleki | Optimality of orthogonal access for onedimensional convex cellular networks[END_REF]. This means that given any user m whose connectivity link to a BS i is guaranteed, then any user node n = m whose distance δ i,n ≤ δ i,m must also be connected to the same BS i. Then, the 1D network topology is chordal bipartite, since all 1D convex network topologies are chordal bipartite [START_REF] Yi | Tdma is optimal for allunicast dof region of tim if and only if topology is chordal bipartite[END_REF].

… … Cell i BS i BS i+1 BS i 1 Cell i+1 Cell i 1 D Interference c i,0 c i,+1 c i, 1
We consider the most interesting case when L/2 ≤ D ≤ L. In this case, we can divide each cell i into three regions, as shown in Fig. 2: a cell center region c i,0 and two cell edge regions c i,-1 and c i,+1 . The length of the cell edge regions c i,-1 and c i,+1 is pL ∀i, and the length of the cell center region c i,0 is (1 -2p)L ∀i, where p ≤ 0.5 is the interference design parameter defined as

p = D - L 2 L . (2)
Each user in cell region c i,j , j ∈ {-1, 0, +1}, shares the same interference profile, therefore, a cell region defines a class of users sharing the same interference. The set of users in region c i,0 is denoted by U i,0 , where these users see interference only from their home BS i, and it's defined as

U i,0 = m ∈ cell i : δ i-1,m > D, δ i+1,m > D}. (3)
The set of users in region c i,-1 is denoted by U i,-1 , where these users see interference only from their home BS i and from the BS i -1, and it's defined as

U i,-1 = {user m ∈ cell i : δ i-1,m ≤ D, δ i+1,m > D}. (4)
Finally, the set of users in region c i,+1 is denoted by U i,+1 , where these users see interference only from their home BS i and from the BS i + 1, and it's defined as

U i,+1 = {user m ∈ cell i : δ i-1,m > D, δ i+1,m ≤ D}. (5)
To study the DoF for this topology, we must first state some useful definitions that will be used in the following.

Definition 1 (Message Conflict Graph). The message conflict graph is an undirected binary graph, where each vertex represents a message W desired by user m and an edge exists between two vertices (messages) if the BS of one message interferes in the TIM representation with the user of the other message.

Definition 2 (User Class Based Conflict Graph). The user class based conflict graph is an undirected binary graph, where each vertex represents a set of users U i,j belonging to the same class and located in c i,j and an edge exists between two vertices (two set of users) if the BS of one set of users interferes in the TIM representation with the other set of users.

Remark 1. The users who belong to the same class of users are represented by a unique vertex in the user class based conflict graph. The messages desired by these users form a clique in the message conflict graph. A clique in the message conflict graph is set of vertices (messages) such that any two are connected by an edge.

The user class based conflict graph of our TIM network topology is presented in Fig. 3.

U i 1, 1 U i, 1 U i+1, 1 U i 1,0 U i,0 U i+1,0 U i 1,+1 U i,+1 U i+1,+1
Fig. 3. The user class based conflict graph of the 1D topology in Fig. 2.

Definition 3 (DoF Region). The DoF region is the closure of all the achievable messages' DoFs.

Remark 2. Since each user in the desires a unique message then the achievable DoF for a user is the achievable DoF of the message desired by this user.

Definition 4 (Symmetric DoF). The symmetric DoF is the largest DoF inside the DoF region that can be achieved simultaneously by all messages (users) in the network.

Remark 3 (Symmetric DoF in the Conflict Graph). In the message conflict graph, the symmetric DoF is the largest DoF value that can be achieved simultaneously by all nodes. This corresponds to a weighted symmetric DoF in the user class based conflict graph, in which each node in the user class based conflict graph achieves the symmetric DoF value weighted by its corresponding clique size in message conflict graph.

Now let us proceed to the DoF solution of the 1D linear TIM problem defined in this section. The DoF solution is per cell and is based on guaranteeing the symmetric DoF for all users in the 1D linear network topology. The following theorem presents the DoF solution.

Theorem 1. For the 1D linear cellular network topology with the interference design parameter p, the information theoretic DoF solution when all the users achieve the symmetric DoF value is

η = 1 1 + p , ( 6
)
where η is the DoF value per cell.

Proof. For chordal bipartite TIM network topologies, the DoF region of the TIM problem is characterized through the cliques of the message conflict graph as presented in [START_REF] Yi | Tdma is optimal for allunicast dof region of tim if and only if topology is chordal bipartite[END_REF]. Based on this and using the user class based conflict graph shown in Fig. 3, the DoF region of our TIM problem is characterized by all the DoF solutions that satisfy

d i-1,-1 + d i-1,0 + d i-1,+1 + d i,-1 ≤ 1, ∀i d i-1,+1 + d i,-1 + d i,0 + d i,+1 ≤ 1, ∀i, (7)
where d i,j , j ∈ {-1, 0, +1}, is the sum of the DoFs of the messages desired by the set of users U i,j . Knowing that a large number M of users are distributed uniformly and continuously inside each linear cell and since we are targeting the symmetric DoF for all users, then each cell region's DoF will be proportional to the size (length in 1D) of the cell region. We can then state that

d i,j = pη, ∀i and ∀j ∈ {-1, +1}, (8)
and

d i,0 = (1 -2p)η, ∀i, (9)
where η = M d sym and d sym is the symmetric user DoF.

Based on ( 7), ( 8) and ( 9), we get

3pη + (1 -2p)η = 1, (10)
thus completing the optimal DoF solution in [START_REF] Maleki | Optimality of orthogonal access for onedimensional convex cellular networks[END_REF].

It is clear from [START_REF] Maleki | Optimality of orthogonal access for onedimensional convex cellular networks[END_REF], that as the interference design parameter p increases, the TIM network topology becomes more connected (i.e., more interference links are considered to be significant in the 1D linear topology) and the DoF per cell decreases.

B. Infinite 2D Downlink Hexagonal Cellular Network Model

Now, let us address the case of the infinite 2D downlink hexagonal cellular network. A possible corresponding TIM network topology is depicted in Fig. 4. This network topology is based on the threshold of interference connectivity which will be defined in our model as the interference distance D. We consider in this paper the case when R ≤ D ≤ 3R/2. It follows that each cell i can be divided into 13 cell regions, a cell center region c i,0 and 12 cell edge regions c i,j where j ∈ {1, 2, . . . , 12}. The set of users in cell i in the cell center region c i,0 is denoted by U i,0 . These users see interference only from their home BS. The set of users in cell i in the cell edge region c i,j where j ∈ {1, 2, . . . 6} is denoted by U i,j where j ∈ {1, 2, . . . , 6}. These users see interference only from their home BS and from the BS in their unique adjacent cell. Then, the set of users in cell i in the cell edge region c i,j where j ∈ {7, 8, . . . , 12} is denoted by U i,j where j ∈ {7, 8, . . . , 12}. These users see interference only from their home BS and from the BSs in their two adjacent cells.

The user class based conflict graph of our TIM network topology is presented in Fig. 5. The graph construction is based on the same properties as the user class based conflict graph for the 1D linear model, however in order to aid in readability, some simplifications were made: 1) the edges between users classes belonging to the same cell are omitted; 2) an edge connecting a given user class to a whole cell aggregates all edges connecting this user class to all user classes in that cell. Through the same analysis as in section III-A, and using the conflict graph of Fig. 5, the following theorem presents the DoF solution of the 2D hexagonal TIM problem.

Theorem 2. For the 2D hexagonal cellular network topology the interference connectivity threshold the DoF solution when all the users achieve the symmetric DoF value is η = 1

+ A 1 A 2 A T ,
where η is the DoF value per cell, and A T , 1 and A 2 defined, using [START_REF] Fewell | Area of common overlap of three circles[END_REF], as follows

A T 3 √ 3R 2 2 , (12)
A 1 = 1 6 πD 2 -R 2 √ 3 4 , (13)
A 2 = √ 3 4 b 2 + 3 D 2 arcsin b 2D - b 4 √ 4D 2 -b 2 3 , (14)
where b is defined as

b = 3D 2 - 3R 2 2 -3R D 2 - 3R 2 4 . (15)
Proof. We will restrain from providing the whole proof here for brevity. The proof can be found similarly to the proof of Theorem 1, considering that the DoF for each cell region is proportional to the cell region size (area).

Figure 6 shows the DoF per cell in the 2D hexagonal network topology as a function of the interference distance D. Based on the DoF solution in Theorem 2 and from Fig. 6, it's clear that as the interference distance D increases, the TIM network topology becomes more connected (i.e., more interference links are considered to be significant in the 2D hexagonal topology) and the DoF per cell decreases.

IV. TRADE-OFF ANALYSIS BETWEEN DOF AND SIR

Determining an optimal interference threshold is an important issue for TIM due to the trade-off between DoF and SIR. In this section, a fractional coloring scheme [START_REF] Necker | Coordinated fractional frequency reuse[END_REF]- [START_REF] Bai | A graph-based interference topology control for ultra-dense networks[END_REF], achieving the optimal DoF solution for both 1D and 2D models is presented. Then, a SIR analysis, based on our proposed model and fractional coloring scheme, is presented. Finally, we show the trade-off between DoF and SIR.

A. Infinite 1D Downlink Linear Cellular Network Model

In [START_REF] Yi | Tdma is optimal for allunicast dof region of tim if and only if topology is chordal bipartite[END_REF], the authors show that if a TIM network topology is chordal bipartite, like the network topology considered herein, then an orthogonal access scheme, such as fractional coloring, is sufficient to achieve the DoF region of the corresponding TIM problem. We propose a fractional coloring scheme that achieves the optimal DoF solution of [START_REF] Maleki | Optimality of orthogonal access for onedimensional convex cellular networks[END_REF], pictured in Fig. 7. This fractional coloring scheme is designed such the different frequency bands F 1 , F 2 , F 3 , and F 4 are allocated for the different set of users U i,j , ∀i, ∀j ∈ {-1, 0, +1}, in such a way that any two set of users that have the same allocated frequency band do not interfere in the TIM scenario (no edge between them in the conflict graph).

Cell i+1 Cell i+2 Cell i Cell i 1 Cell i 2 F4 F3 F2 F F1 U i,0 U i,+1 U i, 1
The SIR for any user m in cell i, using the proposed fractional coloring scheme, is

SIR m = γ i,m j∈I γ i+j,m , (16)
where

I = I 0 = {-2, -1, +1, +2} if m ∈ U i,0 , I = I -1 = {-2, +1} if m ∈ U i,-1 , and I = I +1 = {-1, +2} if m ∈ U i,+1 .
Our objective is to find the cell rate when all users in the network have the same achievable symmetric user rate. This achievable cell rate is defined as follows

R = η • log 2 1 + SIR (w) , (17)
where R is the cell rate, η is as in (6) (multiplicative factor), and SIR (w) is the worst user SIR (log factor), determined by searching, in any cell i, for the worst user SIR in the cell center region and the worst user SIR in the cell edge regions. The worst user SIR in the cell center region c i,0 , denoted by SIR

i,c , is the SIR of user m ∈ U i,0 where δ i,m = L 2 -pL. The worst user SIR in the cell edge regions c i,-1 and c i,+1 , denoted by SIR (w)

i,e , is the SIR of user m ∈ U i,-1 or user m ∈ U i,+1 where δ i,m = L 2 . The worst user SIR SIR (w) at a given p is

SIR (w) = min SIR (w) i,c , SIR (w) i,e . (18)
The achievable cell rate when all users in the network have the same achievable symmetric user rate, is shown in Fig. 8 for path loss factor α = 2, as a function of the interference design parameter p. The trade-off between DoF and SIR, seen in Fig. 8, is as follows. On the one hand, if the interference connectivity threshold is too high (high p) then the topology becomes more connected (low DoF), and thus fewer opportunities to exploit TIM. Also, in this case with high SIR level, the cell rate will be low due to the low DoF at high p. On the other hand, if the interference connectivity threshold is too low (low p) then the topology becomes less connected (high DoF), and hence, plenty of opportunities to exploit TIM will arise. However, the SIR itself will suffer yielding low cell rates. As a matter of fact, this results highlights that a topological feedback may be sufficient in a network to obtain good performance, but the choice of the interference threshold is of utmost importance.

In our scenario the optimal choice of the interference threshold (optimal interference design parameter p * ) happens when SIR

(w) i,c = SIR (w) i,e , (19)
where p = p * fulfills (19), represented as the highest point of the curve in Fig. 8, with p * being approximately 0.23.

B. Infinite 2D Downlink Hexagonal Cellular Network Model

For the 2D model, the fractional coloring scheme that can achieve the optimal DoF solution in [START_REF] Assaad | Optimal fractional frequency reuse (ffr) in multicellular ofdma system[END_REF], is pictured in Fig. 5. This fractional coloring scheme is designed such that 17 different frequency bands are allocated for the different set of users U i,j , ∀i, ∀j ∈ {0, 1, . . . , 12}, in which any two set of users that have the same allocated frequency band do not interfere in the TIM network model (no edge between them in the conflict graph). The achievable cell rate is the same as for the 1D case in (17), but with η being the DoF per cell as defined in [START_REF] Assaad | Optimal fractional frequency reuse (ffr) in multicellular ofdma system[END_REF].

The achievable cell rate when all users in the network have the same achievable symmetric user rate, is shown in Fig. 9 for path loss factor α = 2, as a function of the interference distance D, where the cell radius R is chosen to be 1 km. The horizontal range in Fig. 9 is between 1 and 1.5 due to the range of D given in section III-B. The conclusions taken for the 2D case are the same as for the 1D case, with the optimal interference parameter D * being approximately 1.29 km.

V. CONCLUSION

The TIM problem for a downlink infinite cellular network is considered in the 1D (linear) and the 2D (hexagonal) models. The users are distributed uniformly in each network cell. In order to study user classes based on different interference profiles, a continuous distribution of users is considered. The TIM network topology is then built upon the interference distance threshold and optimal DoF solutions are computed accordingly. A fractional coloring scheme achieving the optimal DoF solution is proposed. We then show the trade-off between DoF and SIR in the network performance, relying on the interference threshold parameter. This latter result shows that the efficiency of a TIM approach is strongly impacted by an appropriate selection of the interference threshold parameter.

Fig. 1 .

 1 Fig. 1. Infinite downlink linear network model.

Fig. 2 .

 2 Fig. 2. Infinite linear network topology.

Interference: circle of radius D c i, 12 c i, 11 c i,10 c i, 9 c i, 8 c i, 7 c i, 6 c i, 5 c i, 4 c i, 3 c i, 2 c i, 1 c i, 0 Fig. 4 .

 121198765432104 Fig. 4. Infinite hexagonal cellular network topology.

Fig. 5 .

 5 Fig. 5. The user class based conflict graph of the 2D hexagonal topology in Fig. 4. The 17 different colors shown in this figure correspond to the fractional coloring scheme solution in section IV.

Fig. 6 .

 6 Fig. 6. DoF per cell as function of interference distance D.

Fig. 7 .

 7 Fig. 7. Fractional coloring scheme solution for the linear model.

Fig. 8 .

 8 Fig. 8. Cell Rate as function of the interference design parameter p.

Fig. 9 .

 9 Fig. 9. Cell Rate as function of interference distance D.


Wolfram Kahl
email: kahl@cas.mcmaster.ca

Finite Limits and Anti-Unification in Substitution Categories

It is well-known that coequalisers and pushouts of substitutions correspond to solutions of unification problems, and therefore do not always exist. But how about equalisers and pullbacks? If the literature contains the answers, they are well-hidden. We provide explicit details and proofs for these constructions in categories with substitutions as morphisms, and in particular work out the details of categorial products for which the universal arrow construction turns out to correspond exactly to anti-unification.

Introduction

Substitutions occur in the formal study of syntactic systems, and are mappings from "variables" to "terms" (or "expressions"). Terms may contain variables, and "application" of substitution to terms produces terms again. [START_REF] Rydeheard | Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms[END_REF] introduced (based on closely related ideas by [START_REF] Lawvere | Functorial semantics of algebraic theories[END_REF]) a categorial treatment of substitutions, where objects are sets considered as sets of variables, and morphisms from V 1 to V 2 are substitutions that map each element of V 1 to a term containing only variables from V 2 . They say: "In this case variables are localized." This is in contrast with most of the conventional literature on substitutions, were mostly a single global set of variables is assumed. For example, [START_REF] Eder | Properties of substitutions and unifications[END_REF] investigates a "more general than" order on idempotent substitutions. [START_REF] Rydeheard | Foundations of equational deduction: A categorical treatment of equational proofs and unification algorithms[END_REF] used their category-theoretic formulation in particular for the construction of a unification algorithm, where unification is defined as coequaliser of substitutions. Since unification problems are not always solvable, coequalisers do not always exist in substitution categories, but since unification problems are important, coequalisers (and pushouts which correspond to unification problems with disjoint variable sets) have received much attention in the literature. However, I have not been able to find explicit statements about equalisers, pullbacks, or products in substitution categories. Since substitution categories are a concrete instance of Kleisli categories, [START_REF] Szigeti | On limits and colimits in the Kleisli category[END_REF] study on limits and colimits in Kleisli categories using adjunctions is related, but, in his own words: "Mention must be made that these results are powerless in concrete instances. [START_REF] Hosseini | Equalizers in Kleisli categories[END_REF] tackle the problem of existence of equalisers in Kleisli categories for a number of more concrete monads, but still without covering the term monad.

One motivation for studying finite limits in substitution categories comes from the fact that substitutions can be components of homomorphisms of attributed graphs [START_REF] Kahl | Categories of coalgebras with monadic homomorphisms[END_REF][START_REF] Kahl | Graph transformation with symbolic attributes via monadic coalgebra homomorphisms[END_REF], and the properties of the resulting categories are key to the applicability of categorial approaches to graph transformation [START_REF] Ehrig | Fundamentals of Algebraic Graph Transformation[END_REF] in the spirit of the "high level replacement (HLR) systems" introduced by [START_REF] Ehrig | From graph grammars to high level replacement systems[END_REF]. In particular for the "adhesive categories" introduced by Lack andSobociński (2004, 2005) as a useful abstraction for frequently-studied HLR properties, existence of pullbacks becomes a key property. Another important question in that context is whether pushouts along all monomorphisms exist, or whether at least useful classes of monomorphisms can be defined along which pushouts exist.

In this paper, we provide concrete constructions and detailed proofs for equalisers, products, and pullbacks in substitution categories. In summary, the instances of basic category-theoretic concepts for the substitution category for a fixed signature take the following shapes, where well-known general facts are included in parentheses for completeness:

1. Epimorphisms are those substitutions where all target variables occur in the image. 2. Monomorphisms are those substitutions for which the image of any variable does not result from applying that substitution to any term different from that variable, as previously shown in [START_REF] Kahl | Graph transformation with symbolic attributes via monadic coalgebra homomorphisms[END_REF]. 3. Equalisers of two substitutions in the substitution category always exist, and are the variable subset injections for the subset on which the two substitutions have the same images -these are the equalisers of the two substitutions in Set, but the proof of the universal property is substitution-specific. 4. Regular monomorphisms are precisely the injective variable renamings. 5. (Coequalisers are most general unifiers, and do not always exist.) 6. Products have as objects the sets of all pairs of not-equally-headed terms;

the construction of the universal morphism is essentially anti-unification. Products of finite (variable) sets are in general infinite. 7. (Coproducts are inherited from Set as for every monad.) 8. Pullbacks always exist (since they can be obtained from products and equalisers). Pullbacks of substitutions between finite (variable) sets have finite pullback objects. 9. (Pushouts correspond to most general unifiers of substitutions with disjoint ranges, and do not always exist.) Pushouts along regular monomorphisms do exist, and regular monomorphisms are stable under pushout.

We are working on a mechanisation of this theory in the dependently-typed programming language and proof assistant Agda [START_REF] Norell | Towards a Practical Programming Language Based on Dependent Type Theory[END_REF]; at the time of writing, proofs for items 2, 3, and 6 are already complete.

Overview

After some background in sections 2 and 3 about monads and the term monad, we will work through the list above, except for the items in parentheses, which are well-known. We devote Sect. 4 to epimorphisms, Sect. 5 to monomorphisms, Sect. 6 to equalisers and regular monomorphisms, Sect. 7 to products, Sect. 8 to pullbacks, and Sect. 9 to pushouts.

2 Notation and Background: Categories and Monads

We assume familiarity with the basics of category theory; for notation, we write "f ∶ A → B " to declare that morphism f goes from object A to object B , or we may refer to the source and target objects of f as src f = A and trg f = B . We use " . , " as the associative binary forward composition operator that maps two morphisms f ∶ A → B and g ∶ B → C to (f . , g) ∶ A → C . The identity morphism for object A is written I A . We assign " . , " higher priority than other binary operators, and assign unary operators higher priority than all binary operators. The category of sets and functions is denoted by Set. For a function f ∶ A → B and an element x ∶ A, we normally denote function application by juxtaposition "f a". (We may need to add parentheses to either subexpression, "(f ) a" or "f (a)".) This juxtaposition has higher precedence than all visible operators.

A functor F from one category to another maps objects to objects and morphisms to morphisms respecting the structure that src, trg, I, and composition constitute; we denote functor application by juxtaposition both for objects, F A, and for morphisms, F f .

A monad on a category C consists is a functor M ∶ C → C for which there are two natural transformations ("polymorphic morphisms") return A ∶ A → M A and Each monad M on C induces the so-called Kleisli category K M that has the same objects as C, but C-morphisms A → M B as morphisms from A to B . Kleisli composition of f ∶ A → M B with g ∶ B → M C will be written f g; this is defined by f g = f . , (M g) . , join C . In the Kleisli category, return is the identity for Kleisli composition, that is, for each Kleisli morphism f from A to B we have

return A f = f and f = f return B .
Note the different symbols " . , " for composition in the base category and " " for composition in the Kleisli category! Both will occur frequently, and also together. They satisfy, among others, the equations (f . , g) h = f . , (g h) and f (g . , return) = f . , M g and (f g) . , M h = f (g . , M h).

Substitution Categories as Kleisli Categories of Term Monads

Let T Σ denote the term functor for signature Σ, that is, T Σ X is the set of Σterms with elements of set X as variables. As usual, T Σ X is defined inductively by the following:

-

Each variable v ∶ X is a term, that is, v ∈ T Σ X .
-If t 1 , . . . , t n ∈ T Σ X are n terms, and f is an n-ary function symbol provided by Σ, then the resulting function symbol application is a term, too:

f (t 1 , . . . , t n ) ∈ T Σ X .
T Σ is an endofunctor on the category Set, and naturally extends to a monad, the term monad. Its "join" natural transformation, join T Σ , produces for each set A (of variables) the function join T Σ ,A ∶ T Σ (T Σ A) → T Σ A which "flattens" nested terms over variables in A (that is, terms over T Σ A as their set of variables).

The "return" natural transformation of the term monad, return T Σ , maps each variable v to the term v . (We will omit the subscript T Σ for join and return.)

The Kleisli category of the term monad T Σ will be denoted T Σ ; its morphisms from set X to set Y are substitutions, that is, functions X → T Σ Y , that is, the sets X and Y are "interpreted" as sets of variables.

The definition of Kleisli composition instantiated for the term monad T Σ takes two arbitrary substitutions

F ∶ X → T Σ Y and G ∶ Y → T Σ Z to their composed substitution F G = F . , T Σ G . , join Z .
Conventionally, this would be described via "application" of substitutions to terms: We write F ▹ t for the application of substitution F ∶ X → T Σ Y to term t ∶ T Σ X , and the substitution composition F G can alternatively be defined by

(F G) v = G ▹ (F v ) , for all v ∶ X .
When starting from the monadic setting, application of substitutions can be defined as follows:

F ▹ t = ((T Σ F ) . , join Y )(t)
For most signatures Σ and most variable sets V , the set of terms T Σ V is infinite, but there are a few exceptions, which are important to keep in mind:

-The set T Σ ∅ of ground terms (i.e., terms without variables) is empty iff Σ has no constant symbols (that is, no zero-ary function symbols). -The set T Σ ∅ of ground terms has exactly n elements for n > 0 iff Σ has no function symbols with arity at least one, and exactly n constant symbols. -For a one-element variable set 1, the set T Σ 1 has at most one element iff Σ has no symbols at all.

We shall need the following definitions:

Definition 3.1. For a substitution σ ∶ V 1 → T Σ V 2 , its range ran σ ∶ P V 2 is the set of all variables occurring in σ v for some v ∶ V 1 .
Definition 3.2. A position is a finite sequence of positive natural numbers, with denoting the empty sequence and k .p denoting the sequence with first element k and tail sequence p.

Positions are used to select subterms:

f (t 1 , . . . , t n ) k .p = t k p if f has arity n, and 1 ≤ k ≤ n; t = t .

Epimorphisms in Substitution Categories

For every monad over category C we have that, if f is epi in C, then f . , return is epi in the Kleisli category. Substitutions of shape f . , return only map to variables. However, not all epis in T Σ are of this shape:

Theorem 4.1. A substitution σ ∶ V 1 → T Σ V 2 is epi in T Σ iff all variables in V 2 occur in the range of σ, that is, ran σ = V 2 . Proof. Recall that σ is epi iff for all τ 1 , τ 2 ∶ V 2 → T Σ V 3 we have that σ τ 1 = σ τ 2 implies τ 1 = τ 2 .
Assume σ is epi. Choose V 3 = {x , y}, and define τ 1 and τ 2 as follows:

τ 1 (v ) = x and τ 2 (v ) = x if v ∈ ran σ y if v ∉ ran σ
Then σ τ 1 = σ τ 2 , and since σ is epi, also τ 1 = τ 2 , which implies that ran σ = V 2 . Conversely, if ran σ = V 2 , and any V 3 and any τ 1 , τ 2 ∶ V 2 → T Σ V 3 with σ τ 1 = σ τ 2 are given, then for each variable v in V 2 , there is at least one u ∈ V 1 and position p in the term σ u such that (σu) p = v ; then

τ 1 v = τ 1 ((σu) p ) = (τ 1 ▹ (σu)) p = (τ 2 ▹ (σu)) p = τ 2 ((σu) p ) = τ 2 v ,
and therefore τ 1 = τ 2 .

Monomorphisms in Substitution Categories

A first version of the following analysis of monomorphisms in substitution categories appeared in the appendix of [START_REF] Kahl | Graph transformation with symbolic attributes via monadic coalgebra homomorphisms[END_REF].

In any monad, if the "return" natural transformation produces monomorphisms (which it does for T Σ ), then monomorphisms in the Kleisli category of this monad are also monomorphisms in the underlying category. Monomorphisms F of the underlying category that are preserved by the monad functor give rise to monomorphisms F . , return in the Kleisli category.

The term functor preserves all monomorphisms: An injective variable mapping

F ∶ V 1 → V 2 gives rise to an injective term mapping T Σ F ∶ T Σ V 1 → T Σ V 2 that only renames variables. The resulting substitution F . , return ∶ V 1 → T Σ V 2
is an injective variable renaming, which is therefore a mono in the category of substitutions, too -this also can easily be seen directly.

However, not all monos in T Σ are of this simple shape.

For σ, being a monomorphism in the category of substitutions exactly means that substitution application of σ does not unify any two different terms. That is, σ is a monomorphism in the category of substitutions iff for any two terms t 1 and t 2 we have

σ ▹ t 1 = σ ▹ t 2 implies t 1 = t 2 .
Due to the quantification over arbitrary terms t 1 and t 2 , this condition is not easy to check directly.

It is easy to see that monomorphisms in the category of substitutions, as a consequence of this condition, cannot map any variables to ground terms. However, this by itself does not constitute a characterisation of monomorphisms.

Fortunately a much simpler condition is (necessary and) sufficient: We can show that monomorphisms in the T Σ are those substitutions that do not identify variables with different terms:

Theorem 5.1. A substitution σ ∶ V 1 → T Σ V 2 is a monomorphism in the cate- gory of substitutions iff for every variable v ∶ V 1 and every term t ∶ T Σ V 1 , we have: σ ▹ t = σ v implies t = v .
Proof. "⇒" follows directly by applying the monomorphism property to the two terms v and t. "⇐": Assume that σ satisfies the given condition. To show that σ is a monomorphism in the category of substitutions it suffices to show that for any two terms t, u ∶ T Σ V 1 with σ ▹ t = σ ▹ u, we have t = u. We show this by induction on the structure of t and u:

-

If t = v is a variable, then σ v = σ ▹ t = σ ▹ u, from which the given property yields v = u.
-The case where u is a variable is analogous.

-If t = f (t 1 , . . . , t n ) and u is not a variable, then σ ▹ t = σ ▹ u implies that there are terms u 1 , . . . , u n such that u = f (u 1 , . . . , u n ) and σ ▹ t i = σ ▹ u i , from which the induction hypothesis yields t i = u i for all i , implying t = u.

For finite substitutions, the condition of Theorem 5.1 directly translates into a decision procedure that for each variable v ∶ V 1 checks whether for any different variable u ∶ V 1 , its image σ u occurs as a subterm in σ v . Due to the observation above, this can be further sped up for the negative case by first checking whether σ v is ground, in which case σ cannot be a monomorphism.

Equalisers

In any category C, an equaliser of two parallel morphisms f , g ∶ A → B is an object S together with a morphism ζ ∶ S → A such that ζ . , f = ζ . , g, and for every other candidate morphism h with h . , f = h . , g there us a unique morphism u such that h = u . , ζ. An equaliser morphism ζ is always mono. In Set, an equaliser for two functions f and g is a subobject monomorphism selecting the subset of A on which f and g coincide.

Kleisli categories do not automatically inherit equalisers from the underlying category.

For two substitutions σ, τ

∶ V 1 → T Σ V 2 , let V 0 together with ζ ∶ V 0 → V 1 be
their equaliser in Set. We now show that V 0 together with ζ . , return V1 is an equaliser for σ and τ in T Σ .

Commutativity follows from the monad laws:

(ζ . , return V1 ) σ = ζ . , σ = ζ . , τ = (ζ . , return V1 ) τ
For the universal property, we need to resort to substitution-specific reasoning. Assume a substitution h

∶ Z → V 1 with h σ = h τ . V 0 ζ . , return V1 E V 1 c σ T τ V 2

!u p p p p p p p p p p p p p p p T h Z

If ran h is empty, then we can define u z = h z since the latter is a closed term, and since ran u is then also empty, we obtain u

(ζ . , return V1 ) = u . , T Σ ζ = h.
If ran h is non-empty, let z ∶ Z be a variable, and p a position such that

(h z ) P = v for some variable v ∶ V 1 . Then σ v = σ ((h z ) P ) = (σ ▹ h z ) P = ((h σ) z ) P = ((h τ ) z ) P = (τ ▹ h z ) P = τ ((h z ) P ) = τ v , so v has to be in the range of ζ. Since ζ is a monomorphism in Set, that is, injective, there is exactly one variable u 0 ∶ V 0 such that ζ u 0 = v . Let ν ∶ V 1 → V 0
be an arbitrary mapping such that ζ . , ν = I V0 -such a mapping exists since V 0 is non-empty. Then we have:

(ν . , ζ) v = v for all v ∈ ran ζ. ( †)
We define u = h . , T Σ ν, and obtain:

u (ζ . , return V1 ) = Definition of u (h . , T Σ ν) (ζ . , return V1 ) = Monad properties h . , T Σ (ν . , ζ) = ( †) with ran h ⊆ ran ζ h
In both cases, u is uniquely determined due to the fact that ζ . , return V1 is a monomorphism in T Σ .

This shows that ζ . , return V1 is an equaliser for σ and τ in T Σ , and we have:

Theorem 6.1. T Σ has equalisers: For two substitutions σ, τ from V 1 to V 2 , an equaliser in T Σ can be obtained as ζ . , return V1 , where ζ is the equaliser in Set of σ and τ as functions in

V 1 → T Σ V 2 .
If we consider any other T Σ -equaliser h of σ and τ , with h ∶ Z → T Σ V 1 , then there must also be a substitution q ∶ V 0 → T Σ Z such that ζ . , return V1 = q h. This equation implies that in particular h must be of shape h 0 . , return V1 for some

(variable renaming) function h 0 ∶ Z → V 1 .
Since regular monomorphisms are defined to be those that are equalisers of some pair of parallel morphisms, and since in Set all monomorphisms are regular, we now also have: Theorem 6.2. The regular mononorphisms in T Σ are precisely the morphisms obtained as ζ . , return from some mononorphism ζ in Set.

Products

For every monad, a coproduct (S , ι, κ) for A and B in the base category give rise to the coproduct (S , ι . , returnS , κ . , returnS ) in the Kleisli category.

M S ι . , return S return S T d d d d d s κ . , return S A E ι S ' κ B
For the term monad, coproducts are just disjoint unions of variable sets.

However, starting from a product (P , π, ρ) for A and B in the base category and trying the same construction does not produce a product in the substitution category:

A π ' P ρ E B return A c © π . , return A d d d d d d ρ . , return B c return B T Σ A T Σ P T Σ B d d d d d d s σ !ψ T τ C
Given σ and τ , we would need to be able to construct a substitution ψ such that ψ (π . , return A ) = σ and ψ (ρ . , return B ) = τ . Let v ∶ C be a variable. Then ψ v must be some term u ∶ T Σ P (over the variable set P = A × B ) for which (π . , return A ) ▹ u = σ v and (ρ . , return B ) ▹ u = τ v . Using the monad laws, these equations are equivalent to the following equations, where π and ρ are mapped over the variables of u:

(T Σ π) u = σ v and (T Σ ρ) u = τ v ( * )
If u is not a variable, then the two left-hand sides of these equations will have the same outermost function symbol.

If we choose, for example, σ v = a and τ v = b for different constant symbols a and b, then no appropriate u can be chosen, and no substitution ψ can be constructed.

The argument above, slightly modified, actually shows that for any product of A and B in T Σ , the choice σ v = a and τ v = b for different constant symbols a and b implies that ψ v must be a variable, and analogously in the more general case where σ v and τ v have different outermost function symbols. We therefore define:

Definition 7.1. Given two (variable) sets V 1 and V 2 , two terms t 1 ∶ T Σ V 1 and t 2 ∶ T Σ V 2 are called strong-head-equal, written t 1 t 2 , if there are an (n-ary) function symbol f and terms s 1,1 , . . . , s 1,n ∶ T Σ V 1 and s 2,1 , . . . , s 2,n ∶ T Σ V 2 such that t 1 = f (s 1,1 , . . . , s 1,n ) and t 2 = f (s 2,1 , . . . , s 2,n ).
We will write t 1 t 2 for ¬(t 1 t 2 ).

The discussion above also shows that, since ψ v is a variable w from the product set P , the information that σ v = a and τ v = b must be contained in that variable.

One might consider to use P = T Σ A × T Σ B , which makes the projection definitions easy: π ∶ P → T Σ A with π(t 1 , t 2 ) = t 1 and analogously for ρ. However, now we have several choices for u

= ψ v if σ v = f (a) and τ v = f (b): We could set u = f ((a, b)) or u = (f (a), f (b))
. (Remember that "variables" in P are pairs of terms!) Both choices would satisfy the required equations ( * ).

This shows that, more generally, pairs (t 1 , t 2 ) with t 1 t 2 should not be "variables" in P .

We obtain that T Σ always has products: Theorem 7.2. For any to sets A and B , the set

P = {(t 1 , t 2 ) ∶ T Σ A × T Σ B t 1 t 2 } together with the projections π ∶ P → T Σ A with π(t 1 , t 2 ) = t 1 and ρ ∶ P → T Σ B with ρ(t 1 , t 2 ) = t 2 forms a product in T Σ .
Proof. Let a set C be given, and two substitutions σ

∶ C → T Σ A and τ ∶ C → T Σ B .
We need to show that there is a unique substitution ψ ∶ C → T Σ P such that ψ π = σ and ψ ρ = τ .

Recall that the anti-unifier of two terms t and u is the most specific generalisation g of the two terms, together with two substitutions ξ 1 and ξ 2 such that ξ 1 ▹ g = t and ξ 2 ▹ g = u. We shall write:

(g, ξ 1 , ξ 2 ) = antiUnif(t, u)
Now let G be the variable set of g (that is, g ∈ T Σ G), and define ξ ∶ G → P with ξ z = (ξ 1 z , ξ 2 z ) for every z ∶ G; this is well-defined since ξ 1 z ξ 2 z by the definition of anti-unification. We use this to define a variant of anti-unification

AntiUnif ∶ (T Σ A × T Σ B ) → T Σ P AntiUnif(t, u) = (T Σ ξ) g
that produces a single term with the structure of g over variables from P , which are pairs of terms in .

For every variable x ∶ C , we now define ψ x = AntiUnif(σ x , τ x ) and (g x , ξ x ,1 , ξ x ,2 ) = antiUnif(σ x , τ x ). Then:

(ψ π) x = Definition of substitution composition π ▹ (ψ x ) = Definition of ψ π ▹ (AntiUnif(σ x , τ x )) = Definition of AntiUnif π ▹ ((T Σ ξ x ) g x ) = π(ξ x z ) = ξ x ,1 z ξ x ,1 ▹ g x =
Definition of antiUnif σ x and analogously (ψ ρ) x = τ x .

Furthermore, if χ ∶ C → T Σ P is given such that χ π = σ and χ ρ = τ , then, for every variable x ∶ C :

-If χ x = (t 1 , t 2 ) is a variable from P , then t 1 t 2 and σ x = (χ π) x = t 1 and τ x = (χ ρ) x = t 2 , and therefore by definition of anti-unification also

ψ x = (t 1 , t 2 ) -If χ x = f (s 1 , . . . , s n ), then σ x = (χ π) x = f (π ▹ s 1 , . . . , π ▹ s n ) τ x = (χ ρ) x = f (ρ ▹ s 1 , . . . , ρ ▹ s n ) and therefore ψ x = f (AntiUnif(π ▹ s 1 , ρ ▹ s 1 ), . . . , AntiUnif(π ▹ s n , ρ ▹ s n )).
By induction over the structure of terms we then obtain χ = ψ.

From the proof, it is obvious that P is infinite as soon as at least one of T Σ A and T Σ B is infinite. Therefore, we have:

Corollary 7.3.
1. Over the category of finite sets, a substitution category has all products only if the signature has no function symbols with arity at least one. 2. Over arbitrary sets, the substitution category T Σ has all products.

Pullbacks of Substitutions

Since T Σ has products and equalisers, the standard definition of pullbacks from these can be used.

Let a cospan of substitutions

B τ1 E D τ2 ' C in the Kleisli category of T Σ be given, that is, two functions τ 1 ∶ B → T Σ D and τ 2 ∶ C → T Σ D. D τ 1 d d d d s τ 2 B π ' P ρ E C d d d d s σ 1 ζ T σ 2 A
The equaliser of ζ ∶ A → T Σ P of π τ 1 and π τ 2 gives rise to the pullback B σ1 ' A σ2 E C with σ 1 = ζ π and σ 2 = ζ ρ; the proof for this is a popular exercise in many introductions to category theory.

Corollary 8.1. For every signature, the resulting substitution category over Set has all pullbacks.

The equaliser ζ selects those pairs (t 1 , t 2 ) from P for which τ 1 ▹ t 1 = τ 2 ▹ t 2 . Since t 1 t 2 , at least one of t 1 and t 2 must be a variable, since if both were constructed from (necessarily different) function symbols, the equality τ 1 ▹ t 1 = τ 2 ▹ t 2 would not be possible.

For the case that t 1 is the variable v 1 , we obtain:

τ 2 ▹ t 2 = τ 1 ▹ t 1 = τ 1 v 1
Since τ 1 v 1 is a finite term, there are only finitely many choices of t 2 satisfying this. Analogously, if t 2 is a variable, then there are only finitely many choices for t 1 . Therefore, if the variable sets B , C , and D are all finite, then also A will be finite, even though P is (in general) infinite.

Theorem 8.2. For every signature, the resulting substitution category over the category of finite sets has all pullbacks.

Pushouts

The question whether V 1 σ ' V 0 τ E V 2 has a pushout in T Σ can be seen as a unification problem for two substitutions with disjoint variables, which corresponds to the standard construction of pushouts from coproducts and coequalisers. Therefore, obviously not all spans in T Σ have pushouts.

An important special case are pushouts along monomorphisms, or even along monomorphisms belonging to a particular class. We have seen in Sect. 5 that in T Σ , monomorphisms may map variables to non-variable terms, and since independent monomorphisms σ and τ may map the same variable to non-unifiable terms, just restricting to monomorphisms does not help here.

We therefore have to restrict our attention to monomorphisms that map variables only to variables, that is, regular monomorphisms in T Σ , which are according to Theorem 6.2 the monomorphisms of shape m . , return where m is a monomorphism in the base category, that is, an injective variable mapping.

Let a substitution σ ∶ V 0 → T Σ V 1 and an injective function ι 2 ∶ V 0 → V 2 be given. Since this is in Set, we can see ι 2 as the first injection of a coproduct

V 0 ι2 E V 2 κ2 ' U , where U needs to be isomorphic to the set V 2 -ran ι 2 . Then define V 3 via another coproduct V 1 ι3 E V 3 κ3 ' U in Set. Now we define τ ∶ V 2 → T Σ V 3
as a universal morphism associated with the coproduct V 2 , namely:

τ = [σ . , T Σ ι 3 , κ 3 . , return V3 ]
Then the following diagram is a pushout in T Σ :

V 0 σ E V 1 ι 2 . , return V2 c c ι 3 . , return V3 V 2 τ E V 3
Commutativity follows easily:

(ι 2 . , return V2 ) τ = Monad properties ι 2 . , τ = Definition of τ ι 2
. , [σ . , T Σ ι 3 , κ 3 . , return V3 ] = Coproduct properties σ . , T Σ ι 3 = Monad properties σ (ι 3

. , return V3 )

Altogether, this shows:

Theorem 9.1. T Σ has pushouts along regular monomorphisms.

Such a pushout just adds the variables of V 2 outside the range of m as additional "unused" target variables to σ.

Already if m is not a monomorphism, pushouts for V 1 σ ' V 0 m . , return E V 2 in T Σ will not exist if there are two variables u, v ∶ V 0 with m u = m v , but for which σ u and σv are not unifiable.

In the context of the proof above, if the

T Σ -cospan V 1 ϕ E V 4 ψ ' V 2 , too, is a T Σ -pushout for V 1 σ ' V 0 ι2 .
, return E V 2 , then χ ∶ V 3 → T Σ V 4 has to be an isomorphism between the two pushout objects V 3 and V 4 , with the inverse satisfying in particular ϕ χ -1 = ι 3

. , return V3 . Due to this equality, the image of ϕ can only contain variable terms, and since ϕ = (ι 3 . , return V3 ) χ is a composition of a monomorphism with an isomorphism, it altogether has to be a regular monomorphism, so we have:

Theorem 9.2. In T Σ , regular monomorphisms are stable under pushout.

Conclusion and Outlook

For categories with variable sets as objects and substitutions as morphisms, we provided explicit characterisations and constructions of monomorphisms, epimorphisms, equalisers, regular monomorphisms, products, pullbacks, and of pushouts along regular monomorphisms. These can be useful in contexts where categories of substitutions become building blocks of more complicated categories, as for example in transformation of symbolically attributed graphs. While in settings with global variable sets, such as that of [START_REF] Eder | Properties of substitutions and unifications[END_REF], anti-unification appears as dual to unification, we identified the construction of the universal morphisms for products as corresponding to anti-unification. This, interestingly, is not at all categorially-dual to the coequalisers or pushouts that correspond to unification.

  join A ∶ M (M A) → M A satisfying return M A . , join A = I and M return A . , join A = I and M join A . , join A = join M A . , join A . Important monads are the List monad, and the term monad T Σ for any (algebraic) signature Σ. For the former, join List,A ∶ List (List A) → List A is the function that flattens (or concatenates) lists of lists.

Acknowledgement: I would like to express my gratitude to the anonymous referees for their constructive comments, which helped significantly to improve the presentation.

Assume another cospan

. , return V2 ) ψ .

( ‡)

Then define χ ∶ V 3 → T Σ V 4 as a universal morphism associated with the coproduct V 3 , namely χ = [ϕ, κ 2 . , ψ]. The resulting triangles commute:

Coproduct properties ϕ and:

. , ψ, κ 2 . , ψ]

=

Coproduct properties ψ

Furthermore, for every other substitution ξ ∶ V 3 → T Σ V 4 with (ι 3

. , return V3 ) ξ = ϕ and τ ξ = ψ we have:

. , ξ, κ 3 . , ξ)]

=

Coproduct properties ξ


Wolfram Kahl
email: kahl@mcmaster.ca

Yuhang Zhao

A Flexible Categorial Formalisation of Term Graphs as Directed Hypergraphs

Term graphs are the concept at the core of important implementation techniques for functional programming languages, and are also used as internal data structures in many other symbolic computation setting, including in code generation back-ends for example in compilers. To our knowledge, there are no formally verified term graph manipulation systems so far; we present an approach to formalising term graphs, as a relatively complex example of graph structures, in the dependentlytyped programming language and proof system Agda in a way that both the mathematical theory and useful executable implementations can be obtained as instances of the same abstract definition.

Introduction

Terms (or expressions) are the conceptual data structure at the heart of almost all symbol manipulation for mathematical reasoning and programming language implementation. Terms as a data structure are a kind of trees, and in many applications, intermediate or result terms arise that contain multiple copies of equal subterms. To save space in software implementations of such applications, all these copies are frequently represented by references to a single copy: Conceptually, the tree is replaced by a (directed, and for the purposes of the current paper always acyclic) graph, a term graph. Nowadays, term graphs are typically considered as jungles, a kind of directed hypergraphs introduced for this purpose by [START_REF] Hoffmann | Implementing term rewriting by jungle evaluation[END_REF] and [START_REF] Corradini | Hyperedge replacement jungle rewriting for termrewriting systems and logic programming[END_REF].

For the purpose of creating a toolset for term graph manipulation supported by machine-checked correctness proofs, we develop a flexible formalisation of term graphs in a categorial setting, with the following goals: -We want to use the formalisation to develop mathematical theories of term graph transformation and how it can be used in particular for correct-byconstruction compiler optimisation passes. -We want to use that same formalisation as basis for executable implementations of these compiler optimisation passes. As our formalisation setting, we use the dependently-typed programming language and proof assistant Agda [START_REF] Norell | Towards a Practical Programming Language Based on Dependent Type Theory[END_REF]. Agda permits us to write definitions essentially in the way they are written for mathematical purposes, and prove properties about them, but all function definitions are also executable, making this a good environment for correct-by-construction tool development.

The body of this paper will start from a sequence of mathematical definitions (expressed in Agda) of datatypes for somewhat simplified term graphs, then consider also an implementation-oriented definition, and proceed to abstract both to a common generalisation. The full complexity of term graphs is the recovered in a few more refinements.

The result is a simple language for defining not only term graphs, but any of a large class of different kind of graph datastructures, when recognising these as coalgebras possibly including dependently-typed operations, as far as dependencies are used with a certain discipline.

Jungle Representation of Term Graphs

We think of term graphs as a kind of data-flow graphs, and we draw the flow from inputs (labelled by their positions in triangles) at the top to output positions at the bottom. We use the jungle approach of [START_REF] Hoffmann | Implementing term rewriting by jungle evaluation[END_REF]; [START_REF] Corradini | Hyperedge replacement jungle rewriting for termrewriting systems and logic programming[END_REF]: We define term graphs as hypergraphs, where each (hyper-)edge is labelled with an operation name, and connected via "input tentacles" (drawn as arrows to the box representing the hyperedge) to the edge's input nodes, and via a single "output tentacle" (pointing away from the edge) to its output node. Term graph inputs correspond to variables in terms; so if we map each input position i to the variable x i , then the term graph in the following drawing to the left represents the term (x 1 + x 2 ) * x 2 :

+ * 1 2 1 + * 1 2 2 1
The term graph drawn above to the right has two output positions, and therefore should be interpreted as a pair of terms; in this case the two output positions are "fed" from the same node, so this is just the pair ⟨(x 1 +x 2 ) * x 2 , (x 1 +x 2 ) * x 2 ⟩. (We could easily switch to considering multi-output edges, but for the purposes of the current paper this would only result in some duplication, without introducing any additional interesting aspects, so we stick with single-output edges.)

The pure "directed hypergraph" aspect of term graph structure, without considering inputs and outputs, and without restricting the edge output assignment to be bijective onto non-input nodes, can be captured via the following signature:

sigDHG ∶= ⟨ sorts: N, E ops: src ∶ E → List N trg ∶ E → N eLab ∶ E → L ⟩
This is a coalgebraic signature in the sense used in [START_REF] Kahl | Categories of coalgebras with monadic homomorphisms[END_REF][START_REF] Kahl | Graph transformation with symbolic attributes via monadic coalgebra homomorphisms[END_REF]: the argument type of each operation symbol is a single sort, and the result type is a term in a language of functor symbols (here including the constant symbol L and the unary List functor symbol) over the sorts (as variables).

Directed Hypergraphs -Simplified

To proceed towards capturing the full term graph structure and reduce adhoc notations, we now switch to using Agda [START_REF] Norell | Towards a Practical Programming Language Based on Dependent Type Theory[END_REF] as our mathematical notation. The following Agda record type definition defines the type DHG 00 to be the type of tuples containing the four sets1 Input, Output, Inner, and Edge, together with the five functions gOut, eOut, eArity, eLabel, and eIn. The choice to have separate functions for assigning each edge its arity (number of edge input positions), its label, and its actual input node sequence has been made to introduce the right kind of problems for discussion in the current paper. Different input positions need to be associated with different nodes -for simplicity, we identify input positions and input nodes, and introduce a separate carrier set for "inner" nodes, that is, nodes that are not input nodes. Both input nodes and inner nodes can be used as edge inputs, so we introduce the abbreviation 2 "Node" for the set of all nodes, constructed as the disjoint sum of the input node set and the inner node set: This models directed hypergraphs with input and output interfaces, but not yet term graphs where eOut needs to be bijective -we will come back to that only in Sect. 11. Dealing with directed hypergraphs is motivated by the fact that we use them as setting for double-pushout (DPO) rewriting of term graphsdirected hypergraphs include the "term graphs with holes" that occur as gluing and host graphs in DPO rewriting steps.

The DHG 00 record type declaration corresponds again to a coalgebraic signature in the sense explained above, after expanding the Node abbreviation, as can be seen in the following reformulation: 4 Interface-Parameterised Directed Hypergraphs

We will need to implement several operations on our directed hypergraphs, in particular sequential composition: If the set of output positions of G 1 coincides with the set of input positions of G 2 , then their sequential composition G 1 G 2 results from "gluing them together" along this common interface. Since we want type-checking to guarantee well-definedness of any applications of we use in programs manipulating term graphs, the input and output interfaces need to be part of the type of G 1 and G 2 . In Agda, this is achieved by making the record type parameterised:

record DHG02 (Input ∶ Set) (Output ∶ Set) ∶ Set1 where field Inner ∶ Set --set of inner (non-input) nodes Edge ∶ Set --set of edges field gOut ∶ Output → Input ⊎ Inner --graph output assignment eOut ∶ Edge → Inner --edge output node eArity ∶ Edge → N --edge arity eLabel ∶ Edge → Label00 --edge label eIn ∶ Edge → List (Input ⊎ Inner) --edge input nodes
(Mathematically, this corresponds to defining a functor from trivial two-sort coalgebras to coalgebras of shape DHG 01 .)

Implemented Directed Hypergraphs

So far, the record types we defined are mathematical datatypes, with sets as components, exactly in the way used for mathematical studies of term graphs. Since we used Agda as our mathematical language, and Agda can be used as a proof checker, we can build a mathematical theory of directed hypergraphs and term graphs on top of these definitions. However, since Agda is also a programming language, we would like to also use our definitions for data structures used in programs that manipulate term graphs. However, records containing Set fields are hard to use -how do you save one of those to a file? The field Edge could be a set of functions. . .

To come from the opposite perspective, consider now what a plausible implementation datatype for directed hypergraphs might look like. We present a "proof-of-concept" implementation based on arrays, using the Vec datatype constructor for dependently-typed vectors from the Agda standard library (Danielsson et al., 2018) -the type "Vec A n" is the type of n-element vectors with elements of type A. (A "production" implementation might for example use some kind of binary trees, or a type of arrays with constant-time access.)

A plausible design is then to use as carrier sets only sets constructed by Fin; for a natural number n, the type "Fin n" is the type of natural numbers less than n. The elements of "Fin n" are precisely the indices that can be used with vectors of type "Vec A n".

However, where the mathamatical data structure contains Sets of size n, the implementation data structure will contain only the index n:

record VecDHG1 (input ∶ N) (output ∶ N) ∶ Set1 where field inner ∶ N edge ∶ N field gOut ∶ Vec (Fin input ⊎ Fin inner) output eOut ∶ Vec (Fin inner) edge eArity ∶ Vec N edge eLabel ∶ Vec Label00 edge eIn ∶ Vec (List (Fin input ⊎ Fin inner)) edge
It is straight-forward to write a function that maps each element of "VecDHG 1 m n" to the mathematical representation of that graph in the type "DHG 02 (Fin m) (Fin n)", and this would populate also the Inner and Edge fields with Fin types. However, it is quite combersome to attempt to define even a partial inverse to that, which makes it essentially infeasible to use operations defined on the "mathematical implementation" DHG 02 to induce operations on the "executable implementation" VecDHG 1 . Perhaps more importantly, there is no good way to "obtain" the definition of VecDHG 1 "from" that of DHG 02 , or even more generally, to adapt DHG 02 to finite node and edge sets -one could do this via an extension that adds finiteness proofs. But using this approach to restrict DHG 02 s to those having node and edge sets of shape "Fin n" would involve a type-level propositional equality that would be extremely awkward to use.

The solution to this problem is to obtain both as instances of a generalised, abstract definition, with essentially the goal of being able to instantiate with Set and → to obtain the mathematical theory, and instantiate with N and flip Vec to obtain the desired implementation. After putting it this way, the natural option is to use a category as parameter.

Abstract Directed Hypergraphs -First Attempt

We now assume that we are in a setting where C is an arbitrary but fixed category with coproducts -the Agda way of expressing this is to locate the development in a parameterised module (with additional parameters for ListF etc.): We shall use the name vecCategory for the category with natural numbers as objects, and where the type of morphisms from m to n is "Vec (Fin n) m"; the coproduct there is just addition.

module (C ∶ Category) (hasCoproduct ∶ HasCoproducts C) [. . . ]
Trying to instantiate C with vecCategory presents the problem that that even if objN and ListF are supplied as module parameters in [. . . ], we will not find any n such that Fin n represents N respectively List (Input ⊞ Inner). (For the sake of the argument, we will ignore the option to restrict to some maximal arity that might be sufficient for some particular application.)

Abstract Directed Hypergraphs -Second Attempt

The solution to this problem is to make use of the type discipline of a coalgebra: Only sorts occur as argument types; infinite types like N and List (Input ⊞ Inner) only occur in the result types. We translate this into a setting where we do not need morphisms starting from all types -we embed the parameter C (that we plan to instantiate with vecCategory), used for the morphisms between all relevant finite sets, including the carrier sets, in a semigroupoid3 S that provides objects also for N and List (Input ⊞ Inner).

The semigroupoid S will need to have morphisms from objects of C to the object objN implementing N, and in the context of our implementation, these can all be implemented as vectors of the types "Vec N k" for natural numbers k. However, S does not need any morphisms starting at objN, so we can characterise S in a way that precisely fits this vector-based implementation: Vectors can contain elements of infinite types, but vectors cannot be infinite.

The (full and faithful, coproduct-preserving, . . . ) semigroupoid functor F embedding C in S becomes another important part of the setting we now adopt:

module (C ∶ Category) (hasCoproduct ∶ HasCoproducts C) (S ∶ Semigroupoid) (F ∶ SGFunctor ′ C S) (objN ∶ S.Obj) (ListF ∶ SGFunctor S S) [. . . ] where
Functions "between sorts", here gOut and eOut, are now morphisms in the parameter category C, while functions from a sort to an "arbitrary" (potentially infinite) type are morphisms in the parameter semigroupoid S, starting from the F-image of the sort. Instantiating C with the category Set and S with the underlying semigroupoid makes the resulting ADHG 1 directly equivalent with DHG 02 . Instantiating C with vecCategory and S with a carefully constructed semigroupoid (S F in appendix B) with arbitrary vectors as morphisms resulting ADHG 1 directly equivalent with VecDHG 1 .

Other easy instantiations are useful, too: For example, instantiating C with the category of all finite sets and S with the semigroupoid of all sets gives us the variant of DHG 02 restricted to finite carrier sets.

Directed Hypergraphs -Dependently Typed

A different issue with DHG 02 is the fact that the types do not enforce that the length of an edge's input node list corresponds to its arity: In terms of DHG 02 , we want to add the following restriction:

∀ (e ∶ Edge) → eArity e ≡ length (eIn e)

It would be possible to add this in the spirit of datatype invariants as the type of an additional field to the record, which then induces a proof obligation at every record construction site. Therefore it is far more attractive to move this invariant into the type system, which is possible in Agda due to its support for dependent types: A dependent function type "(e ∶ Edge) → R e" contains functions mapping each e ∶ Edge to an element of type "R e", where R ∶ Edge → Set is assumed to be some "result" type constructor depending on an Edge argument.

We use the additional expressivity provided by dependent types to move from List to Vec in the result type of eIn, and for each result vector we supply the arity of the edge in question as length: At the same time, we also switched the type of edge labels to come from an arity-indexed label set Label 1 ∶ N → Set.

Although this is not anymore of the shape of a coalgebra signature as described in Sect. 2, this is still a type of coalgebras mathematically, due to the fact that the dependent arguments are used only as arguments to other operations.

Implementation of Dependently-Typed Fields

The implementation type VecDHG 1 is easily adapted to such dependent fields, exploiting the presence of dependent pair types (Σ-types): The type "Σ a ∶ A • B a" is inhabited by pairs "a , b" where a ∶ A and b ∶ B a (where B ∶ A → Set is a type constructor taking an argument of type A).

Straight-forwardly embedding the type constructors for labels and input vectors in Σ-types yields the following refined implementation type:

record VecDHG2 (input ∶ N) (output ∶ N) ∶ Set1 where field inner ∶ N edge ∶ N field gOut ∶ Vec (Fin input ⊎ Fin inner) output eOut ∶ Vec (Fin inner) edge eArity ∶ Vec N edge eLabel ∶ Vec (Σ n ∶ N • Label01 n) edge eIn ∶ Vec (Σ n ∶ N • Vec (Fin input ⊎ Fin inner) n) edge
Such structures will then be subject to the following datatype invariants:

∀ (e ∶ Edge) → fst (lookup e eLabel) ≡ eArity e ∀ (e ∶ Edge) → fst (lookup e eIn) ≡ eArity e A more rational implementation (which can easily be obtained by a systematic transformation from VecDHG 2 ) would store these three equal values only once, and at the same time also be closer to directly representing the functor underlying the coalgebra type here:

record VecDHG3 (input ∶ N) (output ∶ N) ∶ Set1 where field inner ∶ N edge ∶ N field gOut ∶ Vec (Fin input ⊎ Fin inner) output eOut ∶ Vec (Fin inner) edge eInfo ∶ Vec (Σ n ∶ N • Label01 n × Vec (Fin input ⊎ Fin inner) n) edge
10 Dependently-Typed Abstract Directed Hypergraphs

For abstracting dependently-typed operations into the category-semigroupoid setting of Sect. 7, we introduce an minimal interface to dependent objects that can be seen as individual building blocks of a type-category as described by [START_REF] Pitts | Categorical logic[END_REF], adapted so that it "does not demand existence of too many morphisms" for our semigroupoid:

Definition 10.1 For an object I of S, an object D of S is a dependent object indexed over I iff for every object Y ∶ C.Obj and every morphism f from F Y to D in S there is a morphism ind D f from F Y to I in S such that the operation ind D commutes with C-pre-composition, that is, for every object X of C and every morphism g from X to Y in C, the following holds:

ind D (F g f) = F g ind D f
The Σ-types of Sect. 9 are an instance of dependent objects by virtue of implementing ind D f as (Vec.map proj 1 f), extracting the index from dependent pairs. The "trick" of dependent objects is that the dependent-pair-projection proj 1 used here does not need to be a morphism of the semigroupoid S, making it possible to define S in a way that all its morphisms can be implemented based on vectors.

For the abstract variant, we assume a dependent objects Label and a "dependent functor" VecF; the latter needs to map any object A of S to a dependent object with the common index objN. (The dependent functor image of a morphism f can be implemented as f itself tagged with a name of the functor, see appendix B.)

We introduce two new abbreviations, so that operation types now can be of the following three kinds (due to the coalgebra nature, all have to "conceptually start" at sorts, which are objects of C):

C.Mor X Y (straight morphisms in C) X A abbreviates S.Mor (F X) A, where X ∶ C.Obj and A ∶ S.Obj f D abbreviates Σ g ∶ X D • (ind D g = f), where f ∶ X I
That is, f D contains pairs of shape (g , p) where g ∶ X D and p is a proof for the morphism equality of ind D g with f.

For the instance VecDHG 2 , these proofs are exactly proofs for the datatype invariants mentioned there. The final abstract version of our directed hypergraph type therefore also starts closer to VecDHG 2 than to VecDHG 3 : While is essentially just a kind of "casting" that emphasises the "starting at a sort" intention, the type constructor is the real innovation here; thanks to , the presentation of ADHG 2 does not require local variable binders; therefore introduces the possibility of result type dependencies on the result of other operations into coalgebraic signatures while preserving the overall character of traditional signatures. (Technically, and can be considered as parts of a shallowly-embedded DSL for a novel kind of coalgebra signatures.)

Expanding definitions, we see that ELabel ∶ eArity Label from above is a dependent pair of type Σ g ∶ Edge Label • (ind Label g = eArity); for convenience, we give individual names to the two constitutents of this pair, which then have the following types, the second of which corresponds to the first datatype invariant in Sect. 9 (where fst implements ind Label ).

eLabel

∶ Edge Label eLabel-ind ∶ ind Label eLabel = eArity

GS-Monoidal Categories of Abstract Term Graphs

The definition of abstract directed hypergraphs we actually use also has the Node definition again, and therefore is even more readable: As mentioned in Sect. 2, we are really interested in jungles, which are directed hypergraphs with a one-to-one correspondence between edges and inner nodes established by eOut. Since we need directed hypergraphs as common substrate for an adapted kind of double-pushout term graph rewriting, we define jungles separately as "ADHG 3 s where eOut is an isomorphism in C", in Agda:

record AJungle (m n ∶ C.Obj) ∶ Set where field dhg ∶ ADHG3 m n open ADHG3 dhg
--bringing Inner, Edge, eOut, etc. into scope field eOutIsIso ∶ C.IsIso eOut eOut -1 ∶ C.Mor Inner Edge --providing a nice name for the inverse eOut -1 = eOutIsIso C.IsIso. -1

The full setting used as context for this includes a few properties not yet mentioned in Sect. 7; it consists of the following items:

-A category C intended to have (representations of) all possible carrier sets as objects, and (representations of) functions between these as morphisms.

C needs to have coproducts, a terminal object, and a strict initial object. -A semigroupoid S intended to have (representations of) all possible value sets (including label sets, N, vector sets) as objects.

S is only required to contain the morphisms associated with the additional structure below; it can be quite "sparse". -A full and faithful semigroupoid functor F from the semigroupoid underlying C to S that preserves identity morphisms, coproducts, and initial objects. This functor is understood as embedding C into S. -Specifically as setting for the ADHG definitions, a natural number object objN, an objN-indexed dependent object Label, and an objN-indexed dependent functor VecF for vectors satisfying an appropriate vector specification. In this setting, we have implemented large parts of the theory of gs-monoidal categories introduced by Corradini and Gadducci (1999): For term graphs, monoidal composition ⊗ is "parallel composition" that "concatenates" (via coproduct) the input and output interfaces; gs-monoidal categories are monoidal categories with additional transformations ! and ∇: -! A ∶ A → 1l is the terminator and introduces garbage, and -∇ A ∶ A → (A ⊗ A) is the duplicator and introduces sharing. These are present also in cartesian categories such as Lawvere theories, and there they are natural transformations. In gs-monoidal categories they do not need to be natural, which is important for term graphs, where garbage and sharing make a difference.

We have implemented (Zhao, 2018a,b) Agda-verified gs-monoidal categories with ADHGs respectively Jungles as morphisms fully at the abstract level in the category-semigroupoid setting described above. We also implemented Jungle decomposition and proved it correct, which is the core of the result of [START_REF] Corradini | An algebraic presentation of term graphs, via gsmonoidal categories[END_REF] that that term graphs (i.e., jungles) form a free gs-monoidal category. For this part, we followed Corradini and Gadducci's set-up, which specialises C.obj to N, interpreting n ∶ N as the type Fin n -this is justified by the fact that there will be a forgetful functor from every practically useful gsmonoidal category mapping the object monoid to N, and this functor will reflect decomposition. We used this specialisation for decomposition of wiring graphs (which have no edges); apart from that, we elaborated the proofs at the abstract category-semigroupoid level as far as we found feasible. An improved library of dependent functors will make fully abstract proofs possible in the future. We also started to develop a rewriting mechanism for these Jungles via constrained DPO rewriting steps in the category of ADHG matchings, see [START_REF] Kahl | Dependently-typed formalisation of typed term graphs[END_REF].

Conclusion

An important observation arising from the development of our ADHG formalisations is that categorial abstraction is frequently enhanced by embedding a "nice" category in a "big" semigroupoid. Careful choices then allow us to develop theory and implementations at the abstract level, and obtain the conventional Set-based mathematical theory as one instantiation, while correct-by-construction executables can be generated via instantiations with concrete datatypes. In this way, we achieve re-usability of theoretical developments as implementations that are tunable for efficiency.

A Representation Contexts

We now provide a more fine-grained abstraction for the category-semigroupoid setting of Sections 7 and 11. Recall that the key idea is to provide a separate interface, the category C, for objects that can be used as carriers of coalgebra sorts, and "extend" this category to an encompassing semigroupoid S that can contain also other objects that may be used to interpret the result type expressions of coalgebra function symbols. For example, the (conceptually) infinite datatype String will never be used as node set of a graph, but it may well be used for node labels. In addition, a type of "representations" for S-morphisms that "start at C-objects" is assumed -these are the morphisms that may serve as interpretations of coalgebra function symbols. The "upwards arrows" are motivated by visualising the the semigroupoid S above the category C, which is "embedded" into S via R.

S k ,B (U ↗ g) = (S k ,A U ) . , g for U ∶ k ⇗ A, and g ∶ A → B in S S -1 k ,B (f . , g) = (S -1 k ,A f ) ↗ g for f ∶ R k → A and g ∶ A → B in S R f = S k ,R m (R k ,m f ) for f ∶ k → m in C
The implementation setting described in Sect. 7 for obtaining VecDHG 1 from ADHG 1 can be explained as a representation context where -C has N as object collection, and Fin m → Fin n as homset from m to n; -S is the semigroupoid underlying Set; -R ∶ C → S maps n ∶ N to the set Fin n, and is the identity on morphisms;

for each k ∶ N and each set A, the type of representations is k ⇗ A = Vec A k , and S k ,A is the canonical isomorphism between Vec A k and Fin k → A; for each k , m ∶ N, the canonical isomorphism between Fin k → Fin m and Vec (Fin m) k is used as R k ,m ; for each vector U ∶ Vec A k and each Set-morphism g ∶ A → B , the composition is U ↗ g = mapVec g U . Note that there are "more" vectors than there are morphisms in C, and yet more set functions in S than there are vectors.

Theoretically, one could choose to identify k ⇗ A with the S-homset R k → A, but we consider it useful to keep the two separate: The point of having ⇗ as a separate component of representation contexts is that it can be instantiated with morphism implementations for which S provides the semantics in terms of the semigroupoid S, which in turn is intended to provide the connection to Set.

For interpretation of coalgebra signatures (as shown in Sect. 2), we assume a fixed interpretation function F that maps n-ary functor symbols to semigroupoid functors from S n to S that preserve identities (and correspond to meet-preserving relators). If a structure A provides an interpretation of sort symbols as objects in C, then let t A be the resulting interpretation of the type expression t, where each sort s is interpreted as s A = R s A , and functor symbol applications are interpreted as the corresponding functor applications:

F (t 1 , . . . , t n ) A = (F F )( t 1 A , . . . , t n A )
For each type expression T , this gives rise to an identity-preserving semigroupoid functor, written t , from the sort-indexed product category C Sort Σ to S. Definition A.2 Let a coalgebraic signature Σ and a representation context X = (C, S, R, ⇗, S, R, ↗) be given. A Σ-X -coalgebra A consists of for each sort s an object s

A of C -for each function symbol f ∶ s → t a representation f A ∶ s A ⇗ t A Given two such coalgebras A and B , a Σ-X -coalgebra homomorphism φ from A to B consists of -for each sort s a representation φ S ∶ s A ⇗ (R s B ) of the C morphism (R -1 s A ,s B φ S ) ∶ s A → s B ,
such that for each function symbol f ∶ s → t, the following homomorphism property holds:

f A ↗ t (R -1 φ) = φ s ↗ (S s B , t B f B )
This homomorphism property is an equality of representations; in concrete applications this will be a decidable equivalence.

It is easy to see that the Σ-X -coalgebra homomorphisms of Def. A.2 form a category; this is a "good implementation" of Σ-coalgebras in the following sense: Theorem A.3 Let a coalgebraic signature Σ, and a representation context X = (C, Set, R, ⇗, S, R, ↗) using the full category Set for S be given. For each Σ-X -coalgebra A, applying R to each carrier object s A , and applying S to each function symbol interpretation f A maps the Σ-X -coalgebra A to a conventional Set-based coalgebra in a way that gives rise to a full and faithful functor.

In the setting of Sect. 7, the category of Σ-X -coalgebras is therefore equivalent to the subcategory of Σ-coalgebras over Set which results from restriction to finite carrier sets.

B Concretised Representation Context

For an implementation based on, for example, the vectors of Sect. 5, the question arises how to represent not only the components of coalgebras and of morphisms, both of which are representations, but also the results of functor application to morphisms, which are used in the context of the dependent functors mentioned in Sect. 10.

We now assume a language F of functor symbols (with arity). Our goal is to move from an abstract semigroupoid S, such as Set, to one that has a concrete representation amenable to implementation using finite datastructures. (Objects of Set, as far as relevant in this context, are considered to be implemented as datatype identifiers or type expressions.)

Given a representation context X = (C, S, R, ⇗, S, R, ↗) and a functor symbol semantics that maps each functor symbol F ∶ F to a semigroupoid endofunctor F (of corresponding arity) on S, we construct a new concretised representation context X F = (C, S F , R F , ⇗ F , S F , R F , ↗ F ) over the same base category C, where: -A S F object is

• either LIFT k for a C object k ,

• or EMBED A for an S object A,

• or WRAP F (Q 1 , . . . , Q n ) for an n-ary functor symbol F and S F objects Q 1 , . . . , Q n . S F objects are assigned a straightforward "semantics" as S objects:

LIFT k = R k EMBED A = A WRAP F (Q 1 , . . . , Q n ) = F ( Q 1 , . . . , Q n ) -S F morphisms are • either S F k ,Q U ∶ LIFT k → Q for a representation U ∶ k ⇗ F Q, which is a representation in k ⇗ Q , • or MAP F (g 1 , . . . , g n ) ∶ WRAP F (Q 1 , . . . , Q n ) → WRAP F (P 1 , . . . , P n )
for an n-ary functor symbol F and morphisms g i ∶ Q i → P i .

(There are no morphisms starting from EMBED objects.) Morphisms are also given a straightforward semantics in S. -R F , the composition . , F in S F , and the composition ↗ F are determined by the semantics; R F is induced by LIFT.

X F is a well-defined representation context, and if R preserves finite colimits, so does R F . Note that S F is only a semigroupoid, and cannot be a category, since there are no morphisms starting at EMBED objects, not even identity morphisms. This fact is the motivation for asking only for a semigroupoid in this place in a representation context.

For signatures Σ over the functors in F, the concretised representation context X F generates the same Σ-coalgebras as the (possibly abstract) context X , but extends the concretely implementable morphisms to "exactly all morphisms ever required while reasoning about Σ-coalgebra transformation".

Theorem B.1 The category of Σ-X F -coalgebras is equivalent to the subcategory of the corresponding category of Σ-coalgebras in S restricted to carriers in C.

  record DHG1 (Input ∶ Set) (Output ∶ Set) ∶ Set1 where field Inner ∶ Set --set of inner (non-input) nodes Edge ∶ Set --set of edges Node = Input ⊎ Inner --set of all nodes field gOut ∶ Output → Input ⊎ Inner --graph output assignment eOut ∶ Edge → Inner --edge output node eArity ∶ Edge → N --edge arity eLabel ∶ (e ∶ Edge) → Label1 (eArity e) --edge label eIn ∶ (e ∶ Edge) → Vec Node (eArity e) --edge input nodes

  module [. . . ] (objN ∶ S.Obj) (Label ∶ DepObj objN) (VecF ∶ DepFunctor objN) [. . . ] where [. . . ] record ADHG2 (Input ∶ C.Obj) (Output ∶ C.Obj) ∶ Set where field Inner Edge ∶ C.Obj field gOut ∶ C.Mor Output (Input ⊞ Inner) eOut ∶ C.Mor Edge Inner eArity ∶ Edge objN ELabel ∶ eArity Label EIn ∶ eArity VecF (F (Input ⊞ Inner))

  module [. . . ] (objN ∶ S.Obj) (Label ∶ DepObj objN) (VecF ∶ DepFunctor objN) [. . . ] where [. . . ] record ADHG3 (Input ∶ C.Obj) (Output ∶ C.Obj) ∶ Set where field Inner Edge ∶ C.Obj Node = Input ⊞ Inner field gOut ∶ C.Mor Output Node eOut ∶ C.Mor Edge Inner eArity ∶ Edge objN ELabel ∶ eArity Label EIn ∶ eArity VecF (F Node)

  Definition A.1 A representation context X = (C, S, R, ⇗, S, R, ↗) consists of a category C a semigroupoid S a full and faithful semigroupoid functor R ∶ C → S that preserves identities for each object k of C and each object A of S, a collection k ⇗ A of representations, together with a bijection S k ,A between k ⇗ A and the S-homset R k → A, for any two objects k and m of C, a bijection R k ,m between the C-homset k → m and k ⇗ R m, and for each representation U ∶ k ⇗ A and each S-morphism g ∶ A → B a composition U ↗ g in k ⇗ B such that the following are satisfied:

  where [. . . ] --bring _⊞_ and other useful material into scope. . . Then occurrences of Set in DHG 02 are replaced with the type of objects of category C, and operations become morphisms instead of functions:

	record ADHG0 (Input ∶ C.Obj) (Output ∶ C.Obj) ∶ Set where
	field Inner ∶ C.Obj	--inner (non-input) nodes
	Edge ∶ C.Obj	--edges
	field gOut ∶ C.Mor Output (Input ⊞ Inner) --graph output assignment
	eOut ∶ C.Mor Edge Inner	--edge output node
	eArity ∶ C.Mor Edge objN	--edge arity
	eLabel ∶ C.Mor Edge Label10	--edge label
	eIn	∶ C.

Mor Edge (ListF (Input ⊞ Inner)) --edge input nodes

We gloss over the fact that in any real Agda development of these mathematical definitions, Setoid types will normally be used instead of Set. A variant using setoids of the definitions of the current section can be found in(Kahl,

2011, Sect. 3).2 Agda record declarations simultaneously define modules, and as such can contain other definitions besides field declarations.

A semigroupoid is a "category without identity morphisms", analogous to how a semigroup is a "monoid without identity element".