Daouda Diakite

Maxime Martelli

Nicolas Gac

An OpenCL pipeline implementation on Intel FPGA for 3D backprojection

Keywords: Algorithm architecture co-design, Intel FPGA SDK for OpenCL, hardware acceleration, FPGA, Computed Tomography

To accelerate the time-consuming 3D backprojection used by CT reconstruction algorithms, hardware accelerators are needed. Since 2007, GPU is by far the main one. In this article, we propose a pipeline implementation of the 3D back-projection algorithm on a high-end FPGA using Intel FPGA SDK for OpenCL while presenting some optimization metrics for task parallelism. Compared to a non-optimized version on Arria 10, we achieved a speedup of 23 regarding execution time, by applying these techniques correctly. We then compared these results with a low-end FPGA, CPU, and GPU in terms of execution time and energy efficiency.

I. Introduction

P Rogrammable Gate Arrays (FPGAs) is becoming an attractive technology for High-Performance Computing thanks to increasing floating-point computation power and High-Level Synthesis (HLS) tools becoming more and more mature. These tools allow developers to generate a hardware implementation on FPGAs using software programming languages like C, C++, or OpenCL. One of the promises of those tools is to make FPGA development accessible by software engineers. Like GPUs or multi-core CPUs, FPGAs are often considered and included in heterogeneous systems, to speed up timeconsuming applications. One main advantage is also to be more energy-efficient compared to GPUs and CPUs. Some recent work focused on explorations of HLS tools efficiency includes [START_REF] Martelli | 3D Tomography back-projection parallelization on Intel FPGAs using OpenCL[END_REF], [START_REF] Purkayastha | Exploring the efficiency of OpenCL pipe for hiding memory latency on cloud FPGAs[END_REF], [START_REF] Hc | FPGA accelerated PET image reconstruction[END_REF] for Intel OpenCL SDK, or [START_REF] Ravi | FPGA as a hardware accelerator for computation intensive mlem medical image reconstruction[END_REF], [START_REF] Siddiqui | FPGA-based processor acceleration for image processing applications[END_REF] for Xilinx Vivado HLS. In particular, [START_REF] Mansoori | Efficient FPGA implementation of PCA algorithm for large data using hls[END_REF] presented an OpenCL implementation that was better than a Verilog/VHDL design in terms of frequency, latency, and resource utilization. The authors of [START_REF] Purkayastha | LLVM-based automation of memory decoupling for OpenCL applications on FPGAs[END_REF] proposed a novel method that separates memory access from computation for OpenCL kernels based on a Low-Level Virtual Machine (LLVM) compiler. The authors of [START_REF] Knaust | OpenMP to FPGA offloading prototype using OpenCL SDK[END_REF] use OpenMP to generate OpenCL code from a higher abstraction level, which is then synthesized by OpenCL SDK for bitstream generation. These works underline the interest for FPGAs in the High-Performance Computing (HPC) field.

In the past years, FPGAs for Computed Tomography (CT) were configured with Hardware Description Language (HDL) [START_REF] Gac | High Speed 3D Tomography on CPU, GPU, and FPGA[END_REF], [START_REF] Pfanner | High performance parallel backprojection on FPGA[END_REF], [START_REF] Leeser | Parallel-beam backprojection: an FPGA implementation optimized for medical imaging[END_REF], [START_REF] Kim | Forward-Projection Architecture for Fast Iterative Image Reconstruction in CT[END_REF], where the goal was to model a pipeline (from the algorithm) and perform a voxel update at every clock cycle. The main concern of the HDL implementation is the very long development time, even though the results were significant in terms of execution time. More recently, new approaches based on HLS tools for FPGAs were developed, to obtain better reconstruction times and energy efficiency while accelerating development time. One such work proposed a hardware acceleration based-FPGA of the Maximum Likelihood Expectation Maximization (MLEM) algorithm [START_REF] Ravi | FPGA as a hardware accelerator for computation intensive mlem medical image reconstruction[END_REF] and achieved a significant acceleration in execution time compared to an optimized CPU multi-core version.

FPGAs are reconfigurable, and this allows programmers to have a better algorithm architecture adequacy, by leveraging data or task parallelism. Furthermore, tools included in the Intel FPGA SDK for OpenCL enable a developer to implement a wide range of optimizations quickly but give less control compared to the traditional HDL approach.

In this paper, we propose a pipeline implementation of the 3D back-projection algorithm based on the Reflex Attila Arria 10 device, using Intel FPGA SDK for OpenCL 18.1. From a first implementation of this CT algorithm on a low-end DE1-SoC board [START_REF] Martelli | 3D Tomography back-projection parallelization on Intel FPGAs using OpenCL[END_REF], we show in this paper, the benefits of using a higher-end FPGA and explore new optimization possibilities based on task parallelism.

The remainder of this paper is organized as follows: in Section II, we present the back-projection algorithm. Section III introduces some OpenCL metrics relevant to pipeline parallelism, and Section IV details different optimization techniques. The results are discussed in section V, and we conclude this work.

II. 3D computed tomography reconstruction

3D tomography used in medical imaging or nondestructive testing (NDT) aims to acquire the internal structure of 3D objects from external measurements. As illustrated in Fig. 1, an X-ray source and an array of detectors are rotating around the object (3D volume). The radiation emitted from the source is attenuated depending on the object's local density. A sinogram is created by stacking all of the measured attenuations from the detectors acquired at different angles.

The 3D back-projection described in detail in [START_REF] Gac | High Speed 3D Tomography on CPU, GPU, and FPGA[END_REF] algorithm is given by

d(c) = S CT (u(ϕ, c), v(ϕ, c), ϕ).w(ϕ, c) 2 dϕ
u(ϕ, c) = x * cos(ϕ) + y * sin(ϕ) v(ϕ, c) = x * sin(sinϕ) -y * cos(ϕ) + z
As the distribution of the sensor is discrete, the integral transforms in a sum for all ϕ values. This algorithm is particularly suited for SIMD cores, because this sum has to be computed for every voxel of the object, and is best executed on massively parallel architectures. However, one way to accelerate our algorithm is to make use of coalesced memory access patterns, also referred to as memory coalescing. Many times, memory objects are retrieved in large blocks and cached in smaller but faster caches.

III. OpenCL metrics for pipeline

characterization For a given program, instead of having to transform the source code into instructions that depend on the target processor, High-level tools will create an architecture made of elementary blocks for each algorithm. Figure 2 represents a computation architecture that corresponds to the calculation of u and v coordinates for the 3D backprojector. All data goes through the pipeline, and we can see that a new iteration starts every two clock cycles with a pipeline depth of 5 due to data dependency. The overall efficiency of this generated hardware is only 50% in theory.

Three main metrics characterize a pipeline. First, the Initiation Interval (II) represents the number of clock cycles between the launch of consecutive loop iterations. It means that one loop iteration is launched every II hardware clock cycles. The ideal II value is 1, and the offline compiler attempts to achieve that value for a given loop whenever possible, and it is achieved when dependency is absent or handled in one cycle. In most cases, internal iteration dependencies causes poor II value and it can be fixed with some optimization techniques, like shift register pattern. Secondly, the Pipeline depth (P) is the number of cycles required by one data to pass through the Fig. 2: Pipeline fragmentation of a function on FPGA entire calculation pipeline, i.e. the number of stages of the pipeline. For a given amount of iterations n, the global cycle number of a pipeline can be computed with those two metrics: cycles = P + II(n -1). By adding a third metric, the operating frequency (F), it is possible to compute the execution time of a pipeline, as given here:

T = P +II(n-1) F .
Optimizing an OpenCL implementation is finding a balance between those three metrics.

IV. Pipeline parallelism

OpenCL on FPGA supports data-parallel (NDRange) as well as task parallel (Single Work Item) programming models, and this makes FPGAs useful for a wide range of applications.

NDRange kernel is the GPU-like data-parallel computing model on FPGAs using OpenCL, which aims to perform the same set of instructions on multiple elements of a memory object. Each instance of execution is called work-item, which are grouped in work-group. In [START_REF] Martelli | 3D Tomography back-projection parallelization on Intel FPGAs using OpenCL[END_REF] we performed an NDRange implementation of 3D backprojection and presented the OpenCL memory architecture as well as the impact of their utilization. Fig. 3: Back-projection algorithm pipeline architecture As Intel FPGA SDK for OpenCL allows both data and task (pipeline) parallelism, the choice of a type of parallelism, based on the application, requires adequate knowledge of both the application specificity and the tools. In our case, since FPGA resources do not allow massive data parallelism, we chose the pipeline parallelism approach to implement the 3D back-projection algorithm. Even before HLS tools, FPGAs were well known for their deep and efficient pipeline execution pattern, resulting in good performances and low latency. For instance, in computed tomography, a highly efficient hardware architecture for forward projection in Computed Tomography based on Xilinx Virtex-5 FPGA was proposed in [START_REF] Kim | Forward-Projection Architecture for Fast Iterative Image Reconstruction in CT[END_REF] using a floating-point to fixed-point conversion and a two-level memory, for separable-footprint (SF) forward-projector. Some OpenCL optimization techniques were presented in previous work [START_REF] Martelli | 3D Tomography back-projection parallelization on Intel FPGAs using OpenCL[END_REF], such as memory architecture and memory pre-fetching, as well as the difference between NDRange kernel and Single Work Item (SWI) kernel.

Here, we will present other SWI optimizations based. The 3D back-projector is divided into several pipeline stages as shown in Fig. 3, which correspond to the crucial steps of the algorithm, this function level pipelining and each block can be split at loop level.

Fig. 4: Loop unroll versus loop pipeline

A. Loop pipelining

In SWI design, the offline compiler automatically tries to pipeline all the loops in the kernel. The idea is to split the body of the loop in a succession of micro-operations that can execute concurrently. The advantage is that the pipelined loop can launch a new iteration at every clock cycle by using the same hardware resources as the traditional sequential one but with better performances.

On FPGAs, the loop pipeline is the best solution in terms of resources and performance ratio. However, an efficient pipeline must not stall which means it has to perform an ideal initiation interval.

In certain rare cases, achieving an II value of 1 might lower the kernel maximum operating frequency, therefore lead to poor performances; for such a loop, it is more convenient to use the ii pragma to fix the II value that performs the best frequency. It is also possible to fix the maximum operating frequency by using the F max attribute or by including it in the aoc command at compile time. However, if the offline compiler cannot meet all the constraint bitstream generation will be impossible.

B. Loop unrolling

Another loop optimization is the unrolling, which consists of replicating, with a configurable factor, the body of the loop. Unlike pipelining, unrolling also replicates hardware resources, which by the way, maximize memory bandwidth utilization i.e maximally unrolling the most nested loop increases the amount of memory access per iteration; this is because the unrolled loop is closest to the computation. A loop can be fully or partially unrolled depending on the available logic element or the size of the cache memory (if applicable), the cache misses will increase if it cannot deliver all the data needed for computation.

V. Results and discussion

We used for this work the FPGA Attila Arria 10 device, which offers 8 GB of DDR4 memory and a maximum FPGA frequency of 405 MHz. The FPGA was in PCIe connection with the host system. The considered volume is a 256 3 voxel, with 256 angles variations. Each kernel execution is monitored through the Intel FPGA dynamic Profiler for OpenCL. For each kernel, this tool provides, amongst other things, the operating frequency, the execution time, the logic utilization, and the latency, bandwidth, and stall of most memory access. The coefficient α and β are stored in the local memory due to their size and their frequent solicitation for each detector coordinates calculation.

In SWI kernel, the loops are pipelined automatically; the challenge is to feed the loop in the most efficient way, which brings us back to the loop unrolling. For a nested loop algorithm, which loop to unroll and which unrolling factor have to be chosen. One way to get to achieve the finest granularity possible is first to unroll the most nested loop and gradually consider the rest of the loops as long as the hardware resources allow. Based on this, in our case, the loop to be unrolled is the ϕ. This unrolling does not mean that several voxels are updated by clock cycle but allows the accumulation of the sensor contributions to be accelerated according to the projection angles. However, our first implementation on Arria, in table I, is the CPU-like version FPGA-friendly implemented to get an efficient pipeline with ideal II value, and the unroll1 forces the compiler not to unroll the loop. The offline compiler achieves for this version an operating frequency of 196,97 Mhz with an execution time of 124,82 s. This is the result of under-utilization (only 24% of hardware resources In table I) of available resources on Arria 10 device. Therefore it does not take full advantage of the parallelism potential. Exceeding this frequency by applying the optimizations based on SWI, will be almost impossible as the depth of the pipeline will be variable according to the number of replication.

By replicating 16 times (unroll 16), we double the number of resources and get a 6.5 fold acceleration compared to the first version. We notice that the offline compiler sacrificed F max to achieve the II value of 1. The best execution time was obtained by a replication factor of 32 with 80% logic utilization at 150M hz. This version is the most optimal and takes advantage of the automatic cache mechanism. Having the same features of this version with a larger frequency, using F max attribute, was not possible for the offline compiler. It increased the number of constraints at the place and route time.

For this algorithm on Arria 10 device, the maximum possible replication factor is 40. Once greater than 40 we exceed 100% of the device capabilities. This version is suboptimal not only because of the low frequency, but because the number of iterations is not divisible by 40. There will be an epilogue to handle, which will substantially increase the depth of the pipeline and lead to poor performances. It is imperative, as far as possible, to know the number of iterations of a given loop at compile time to have a bitstream that best fit the algorithm.

A. FPGAs Arria 10 vs DE1-SoC

By comparing results shown in Table I with those obtained previously in [START_REF] Martelli | 3D Tomography back-projection parallelization on Intel FPGAs using OpenCL[END_REF], we observe that DE1-SoC SWI implementations were limited by its logical resources, as the tool was unable to generate an efficient pipeline kernel. Arria 10 implementations deliver better performance than both SWI and NDRange versions on DE1-SoC with 12.6 and 3.1 speedup respectively. It should be noted that interpolation was replaced by the nearest neighbor method on the DE1-SoC and the Arria 10 because it required more resources and computation. Besides, on DE1-SoC device the accumulation of a variable cost six clock cycle instead of one cycle for Arria 10. In terms of efficiency, the DE1-SoC is more efficient than the Arria 10 device when considering the number of logic elements.

B. FPGA, CPU, GPU

The GPUs are far ahead regarding performance (Table II), mostly thanks to their high core count and frequency, which makes them more suited for massive data-parallel computing. However, FPGA implementation provides better execution time than an optimized multi-core CPU version despite its low operating frequency. Overall, GPUs still consume less energy than FPGAs despite requiring more instantaneous power.

VI. Conclusions

In this work, we presented a pipeline implementation of a 3D back-projector on an Intel FPGA Arria 10. FPGA achieved better performance than CPU, but it does not perform as well as the optimized versions on GPUs. Considering the specifics of the FPGAs and metrics presented, the offline compiler can generate a pipeline architecture similar, however less effective, to those generated through HDL languages.

In SWI implementation, parallelism is to be extracted in the body of the function, and optimizations must be FPGA-centric to take full advantage of this architecture. The FPGA leading manufacturers recommend this approach, but if the application does not match this type of parallelism, it is a good idea to favor data parallelism. Tomography algorithms are better suited for massive data computing, which explains why GPUs are currently favored in this field.

To stand up to GPUs in tomography, FPGAs need to improve their ability to express data parallelism better, like having adapted memory buses or more DSP.

Fig. 1 :

 1 Fig. 1: 3D Computed Tomography

TABLE I

 I

	: Performances comparison between FPGAs Ar-
	ria 10 (764k LUTs) and DE1-SoC (118k LUTs)

TABLE II

 II

We would like to thank Daniel Charlet from the LAL (Orsay, France) for granting us access to an Arria 10 board.


published or not. The documents may come

Open data on beads, pendants, blanks from the Ceramic

Age Caribbean

Open data on beads, pendants, blanks from the Ceramic Age Caribbean The paper 'A database of lapidary artifacts in the Caribbean for the Ceramic Age' by Queffelec et al. [1] presents a description of a dataset of nearly 5000 lapidary artefacts from over 100 sites. The data are dominated by beads and pendants, which are mostly made from Diorite, Turquoise, Carnelian, Amethyst, and Serpentine. The raw material data is especially valuable as many of these are not locally available on the island. This holds great potential for exchange network analysis. The data may be especially useful for investigating one of the fundamental questions of this region: whether the Cedrosan and Huecan are separate, little related developments, with different origins, or variants or a single tradition [START_REF] Reed | A comparison of Huecan and Cedrosan Saladoid ceramics at the Trants site, Montserrat[END_REF].

Ben Marwick based on reviews by Clarissa Belardelli, Robert Bischoff, Stefano Costa and Li-Ying Wang

In addition to metric and technological details about the artefacts, the data include a variety of locational details, including coordinates, distance to coast, and altitude. This enables many opportunities for future spatial analysis and geostatistical modelling to understand human behaviours relating to ornament production, use, and discard. I recommend the authors make a minor revision to Table 1 (spatial coverage of the dataset) to make the column with the citations conform to the same citation style used in the rest of the text. I warmly commend the authors for making transparency and reproducibility a priority when preparing their manuscript. Their use of the R Markdown format for writing reproducible, dynamic documents [START_REF] Marwick | Computational Reproducibility in Archaeological Research: Basic Principles and a Case Study of Their Implementation[END_REF] is highly impressive. This is an excellent example for others in the international archaeological science community to follow. The paper is especially useful for researchers who are new to R and R Markdown because of the elegant and accessible way the authors document their research here.

[1] Queffelec, A., Fouéré, P. and Caverne, J.-B. 2021. A database of lapidary artifacts in the Caribbean for the Ceramic Age. SocArXiv, 7dq3b, ver. 4 Peer-reviewed and recommended by PCI Archaeology. https://doi.org/10.31235/osf.io/7dq3b

Open Access

Published: 28 February 2021

This manuscript is a most welcome announcement of a database of lapidary artifacts from the Ceramic period of the Caribbean islands. Open data such as presented here is essential for the sustainability of archaeology as a discipline and a community. I recognise the authors' impressive efforts to make this manuscript transparent and reproducible by writing in R Markdown. This has enabled the reviewers to identify some specific corrections necessary before we can recommend the article. The reviewers have also made many suggestions for improving the English text to make the text easier to understand. I request that the authors study the reviews and make all of the revisions requested (the reviewers often spot the same things, so this will not be a big task). Please also look into the suggestions to improve the text and make those changes (especially those made by Bischoff on the PDF he attached to his review). I believe that once these revisions are complete, we can recommend the article to the scholarly community.

Preprint DOI: 10.31235/osf.io/7dq3b

Reviewed by Clarissa Belardelli, 2020-12-13 16:20

I am going to articulate my review into three parts: 1. Scientific content 2. Bibliography, figure captions 3. Translation 1. Scientific content The paper is very good and the argument amazing. method is well conscructed; the overview maybe is not too vaste but there is a good bibliography. However something is not clear: P. 4: "Presently, the dataset of lapidary artifacts contains 0 entries, originating from 87 sites": so, how many entries does the dataset contain? P. 5: "We will thus describe only the English tables Islands, Sites and Beads. Each table also exists in French There are some minor mistakes. I noticed two of them but there could be more. Here, one: -P. 6: State specifies is (IF) the object is complete or broken To be corrected! Finally, the paper is good but needs some more attention.

Reviewed by Robert Bischoff, 2020-11-30 22:06

This paper describes a database of lapidary artifacts from the Ceramic period of the Caribbean islands. A brief background of the setting and cultural history is provided, as well as a discussion on prior lapidary research. The bulk of the paper is a description of the data collection methods, database structure, and repository locations. The description contains the necessary metadata to interpret and access the database (URLs are provided), including caveats regarding data quality and limitations. Many archaeologists and researchers in other disciplines have called for more open-access databases with appropriate metadata. This article and database answer that call and provide a large database with location data that should be useful for researchers in the Caribbean as well as researchers and educators looking for high-quality datasets. I would prefer to see a short case study demonstrating the potential this database has for providing new archaeological interpretations; however, the article as written merits recommendation with the addition of some minor revisions to the article and by addressing a few problems with the database. The strength of this paper is its clear description of the different elements of the database and how they fit together with enough detail to confidently use the database to address research questions. The tables and figures are helpful and of good quality. The inclusion of the Rmarkdown document is an excellent example of open source science, and I had no trouble reproducing it. This will be useful for anyone looking to adopt a similar format for their own work. The database itself is of good quality compared to many archaeological databases and contains a number of useful fields. The location data does not have any obvious errors. There are a few important issues that need to be addressed prior to a recommendation. The Islands table discussed in the text is not included in the OSF repository and has not been reviewed. I used the tables in the OSF repository to examine the database. I was not able to join all of the sites to the beads tables in English or French. I also tried using the IndexSite field to join to the first part of the IndexB field (I removed the three-digit numbers at the end of IndexB), but I found a similar problem to just using the Site field. This should be fixed prior to a recommendation. I suggest including the IndexSite field in the BEADS table as it will be easier to avoid problems with typos and will be a more stable key for joining tables. There are three rows in the BEADS and PERLES tables that are exact duplicates and should be removed (GR-01-044, GR-01-099, and GR-01-128). There are also several rows that are included in the BEADS table but missing in the French version called PERLES. Some of the terms in the English version have not been translated from French. For example, the same field has entries for "Bead-Pendant" and "Bead-pendentif." This will cause problems aggregating the data. There is one small problem I identified in the Rmarkdown document. The size of the database is calculated by the length of the IndexP field, but the English version is loaded which is called IndexB and results in a value of zero. Perhaps using nrow(Data) would be simpler. Some minor changes to language and phrasing in the article are suggested.

Download the review (PDF file)

Reviewed by Stefano Costa, 2020-12-18 15:00

This data paper describes an interesting and very wide-ranging dataset about a specific artifact category found in archaeological contexts across the Caribbean region. I can recommend its publication with some revisions described in the following review comments.

Section 1

Spatial coverage

Since the spatial distribution of sites is concentrated in the Eastern part of the Caribbean, with the exception of Jamaica and Bahamas, it seems useful to provide a more detailed description of the coverage beyond the geographic bounding box, perhaps including the names of smaller archipelago groups.

The authors mention that some islands did not yield any lapidary artifact, or at least none that we could find in the literature and I think it is important to give a list of what islands were investigated but yielded no results.

The map in figure 1 is a little confusing because some of the site IDs do not match those in the table or the sites listed in the table are not labeled on the map. It could be useful to draw the bounding box in the map, perhaps differentiating islands that are included in the dataset versus those that are not included.

Section 2 Steps

When the authors write that the dataset of lapidary artifacts contains 0 entries.

this must be corrected with the actual number, by changing the code snippet at line 86 of the PAAFdatapaper.Rmd source file from r length(Data$index_P) to r length(Data$index_B), which correctly gives 5011 entries.

Section 3 Dataset description

The ISLANDS and ILES tables are not included in the archived dataset at SocArXiv / OSF. These must be added for the dataset to be complete.

The dataset description is very detailed and well organised. There is a lot of potential for reuse and further analysis with the radiocarbon data, as published JOAD data papers have shown: I may suggest to split the Date_BP field in two separate fields, to have better error checking (it becomes two integer fields instead of a text field) and make it easier to reuse the information. If the field contains more than one date, perhaps a separate table could be added.

It is unclear why the dataset is described as CSV but the reproducible paper is based on the XLSX version, this could create unnecessary complexity and/or mismatch between different versions of the dataset.

The Filemaker server is useful for quick interaction and most importantly contains photographs and drawings. A reason for not including those in the archived dataset should be given, since it represents a major source of information for the study.

Reviewed by Li-Ying Wang, 2020-12-19 05:22

This paper describes the dataset of lapidary artifacts during the Ceramic period in the Caribbean islands. My comment below is based on the criteria listed on JOAD website that focuses on the description of the data and best practices for data deposition.

For the method section, I think the paper provides good information for understanding how the dataset was created, including the source of data, the methodology for collecting data, sampling strategy, quality control, and constraints. But I would like to suggest to the authors to provide more details about how they searched the ornament-related words in literature. For example, they mentioned "the words…have been systematically searched for." What is the exact method for systematically searching? I think it would be better to specify. Similar issues for the quality control section, how did they do for data cleaning? For constraints, how did they indicate the missing values in the dataset? I can see most missing values are indicated by blank in csv files, but some are indicated by a dash. Are these the same? This needs to be corrected or clarified. This can be addressed in the main text since incompleteness is a constraint in their dataset as they recognized.

In addition to the above questions, there are some mistakes in the text:

1, Page 4, 2.1 steps: "the dataset of lapidary artifacts contains 0 entries, originating from 87 sites". Surely zero is not correct. There should be a number instead of 0.

2, Page 4, 2.4 constraints, "The quality of information has been problematic for several topic of the database" should this be 'topics' as a plural?

3, Also, this sentence "the quality of the reproduction of ancient photographs in the numeric documents now accessible for this literature" is unclear and would be better to rephrase.

For the openness of data, they deposited their dataset on OSF where can be easily accessed and examined. The data is actionable and mostly labeled nicely. However, the information in the manuscript and repository about the number of files is not consistent with each other. In the 3.7.1 Download section, there are six csv files listed in the main text, but only four csv files are uploaded to OSF. The "ILES" and "ISLANDS" files are missing. Also, in OSF, what are the xlsx files under the folder of Data paper JCA2020? The file structure and naming on OSF is confusing and needs to match exactly what is described in the paper. They should make it clearer in the paper and use more informative names instead of just "Table 01.xlsx" to guide readers or users.

This paper meets most of the requirements for publishing. It is well organized with detailed archaeological contexts at the beginning, followed by data information, but the current version has some incorrect descriptions that are required to be solved. I recommend acceptance after the corrections of the issues mentioned above.

Author's reply:

Thank you Mr. Marwick for handling the review process of our manuscript and underlining the efforts for transparency and reproducibility. We have now read and answered to the comments of the four reviewers.

  A recommendation of: Alain Queffelec, Pierrick Fouéré, Jean-Baptiste Caverne. A database of lapidary artifacts in the Caribbean for the Ceramic Age 10.31235/osf.io/7dq3b version 3 Submitted: 13 November 2020, Recommended: 28 February 2021 Cite this recommendation as: Ben Marwick (2021) Open data on beads, pendants, blanks from the Ceramic Age Caribbean. Peer Community in Archaeology, 100009. 10.24072/pci.archaeo.100009

  some problems in the rendering of bibliography, but perhaps it depends on my pc. Cody's quote is different in the three titles of the bibliography: why? In the text, figures are referred to with "Fig." but each caption has "Figure": why? Fig. 4: Figure 4: A. Screenshot of the ArkeoGIS application, a simplified GIS online system. B. Zoom on Guadeloupe, sowhing the potential of the ArkeoGIS visualization tool. (showing) To be corrected! 3. Translation In general, your english could be better. You should ask for a native speaker who helps you.

Our answers are integrated in the document attached, in blue and italic. We have modified our manuscript accordingly and uploaded the new version on the preprint server, as well as the new versions of the different files for the database and the R markdown document. Download author's reply (PDF file)


Kostia Chardonnet

Benoît Valiron

Renaud Vilmart

Geometry of Interaction for ZX-Diagrams

Keywords: 2012 ACM Subject Classification Theory of computation → Quantum computation theory, Theory of computation → Linear logic, Theory Quantum Computation, Linear Logic, ZX-Calculus, Geometry of Interaction

ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this paper we propose a token-machinebased asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams.

Introduction

Quantum computing is a model of computation where data is stored on the state of particles governed by the law of quantum physics. The theory is well established enough to have allowed the design of quantum algorithms whose applications are gathering interests from both public and private actors [START_REF] Ménard | A game plan for quantum computing[END_REF][START_REF] Qureca | Overview on quantum initiatives worldwide[END_REF][START_REF] Gibney | Quantum gold rush: the private funding pouring into quantum start-ups[END_REF] Together with the progresses in physical capabilities, quantum computers are envisioned as a disruptive technology in the coming years [START_REF] Jaeger | The Second Quantum Revolution[END_REF].

One of the fundamental properties of quantum objects is to have a dual interpretations.

In the first one, the quantum object is understood as a particle: with a definite, localized point in space, distinct from the other particles. Light can be for instance regarded as a set of photons. In the other interpretation, the object is understood as a wave: it is "spread-out" in space, possibly featuring interference. This is for instance the interpretation of light as an electromagnetic wave.

The standard model of computation uses quantum bits (qubits) for storing information and quantum circuits [START_REF] Nielsen | Quantum Computation and Quantum Information[END_REF] for describing quantum operations with quantum gates, the quantum version of Boolean gates. In this model, on one hand quantum bits are intuitively seen as tokens flowing inside the wires of the circuit. On the other hand, the state of all of the quantum bits of the memory is mathematically represented as a vector in a (finite dimensional) Hilbert: the set of quantum bits is a wave flowing in the circuit, from the inputs to the output, while the computation generated by the list of quantum gates is a linear map from the Hilbert space of inputs to the Hilbert space of outputs. Although the pervasive model for quantum computation, quantum circuits' operational semantics is only given in an intuitive manner. A quantum circuit informally describes a series of "gate applications", akin to some sequential, low-level assembly language where quantum gates are opaque black-boxes.

Quantum circuits do not feature any native formal operational semantics giving rise to abstract reasoning, equational theory or well-founded rewrite system. To be able to reason on quantum circuits, until recently the only choice was to rely on the unitary-matrix semantics

23:2

Geometry of Interaction for ZX-Diagrams of circuits. However, because the dimension of the matrix corresponding to a circuit is exponential on the number of qubits involved, this solution is very expensive and limited to simple cases.

To bring some scalability to the approach, a recent proposal is sum-over-path semantics [1,[START_REF] Chareton | A deductive verification framework for circuit-building quantum programs[END_REF]. Still based on the original mathematical representation of state-as-a-vector, the sumover-path of a quantum circuit synthesizes the operation described by the circuit into a few simple constructs: a Boolean operation as action on the basis states, and a so-called phase polynomial, bringing to circuits a formal flavor of wave-style semantics.

The main line of work formalizing a token-based operational semantics for quantum circuit [START_REF] Dal Lago | The geometry of parallelism. classical, probabilistic, and quantum effects[END_REF] is based on Geometry of Interaction (GoI) [START_REF] Girard | Towards a geometry of interaction[END_REF][START_REF] Girard | Geometry of interaction I: interpretation of system f[END_REF][START_REF] Girard | Geometry of interaction II: deadlock-free algorithms[END_REF][START_REF] Girard | Geometry of interaction III: accommodating the additives[END_REF][START_REF] Girard | Geometry of interaction IV: the feedback equation[END_REF][START_REF] Girard | Geometry of interaction V: logic in the hyperfinite factor[END_REF][START_REF] Girard | Geometry of interaction VI: a blueprint for transcendental syntax[END_REF]. Among its many instantiations, GoI can be seen as a procedure to intepret a proof-nets [START_REF] Girard | Proof-nets: the parallel syntax for proof-theory[END_REF] -graphical representation of proofs of linear logic [START_REF] Girard | Linear logic[END_REF]-as a token-based automaton [START_REF] Danos | Reversible, irreversible and optimal λ-machines[END_REF][START_REF] Asperti | Paths, computations and labels in the λ-calculus[END_REF]. The flow of a token inside a proof-net characterizes an invariant of the proof -its computational content. This framework is used in [START_REF] Dal Lago | The geometry of parallelism. classical, probabilistic, and quantum effects[END_REF] to formalize the notion of qubits-as-tokens flowing inside a higher-order term representing a quantum computation -that is, computing a quantum circuit. However, in this work, quantum gates are still regarded as black-boxes, and tokens are purely classical objects requiring synchronicity: to fire, a two-qubit gate needs its two arguments to be ready.

In recent years, an alternative model of quantum computation with better formal properties has however emerged: the ZX calculus [START_REF] Coecke | Interacting quantum observables: categorical algebra and diagrammatics[END_REF]. Originally motivated by a categorical interpretation of quantum theory, the ZX-Calculus is a graphical language that represents linear maps as special kinds of graphs called diagrams. The calculus comes with a well-defined equational theory making it possible to reason on quantum computation by means of local graph rewriting. Unlike the qunatum circuit framework, ZX-Calculus also comes with, a small set of canonical generators with a well-defined semantics.

Reasonning about ZX can therefore be done in two ways: with the linear operator semantics (aka matrix semantics), or through graph rewriting. This graphical language has been shown to be amenable to many extensions and is being used in a wide spectrum of applications ranging from quantum circuit optimization [START_REF] Duncan | Graph-theoretic simplification of quantum circuits with the zx-calculus[END_REF][START_REF] Backens | There and back again: A circuit extraction tale[END_REF], verification [START_REF] Hillebrand | Quantum protocols involving multiparticle entanglement and their representations[END_REF][START_REF] Duncan | Verifying the Steane code with Quantomatic[END_REF][START_REF] Duncan | Verifying the smallest interesting colour code with quantomatic[END_REF] and representation such as MBQC patterns [START_REF] Duncan | Rewriting measurement-based quantum computations with generalised flow[END_REF] or error-correction [START_REF] De | The ZX calculus is a language for surface code lattice surgery[END_REF][START_REF] Niel De Beaudrap | Pauli Fusion: a computational model to realise quantum transformations from ZX terms[END_REF].

As a summary, despite their ad-hoc construction, quantum circuits can be seen from two perspectives: computation as a flow of particles (i.e. tokens), and as a wave passing through the gates. On the other hand, although ZX-Calculus is a well-founded language, it still misses such a perspective.

In this paper, we aim at providing ZX with a particle-style and a wave-style semantics, similarly to what has been done for quantum circuits.

Following the idea of applying a token machine to proof-nets in order to study its computational content, we present in this paper a token machine for the ZX-Calculus and its extension to mixed processes [START_REF] Coecke | Environment and Classical Channels in Categorical Quantum Mechanics[END_REF][START_REF] Carette | Completeness of Graphical Languages for Mixed States Quantum Mechanics[END_REF]. We show how it links to the standard interpretation of ZX-diagrams. While the standard interpretation of ZX-diagrams proceeds with conventional graph rewriting, the tokens flowing inside the diagram do not modify it, and the computation emerges from their ability to enter into superposition. We derive two perspectives on this phenomenon: one purely token-based and one based on a sum-over-path interpretation.

Plan of the paper. The paper is organized as follows : in Section 2 we present the ZX-Calculus and its standard interpretation into Qubit, and its axiomatization.

In Section 3 we present the actual asynchronous token machine and its semantics and show that it is sound and complete with regard to the standard interpretation of ZX-diagrams.

We then modify it in Section 4 to use a Sum-Over-Path interpretation in order to avoid an exponential blow up in the number of state in our Token Machine. Next, in Section 5 we present an extension of the ZX-Calculus to mixed processes and adapt the token machine to take this extension into account. Finally, in Section 6 we discuss synchronicity and other ways to represent the Token Machine. Proofs are in the appendix.

2

The ZX-Calculus

The ZX-Calculus is a powerful graphical language for reasoning about quantum computation introduced by Bob Coecke and Ross Duncan [START_REF] Coecke | Interacting quantum observables: categorical algebra and diagrammatics[END_REF]. A term in this language is a graph -called a string diagram-built from a core set of primitives. In the standard interpretation of ZX-Calculus, a string diagram is interpreted as a matrix. The language is equipped with an equational theory preserving the standard interpretation.

Pure Operators

The so-called pure ZX-diagrams are generated from a set of primitives, given on the right: the Identity, Swap, Cup, Cap, Green-spider and H-gate:

       e0 , e0 e1
, e0 e1 , e0 e1 , ...

e1 en e ′ 1 e ′ m ... α , e0 e1        n,m∈N α∈R ei,e ′ i ∈E
We shall be using the following labeling convention: wires (edges) are labeled with e i , taken from an infinite set of labels E. We take for granted that distinct wires have distinct labels. ZX-primitives can be composed as follows.

Sequentially If E(D 1 ) ∩ E(D 2 ) = ∅, then:

D 2 • D 1 := ... ... ... D 2 D 1 [I(D2)←O(D1)] 115 E(D 2 • D 1 ) = E(D 1 ) ∪ E(D 2 ) \ I(D 2 ) 116 I(D 2 • D 1 ) = I(D 1 ) 117 O(D 2 • D 1 ) = O(D 2 )
118

Where [I(D 2 ) ← O(D 1 )] is the substitution of the names of the labels of I(D 2 ) by those of O(D 1 ) done left to right.

In parallel If E(D 1 ) ∩ E(D 2 ) = ∅, then: D 1 ⊗ D 2 := ... ... D 1 ... ... D 2 122 E(D 1 • D 2 ) = E(D 1 ) ∪ E(D 2 ) 123 I(D 1 ⊗ D 2 ) = I(D 1 ) :: I(D 2 ) 124 O(D 1 ⊗ D 2 ) = O(D 1 ) :: O(D 2 )
125

We write ZX for the set of all ZX-diagrams.

Notice that when composing diagrams with (_ • _), we "join" the outputs of the top We write σ for a permutation of wires, i.e any diagram generated by , with sequential and parallel composition. We write the Cap as η and the Cup as ϵ. We write Z n k (α) (resp, X n k ) for the green-node (resp, red-node) of n inputs, k outputs and parameter α and H for the H-gate. In the remainder of the paper we omit the edge labels when not necessary . Finally, by abuse of notation a green or red node with no explicit parameter holds the angle 0:

Standard Interpretation

In the standard interpretation [START_REF] Coecke | Interacting quantum observables: categorical algebra and diagrammatics[END_REF], a diagram D is mapped to a finite dimensional Hilbert space of dimensions some powers of 2:

D ∈ Qubit := {C 2 n → C 2 m | n, m ∈ N}.
If D has n inputs and m outputs, its interpretation is a map D : C

= id C 2 = |0⟩⟨0| + |1⟩⟨1| = i,j∈{0,1} |ji⟩⟨ij| = † = |00⟩ + |11⟩ = |+⟩⟨0| + |-⟩⟨1| α n ... ... m = |0 m ⟩⟨0 n | + e iα |1 m ⟩⟨1 n | α n ... ... m = |+ m ⟩⟨+ n | + e iα |-m ⟩⟨-n |
Wires are interpreted with the two-dimensional Hilbert space, with orthonormal basis written as {|0⟩ , |1⟩}, in Dirac notation [START_REF] Nielsen | Quantum Computation and Quantum Information[END_REF]. Vectors of the form |.⟩ (called "kets") are considered as vector columns, and therefore |0⟩ = ( 1 0 ), |1⟩ = ( 0 1 ), and

α |0⟩ + β |1⟩ = ( α β ).
Horizontal juxtaposition of wires is interpreted with the Kronecker, or tensor product. The tensor product of spaces V and W whose bases are respectively {v i } i and {w j } j is the vector space of basis {v i ⊗ w j } i,j , where v i ⊗ w j is a formal object consisting of a pair of v i and . Dirac also introduced the notation "bra" ⟨x|, standing for a row vector. So for instance, α ⟨0|

+ β ⟨1| is ( α β ). If |ϕ⟩ = α |0⟩ + β |1⟩, we
then write ⟨ϕ| for the vector α ⟨0| + β ⟨1| (with (.) the complex conjugation). The notation for tensors of bras is similar to the one for kets. For instance, ⟨x| ⊗ ⟨y| = ⟨xy|. Using this notation, the scalar product is transparently the product of a row and a column vector:

ϕ ψ , and matrices can be written as sums of elements of the form |ϕ⟩⟨ψ|. For instance, the identity on

C 2 is ( 1 0 0 1 ) = ( 1 0 0 0 ) + ( 0 0 0 1 ) = ( 1 0 ) ( 1 0 ) + ( 0 1 ) ( 0 1 ) = |0⟩⟨0| + |1⟩⟨1|.
For more information on how Hilbert spaces, tensors, compositions and bras and kets work, we invite the reader to consult e.g. [START_REF] Nielsen | Quantum Computation and Quantum Information[END_REF].

Properties and structure

In this section, we list several definitions and known results that we shall be using in the remainder of the paper. See e.g.

[39] for more information. Universality. ZX-diagrams are universal in the sense that for any linear map f : n → m, there exists a diagram D of ZX

such that D = f .
The price to pay for universality is that different diagrams can possibly represent the same quantum operator. There exists however a way to deal with this problem: an equational theory. Several equational theories have been designed for various fragments of the language [START_REF] Backens | The ZX-calculus is complete for stabilizer quantum mechanics[END_REF][START_REF] Jeandel | A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics[END_REF][START_REF] Hadzihasanovic | Two complete axiomatisations of pure-state qubit quantum computing[END_REF][START_REF] Jeandel | Diagrammatic reasoning beyond Clifford+T quantum mechanics[END_REF][START_REF] Jeandel | A generic normal form for zxdiagrams and application to the rational angle completeness[END_REF][START_REF] Vilmart | A near-minimal axiomatisation of zx-calculus for pure qubit quantum mechanics[END_REF].

Core axiomatization. Despite this variety, any ZX axiomatization builds upon the core set of equations provided in Figure 1, meaning that edges really behave as wires that can be bent, tangled and untangled. They also enforce the irrelevance on the ordering of inputs and outputs for spiders. Most importantly, these rules preserve the standard interpretation given in Section 2.2. We will use these rules -sometimes referred to as "only connectivity matters"-, and the fact that they preserve the semantics extensively in the proofs of the results of the paper.

In particular, diagrams are always considered modulo the equivalence relation presented in Figure 1.

Completeness. The ability to transform a diagram D 1 into a diagram D 2 using the rules of some axiomatization zx (e.g. the core one presented in Figure 1) is denoted zx

⊢ D 1 = D 2 .
The axiomatization is said complete whenever any two diagrams representing the same operator can be turned into one another using this axiomatization. Formally:

D 1 = D 2 ⇐⇒ zx ⊢ D 1 = D 2
It is common in quantum computing to work with restrictions of quantum mechanics. Such restrictions translate to restrictions to particular sets of diagrams -e.g. the π 4 -fragment which consists of all ZX-diagrams where the angles are multiples of π 4 . There exist axiomatization that were proven to be complete for the corresponding fragment (all the aforementioned references tackle the problem of completeness).

The developments of this paper are given for the ZX-Calculus in its most general form, but everything in the following also works for fragments of the language.

Input and output wires. An important result which will be used in the rest of the paper is the following:

▶ Theorem 3. There are isomorphisms between {D ∈ ZX | D : n → m} and {D ∈ ZX | D : n -k → k + m} (when k ≤ n). ◀ C V I T 2 0 1 6 23:6

Geometry of Interaction for ZX-Diagrams

To see how this can be true, simply add cups or caps to turn input edges to output edges (or vice versa), and use the fact that we work modulo the rules of Figure 1.

When k = n, this isomorphism is referred to as the map/state duality. A related but more obvious isomorphism between ZX-diagrams is obtained by permutation of input wires (resp. output wires).

Notions of Graph Theory in ZX

for 1 ≤ i, j ≤ n, g i = g j if and only if i = j, for 0 ≤ i < n, e i , e i+1 ∈ E(g i+1 ). If e i ∈ I(g i ) (resp. e i ∈ O(g i+1 )), we say that e i is ↑-oriented (resp. ↓-oriented) in the path.

A Token Machine for ZX-diagrams

Inspired by the Geometry of Interaction [START_REF] Girard | Towards a geometry of interaction[END_REF][START_REF] Girard | Geometry of interaction I: interpretation of system f[END_REF][START_REF] Girard | Geometry of interaction II: deadlock-free algorithms[END_REF][START_REF] Girard | Geometry of interaction III: accommodating the additives[END_REF][START_REF] Girard | Geometry of interaction IV: the feedback equation[END_REF][START_REF] Girard | Geometry of interaction V: logic in the hyperfinite factor[END_REF][START_REF] Girard | Geometry of interaction VI: a blueprint for transcendental syntax[END_REF] and the associated notion of token machine [START_REF] Danos | Reversible, irreversible and optimal λ-machines[END_REF][START_REF] Asperti | Paths, computations and labels in the λ-calculus[END_REF] for proof nets [START_REF] Girard | Proof-nets: the parallel syntax for proof-theory[END_REF], we define here a first token machine on pure ZX-diagrams. The token consists of an edge of the diagram, a direction (either going up, noted ↑, or down, noted ↓) and a bit (state). The idea is that, starting from an input edge the token will traverse the graph and duplicate itself when encountering an n-ary node (such as the green and red) into each of the input / output edges of the node. Notice that it is not the case for token machines for proof-nets where the token never duplicates itself. In the token state

t = i α i t 1,i • • • t ni,i
, where the t k,i 's are tokens, the components ▶ Convention 9. In token states, the sum (+) stands for the superposition and the product for additional tokens within a given diagram. We follow the usual convention of algebras of polynomials: for instance, if t i stands for some token (e

α i t 1,i • • • t ni,i
i d i b i ), then (t 1 +t 2 )t 3 = (t 1 t 2 )+(t 1 t 3 ),
that is, the superposition of t 1 ,t 2 flowing in D and t 1 ,t 3 flowing in D. Similarly, we consider token states modulo commutativity of sum and product, so that for instance the monomial t 1 t 2 is the same as t 2 t 1 .

Diffusion and Collision Rules

The tokens in a ZX-diagram D are meant to move inside D. The set of rules presented in this section describes an asynchronous evolution, meaning that given a token state, we will rewrite only one token at a time. The synchronous setting is discussed in Section 6.

▶ Definition 10 (Asynchronous Evolution). Token states on a diagram D are equipped with two transition systems:

a collision system (⇝ c ), whose effect is to annihilate tokens; a diffusion sub-system (⇝ d ), defining the flow of tokens within D.

The two systems are defined as follows. With X ∈ {d, c} and 1 ≤ j ≤ n i , if t i,j are tokens in tk(D), then using Convention 9,

i α i t i,1 • • • t i,j • • • t i,ni ⇝ X i α i t i,1 • • • k β k t ′ k • • • t i,ni
provided that t i,j ⇝ X k β k t ′ k according to the rules of Table 1. In the table, each rule corresponds to the interaction with the primitive diagram constructor on the left-hand-side.

Variables x and b span {0, 1}, and ¬ stands for the negation. In the green-spider rules, e iαx stands for the the complex number cos(αx) + i sin(αx) and not an edge label.

Finally, as it is customary for rewrite systems, if (→) is a step in a transition system, (→ * ) stands for the reflexive, transitive closure of (→).

We aim at a transition system marrying both collision and diffusion steps. However, for consistency of the system, the order in which we apply them is important as illustrated by the following example.

▶ Example 11. Consider the equality given by the ZX equational theory: = .

If we drop a token with bit 0 at the top, we hence expect to get a single token with bit 0 at the bottom. We underline the token that is being rewriting at each step. This is what we get when giving the priority to collisions: If however we decide to ignore the priority of collisions, we may end up with a non-terminating run, unable to converge to (d ↓ 0):

a d b c :: (a ↓ 0) ⇝ d (b ↓ 0)(c ↓ 0) ⇝ c (d ↓ 0)(c ↑ 0)(c ↓ 0) ⇝ (d ↓ 0) C V I T 2 0 1 6 23:8 Geometry of Interaction for ZX-Diagrams e0 (e 0 ↓ x)(e 0 ↑ x) ⇝ c 1 (Positive Collision) e0 (e 0 ↓ x)(e 0 ↑ ¬x) ⇝ c 0 (Negative Collision) e0 e1 (e b ↓ x) ⇝ d (e ¬b ↑ x) ( -diffusion) e0 e1 (e b ↑ x) ⇝ d (e ¬b ↓ x) ( -diffusion) (e k ↓ x) ⇝ d e iαx i̸ =k (e i ↑ x) j (e ′ j ↓ x) (e ′ k ↑ x) ⇝ d e iαx j̸ =k (e ′ j ↓ x) i (e i ↑ x) (e 0 ↓ x) ⇝ d (-1) x 1 √ 2 (e 1 ↓ x) + 1 √ 2 (e 1 ↓ ¬x) (e 1 ↑ x) ⇝ d (-1) x 1 √ 2 (e 0 ↑ x) + 1 √ 2 (e 0 ↑ ¬x) ...
(a ↓ 0) ⇝ d (b ↓ 0)(c ↓ 0) ⇝ d (d ↓ 0)(c ↑ 0)(c ↓ 0) ⇝ d (d ↓ 0)(a ↑ 0)(b ↓ 0)(c ↓ 0) ⇝ d . . .
We therefore set a rewriting strategy as follows.

▶ Definition 12 (Collision-Free). A token state s of tkS(D) is called collision-free if:

∀s ′ ∈ tkS(D), s ̸ ⇝ c s ′
▶ Definition 13 (Token Machine Rewriting System). We define a transition system ⇝ as exactly one ⇝ d rule followed by all possible ⇝ c rules. In other words,

t ⇝ u iff (∃t ′ • t ⇝ d t ′ ⇝ * c u and u is collision-free)

Strong Normalization and Confluence

The token machine Rewrite System of Definition 13 ensures that the collisions that can happen always happen. The system does not a priori forbid two tokens on the same edge, provided that they have the same direction. However this is something we want to avoid as there is no good intuition behind it: We want to link the token machine to the standard interpretation, which is not possible if two tokens can appear on the same edge.

In this section we show that, under a notion of well-formedness characterizing token uniqueness on each edge, the Token State Rewrite System (⇝) is strongly normalizing and confluent.

▶

P (p, t) =        1 if e ∈ p

Semantics and Structure of Normal Forms

In this section, we discuss the structure of normal forms, and relate the system to the standard interpretation presented in Section 2.

▶ Proposition 26 (Single-Token Input). Let D : n → m be a connected ZX-diagram with

I(D) = [a i ] 0<i≤n and O(D) = [b i ] 0<i≤m , 0 < k ≤ n and x ∈ {0, 1}, such that: D • (id k-1 ⊗ |x⟩ ⊗ id n-k ) =
2 m+n-1 q=1 λ q |y 1,q , ..., y m,q ⟩⟨x 1,q , ..., x k-1,q , x k+1,q , ..., x n,q | Then:

(a k ↓ x) ⇝ * 2 m+n-1 q=1 λ q i (b i ↓ y i,q ) i̸ =k (a i ↑ x i,q ) ◀
This proposition conveys the fact that dropping a single token in state x on wire a k gives the same semantics as the one obtained from the standard interpretation on the ZX-diagram, with wire a k connected to the state |x⟩.

If: D • 2 n q=1 λ q |x 1,q , ..., x n,q ⟩ = 2 m q=1
λ ′ q |y 1,q , ..., y m,q ⟩ then:

2 n q=1 λ q n i=1 (a i ↓ x i,q ) ⇝ * 2 m q=1 λ ′ q m i=1 (b i ↓ y i,q ) ◀
This proposition is a direct generalization of the proposition 26. Thanks to all of that, we can show that we can start evaluating not only on a single or even multiple input wires, but in fact on any wire in the ZX-diagram, as long as we respect well-formedness and cycle-balancedness.

But we need to be careful about collisions. For that to hold, we need to rewrite each part of the sum independently before computing the sum.

▶ Theorem 29 (Arbitrary Wire Initialisation). Let D be a connected ZX-diagram, with

I(D) = [a i ] 1≤i≤n , O(D) = [b i ] 1≤i≤m
, and e ∈ E(D) ̸ = ∅ such that (e ↓ x)(e ↑ x) ⇝ * t x for x ∈ {0, 1}

with t x terminal (the rewriting terminate by Corollary 25). Then:

D = 2 m+n q=1 λ q |y 1,q . . . y m,q ⟩⟨x 1,q . . . x n,q | =⇒ t 0 + t 1 = 2 m+n q=1 λ q i (b i ↓ y i,q ) i (a i ↑ x i,q ) ◀ 4

Sum-Over-Paths Token Machine

A serious drawback of the previous token machine is that the token state grows exponentially quickly in the number of nodes in the diagram. A more compact representation (linear in the size of the diagram as we will see in Prop. 36) can be obtained by adapting the concept of sums-over-paths (SOP) [1] to our machine. This can be obtained naturally, as strong links between ZX-Calculus and SOP morphisms were already shown to exist [START_REF] Lemonnier | Hypergraph simplification: Linking the path-sum approach to the zh-calculus[END_REF][START_REF] Vilmart | The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford[END_REF].

Intuitively, SOP will allow us to manipulate token states in a symbolic way, where for instance (e ↓ 0) + (e ↓ 1) will be represented by (e ↓ y). We can link this formalism back to the previous one, by defining a map that associates any SOP-token-state to a "usual" token-state. This map simply evaluates the term by having all its variables span {0, 1}:

▶
(s, ⃗ y, P, {t j } 0≤j<p ) ∈ R × V n × R[⃗ y]/(1, {y 2 i -y i } 0≤i<n ) × tk SOP (D)[⃗ y] p where R[⃗ y]/(1, {y 2 i -y i } 0≤i<n )
▶ Definition 32. We define [.] tk : tkS SOP (D) → tkS(D) by:

  s ⃗ y e 2iπP (⃗ y) j (p j , d j , B j (⃗ y))   tk := s ⃗ y∈{0,1} n e 2iπP (⃗ y) j (p j , d j , B j (⃗ y)) ▶ Example 33. 1 √ 2 y0,y1 e 2iπ y 0 y 1 2 (e 0 ↑ y 0 )(e 1 ↓ y 1 ) tk = 1 √ 2 (e 0 ↑ 0)(e 1 ↓ 0) + (e 0 ↑ 1)(e 1 ↓ 0) +(e 0 ↑ 0)(e 1 ↓ 1) -(e 0 ↑ 1)(e 1 ↓ 1)
We give the adapted set of rewrite rules for our SOP-token-machine in Table 2. In the rewrite rules of our token machine, we have to map elements of F 2 [⃗ y] to elements of

R[⃗ y]/(1, {y 2

i -y i }) for the Boolean polynomials to be sent to the phase polynomial. The map (.) :

F 2 [⃗ y] → R[⃗ y]/1(1, {y 2 i -y i })
that does this is defined as:

B ⊕ B ′ = B + B ′ -2 BB ′ BB ′ = B B ′ y i = y i 0 = 0 1 = 1 C V I T
(e 0 ↓ B)(e 0 ↑ B ′ ) ⇝ c 1 2 z e 2iπ z 2 ( B⊕B ′ ) (Collision) e0 e1 (e b ↓ B) ⇝ d (e ¬b ↑ B) ( -diffusion) e0 e1 (e b ↑ B) ⇝ d (e ¬b ↓ B) ( -diffusion) (e k ↓ B) ⇝ d e 2iπ( α 2π B) j̸ =k (e j ↑ B) j (e ′ j ↓ B) (e ′ k ↑ B) ⇝ d e 2iπ( α 2π B) j (e j ↑ B) j̸ =k (e ′ j ↓ B) (e 0 ↓ B) ⇝ d 1 √ 2 z e 2iπ( z 2 B) (e 1 ↓ z) (e 1 ↑ B) ⇝ d 1 √ 2 z e 2iπ( z 2 B) (e 0 ↑ z) ...
j (e j , d j , b j ) ⇝ ss ′ ⃗ y,⃗ y ′ e 2iπ(P +P ′ ) j (e ′ j , d ′ j , b ′ j ) j (e j , d j , b j ).
Just as before, the rewrite system is defined by first applying a diffusion rule then all possible collision rules.

This set of rules mimics the previous one for SOP-token-states, except that it "synchronizes" rewrites on all the terms at once (but not on all tokens). . In the former machine, this leads to

(a ↓ 0) + (a ↓ 1) ⇝ (b ↓ 0)(c ↓ 0) + (a ↓ 1) ⇝ (b ↓ 0)(c ↓ 0) + (b ↓ 1)(c ↓ 1).
while in the latter:

y (a ↓ y) ⇝ sop y (b ↓ y)(c ↓ y)
In both cases the result is the same when interpreted as usual token states. We notice that the ⇝ sop token machine only took one step compared to the standard one, which leads to the following proposition:

▶ Proposition 35.
For any D ∈ ZX and s, s ′ ∈ tkS SOP (D), whenever s ⇝ sop s ′ we have

[s] tk ⇝ * [s ′ ] tk . ◀
We can show a result on the growth size of the token-state as it rewrites, which was the motivation for the use of this formalism.

23:13

The requirement on Boolean polynomials may seem overly restrictive. However, it is invariant under rewriting: starting with a token-state in this form ensures polynomial growth.

Polarity can be defined in this setting (and is even more natural, as we do not need to consider each term individually) providing the notions of well-formedness and cyclebalancedness. The main results from Section 4 are valid in this setting. We recover strong normalization for well-formed, cycle-balanced token-states (Theorem 22), Local Confluence (Proposition 23) and their corollaries, such as uniqueness of normal forms (Corollary 25).

Non-empty terminal token states can also be interpreted as SOP-morphisms. Suppose an SOP-token state

S = s ⃗ y ′ e 2iπP i (b i ↓ B i (⃗ y ′ )) i (a i ↑ A i (⃗ y ′ )) on a diagram D with I(D) = [a i ] 1≤i≤n and O(D) = [b i ] 1≤i≤m . Then [S] SOP := s ⃗ y e 2iπP (⃗ y) |B 0 (⃗ y), ...⟩⟨A 0 (⃗ y), ...|
is the SOP morphism associated to S. We have the following commutative diagram:

tkS SOP ↓ tkS ↓ SOP Qubit [.] tk [.] SOP .
.

where tkS SOP ↓ (resp. tkS ↓) is the set of non-empty wellformed terminal SOP-token states (resp. token states), and tkS ↓ .

→ Qubit is the interpretation obtained from Theorem 29.

Extension to Mixed Processes

The token machines presented so far worked for so-called pure quantum processes i.e. with no interaction with the environment. To demonstrate how generic our approach is, we show how to adapt it to the natural extension of mixed processes, represented with completely positive maps (CPM). This in particular allows us to represent quantum measurements.

ZX-diagrams for Mixed Processes

The interaction with the environment can be modeled in the ZX-Calculus by adding a unary generator to the language [START_REF] Coecke | Environment and Classical Channels in Categorical Quantum Mechanics[END_REF][START_REF] Carette | Completeness of Graphical Languages for Mixed States Quantum Mechanics[END_REF], intuitively enforcing the state of the wire to be classical.

We There is a canonical way to map a ZX -diagram to a ZX-diagram in a way that preserves the semantics: the so-called CPM-construction [START_REF] Selinger | Dagger compact closed categories and completely positive maps[END_REF]. We define the map (conveniently named)

CPM as the map that preserves compositions (_ • _) and (_ ⊗ _) and such that:

CPM = CPM = CPM = CPM = CPM ( ) = CPM α n ... ... m = α ... m -α n ... CPM α n ... ... m = α ... m -α n ... CPM =
With respect to what happens to edge labels, notice that every edge in D can be mapped to 2 edges in CPM(D). We propose that label e induces label e in the first copy, and e in the second, e.g, for the identity diagram:

e0 -→ e0 e0
In the general ZX-Calculus, it has been shown that the axiomatization itself could be extended to a complete one by adding only 4 axioms [START_REF] Carette | Completeness of Graphical Languages for Mixed States Quantum Mechanics[END_REF].

C V I T

Token Machine for Mixed Processes

We now aim to adapt the token machine to ZX , the formalism for completely positive maps.

Since the formalism of sum-over-paths gave us an easier machine to work with, where terms are smaller while guaranteeing a simulation result with respect to the first token machine, we will use it to define the token machine for completely positive maps.

▶ Definition 38. Let D be a ZX-diagram. A SOP -token is a quadruplet (p, d, B, B ′ ) ∈ E(D) × {↓, ↑} × F 2 [⃗ y] × F 2 [⃗ y]
(s, ⃗ y, P, {t j } 0≤j<p ) ∈ R × V n × R[⃗ y]/(1, {y 2 i -y i } 0≤i<n ) × tk SOP (D)[⃗ y] p
To better reflect what this quadruplet represents, we usually write it as:

s ⃗ y e 2iπP (⃗ y) (p 0 , d 0 , B 0 (⃗ y), B ′ 0 (⃗ y))...(p m-1 , d m-1 , B m-1 (⃗ y), B ′ m-1 (⃗ y))
We denote the set of SOP -token-states on D by tkS SOP (D)

In other words, the difference with the previous machine is that tokens here have an additional Boolean function (e.g. (a ↓ x, y)). The rewrite rules are given in Table 3.

e0 (e 0 ↓ B 0 , B 1 ) × (e 0 ↑ B ′ 0 , B ′ 1 ) ⇝ c 1 4 z0,z1 e 2iπ( z 0 2 B0⊕B1+ z 1 2 B ′ 0 ⊕B ′ 1 ) (Collision) e0 e1 (e b ↓ B, B ′ ) ⇝ d (e ¬b ↑ B, B ′ ) ( -diffusion) e0 e1 (e b ↑ B, B ′ ) ⇝ d (e ¬b ↓ B, B ′ ) ( -diffusion) (e k ↓ B 0 , B 1 ) ⇝ d e 2iπ α 2π ( B0-B1) j̸ =k (e j ↑ B 0 , B 1 ) × j (e ′ j ↓ B 0 , B 1 ) (e ′ k ↑ B 0 , B 1 ) ⇝ d e 2iπ α 2π ( B0-B1) j (e j ↑ B 0 , B 1 ) × j̸ =k (e ′ j ↓ B 0 , B 1 ) (e 0 ↓ B, B ′ ) ⇝ d 1 2 z,z ′ e 2iπ( z 2 B+ z ′ 2 B ′ ) (e 1 ↓ z, z ′ ) (e 1 ↑ B, B ′ ) ⇝ d 1 2 z,z ′ e 2iπ( z 2 B+ z ′ 2 B ′ ) (e 0 ↑ z, z ′ ) e0 (e 0 ↓ B, B ′ ) ⇝ d 1 2 z e 2iπ z 2 ( B⊕B ′ ) (Trace-Out) ... e1 en e ′ 1 e ′ m ... α e0 e1 ( -Diffusion) ( ... ...

-Diffusion)

Table 3 The rewrite rules for ⇝ .

It is possible to link this formalism back to the mixed processes-free SOP-token-states, using the existing CPM construction for ZX-diagrams. We extend this map by CPM :

tkS SOP (D) → tkS SOP (CPM(D)), defined as:

s ⃗ y e 2iπP (⃗ y) j (p j , d j , B j (⃗ y), B ′ j (⃗ y)) → s ⃗ y e 2iπP (⃗ y) j (p j , d j , B j (⃗ y))(p j , d j , B ′ j (⃗ y))
CPM(D) can be seen as two copies of D where is replaced. Each token in D corresponds to two tokens in CPM(D), at the same spot but in the two copies of D. The two Boolean polynomials B and B ′ represent the Boolean polynomials of the two corresponding tokens.

We can then show that this rewriting system is consistent:

▶ Theorem 39. Let D be a ZX -diagram,

Conclusion and Future Work

Since quantum circuits can be mapped to ZX-diagrams, our token machines induce a notion of asynchronicity for quantum circuits. This contrasts with the notion of token machine defined in [START_REF] Dal Lago | The geometry of parallelism. classical, probabilistic, and quantum effects[END_REF] where some form of synchronicity is enforced.

Our token machine can however be made synchronous: all tokens in a token state then move at once. This implies adapting the rules to take into account all incoming tokens for each generator. For instance, in the ... ... -Diffusion -rule the product i (e i ↓ x i ) rewrites into δ x1,...,xn e iαx1 i (e ′ i ↓ x 1 ). This notion of synchronicity is to be contrasted with [START_REF] Dal Lago | The geometry of parallelism. classical, probabilistic, and quantum effects[END_REF] where tokens have to wait for all other incoming tokens before going through a gate.

The presentation we followed clearly distinguishes between ZX-diagrams and token states on them. We could instead see tokens as part of the ZX-diagram. For instance, (e ↓ x) on D could be a literal node ↓ x e on D. For our first token machine, this would imply representing a token state by a sum of diagrams with tokens on them. In the SOP framework, however, we would simply get a single diagram with tokens on them and global scalar and polynomial in the variables.

In this paper, we showed that our tokens could start at any edge, in a configuration that respects well-formedness and cycle-balancedness. We may also consider a "pulse" version, in which each node emits one token in all of its edges at once, during the evaluation of the token machine. This pulse version can be seen as a generalization of the initialization of the token state in Theorem 29: the intuition is

↑ x = ⇝ ↓ x x .

C V I T 2 0 1 6

Since e / ∈ p (we would not have a path then), then p ′ := (e 0 , ..., e n , e) is a path (or possibly a cycle) such that P (p ′ , t) = 2. This is forbidden by well-formedness. Hence, every generator can be visited at most once. As a consequence, the lexicographic order (#g, #tk) (where #g is the number of non-visited generators in the diagram, and #tk the number of tokens in the diagram) strictly reduces with each rewrite. This finishes the proof of termination. ◀ Proof of Proposition 23. We are going to reason on every possible pairs of rewrite rules that can be applied from a single token state s. Notice first, that if the two rules are applied on two different terms of s, such that the rewriting of a term creates a copy of the other, they obviously commute, so

s ⇝ s 2 ⇝ ⇝ s 1 ⇝ s ′ . C V I T 2 0 1 6

23:20 Geometry of Interaction for ZX-Diagrams

In the case where s = αt + βt 1 + s 0 such that t 1 ⇝ s ′ and t ⇝ i λ i t i , we have:

⇝ αt + βs ′ + s 0 ⇝ i αλ i t i + βs ′ + s 0 s ⇝ ⇝ (αλ 1 + β)t 1 + i̸ =1 αλ i t i + s 0 ⇝ (αλ 1 + β)s ′ + i̸ =1 αλ i t i + s 0
Then, we can, in the following, focus on pairs of rules applied on the same term.

The term we focus on is obviously collision-free, by hypothesis and by preservation of collision-freeness by ⇝.

Suppose the two rewrites are applied on tokens at positions e and e ′ . We may reason using the distance between the two edges.

the case d(e, e ′ ) = 0 would imply a collision, which is impossible by collision-freeness if d(e, e ′ ) ≥ 3, the two rules still don't interfere, they commute (up to collisions which do not change the result)

if d(e, e ′ ) = 2, there will be common collisions (i.e. collisions between tokens created by each of the diffusions), however, the order of application of the rules will not change the bits in the tokens we will apply a collision on, so the result holds if d(e, e ′ ) = 1, then the two tokens have to point to the same generator. If they didn't, (e, e ′ ) would form a path such that |P ((e, e ′ ), t)| = 2 which is forbidden by well-formedness.

We can then show the property for all generators:

Case e0 e1 . (e 0 ↓ x)(e 1 ↓ x ′ ) ⇝ d (e 1 ↑ x)(e 1 ↓ x ′ ) ⇝ d ⇝ c (e 0 ↓ x)(e 0 ↑ x ′ ) ⇝ c x x ′
Case e0 e1 : similar.

Case

...

e1 en e ′ 1 e ′ m ... α . e iαx i̸ =1 (e i ↑ x) i (e ′ i ↓ x)(e ′ 1 ↑ x ′ ) ⇝ c ⇝ d x x ′ e iαx i̸ =1 (e i ↑ x) i̸ =1 (e ′ i ↓ x) (e 1 ↓ x)(e ′ 1 ↑ x ′ ) | | ⇝ d x x ′ e iαx ′ i̸ =1 (e i ↑ x ′ ) i̸ =1 (e ′ i ↓ x ′ ) e iαx ′ i (e i ↑ x ′ ) i̸ =1 (e ′ i ↓ x)(e 1 ↓ x) ⇝ c Case e0 e1 . 1 √ 2 ((-1) x (e 1 ↓ x)(e 1 ↑ x ′ ) + (e 1 ↓ ¬x)(e 1 ↑ x ′ )) ⇝ 2 c ⇝ d 1 √ 2 (-1) x x x ′ + ¬x x ′ (e 0 ↓ x)(e 1 ↑ x ′ ) | | ⇝ d 1 √ 2 (-1) x ′ x x ′ + x ¬x ′ 1 √ 2 (-1) x ′ (e 0 ↓ x)(e 0 ↑ x ′ ) + (e 0 ↓ x)(e 0 ↑ ¬x ′ ) ⇝ 2 c
◀ Proof of Proposition 26. Let us first notice that, using the map/state duality, we have

(a k ↓ x) ⇝ * 2 m+n-1 q=1 λ q i (b i ↓ y i,q ) i̸ =k (a i ↑ x i,q ) in D iff we have (a k ↓ x) ⇝ * 2 m+n-1 q=1 λ q i (b i ↓ y i,q ) i̸ =k (a ′ i ↓ x i,q ) in D ′ where D ′ ... := ... D ... ... a k a k a ′ 1 a ′ n
. Hence, we can, w.l.o.g. consider in the following that n = 1. We also notice that thanks to the confluence of the rewrite system, we can consider diagrams up to "topological deformations", and hence ignore cups and caps.

We then proceed by induction on the number N of "non-wire generators" (i.e. Z-spider, X-spiders and H-gates) of D, using the fact that the diagram is connected:

If N = 0, then D = , where the result is obvious.

If N = 1, then D ∈    , , α ... ... , α ... ...   
. The result in this base case is then a straightforward verification (self-loops in green and red nodes simply give rise to collisions that are handled as expected).

For N + 1, there exists D ′ with N non-wire generators and such that

D ∈      D ′ ... , D ′ ... ... α , D ′ ... ... α     
(we should actually take into account the self loops, but they do not change the result). Let us look at the first two cases, since the last one can be induced by composition.

If D = D ′ ... a a ′ b1 bm
, then D ′ is necessarily connected, by connectivity of D. Then:

(a ↓ x) ⇝ (-1) x √ 2 (a ′ ↓ x) + 1 √ 2 (a ′ ↓ ¬x) ⇝ * (-1) x √ 2 2 m q=1 λ q m i=1 (b i ↓ y i,q ) + 1 √ 2 2 m q=1 λ ′ q m i=1 (b i ↓ y i,q ) = 2 m q=1 λ ′ q + (-1) x λ q √ 2 m i=1 (b i ↓ y i,q )
where by induction hypothesis

D ′ |x⟩ = 2 m q=1 λ q |y 1,q , ..., y m,q ⟩ and D ′ |¬x⟩ = 2 m q=1
λ ′ q |y 1,q , ..., y m,q ⟩ so:

D |x⟩ = D ′ • H |x⟩ = D ′ • H |x⟩ = D ′ • (-1) x √ 2 |x⟩ + 1 √ 2 |¬x⟩ = (-1) x √ 2 D ′ |x⟩ + 1 √ 2 D ′ |¬x⟩ = 2 m q=1 λ ′ q + (-1) x λ q √ 2 |y 1,q , ..., y m,q ⟩ C V I T
(a ↓ x) ⇝ e iαx ℓ i (a ℓ,i ↓ x) ⇝ * e iαx ℓ   2 m ℓ +n ℓ -1 q=1 λ q,ℓ i̸ =1 (a ℓ,i ↓ x)(a ℓ,i ↑ x ℓ,i,q ) i (b ℓ,i ↓ y ℓ,i,q )   ⇝ * e iαx ℓ   2 m ℓ +n ℓ -1 q=1 λ q,ℓ δ x,x ℓ,i,q i (b ℓ,i ↓ y ℓ,i,q )   = e iαx ℓ 2 m ℓ q=1 λ ′ q,ℓ i (b ℓ,i ↓ y ℓ,i,q ) = e iαx 2 m 1 q1=1 ... 2 m k q k =1 λ ′ q1,1 ...λ ′ q k ,k i (b 1,i ↓ y 1,i,q1 )... i (b k,i ↓ y k,i,q k ) = 2 m q=1 λ ′ q i (b i ↓ y i,q )
where the first is the diffusion through a Z-spider, and the second set of rewrites is the induction hypothesis applied to each connected component.

D |x⟩ = (D 1 ⊗ ... ⊗ D k ) • Z 1 k (α) |x⟩ = ( D 1 ⊗ ... ⊗ D k ) • Z 1 k (α) |x⟩ = e iαx ( D 1 ⊗ ... ⊗ D k ) • |x, ..., x⟩ = e iαx D 1 |x, ..., x⟩ ⊗ ... ⊗ D k |x, ..., x⟩ = e iαx   2 m 1 +n 1 -1 q1 λ q1,1 |y 1,1,q1 , ..., y 1,m1,q1 ⟩ x 1,2,q1 , ..., x 1,n1,q1 x, ..., x   ⊗ ... ⊗   2 m k +n k -1
q k λ q k ,k |y k,1,q1 , ..., y k,m1,q k ⟩ x k,2,q k , ..., x k,n1,q k x, ... q k λ ′ q k ,k |y k,1,q1 , ..., y k,m1,q k ⟩ = 2 m q=1 λ ′ q |y 1,q , ..., y m,q ⟩ where the third line is obtained by induction hypothesis, and all λ ′ match the ones obtained from the rewrite of token states.

◀

Proof of Lemma 27. There exist several methods to build a diagram D f such that D f = f , using the universality of quantum circuits together with the map/state duality [START_REF] Coecke | Interacting quantum observables: categorical algebra and diagrammatics[END_REF], or using normal forms [START_REF] Jeandel | A generic normal form for zxdiagrams and application to the rational angle completeness[END_REF]. The novelty here is that the diagram should be connected. This problem can be fairly simply dealt with:

Suppose we have such a D f that has several connected components. We can turn it into an equivalent diagram that is connected. Let us consider two disconnected components of D f . Each of these disconnected components either has at least one wire, or is one of { α , α }.

In either case, we can use the rules of ZX ((I g ) or (H)) to force the existence of a green node. These green nodes in each of the connected components can be "joined" together like this: (a ′ ↓ 0) ⇝ * 2 n q=1 λ q n i=1 (a i ↓ x i,q ) and (a ′ ↓ 0) ⇝ * 2 m q=1 λ ′ q m i=1 (b i ↓ y i,q )

The first run comes from Proposition 26 on D ′ which is connected. The second run results from Proposition 26 on D • D ′ which is also connected. The proposition also gives us that:

D • 2 n q=1 λ q |x 1,q , ..., x n,q ⟩ = D • D ′ • |0⟩ = D • D ′ • |0⟩ = 2 m q=1
λ ′ q |y 1,q , ..., y m,q ⟩ Finally, by confluence in D • D ′ , we get . We can easily see that a rewriting of the token states (e ↓ 0)(e ↑ 0) and (e ↓ 1)(e ↑ 1) in D correspond step by step to a rewriting of the token states (e 0 ↓ 0)(e 1 ↑ 0) and (e 0 ↓ 1)(e 1 ↑ 1) in D ′ . We can then focus on D ′ , whose interpretation is taken to be

2 n q=1 λ q n i=1 (a i ↓ x i,q ) ⇝ * 2 m q=1 λ ′
D ′ = 2 m+n+2
q=1 λ ′ q y ′ 1,q , ..., y ′ m+1,q x ′ 1,q , ..., x ′ n+1,q such that (id ⊗m ⊗ ⟨0|) • D ′ • (id ⊗n ⊗ |0⟩) + (id ⊗m ⊗ ⟨1|) • D ′ • (id ⊗n ⊗ |1⟩) = D from which we get:

D = 2 m+n+2
q=1 λ ′ q δ 0,y ′ m+1,q δ 0,x ′ n+1,q y ′ 1,q , ..., y ′ m,q x ′ 1,q , ..., x ′ n,q + 2 m+n+2 q=1 λ ′ q δ 1,y ′ m+1,q δ 1,x ′ n+1,q y ′ 1,q , ..., y ′ m,q x ′ 1,q , ..., x ′ n,q

We now have to consider two cases: D ′ is still connected: By Proposition 26, for x ∈ {0, 1}:

(e 0 ↓ x)(e 1 ↑ x) ⇝ * 2 m+n+2 q=1 λ ′ q δ x,x ′ n+1,q i (a i ↑ x ′ i,q ) i (b i ↓ y ′ i,q )(e 1 ↓ y ′ m+1,q )(e 1 ↑ x)

⇝ 2 m+n+2
q=1 λ ′ q δ x,y ′ m+1,q δ x,x ′ n+1,q i (a i ↑ x ′ i,q ) i (b i ↓ y ′ i,q )

We hence have (e 0 ↓ 0)(e 1 ↑ 0) ⇝ * t 0 = 2 m+n+2 q=1 λ ′ q δ 0,y ′ m+1,q δ 0,x ′ n+1,q i (a i ↑ x ′ i,q ) i (b i ↓ y ′ i,q ) (e 0 ↓ 1)(e 1 ↑ 1)

⇝ * t 1 = 2 m+n+2 q=1 λ ′ q δ 1,y ′ m+1,q δ 1,x ′ n+1,q i (a i ↑ x ′ i,q ) i (b i ↓ y ′ i,q )
so t 0 + t 1 corresponds to the interpretation of D.

  The real number α attached to the green spiders is called the angle. ZX-diagrams are read top-to-bottom: dangling top edges are the input edges and dangling edges at the bottom are output edges. For instance, Swap has 2 input and 2 output edges, while Cup has 2 input edges and no output edges. We write E(D) for the set of edge labels in the diagram D, and I(D) (resp. O(D)) for the list of input edges (resp. output edges) of D. We denote :: the concatenation of lists.

▶

  diagram with the inputs of the bottom diagram. This requires that the two sets of edges have the same cardinality. The junction is then made by relabeling the input edges of the bottom diagram by the output labels of the top diagram (hence the "[I(D2)←O(D1)]" in the composition). Convention 1. We define a second spider, red this time, by composition of Green-spiders and H-gates, as shown on the right.

w

  j . We denote |x⟩ ⊗ |y⟩ as |xy⟩. In the interpretation of spiders, we use the notation |0 m ⟩ to represent an m-fold tensor of |0⟩. As a shortcut notation, we write |ϕ⟩ for column vectors consisting of a linear combinations of kets. Shortcut notations are also used for two very useful states: |+⟩ := |0⟩+|1⟩ √ 2 and |-⟩ := |0⟩-|1⟩ √ 2

Figure 1

 1 Figure 1 Connectivity rules. D represents any ZX-diagram, and σ, σ ′ any permutation of wires.

Theorem 3 ▶ Definition 4 (

 34 is essential: it allows us to transpose notions of graphs into ZX-Calculus. It is for instance possible to define a notion of connectivity. Connected Components). Let D be a non-empty ZX-diagram. Consider all of the possible decompositions with D 1 , ..., D k ∈ ZX and σ, σ ′ permutations of wires: largest such k is called the number of connected components of D. It induces a unique decomposition up to permutation of wires. The induced D 1 , ..., D n are called the connected components of D. If D has only one connected component, we say that D is connected. ▶ Definition 5 (Paths). Let D be a ZX-diagram. A path in D between the edges e 0 and e n is a sequence (e 0 , ..., e n ) of edges of D such that there exists a sequence (g 1 , ..., g n ) of atomic (generator) sub-diagrams of D,

▶

  We denote with Paths(e 0 , e n ) the set of paths between e 0 and e n in D, and Paths(D) the set of all paths in D. If Paths(e 0 , e n ) = ∅, we say that e 0 and e n are disconnected. Finally, the length of the path p = (e 0 , ..., e n ) is |p| = n. ▶ Definition 6 (Distance). Let e and e ′ be connected edges in a ZX-diagram D. We define: d(e, e ′ ) := min p∈Paths(e,e ′ ) Definition 7 (Cycles). A cycle is defined as a path (e 0 , ..., e n ) where e 0 = e n . We denote Cycles(D) the set of all cycles in D.

  This duplication is necessary to make sure we capture the whole linear map encoded by the ZX-diagram. Due to this duplication, two tokens might collide together when they are on the same edge and going in different directions. The result of such a collision will depend on the states held by both tokens. For a cup, cap or identity diagram, the token will simply traverse it. As for the Hadamard node the token will traverse it and become a superposition of two tokens with opposite states. Therefore, as tokens move through a diagram, some may be added, multiplied together, or annihilated. ▶ Definition 8 (Tokens and Token States). Let D be a ZX-diagram. A token in D is a triplet (e, d, b) ∈ E(D) × {↓, ↑} × {0, 1}. We shall omit the commas and simply write (e d b). The set of tokens on D is written tk(D). A token state s is then a multivariate polynomial over C, evaluated in tk(D). We define tkS(D) := C[tk(D)] the algebra of multivariate polynomials over tk(D).

  are called the terms of t. A monomial (e 1 d 1 , b 1 ) • • • (e n d n , b n ) encodes the state of n tokens in the process of flowing in the diagram D. A token state is understood as a superposition -a linear combinationof multi-tokens flowing in the diagram.

Definition 14 (

 14 Polarity of a Term in a Path). Let D be a ZX-diagram, and p ∈ Paths(D) be a path in D. Let t = (e, d, x) ∈ tk(D). Then:

Proposition 26 can▶

 26 be made more general. However, we first need the following result on ZX-diagrams: ▶ Lemma 27 (Universality of Connected ZX-Diagrams). Let f : C 2 n → C 2 m . There exists a connected ZX-diagram D f : n → m such that D f = f . ◀ Proposition 28 (Multi-Token Input). Let D be a connected ZX-diagram with I(D) = [a i ] 1≤i≤n and O(D) = [b i ] 1≤i≤m ; with n ≥ 1.

e▶ Example 31 .e 2iπ y 0 y 1 2 (e 0

 3120 2iπP (⃗ y) (p 0 , d 0 , B 0 (⃗ y))...(p m-1 , d m-1 , B m-1 (⃗ y))We denote the set of SOP-token-states on D by tkS SOP (D). Let D = ↑ y 0 )(e 1 ↓ y 1 ) ∈ tkS SOP (D).

2 0 1 6 23: 12

 612 Geometry of Interaction for ZX-Diagramse0

▶ Example 34 .

 34 Let us compare the behavior of the previous token machine to the SOP machine. We send tokens in states 0 and 1 down the wire a in the diagram a b c

▶ Proposition 36 .

 36 Let D ∈ ZX and s, s ′ ∈ tkS SOP(D) such that all Boolean polynomials B j in s are reduced to a single term of degree ≤ 1, and such that s ⇝ sop s ′ . Then, the size of s ′ is bounded by: S(s ′ ) ≤ S(s) + ∆(D) where S denotes the cumulative number of terms in the phase polynomial and the number of tokens in the token-state, and where ∆(D) represents the maximum arity of generators in D. ◀

  denote with ZX the set of diagrams obtained by adding to the usual generators of the ZX-Calculus. Similar to what is done in quantum computation, the standard interpretation . for ZX maps diagrams to CPMs. If D ∈ ZX we define D as ρ → D † • ρ • D , and we set as ρ → Tr(ρ), where Tr(ρ) is the trace of ρ.

2 0 1 6 23: 14

 614 Geometry of Interaction for ZX-Diagrams ▶ Example 37. A ZX -diagram and its associated CPM construction is shown on the right.

References1

  Matthew Amy. Towards large-scale functional verification of universal quantum circuits. In Peter Selinger and Giulio Chiribella, editors, Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3-7th June 2018, volume 287 of EPTCS, pages 1-21, 2018. doi:10.4204/EPTCS.287.1.

  x1,i,q 1 |y 1,1,q1 , ..., y 1,m1,q1 ⟩ +n k -1q k λ q k ,k i δ x,x k,i,q k |y k,1,q1 , ..., y k,m1,q k ⟩ |y 1,1,q1 , ..., y 1,m1,q1 ⟩ ⊗ ... ⊗ 2 m k

  It is hence possible to connect every different connected components of a diagram in a way that preserves the semantics. ◀ Proof of Proposition 28. Using Lemma 27, there exists a connected ZX-diagram D ′ with I(D ′ ) = [a ′ ] and such that D ′ |0⟩ = 2 nq=1 λ q |x 1,q , ..., x n,q ⟩. Consider now a derivation from the token state (a ′ ↓ 0) in D • D ′ :

  i ↓ y i,q ) in D. ◀ Proof of Theorem 29. First, let us single out e in the diagram D = build a second diagram by cutting e in half and seeing each piece of wire as an input and an

DB Proof of Section 4 Proof of Proposition 35 .

 435 ′ is now disconnected: Since D was connected, the two connected components of D were connected through e. Hence, D ′ only has two connected components, one connected to e 0 and the other to e 1 . By applying Proposition 26 to both connected components, we get the desired result.◀ By a straightforward induction on ⇝ sop . ◀

  2 n → C 2 m (by abuse of notation we shall use the notation D : n → m). It is defined inductively as follows.

	...
	D 1 ... ... D 2	=	... ... D 2 •	... ... D 1	... ... D 1	... ... D 2	=	... ... D 1 ⊗	... ... D 2

Table 1

 1 Asynchronous token-state evolution, for all x, b ∈ {0, 1}

0 1 6 23:10 Geometry of Interaction for ZX-Diagrams Intuitively

  In the following, we shall simply refer to such subterms as "terms of t". In the (piece of) diagram presented on the right, the blue directed line p = (e 0 , e 1 , e 2 , e 3 , e 4 ) is a path. The orientation of the edges in the path is represented by the arrow heads, and e 3 for instance is ↓-oriented in p which implies that we have P (p, (e 3 ↑ x)) = -1. We say that s is well-formed if for every term t in s and every path p ∈ Paths(D) we have P (p, t) ∈ {-1, 0, 1}.▶ Proposition 17 (Invariance of Well-Formedness). Well-formedness is preserved by (⇝): if s ⇝ * s ′ and s is well-formed, then s ′ is well-formed.To show that being cycle-balanced implies termination, we need the following intermediate lemma. This essentially captures the fact that a token in the diagram comes from some other token that "traveled" in the diagram earlier on. , this means that tokens inside a cycle will cancel themselves out if the token state is cycle-balanced. Since cycles are the only way to have a non-terminating token machine, we are sure that our machine will always terminate.

	e0 ▶ Proposition 23 (Local Confluence). Let D be a ZX-diagram, and s ∈ tkS(D) be well-e2 e3 e4 formed and collision-free. Then, for all s 1 , s 2 ∈ tkS(D) such that s 1 ⇝ s ⇝ s 2 , there exists
	s ′ ∈ tkS(D) such that s 1 ⇝ * s ′ *	⇝	s 2 .	e1	◀
	▶ Corollary 24 (Confluence). Let D be a ZX-diagram. The rewrite system ⇝ is confluent
	for well-formed and cycle-balanced token states.		◀
	▶ Corollary 25 (Uniqueness of Normal Forms). Let D be a ZX-diagram. A well-formed and
	cycle-balanced token state admits a unique normal form under the rewrite system ⇝.	◀

and e is d-oriented -1 if e ∈ p and e is ¬d-oriented 0 if e / ∈ p We extend the definition to subterms α t 1 ...t m of a token-states t: P (p, 0) = P (p, 1) = 0, P (p, α t 1 ...t m ) = P (p, t 1 ) + ... + P (p, t m ). ▶ Example 15. ▶ Definition 16 (Well-formedness). Let D be a ZX-diagram, and s ∈ tkS(D) a token state on D. ◀ Well-formedness prevents the unwanted scenario of having two tokens on the same wire, and oriented in the same direction (e.g. (e 0 ↓ x)(e 0 ↓ y)). As shown in the Proposition 18, this property is in fact stronger. ▶ Proposition 18 (Full Characterisation of Well-Formed Terms). Let D be a ZX-diagram, and s ∈ tkS(D) be not well-formed, i.e. there exists a term t in s, and p ∈ Paths(D) such that |P (p, t)| ≥ 2. Then we can rewrite s ⇝ s ′ such that a term in s ′ has a product of at least two tokens of the form (e 0 , d, _). ◀ Although well-formedness prevents products of tokens on the same wire, it does not guarantee termination: for this we need to consider polarities along cycles. ▶ Proposition 19 (Invariant on Cycles). Let D be a ZX-diagram, and c ∈ Cycles(D) a cycle. Let t 1 , . . . , t n be tokens, and s be a token state such that t 1 ...t n ⇝ * s. Then for every non-null term t in s we have P (c, t 1 ...t n ) = P (c, t). ◀ This proposition tells us that the polarity is preserved inside a cycle. By requiring the polarity to be 0, we can show that the token machine terminates. This property is defined formally in the following. ▶ Definition 20 (Cycle-Balanced Token State). Let D be a ZX-diagram, and t a term in a token state on D. We say that t is cycle-balanced if for all cycles c ∈ Cycles(D) we have P (c, t) = 0. We say that a token state is cycle-balanced if all its terms are cycle-balanced. ▶ Lemma 21 (Rewinding). Let D be a ZX-diagram, and t be a term in a well-formed token state on D, and such that t ⇝ * i λ i t i , with (e n , d, x) ∈ t 1 . If t is cycle-balanced, then there exists a path p = (e 0 , ..., e n ) ∈ Paths(D) such that e n is d-oriented in p, and P (p, t) = 1. ◀ We can now prove strong-normalization. ▶ Theorem 22 (Termination of well-formed, cycle-balanced token state). Let D be a ZXdiagram, and s ∈ tkS(D) be well-formed. The token state s is strongly normalizing if and only if it is cycle-balanced. ◀ C V I T 2

Table 2

 2 Rewrite rules for ⇝sop.

The provided rewrite rules do not give the full picture, for simplicity. If a rule gives

(e, d, b) ⇝ sop s ′ ⃗ y ′ e 2iπP ′ j (e ′ j , d ′ j , b ′ j ),

we have to apply it to a full SOP-token-state as follows: s ⃗ y e 2iπP (e, d, b)

  where ⃗ y := (y i ) 0≤i<n are variables from a set of variables V.

We denote the set of SOP -tokens on D with variables ⃗ y by tk SOP (D)[⃗ y]. Similar to what was done in Definition 30, a SOP -token-state is a quadruplet

  and t 1 , t 2 ∈ tkS SOP(D). Then whenevert 1 ⇝ t 2 we have CPM(t 1 ) ⇝In fact, the ⇝ rewriting rule will only be simulated by 2 rewriting rules (⇝ sop ), except in the case of the Trace-out where (⇝ sop ) only needs to apply one rule.Again, the notions of polarity, well-formedness and cycle-balancedness can be adapted, and again, we get strong normalization(Theorem 22), confluence (Corollary 24), and uniqueness of normal forms (Corollary 25) for well-formed and cycle-balanced token states.

	{1,2} sop CPM(t 2 ).	◀

2 0 1 6 23:22 Geometry of Interaction for ZX-Diagrams

	which is the expected result.
	...
	Now, if D = D ′ ...
		a
		α
	D = D ′ ... ... α	... a1,1 a1,n 1 a k,1 ... a k,n k = ... D 1 ... σ ... D k ... b1 bm bm 1 bm-m k
	with D i connected. Then:

α

, we can decompose D ′ in its connected components:

A

Proofs of Section 3

Proof of Proposition 17. Let D be a ZX-diagram, and s be a well-formed token state on D.

Let t be a term of s, and e 0 be the edge where a rewriting occurs. If the rewriting does not affect t, then the well-formedness of t obviously holds. If it does, and t ⇝ c,d q t q , we have to check two cases:

Collision: let p ∈ Paths(D). If no tokens remain in the term t q , then P (p, t q ) = 0.

Otherwise:

if e 0 / ∈ p, then P (p, t q ) = P (p, t)

if e 0 ∈ p, then P (p, t q ) = P (p, t) + 1 -1 because the two tokens have alternating polarity Diffusion: let p ∈ Paths(D), and (e 0 , d, x) ⇝ d q λ q i∈S (e i , d i , x i,q ) (this captures all possible diffusion rules). We can show that we can rewrite t into a token state with term t ′ = (e i , d, _)(e i , d, _)t ′′ . We do so by induction on n = |p| -1.

If n = 0, we have a path constituted of one edge, such that |P (p, t)| ≥ 2. Even after doing all possible collisions, we are left with |P (p, t)| tokens on e 0 , and oriented accordingly.

For n + 1, we look at e 0 , build p ′ := (e 1 , ..., e n ), and distinguish four cases. If there is no token on e 0 , we have P (p ′ , t) = P (p, t), so the result is true by induction hypothesis on p ′ . If we have a product of at least two tokens going in the same direction, the result is directly true. If we have exactly one token going in each direction, we apply the collision rules, and still have P (p ′ , t) = P (p, t), so the result is true by induction hypothesis on p ′ .

Finally, if we have exactly one token (e 0 , d, _) on e 0 , either e 0 is not d-oriented, in which case P (p ′ , t) = P (p, t) + 1, or e 0 is d-oriented, in which case the adequate diffusion rule on (e 0 , d, _) will rewrite t ⇝ q t q with P (p ′ , t q ) = P (p, t). ◀

Proof of Proposition 19. The proof can be adapted from the previous one, by forgetting the cases related to the extremity of the paths, as well as the null terms (which can arise

23:19

from collisions). It can then be observed that the quantity P in this simplified setting is more than bounded to {-1, 0, 1}, but preserved. ◀ Proof of Lemma 21. We reason by induction on the length k of the rewrite that leads from

If k = 0, we have (e n , d, x) ∈ t, so the path p := (e n ) is sufficient.

For k + 1, suppose t ⇝ i λ i t i , and

with (e n , d, x) ∈ t ′ 1 . By induction hypothesis, there is p = (e 0 , ..., e n ) such that P (p, t 1 ) = 1.

We now need to look at the first rewrite from t. However, e :: p may not be a path anymore. If c = (e, e 0 , ..., e ℓ ) forms a cycle, then, since P (c, t) = 0, we can simply keep the path p ′ := (e ℓ+1 , ..., e n ) with P (p ′ , t) = 1 ◀ Proof of Theorem 22.

[⇒]: Suppose ∃c ∈ Cycles(D) and t a term of s such that P (c, t) ̸ = 0. By well-formedness, P (c, t) ∈ {-1, 1}. Any terminal term t ′ has P (c, t ′ ) = 0, so by preservation of the quantity P (c, _), t (and henceforth s) cannot terminate.

[⇐]: We are going to show for the reciprocal that, if t is well-formed, and if the constraint P (c, t) = 0 is verified for every cycle c, then any generator in the diagram can be visited at most once. More precisely, we show that if a generator is visited in a term t, then it cannot be visited anymore in all the terms derived from t. However, the same generator can be visited once for each superposed term (e.g. once in t 1 and once in t 2 for the token state

Consider an edge e with token exiting generator g in the term t. Suppose, by reductio ad absurdum, that a token will visit g again in t ′ (obtained from t), by edge e n with orientation d.

By Lemma 21, there exists a path p = (e 0 , ..., e n ) such that P (p, t) = 1 and e n is d-oriented.

23:25

Proof of Proposition 36. Let D ∈ ZX and s ∈ tkS SOP (D) such that its B j ∈ {0, 1, y} y∈V for all j. Note that all collisions at worst do not change the size of the term (at best reduce the size). Indeed, we turn two tokens into at most two terms in the phase polynomial, since

) because we work modulo 1 in the phase polynomial.

Hence, since a rewrite step consists in a diffusion step followed by some collision rule,

showing the result only for diffusions is enough.

Diffusions through Cups and Caps do not change the size.

A diffusion through H adds a single term in the phase polynomial. However, since H is in the diagram, ∆(D) ≥ 2, so the proposition holds.

A diffusion through a Green-spider with arity δ adds δ -2 tokens, and a single term in the phase polynomial. However, δ ≤ ∆(D).

◀

C Proof of Section 5

Proof of Theorem 39. Diffusion rules are trivial. Beware in the case of the Ground, as the CPM will produce a cup, the ⇝ does not produce a new token when applying the Trace-Out rule, meanwhile the ⇝ sop machine will do two rewriting rules to pass through the cup. ◀