Guillaume Bonfante
email: guillaume.bonfante@loria.fr

Yves Guiraud
email: yves.guiraud@loria.fr

Adam Cichon

Pierre Lescanne

Polygraphic programs and polynomial-time functions

Keywords: Polygraph, Polygraphic program, Polygraphic interpretation, Computability, Complexity, Polynomial time. ACM -F.1.1, F.4 [],[]) | x::[] -> (x::[],[]) | x::y::l -> let (l1,l2)=split

come

In a polygraph, one can consider, at the same level as other operations, function symbols with many outputs. For example, the above definition of the split function becomes, in the polygraphic language:

With these rules, one can actually "see" how the computation is made, by "unzipping" lists. Also, one can internalize in polygraphs the sharing operation of termgraphs [START_REF] Plump | Term graph rewriting, Handbook of Graph Grammars and Computing by Graph Transformation[END_REF], described as an explicit and local duplication. As a consequence, the rules generating computations become linear: the operations for pointers management can be "seen" within the rules. Actually, in our analysis, we evaluate explicitly the number of structural steps of computation: allocations, deallocations and switches of pointers. In other words, we make explicit the design of a garbage collector. The question of sharing has been widely studied for efficient implementations of functional programming languages and several solutions have been found: for instance, Dan Dougherty, Pierre Lescanne and Luigi Liquori proposed the formalism of addressed term rewriting systems [START_REF] Dougherty | Addressed term rewriting systems: application to a typed object calculus[END_REF]. Let us mention another approach for this kind of issues due to Martin Hofmann [START_REF] Hofmann | A type system for bounded space and functional in-place update[END_REF]: he developed a typing discipline, with a diamond type, for a functional language which allows a compilation into an imperative language such as C, without dynamic allocation.

The computational model of polygraphic programs, a subclass of polygraphs, is explained in the first part of this document, where we give their semantics and prove a completeness result: every Turingcomputable function can be computed by a polygraphic program.

Complexity analysis of polygraphic programs -Here we use tools inspired by polynomial interpretations, which have been introduced by Dallas Lankford to prove termination of term rewriting systems [START_REF] Lankford | On proving term rewriting systems are noetherian[END_REF]. They associate to each term a polynomial with natural numbers as coefficients, in a way that is naturally compatible with contexts and substitutions. When, for each rule, the interpretation of the lefthand side is greater than the one of the right-hand side, one gets a termination proof. For example, let us consider the following term rewriting system that computes the double function on natural numbers:

d(0) → 0 d(s(x)) → s(s(d(x))).
One proves its termination with the interpretation defined by ϕ(0) = 1, ϕ(s(x)) = ϕ(x) + 1 and ϕ(d(x)) = 3ϕ(x). Indeed, one checks that the following inequalities hold:

have considered more precisely the computational power of these systems [START_REF] Cichon | Polynomial interpretations and the complexity of algorithms[END_REF]. Adam Cichon, Jean-Yves Marion and Hélène Touzet, with the first author, have identified complexity classes by means of restrictions on polynomial interpretations [START_REF] Bonfante | Complexity classes and rewrite systems with polynomial interpretation[END_REF][START_REF]Algorithms with polynomial interpretation termination proofs[END_REF].

Let us explain how this works on the example of the double function. The given interpretation sends the term d(s n (0)) to the natural number 3n + 3: since each rule application will strictly decrease this number, one knows that it takes at most 3n + 3 steps to get from this term to its normal form s 2n (0). Actually, the considered interpretation gives a polynomial bound, with respect to the size of the argument, on the time taken to compute the double function with this program.

In order to analyze polygraphs, we use algebraic tools called polygraphic interpretations, which have been introduced to prove termination of polygraphs [START_REF]Termination orders for 3-dimensional rewriting[END_REF]. Intuitively, one considers that circuits are crossed by electrical currents. Depending on the intensity of the currents that arrive to it, each circuit gate produces some heat. Then one compares circuits according to the total heat each one produces. Building a polygraphic interpretation amounts at fixing how currents are transmitted by each gate and how much heat each one emits.

The current part is called a functorial interpretation. Algebraically, it is similar to a polynomial interpretation of terms and we also use it as an estimation of the size of values, like quasi-interpretations [START_REF] Bonfante | Quasi-interpretations: a way to control resources[END_REF]. The heat part is called a differential interpretation and it is specific to the algebraic structure of polygraphs. We use it to bound the number of computation steps remaining before reaching a result. Let us note that the distinction between these two parts makes it possible for polygraphic interpretations to cope with non-simplifying termination proofs, like Thomas Arts and Jürgen Giesl's dependency pairs [START_REF] Arts | Termination of term rewriting using dependency pairs[END_REF].

However, some new difficulties arise with polygraphs. For example, since duplication and erasure are explicit in our model, we must show how to get rid of them for the interpretation. In our setting, the programmer focuses on computational steps (as opposed to structural steps) for which he has to give an interpretation. From this interpretation, we give a polynomial upper bound on the number of structural steps that will be performed.

In this work, we focus on polynomial-time computable functions or, shorter, FPTIME functions. The reason comes from Stephen Cook's thesis stating that this class corresponds to feasible computable functions. But it is strongly conjectured that the preliminary results developed in this paper can be used for other characterizations. In particular, the current interpretations can be seen as sup-interpretations, following [START_REF] Marion | Resource analysis by sup-interpretation[END_REF]: this means that values have polynomial size.

Coming back to FPTIME, in the field of implicit computational complexity, the notion of stratification has shown to be a fundamental tool of the discipline. This has been developed by Daniel Leivant and Jean-Yves Marion [START_REF] Leivant | A foundational delineation of computational feasability[END_REF][START_REF] Leivant | Lambda-calculus characterizations of poly-time[END_REF] and by Stephen Bellantoni and Stephen Cook [START_REF] Bellantoni | A new recursion-theoretic characterization of the poly-time functions[END_REF] to delineate FPTIME. Other characterizations include Neil Jones' "Life without cons" WHILE programs [START_REF]Logspace and ptime characterized by programming languages[END_REF] and Karl-Heinz Niggl and Henning Wunderlich's characterization of imperative programs [START_REF] Niggl | Certifying polynomial time and linear/polynomial space for imperative programs[END_REF]. There is also a logical approach to implicit computational complexity, based on a linear type discipline, in the seminal works of Jean-Yves Girard on light linear logic [START_REF] Girard | Light linear logic[END_REF], Yves Lafont on soft linear logic [START_REF]Soft linear logic and polynomial time[END_REF] or Patrick Baillot and Kazushige Terui [START_REF] Baillot | Light types for polynomial time computation in lambda-calculus[END_REF].

The second part of this document is devoted to general results about polygraphic interpretations of polygraphs. There, we explore the pieces of information they can give us about size issues. Then, in the third part, we apply these results to polygraphic programs. In particular, we identify a subclass P of these objects that compute exactly the functions that can be computed in polynomial-time by a Turing machine, or FPTIME functions for short.

A computational model based on polygraphs

General notations -Throughout this document, we use several notations that we prefer to group here for easier further reference.

If X is a set and p is a natural number, we denote by X p the cartesian product of p copies of X. If X is an ordered set, we equip X p with the product order, which is defined by (x 1 , . . . , x p ) ≤ (y 1 , . . . , y p ) whenever x i ≤ y i holds for every i ∈ {1, . . . , p}.

If f : X → X and g : Y → Y are maps, then f × g denotes the product map from X × X to Y × Y . Let f, g : X → Y be two maps. If Y is equipped with a binary relation , then one compares f and g pointwise, which means that f g holds when, for every x ∈ X, one has f(x) g(x) in Y. Similarly, if Y is equipped with a binary operation , then one defines f g as the map from X to Y sending each x of X to the element f(x) g(x) in Y.

The sets N of natural numbers and Z of integers are always assumed to be equipped with their natural order. For every n in N, we denote by µ n the maximum map max {x 1 , . . . , x n } and by N[x 1 , . . . , x n ] the set of polynomials over n variables and with coefficients in N. If f : N m → N n is a map and if k ∈ N, one denotes by kf the map sending (x 1 , . . . , x m ) to (ky 1 , . . . , ky n ), if (y 1 , . . . , y n ) is f(x 1 , . . . , x m ).

A computational model based on polygraphs 1.A first glance at polygraphs

On a first approach, one can consider polygraphs as rewriting systems on algebraic circuits, made of: Types -They are the wires, called 1-cells. Each one conveys information of some elementary type. To represent product types, one uses several wires, in parallel, calling such a construction a 1-path. For example, the following 1-path represents the type of quadruples made of an integer, a boolean, a real number and a boolean:

int bool real bool
The 1-paths can be composed in one way, by putting them in parallel:

v u v = 0 u
Operations -They are represented by circuits, called 2-paths. The gates used to build them are called 2-cells. The 2-paths can be composed in two ways, either by juxtaposition (parallel composition) or by connection (sequential composition):

1 = f f g g 0 f g = f g
Each 2-path (or 2-cell) has a finite number of typed inputs, a 1-path called its 1-source, and a finite number of typed outputs, a 1-path called its 1-target:

t 1 (f) f s 1 (f)

A first glance at polygraphs

Several constructions represent the same operation. In particular, wires can be stretched or contracted, provided one does not cross them or break them. This can be written either graphically or algebraically:

≡ f f f g g g ≡ f 0 s 1 (g) 1 t 1 (f) 0 g ≡ f 0 g ≡ s 1 (f) 0 g 1 f 0 t 1 (g) .
Computations -They are rewriting paths, called 3-paths, transforming a given 2-path, called its 2source, into another one, called its 2-target. The 3-paths are generated by local rewriting rules, called 3-cells. The 2-source and the 2-target of a 3-cell or 3-path are required to have the same input and output, i.e. the same 1-source and the same 1-target. A 3-path is represented either as a reduction on 2-paths or as a genuine 3-dimensional object:

t 2 (F) : F s 2 (F) s 2 (F) F t 1 (F) t 2 (F) s 1 (F)
The 3-paths can be composed in three ways, two parallel ones coming from the structure of the 2-paths, plus one new, sequential one:

F s 2 (F) s 2 (G) t 2 (F) t 2 (G) : = F 0 G G G s 2 (F) s 2 (G) t 2 (F) t 2 (G) : = F 1 G F G s 2 (F) t 2 (G) : = F 2 G F
The 3-paths are identified modulo relations that include topological moves such as:

≡ ≡ ≡ ≡ ≡ ≡
These graphical relations have an algebraic version given, for 0 ≤ i < j ≤ 2, by:

F i s j (G) j t j (F) i G ≡ F i G ≡ s j (F) i G j F i t j (G) .

A computational model based on polygraphs

So far, we have described a special case of 3-polygraphs. A n-polygraph is a similar object, made of cells, paths, sources, targets and compositions in all dimensions up to n.

Remark. Polygraphs provide a uniform, algebraic and graphical description of objects coming from different domains: abstract, string and term rewriting systems [START_REF]Towards an algebraic theory of boolean circuits[END_REF][START_REF] Guiraud | Présentations d'opérades et systèmes de réécriture[END_REF][START_REF]Termination orders for 3-dimensional rewriting[END_REF], abstract algebraic structures [START_REF] Burroni | Higher-dimensional word problems with applications to equational logic[END_REF][START_REF] Guiraud | Présentations d'opérades et systèmes de réécriture[END_REF][START_REF] Loday | Generalized bialgebras and triples of operads[END_REF], Feynman and Penrose diagrams [START_REF] Baez | A history of n-categorical physics[END_REF], braids, knots and tangles diagrams equipped with the Reidemeister moves [START_REF] Adams | The knot book[END_REF][START_REF] Guiraud | Présentations d'opérades et systèmes de réécriture[END_REF], Petri nets [START_REF]Two polygraphic presentations of Petri nets[END_REF] and propositional proofs of classical and linear logics [START_REF]The three dimensions of proofs[END_REF].

Polygraphs

On a first reading, one can skip the formal definition of polygraph and just keep in mind the graphical introduction. We define n-polygraphs by induction on the dimension n: given a definition of (n -1)polygraphs, we define a n-polygraph as a base (n -1)-polygraph extended with a set of n-cells. Let us initiate the induction with 0-polygraphs and 1-polygraphs.

Definition 1.2.1. A 0-polygraph is a set P. Its 0-cells and 0-paths are its elements.

Definition 1.2.2. A 1-polygraph is a data P = (B, P 1 , s, t) made of a 0-polygraph B, a set P 1 and two maps s and t from P 1 to B. The 0-cells and 0-paths of P are the ones of B. Its 1-cells are the elements of P 1 . One inductively defines the set P 1 of 1-paths of P, together with the 0-source map s 0 and the 0-target map t 0 , both from 1-paths to 0-paths, as follows:

• Every 0-cell x is a 1-path, with s 0 (x) = t 0 (x) = x.
• Every 1-cell ξ is a 1-path, with s 0 (ξ) = s(ξ) and t 0 (ξ) = t(ξ).

• If u and v are 1-paths such that t 0 (u) = s 0 (v), then u 0 v is a 1-path called the 0-composition of u and v. One defines s 0 (u 0 v) = s 0 (u) and t 0 (u 0 v) = t 0 (v).

The 1-paths are identified modulo the following relations:

• Associativity: (u 0 v) 0 w = u 0 (v 0 w) .

• Local units: s 0 (u) 0 u = u = u 0 t 0 (u) .

Example 1.2.3. A graph yields a 1-polygraph, with vertices as 0-cells and arrows as 1-cells. The 1-paths are the paths in the graph.

Example 1.2.4. A set X can be seen as a 1-polygraph, with one 0-cell and itself as set of 1-cells: in that case, the set X of 1-paths is exactly the free monoid generated by X or, equivalently, the set of words over the alphabet X.

Example 1.2.5. An abstract rewriting system is a binary relation R over a set X. Such an object yields a 1-polygraph P with P 0 = X, P 1 = R, s 0 (x, y) = x and t 0 (x, y) = y. Then, the 1-paths of this 1-polygraph are in bijective correspondence with the rewriting paths generated by (X, R).

Now, let us fix a natural number n ≥ 2 and assume that one has defined what a (n -1)-polygraph P is, how one builds its sets P k of k-cells and P k of k-paths, k ∈ {0, . . . , n}, and its j-source map s j and j-target map t j from P k to P j , j ∈ {0, . . . , k -1}.

Polygraphs

Definition 1.2.6. An n-polygraph is a data P = (B, P n , s, t) made of an (n -1)-polygraph B, a set P n and two maps s and t from P n to B n-1 , such that the globular relations hold:

s n-2 • s = s n-2 • t and t n-2 • s = t n-2 • t.
For every k in {0, . . . , n -1}, the k-cells and k-paths of P are the ones of B. The n-cells of P are the elements of P n . One inductively defines the set P n of n-paths of P, the (n -1)-source map s n-1 , the (n -1)-target map t n-1 and, for every k ∈ {0, . . . , n -2}, extensions to n-paths of the k-source map s k and the k-target map t k of B:

• For every k ∈ {0, . . . , n -1}, every k-cell ξ is an n-path, with s n-1 (ξ) = t n-1 (ξ) = ξ.
Values of other source and target maps do not change.

• Every n-cell ϕ is an n-path, with s n-1 (ϕ) = s(ϕ) and t n-1 (ϕ) = t(ϕ). If k ∈ {0, . . . , n -2}, then s k and t k are respectively extended by

s k (ϕ) = s k • s n-1 (ϕ) and by t k (ϕ) = t k • t n-1 (ϕ).
• If k ∈ {0, . . . , n -1} and if f and g are n-paths such that t k (f) = s k (g) holds, then f k g is an n-path called the k-composition of f and g. For j ∈ {0, . . . , n -2}, one defines:

s j (f k g) = s j (f) if j ≤ k s j (f) k s j (g) if j > k and t j (f k g) = t j (g) if j ≤ k t j (f) k t j (g) if j > k.
One does not distinguish two n-paths that only differ by the following relations:

• Associativity: (f k g) k h = f k (g k h), for 0 ≤ k ≤ n -1. • Local units: s k (f) k f = f = f k t k (f), for 0 ≤ k ≤ n -1. • Exchange: (f 1 j f 2 ) k (g 1 j g 2 ) = (f 1 k g 1 ) j (f 2 k g 2 ), for 0 ≤ j < k ≤ n -1.
Example 1.2.7. Let us consider a word rewriting system (X, R), made of set X and a binary relation R over X . From it, one builds a 2-polygraph P with one 0-cell, P 1 = X, P 2 = R, s 1 (u, v) = u and t 1 (u, v) = v. There is a bijection between the 2-paths of P and the rewriting paths generated by (X, R), considered modulo the commutation squares between two non-overlapping rule applications. Moreover the circuit-like pictures provide graphical representations for word rewriting: wires are letters, gates are applications of rewriting rules and circuits are traces of computations.

Example 1.2.8. Term rewriting systems generate 3-polygraphs, as explained by Albert Burroni [START_REF] Burroni | Higher-dimensional word problems with applications to equational logic[END_REF], Yves Lafont [START_REF]Towards an algebraic theory of boolean circuits[END_REF] and the second author [START_REF]Termination orders for 3-dimensional rewriting[END_REF][START_REF]The three dimensions of proofs[END_REF]. The polygraphic programs one considers here are light versions of these [START_REF]Polygraphs for termination of left-linear term rewriting systems[END_REF].

Example 1.2.9. Petri nets correspond exactly to 3-polygraphs with one 0-cell and no 1-cell: one identifies places with 2-cells and transitions with 3-cells [START_REF]Two polygraphic presentations of Petri nets[END_REF]. Definition 1.2.10. Let us fix a natural number n and an n-polygraph P. The polygraph P is finite when it has a finite number of cells in every dimension. A family X of n-cells of P can be seen as an n-polygraph with the same cells as P up to dimension n -1.

A computational model based on polygraphs

If 0 ≤ j < k ≤ n, two k-paths f and g are j-composable when t j (f) = s j (g). They are j-parallel when s j (f) = s j (g) and t j (f) = t j (g). When j = k -1, one simply says composable and parallel. Similarly, the (k -1)-source and (k -1)-target of a k-path are simply called its source and target.

If 0 ≤ k ≤ n, given a subset X of P k and a k-path f, the size of f with respect to X is the natural number denoted by ||f|| X and defined as follows, by structural induction on f:

||f|| X =      0 if f is a cell and f / ∈ X, 1 if f ∈ X, ||g|| X + ||h|| X if f = g j h, for some 0 ≤ j < k.
When X is reduced to one cell ϕ, one writes ||f|| ϕ instead of ||f|| {ϕ} . The size of f is its size with respect to P k , simply written ||f||. A k-path is degenerate when it has size 0 and elementary when its size is 1.

Remark. One must check that the definition of the size of a k-path (with respect to a set of k-cells X) is correct. This is done by computing this map on both sides of the relations of associativity, local units and exchange and ensuring that both results are equal.

One proves that any non-degenerate k-path f of size p can be written

f = f 1 k-1 • • • k-1 f p ,
where each f i is an elementary k-path. Moreover, if k ≥ 1, then any elementary k-path f can be written as follows:

f = g k k-1 g k-1 k-2 • • • 1 (g 1 0 ϕ 0 h 1 ) 1 • • • k-2 h k-1 k-1 h k ,
where ϕ is a uniquely defined k-cell, while g j and h j are j-paths, for every j ∈ {1, . . . , k}. For example, any elementary 3-path F can be decomposed as F = f 1 (u 0 α 0 v) 1 g, where α is a uniquely determined 3-cell, f and g are 2-paths, u and v are 1-paths. As a consequence:

g s 2 F = u v s 2 α f t 2 F = u v t 2 α f g s 2 F = f 1 (u 0 s 2 α 0 v) 1 g t 2 F = f 1 (u 0 t 2 α 0 v) 1 g
In order to study the computational properties of polygraphs, we use notions of higher-dimensional rewriting theory [START_REF]Termination orders for 3-dimensional rewriting[END_REF] that, in turn, make reference to abstract rewriting ones [START_REF] Baader | Term rewriting and all that[END_REF].

Definition 1.2.11. The reduction graph associated to an n-polygraph P is the graph with (n -1)-paths of P as objects and elementary n-paths of P as arrows. Rewriting notions of normal forms, termination, (local) confluence, convergence, etc. are defined on P by taking back the ones of its reduction graph.

Remark. One can check that, given two parallel (n -1)-paths f and g in an n-polygraph P, there exists a path from f to g in the reduction graph of P if and only if there exists a non-degenerate n-path F with source f and target g in P.

In what follows, we focus on 3-polygraphs and introduce some special notions and notations for them.

Definition 1.2.12. Let P be a 3-polygraph. The fact that f is a k-path of P with source x and target y is denoted by f : x → y when k = 1, by f : x ⇒ y when k = 2, by f : x y when k = 3. If f is a k-path of P and X a family of k-cells then, instead of ||f|| X , one writes |f| X when k = 1 and |||f||| X when k = 3. When f : x ⇒ y, then |x|, |y| and (|x| , |y|) are respectively called the arity, the coarity and the valence of f. • The set P S 2 is made of the following elements, called structure 2-cells, where ξ and ζ range over the set of 1-cells of P:

ξ,ζ : ξ 0 ζ ⇒ ζ 0 ξ, ξ : ξ ⇒ ξ 0 ξ, ξ : ξ ⇒ * .
When the context is clear, one simply writes , and . The following elements of P S 2 are called structure 2-paths and they are defined by structural induction on their 1-source:

* * ξ = ξ * ξ = ξ = ξ 0 x ζ ζ ξ x x 0 ξ x ξ * = * = = ξ x = x 0 ξ ζ ζ ξ x * x 0 ξ = • The set P C
2 is made of 2-cells with coarity 1, i.e. of the shape , called constructor 2-cells.

• The elements of P F 2 are called function 2-cells.

• The elements of P S 3 , called structure 3-cells, are defined, for every constructor 2-cell : x ⇒ ξ and every 1-cell ζ, by:

x ζ ζ ξ ζ x ξ ζ x ξ ξ x ξ ξ x x x ζ ζ ξ x ζ ξ ζ
• The elements of P R 3 are called computation 3-cells and each one has a 2-source of the shape t 1 , with t ∈ P C 2 and ∈ P F 2 .

Remark. In this study, we have decided to split structure cells from computation cells. From a traditional programming perspective, permutations, duplications and erasers are given for free in the syntax. With polygraphs, this is not the case. However, by putting these operations in a "special" sublayer, we show that the programmer has not to bother with structure cells: one can stay at the top-level, letting the sublevel work on its own. 1. Its 1-cells are n, for natural numbers, and l, for lists of natural numbers.

2. Its 2-cells are made of eight structure 2-cells, plus:

(a) Constructor 2-cells, for the natural numbers 0, . . . , N, the empty list and the list constructor:

n : * ⇒ n 0≤n≤N , : * ⇒ l, : n 0 l ⇒ l.
(b) Function 2-cells, respectively for the main sort and the two auxiliary split and merge:

: l ⇒ l, : l ⇒ l * 0 l, : l * 0 l ⇒ l.
3. Its 3-cells are made of 6N + 18 structure 3-cells, plus N 2 + 2N + 8 computation 3-cells:

p > q p q p q p q p q p ≤ q

Remark. One may object that sorting lists when the a priori bound N is known can be performed in a linear number of steps: one reads the list and counts the number of occurrences of each element, then produces the sorted list from this information. Nevertheless, the presented algorithm (up to the test ≤ on the natural numbers p and q) really mimics the "mechanics" of the fusion sort algorithm and, actually, we rediscover the complexity bound as given by Yiannis Moschovakis [START_REF] Moschovakis | What is an algorithm?[END_REF].

Why don't we internalize the comparison of numbers within the polygraphic program? This comes from the fact that the if-then-else construction implicitly involves an evaluation strategy: one first computes the test argument then, depending on this result, one computes exactly one of the other two arguments. As defined here, polygraphs algebraically describe the computation steps, but not the evaluation strategy. We let such a task for further research.

Semantics of polygraphic programs 1.4 Semantics of polygraphic programs

One defines an interpretation • of the elements of a polygraphic program into sets and maps, then one uses it to define the notion of function computed by such a program. Definition 1.4.1. Let P be a polygraphic program. For a 1-path u, a value of type u is a 2-path in P C 2 with source * and target u; their set is denoted by u . Given a 2-path f : u ⇒ v, one denotes by f the (partial) map from u to v defined as follows: if t is a value of type u and if t 1 f has a unique normal form t that is a value (of type v), then f (t) is t ; otherwise f is undefined on t.

Among the following properties, the one for degenerate 2-paths explains the fact that u has two meanings: it is either the set of values of type u or the identity of this set.

Proposition 1.4.2. Let P be a polygraphic program. The following properties hold on 1-paths:

• The set * is reduced to the 0-cell * .

• For every u and v, one has

u 0 v = u × v .
The following properties hold on 2-paths:

• If u is degenerate then it is sent by • to the identity of the set u .
• For every f and g, one has

f 0 g = f × g . • If f and g are composable, then f 1 g = g • f holds.
Finally, for every 3-path F, the equality s 2 F = t 2 F holds. Definition 1.4.3. Let P be a polygraphic program. Let u, v be 1-paths and let f be a (partial) map from u to v . One says that P computes f when there exists a 2-cell such that = f. Example 1.4.4. In a polygraphic program P, every constructor 2-cell with arity n satisfies the equality

(t 1 , . . . , t n ) = (t 1 0 • • • 0 t n ) 1 .
Since the right member is always a normal form, one can identify values of coarity 1 with the closed terms of a term algebra. Moreover, the polygraphic program P computes erasers, duplications and permutations on these terms, since (t) = * , (t) = (t, t) and (t, t ) = (t , t) hold.

Thus, every polygraphic program computes one total map for each of its structure and constructor 2-cells.

We give sufficient conditions to ensure that this is also the case on function 2-cells.

Definition 1.4.5. A polygraphic program P is complete if every 2-path of the form t 1 is reducible when t is a value and is a function 2-cell.

Proposition 1.4.6. Let P be a convergent and complete polygraphic program. Then, for every structure or function 2-cell

: u ⇒ v, the map : u → v is total.
Proof. We start by recalling that the structure 3-cells, alone, are convergent [START_REF]Termination orders for 3-dimensional rewriting[END_REF][START_REF]The three dimensions of proofs[END_REF]. Furthermore, they are orthogonal to the computation 3-cells and every 2-path of the shape t 1 is reducible when t is a value and is a structure 2-cell. Hence, as a polygraph, P is convergent and the 2-paths * ⇒ x that are in normal form are exactly the values of type x.

A computational model based on polygraphs

Example 1.4.7. Let us check that the polygraphic program D computes euclidean division. The set n is equipotent to the set N of natural numbers through the bijection 0 = and n + 1 = n 1 . This polygraphic program is weakly orthogonal, hence locally confluent, and complete. We will also see later that it terminates. Thus it computes two maps from n 0 n N 2 to n N, one for and one for . By induction on the arguments, one gets:

(m, n) = max {0, m -n} and (m, n) = m/(n + 1) .
Example 1.4.8. In the polygraphic program F, one has n {0, . . . , N} and l 0, . . . , N , thanks to the bijective correspondences n = n , [ ] = and x :: l = (x 0 l) 1 . This polygraphic program is weakly orthogonal, hence locally confluent, and complete. It is also terminating, as we shall see later. Thus, it computes one map for each of , and . For example, the map takes a list of natural numbers as input and returns the corresponding ordered list. Let us give an example of computation generated by this program. Let us consider the list [2; 1] of natural numbers and apply the fusion sort function on it. The list is coded by the following value:

[2; 1] = 1 0 1 2 0 1 = 1 2 .
The value [2; 1] is, by definition, the unique normal form of the 2-path [2; 1] 1 . Thereafter, one presents a normalizing 3-path, obtained by 2 -composition of smaller 3-paths, where we have given self-explanatory "names" to the involved 3-cells, without further explanations. After computation, one gets the expected

[2; 1] = [1; 2]
as the target of this 3-path. :

1 2 2 1 2 1 1 2 0 1 , 0 1 : 1 2 1 2 2 1 2 1 2 0 2 1 : 2 1 2 1 2 1 3 ( 2 , 1 ) : 2 1 1 2 2 2 1 1 0 2 1 : 2 1 2 1 .
1.5. Polygraphic programs are Turing-complete

Polygraphic programs are Turing-complete

This completeness result is not a surprising one. Indeed, one could argue, for instance, that polygraphic programs simulate term rewriting systems, a Turing-complete model of computation. Our proof, similar to the one concerning interaction nets [START_REF] Lafont | Interaction nets[END_REF], prepares for the encoding of Turing machines with clocks, used for Theorem 3.4.4.

Definition 1.5.1. A Turing machine is a family M = (Σ, Q, q 0 , q f , δ) made of:

• A finite set Σ, called the alphabet; one denotes by Σ its extension with a new element, denoted by and called the blank character.

• A finite set Q, whose elements are called states, two distinguished elements q 0 , the initial state, and q f , the final state. A configuration of M is an element (q, a, w l , w r ) of the product set Q × Σ × Σ × Σ : here q is the current state of the machine, a is the currently read symbol, w l is the word at the left-hand side of a and w r is the word at the right-hand side of a. For further convenience, the word w l is written in reverse order, so that its first letter is the one that is immediately at the left of a.

• A map δ : (Q -{q f }) × Σ → Q × Σ × {L,
The transition relation of M is the binary relation denoted by → M and defined on the set of configurations of M as follows, where e denotes the neutral element of Σ :

• If δ(q 1 , a) = (q 2 , c, L) then (q 1 , a, e, w r ) → M (q 2 , , e, cw r ) , (q 1 , a, bw l , w r ) → M (q 2 , b, w l , cw r ) .

• If δ(q 1 , a) = (q 2 , c, R) then (q 1 , a, w l , e) → M (q 2 , , cw l , e) , (q 1 , a, w l , bw r ) → M (q 2 , b, cw l , w r ) .

One denotes by → * M the reflexive and transitive closure of → M . Let f : Σ → Σ be a map. One says that M computes f when, for any w in Σ , there exists a configuration of the shape (q f , a, v, f(w)) such that (q 0 , , e, w) → * M (q f , a, v, f(w)) holds (in that case, this final configuration is unique).

Theorem 1.5.2. Polygraphic programs form a Turing-complete model of computation.

Proof. We fix a Turing machine M = (Σ, Q, q 0 , q f , δ) and a map f computed by M. From this Turing machine, we build the following polygraphic program P(M):

1. It has one 1-cell w, standing for the type of words over Σ.

2. Apart from the three structure 2-cells, its 2-cells consist of:

(a) Constructor 2-cells: : * ⇒ w, for the empty word, plus one a : w ⇒ w for each a in Σ.

(b) Function 2-cells: : w ⇒ w, for the map f, plus one q a : w 0 w ⇒ w for each pair (q, a) in Q × Σ, for the behaviour of the Turing machine.

Polygraphic interpretations

3. Its 3-cells are the structure ones, plus the following computation 3-cells -the first one initializes the computation, the four subsequent families simulate the transitions of the Turing machine and the final cell starts the computation of the result:

c c b c c both when δ(q 1 , a) = (q 2 , c, L) both when δ(q 1 , a) = (q 2 , c, R) b q 2 a q 2 b q 0 a q 1 a q 1 q 1 a q 1 a q 2 q 2 b q f
One checks that w Σ through e = and aw = w 1 a . Then, to every configuration (q, a, w l , w r ), one associates the 2-path (q, a, w l , w r ) = w l 0 w r 1 q a . The four cases in the definition of the transition relation of M are in one-to-one correspondence with the four middle families of 3-cells of the polygraph P(M). Hence the following equivalence holds:

(q, a, w l , w r ) → * M (q , a , w l , w r ) if and only if (q, a, w l , w r ) (q , a , w l , w r ).

Finally, let us fix a w in Σ . Since M computes f, there exists a unique configuration (q f , a, v, f(w)), such that (q 0 , , e, w) → * M (q f , a, v, f(w)) holds. As a consequence, w 1 has a unique normal form, so that the following equalities hold, yielding = f:

(w) = q 0 0 w = q f a v 0 f(w) = f(w).

Polygraphic interpretations

Here, we present general results about information that can be recovered from functorial and differential interpretations of 3-polygraphs.

Functorial interpretations

Definition 2.1.1. A functorial interpretation of a 3-polygraph P is a pair ϕ = (ϕ 1 , ϕ 2 ) made of:

1. a map ϕ 1 sending every 1-path u of size n to a non-empty part of (N -{0}) n ;

2. a map ϕ 2 sending every 2-path f : u ⇒ v to a monotone map from ϕ 1 (u) to ϕ 1 (v).

The following equalities, called functorial relations, must be satisfied:

• if u is a degenerate 2-path, then ϕ 2 (u) is the identity of ϕ 1 (u); 2.1. Functorial interpretations • if u and v are 0-composable 1-paths, then ϕ 1 (u 0 v) = ϕ 1 (u) × ϕ 1 (v) holds; • if f and g are 0-composable 2-paths, then ϕ 2 (f 0 g) = ϕ 2 (f) × ϕ 2 (g) holds; • if f and g are 1-composable 2-paths, then ϕ 2 (f 1 g) = ϕ 2 (g) • ϕ 2 (f) holds.
One simply writes ϕ for both ϕ 1 and ϕ 2 . Intuitively, for every 2-cell , the map ϕ( ) tells us how , seen as a circuit gate, transmits currents downwards. In practice, one computes the value of a current interpretation on a 2-path by computing it on the 2-cells it contains and assembling them in an intuitive way. The following result formalizes this fact.

Lemma 2.1.2. A functorial interpretation of a 3-polygraph P is entirely and uniquely defined by its values on the 1-cells and 2-cells of P.

Proof. Using the functorial relations, one checks that a functorial interpretation takes the same values on both sides of the relations of associativity, local units and exchange on 2-paths: this property comes from the fact that set-theoretic maps satisfy these same relations. Then the functorial relations give the values of a current interpretation on 2-paths of size n + 1 from its values on 2-paths of size k ≤ n.

A direct consequence of Lemma 2.1.2 is that, when one wants to introduce a functorial interpretation, one only has to give its values on the 1-cells and on the 2-cells. Let us note that every functorial interpretation ϕ must send the 0-cell * to some single-element part of N -{0}. Hence, it must assign each ξ to the only map from ϕ(ξ) to ϕ( * ).

ϕ(n) = N -{0} , ϕ( ) = 1, ϕ( )(x) = x + 1, ϕ( )(x, y) = ϕ( )(x, y) = x.
ϕ(n) = {1} , ϕ(l) = 2N + 1, ϕ( n ) = ϕ( ) = 1, ϕ( )(x, y) = x + y + 1, ϕ( )(x) = x, ϕ( )(x, y) = x + y -1, ϕ( )(2x + 1) = 2 • x 2 + 1, 2 • x 2 + 1 .

Polygraphic interpretations

Example 2.1.6. Let P be a polygraphic program. One denotes by ν the functorial interpretation on the subpolygraph P C 2 defined, for every 1-cell ξ, by ν(ξ) = N -{0} and, for every constructor 2-cell with arity n, by: ν

( )(x 1 , . . . , x n ) = x 1 + • • • + x n + 1.
One checks that ν(t) = ||t|| holds for every value t with coarity 1. Thus, given values t 1 , . . . , t n with coarity 1, the following equality holds in N n :

ν(t 1 0 • • • 0 t n ) = ||t 1 || , . . . , ||t n || .
We use the functorial interpretation ν to describe the size of arguments of a function.

Lemma 2.1.7. Let ϕ be a functorial interpretation of a 3-polygraph P. Let f, g, h and k be 2-paths such that ϕ(f) ≤ ϕ(g) and ϕ(h) ≤ ϕ(k) hold. Then, for every i ∈ {0, 1} such that

f i h is defined, the inequality ϕ(f i h) ≤ ϕ(g i k) is satisfied.
Proof. One has:

ϕ(f 0 h) = ϕ(f) × ϕ(h) ≤ ϕ(g) × ϕ(k) = ϕ(g 0 k).
Indeed, the two equalities are given by the functorial relations that ϕ satisfies, while the middle inequality comes from the hypotheses and the fact that one uses a product order. Then one has:

ϕ(f 1 h) = ϕ(h) • ϕ(f) ≤ ϕ(h) • ϕ(g) ≤ ϕ(k) • ϕ(g) = ϕ(g 1 k).
The equalities come from the functorial relations; the first inequality uses the hypothesis ϕ(f) ≤ ϕ(g) and the fact that ϕ(h) is monotone; the second inequality uses ϕ(h) ≤ ϕ(k) and the fact that maps are compared pointwise.

Compatible functorial interpretations

Definition 2.2.1. Let ϕ be a functorial interpretation of a 3-polygraph P. For every 3-cell α of P, one says that ϕ is compatible with α when the inequality ϕ(s 2 α) ≥ ϕ(t 2 α) holds. One says that ϕ is compatible when it is compatible with every 3-cell of P.

Example 2.2.2. The functorial interpretations given in Examples 2.1.4 and 2.1.5 are compatible with all the 3-cells of the corresponding 3-polygraph. We will see later that the values they take on structure 2-cells ensure that they are compatible with all the structure 3-cells. Concerning the computation 3-cells, let us consider, for example, the third one associated to the sort function 2-cell . For the source, one gets:

ϕ (1, 1, 2x + 1) = ϕ 1, ϕ( )(1, 2x + 1) = ϕ( ) • ϕ( )(1, 2x + 3) = ϕ( )(2x + 5) = 2x + 5.

Differential interpretations

Now, for the target, going quicker:

ϕ       (1, 1, 2x + 1) = ϕ( ) 2 • x/2 + 3, 2 • x/2 + 3 = 2x + 5.
Proposition 2.2.3. Let ϕ be a compatible functorial interpretation of a polygraphic program. Then, for every 3-path F, the inequality ϕ(s 2 F) ≥ ϕ(t 2 F) holds.

Proof. We proceed by induction on the size of 3-paths. If F is a degenerate 3-path, then s 2 F = t 2 F holds and, thus, so does ϕ(s 2 F) = ϕ(t 2 F).

Let us assume that F is an elementary 3-path. Then one decomposes s 2 F and t 2 F, using a 3-cell α, 2-paths f, g and 1-paths u, v, yielding:

ϕ(s 2 F) = ϕ f 1 (u 0 s 2 α 0 v) 1 g and ϕ(t 2 F) = ϕ f 1 (u 0 t 2 α 0 v) 1 g .
The functorial interpretation ϕ is compatible with α, hence ϕ(s 2 α) ≥ ϕ(t 2 α) holds. Then one applies Lemma 2.1.7 four times to get ϕ(s 2 F) ≥ ϕ(t 2 F). Now, let us fix a non-zero natural number N and assume that the property holds for every 3-path of size N. Let us consider a 3-path F of size N + 1. Then one decomposes F into G 2 H where G is a 3-path of size N and H is an elementary 3-path. One concludes using the induction hypothesis on G and the previous case on H.

Differential interpretations

In this work, we use differential interpretations as an abstraction of "heats", but also, later, to define the property of conservativeness on "currents". For this reason, we introduce the following abstraction: Definition 2.3.1. A (strictly) ordered commutative monoid is an ordered set (M, ) equipped with a commutative monoid structure (+, 0) such that + is (strictly) monotone in both arguments.

Example 2.3.2. Concretely, in what follows, we consider N equipped with its natural order and either the addition (strict case) or the maximum map (non-strict case), both with 0 as neutral element.

Definition 2.3.3. Let M be an ordered commutative monoid, let P be a 3-polygraph and let ϕ be a functorial interpretation of P. A differential interpretation of P over ϕ into M is a map ∂ that sends each 2-path of P with 1-source u to a monotone map ∂ from ϕ(u) to M, such that the following conditions, called differential relations, are satisfied:

• If u is degenerate then ∂u = 0. • If f and g are 0-composable then ∂(f 0 g)(x, y) = ∂f(x) + ∂g(y) holds. • If f and g are 1-composable then ∂(f 1 g) = ∂f + ∂g • ϕ(f) holds.
Intuitively, given a 2-cell , the map ∂ tells us how much heat it produces, when seen as a circuit gate, depending on the intensities of incoming currents. In order to compute the heat produced by a 2-path, one determines the currents that its 2-cells propagate and, from those values, the heat each one produces; then one sums up all these heats.

Polygraphic interpretations

Lemma 2.3.4. A differential interpretation of a polygraph P is entirely and uniquely determined by its values on the 2-cells of P.

Proof. First, we prove that the differential relations imply that a differential interpretation takes the same values on each side of the relations of associativity, local units and exchange. For example, let us check this for the exchange relation. For that, let us fix 2-paths f, g, h and k such that both t 1 (f) = s 1 (h) and t 1 (g) = s 1 (k) are satisfied. We consider x in ϕ(s 1 (f)) and y in ϕ(s 1 (g)) and, using the functorial relations of ϕ and the differential relations of ∂, we compute each one of the following equalities in M:

∂ (f 0 g) 1 (h 0 k) (x, y) = ∂f(x) + ∂g(y) + ∂h • ϕ(f)(x) + ∂k • ϕ(g)(y) , ∂ (f 1 h) 0 (g 1 k) (x, y) = ∂f(x) + ∂h • ϕ(f)(x) + ∂g(y) + ∂k • ϕ(g)(y) .
One concludes using the associativity and commutativity of + in M. After that, one checks that the differential relations determine the values of a differential interpretation on 2-paths of size n + 1 from its values on 2-paths of size k ≤ n.

∂ (2x + 1) = 2x 2 + 1, ∂ (2x + 1) = x/2 + 1, ∂ (2x + 1, 2y + 1) = 1 if xy = 0, x + y otherwise.
Lemma 2.3.8. Let P be a 3-polygraph, with a differential interpretation ∂, over a functorial interpretation ϕ, into an ordered commutative monoid (M, +, 0, ). Let f, g, h, k be 2-paths such that the inequalities ϕ(f) ≤ ϕ(g), ∂f ∂g and ∂h ∂k hold. Then, for every i ∈ {0, 1} such that

f i h is defined, one has ∂(f i h) ∂(g i k).
Moreover, when M is strictly ordered and either ∂f ≺ ∂g or ∂h ≺ ∂k hold, one has ∂(f i h) ≺ ∂(g i k).

Proof. One computes, for x ∈ ϕ(s 1 f) and y ∈ ϕ(s 1 h):

∂(f 0 h)(x, y) = ∂f(x) + ∂h(y) ∂g(x) + ∂k(y) = ∂(g 0 k)(x, y).

Compatible differential interpretations

Indeed, the two equalities are given by the differential relations that ∂ satisfies; the inequality uses the hypotheses, the fact that maps are compared pointwise and the monotony of +. Moreover, if + is strictly monotone and if one of ∂f ≺ ∂g or ∂h ≺ ∂k holds, then the middle inequality is strict. Now, one checks:

∂(f 1 h) = ∂f + ∂h • ϕ(f) ∂g + ∂k • ϕ(g) = ∂(g 1 k).
The equalities come from the differential relations; the inequality comes from the hypotheses ∂f ∂g, ∂h ∂k and ϕ(f) ≤ ϕ(g), plus the monotony of ∂h and + and the fact that maps are compared pointwise. When + is strictly monotone and when either ∂f ≺ ∂g or ∂h ≺ ∂k hold, the middle inequality is strict.

Compatible differential interpretations

Definition 2.4.1. Let P be a 3-polygraph equipped with a functorial interpretation ϕ and a differential interpretation ∂ of P over ϕ and into an ordered commutative monoid M. For every 3-cell α, one says that ∂ is compatible with α when ∂(s 2 α) ∂(t 2 α) holds. It is said to be strictly compatible with α when ∂(s 2 α) ∂(t 2 α) holds. One says that ∂ is (strictly) compatible when it is with every 3-cell of P.

Example 2.4.2. The differential interpretations given in Examples 2.3.6 and 2.3.7 are compatible with every structure 3-cell and strictly compatible with every computation 3-cell of their 3-polygraph.

Indeed, in the source and the target of every structure 3-cell α, only constructor and structure 2-cells appear. The considered differential interpretations sends these to zero, yielding ∂(s 2 α) = ∂(t 2 α) = 0.

For an example of compatibility with a computation 3-cell, we consider the third 3-cell of the fusion sort function 2-cell . On one hand, one gets:

∂ (1, 1, 2x + 1) = ∂ (2x + 5) = 2(x + 2) 2 + 1 = 2x 2 + 8x + 9.
And, on the other hand, one computes: Proof. We proceed by induction on the size of 3-paths. If F is a degenerate 3-path, then one has s 2 F = t 2 F and, thus, ∂(s 2 F) = ∂(t 2 F) also.

∂       (1, 1, 2x + 1) =    ∂ 2 x/2 + 3 + ∂ 2 x/2 + 3 + ∂ (2x + 1) + ∂ 2 x/2 + 3, 2 x/2 + 3 = 2 • x/2 + 1 2 + 2 • x/2 + 1 2 + x + x/2 + 4 = 2 x/2 2 +
Let us assume that F is an elementary 3-path. We decompose F using a 3-cell α, 2-paths f, g and 1-paths u, v, yielding:

∂(s 2 F) = ∂ f 1 (u 0 s 2 α 0 v) 1 g and ∂(t 2 F) = ∂ f 1 (u 0 t 2 α 0 v) 1 g .
By

F) ∂(t 2 F). If M is N, this means that ∂(s 2 F) -∂(t 2 F) ≥ 1 = |||F|||.
Finally, let us fix a non-zero natural number N and assume that the property holds for every 3-path of size N. Let us consider a 3-path F of size N + 1. Then one decomposes F into G 2 H where G is a 3-path of size N and H is an elementary 3-path. Then we apply the induction hypothesis to G and the previous case to H to conclude.

Conservative functorial interpretations

Intuitively, the following definition gives a bound on all the intensities of currents that one can find in the vicinity of any 2-cell inside a 2-path. Definition 2.5.1. Let P be a 3-polygraph equipped with a functorial interpretation ϕ. One denotes by ∂ ϕ the differential interpretation of P, over ϕ and into (N, max, 0), sending every 2-cell with valence (m, n), i.e. with arity m and coarity n, to the following map from ϕ(s 1 ) to N:

∂ ϕ = max µ m , µ n • ϕ( ) ,
i.e. ∂ ϕ (x 1 , . . . , x m ) = max {x 1 , . . . , x m , y 1 , . . . , y n } if (y 1 , . . . , y n ) denotes ϕ( )(x 1 , . . . , x m ).

For every 3-cell α of P, one says that ϕ is conservative on α when ∂ ϕ is compatible with α. One says that ϕ is conservative when it is conservative on every 3-cell of P, i.e. when ∂ ϕ is compatible.

Example 2.5.2. The functorial interpretations of Examples 2.1.4 and 2.1.5 are conservative. Indeed, we shall see later that their values on structure and constructor 2-cells ensure that they are conservative on structure 3-paths. Let us check conservativeness on, for example, the last computation 3-cell of the sort function 2-cell :

∂ ϕ (1, 1, 2x + 1) = max 1, 2x + 1, 2x + 2, 2x + 3 = 2x + 3 = max 1, 2x + 1, 2 • x/2 + 1, 2 • x/2 + 1, 2 • x/2 + 2, 2 • x/2 + 2, 2x + 3 = ∂ ϕ       (1, 1, 2x + 1).
When a functorial interpretation is both compatible and conservative, the intensities of currents inside 2-paths do not increase during computations.

Proposition 2.5.3. Let ϕ be a compatible and conservative functorial interpretation of a polygraphic program. Then, for every 3-path F, the inequality

∂ ϕ (s 2 F) ≥ ∂ ϕ (t 2 F) holds.
Proof. By definition of conservativeness and using Proposition 2.4.3 on ∂ ϕ .

Polygraphic interpretations

Definition 2.6.1. A polygraphic interpretation of a 3-polygraph P is a pair (ϕ, ∂) made of a functorial interpretation ϕ of P, together with a differential interpretation ∂ of P over ϕ and into (N, +, 0). In that case, ϕ and ∂ respectively are the functorial part and the differential part of (ϕ, ∂).

Let us fix a 3-cell α. A polygraphic interpretation (ϕ, ∂) is compatible (with α) when both ϕ and ∂ are. It is strictly compatible (with α) when ϕ is compatible with α and ∂ is strictly compatible (with α). It is conservative (on α) when ϕ is.

Example 2.6.2. The functorial and differential interpretations we have built on the polygraphic programs of division and of fusion sort are two examples of polygraphic interpretations that are conservative, compatible with every structure 3-cell and strictly compatible with every computation 3-cell.

Let us consider the trivial functorial interpretation and the differential interpretation ||•|| X over it, for some family X of 2-cells. They form a polygraphic interpretation that is conservative but that has no general reason to be compatible with any 3-cell.

We recall the following theorem: Theorem 2.6.3 ([18]). If a 3-polygraph has a polygraphic interpretation which is strictly compatible with all of its 3-cells, then it terminates.

Proof. By application of Proposition 2.4.3, one knows that ∂(s 2 F) > ∂(t 2 F) holds for every elementary 3-cell F. Furthermore, these are maps with values into N. Since there is no infinite strictly decreasing sequence of such maps for the pointwise order, one concludes that P must terminate.

In what follows, we use Theorem 2.6.3 in several steps, thanks to the following result: Proposition 2.6.4. Let P be a 3-polygraph and let X be a set of 3-cells of P. Let us assume that there exists a compatible polygraphic interpretation on P whose restriction to X is strictly compatible. Then P terminates if and only if P -X does.

Proof. If P terminates, its reduction graph has no infinite path. Since it contains the reduction graph of the 3-polygraph P -X, the latter does not have any infinite path either. Hence P -X terminates.

Conversely, let us assume that P does not terminate. Then there exists an infinite sequence (F n ) n∈N of elementary 3-paths in P such that, for every n ∈ N, F n and F n+1 are composable. The polygraphic interpretation is compatible, hence one can apply Proposition 2.4.3 to get the following infinite sequence of inequalities in N:

∂(s 2 F 0 ) ≥ ∂(t 2 F 0 ) = ∂(s 2 F 1 ) ≥ (• • • ) = ∂(s 2 F n ) ≥ ∂(t 2 F n ) = ∂(s 2 F n+1 ) ≥ (• • • )
Furthermore, for every n ∈ N such that F n ∈ X , one has a strict inequality ∂(s 2 F n ) > ∂(t 2 F n ) since the polygraphic interpretation is strictly compatible with every 3-cell of X. Hence, there are only finitely many n in N such that F n is in X : otherwise, one could extract, from (∂(s 2 F n )) n∈N , an infinite, strictly decreasing sequence of maps with values in N. Thus, there exists some n 0 ∈ N such that (F n ) n≥n 0 is an infinite path in the reduction graph of P -X: this means that P -X does not terminate.

Example 2.6.5. Let us consider the polygraphic programs for division and fusion sort, given in Examples 1.3.2 and 1.3.3. We have seen that each one admits a compatible polygraphic interpretation that is strictly compatible with their computation 3-cells. Furthermore, as proved later, the structure 3-cells, alone, terminate. Thus Proposition 2.6.4 gives the termination of both polygraphic programs.

Actually, in what comes next, we produce a standard differential interpretation that is strictly compatible with structure 3-cells. However, in general, it is not compatible, even in a non-strict way, with computation 3-cells: informally, each application of such a cell can increase the "structure heat". The purpose of the rest of this section is to bound this potential augmentation. Lemma 2.6.6. Let P be a 3-polygraph equipped with a polygraphic interpretation (ϕ, ∂). Then, for every 2-path f in P and every x in ϕ(s 1 f), the following inequality holds in N:

∂f(x) ≤ ∈P 2 ||f|| • ∂ ∂ ϕ f(x), . . . , ∂ ϕ f(x) .
Remark. Let us note that we apply ∂ to arguments ∂ ϕ f(x) that are not necessarily in its domain. In that case, one considers an extension of ∂ sending x to ∂ (y), where y is the maximum element of the set ϕ(s 1 ) that is below x.

Proof. We proceed by induction on the size of the 2-path f. Let us assume that f is degenerate. Then one has ||f|| = 0 for every 2-cell and, since ∂ is a differential interpretation, ∂f = 0. Hence both sides of the sought inequality are equal to 0. Now, let us consider an elementary 2-path f. One decomposes f into u 0 0 v, where is a 2-cell and u and v are 1-paths. Then ||f|| is 1 when is and 0 otherwise. Let us fix x, y and z respectively in ϕ(u), ϕ(s 1 ) and ϕ(v). Using the differential relations of ∂ and ∂ ϕ , one gets ∂f(x, y, z) = ∂ (y) and ∂ ϕ f(x, y, z) = ∂ ϕ (y). If has valence (m, n) and y = (y 1 , . . . , y m ), one uses the definition of ∂ ϕ to get, for every i ∈ {1, . . . , m}:

∂ ϕ (y) = max µ m (y), µ n • ϕ( )(y) ≥ y i .
Then one computes:

∈P 2 ||f|| • ∂ ∂ ϕ f(x, y, z), . . . , ∂ ϕ f(x, y, z) = ∂ ∂ ϕ (y), . . . , ∂ ϕ (y) ≥ ∂ (y 1 , . . . , y m ) = ∂f(x, y, z).
Finally, let us fix a non-zero natural number N and assume that the property holds for every 2-path of size at most N. We consider a 2-path f of size N + 1: there exists a decomposition f = g 1 h where g and h are 2-paths of size at most N. Then, using the differential relations of ||•|| , for any 2-cell , and of ∂ ϕ , one gets:

||f|| = ||g|| + ||h|| and ∂ ϕ (f) = max { ∂ ϕ g, ∂ ϕ h • ϕ(g) } .
We fix a x in ϕ(s 1 f) and compute:

∂f(x) = ∂(g 1 h)(x) = ∂g(x) + ∂h • ϕ(g)(x) ≤ ∈P 2 ||g|| • ∂ ∂ ϕ g(x), . . . , ∂ ϕ g(x) + ∈P 2 ||h|| • ∂ ∂ ϕ h • ϕ(g)(x), . . . , ∂ ϕ h • ϕ(g)(x) ≤ ∈P 2 ||g|| • ∂ ∂ ϕ f(x), . . . , ∂ ϕ f(x) + ∈P 2 ||h|| • ∂ ∂ ϕ f(x), . . . , ∂ ϕ f(x) = ∈P 2 ||g|| + ||h|| • ∂ ∂ ϕ f(x), . . . , ∂ ϕ f(x) = ∈P 2 ||f|| • ∂ ∂ ϕ f(x), . . . , ∂ ϕ f(x) .
Proposition 2.6.7. Let P be a 3-polygraph, let α be a 3-cell of P and let F be an elementary 3-path in α . One assumes that P is equipped with a polygraphic interpretation (ϕ, ∂) such that ϕ is compatible with and conservative on α. Then, for every x ∈ ϕ(s 1 F), the following inequality holds in Z:

∂(t 2 F)(x) -∂(s 2 F)(x) ≤ ∈P 2 ||t 2 (α)|| • ∂ ∂ ϕ (s 2 F)(x), . . . , ∂ ϕ (s 2 F)(x) .
Proof. Since F is a 3-path of size 1 in α , one can decompose s 2 F and t 2 F as follows:

g s 2 F = u v s 2 α f and t 2 F = u v t 2 α f g .
Let us denote by p, q and m the respective sizes of u, v and s 1 F. The map ϕ(f) takes its values in a part of N p+m+q : we decompose it into three maps denoted by ϕ 1 (f), ϕ 2 (f) and ϕ 3 (f), with the same domain and respectively taking their values in parts of N p , N m and N q . Let us fix a x ∈ ϕ(s 1 F). The functorial and differential relations give:

∂(s 2 F)(x) = ∂f(x) + ∂(s 2 α) • ϕ 2 (f)(x) + ∂g ϕ 1 (f)(x), ϕ(s 2 α) • ϕ 2 (f)(x), ϕ 3 (f)(x) .

Complexity of polygraphic programs

With the same arguments, one gets the same decomposition for ∂(t 2 F), with s 2 α replaced by t 2 α. Thus, the following holds in Z:

∂(t 2 F)(x) -∂(s 2 F)(x) = ∂(t 2 α) • ϕ 2 (f)(x) -∂(s 2 α) • ϕ 2 (f)(x) + ∂g ϕ 1 (f)(x), ϕ(t 2 α) • ϕ 2 (f)(x), ϕ 3 (f)(x) -∂g ϕ 1 (f)(x), ϕ(s 2 α) • ϕ 2 (f)(x), ϕ 3 (f)(x) . Let us prove that ∂(t 2 F)(x) -∂(s 2 F)(x) ≤ ∂(t 2 α) • ϕ 2 (f)(x) holds. First, one has ∂(s 2 α) ≥ 0.
Moreover, ϕ is compatible with α, which means that ϕ(s 2 α) ≥ ϕ(t 2 α) holds; since the map ∂g is monotone, the following holds in N:

∂g ϕ 1 (f)(x), ϕ(s 2 α) • ϕ 2 (f)(x), ϕ 3 (f)(x) ≥ ∂g ϕ 1 (f)(x), ϕ(t 2 α) • ϕ 2 (f)(x), ϕ 3 (f)(x) .
There remains to bound ∂(t 2 α) • ϕ 2 (f)(x). One applies Lemma 2.6.6 to t 2 (α) to get:

∂(t 2 α) • ϕ 2 (f)(x) ≤ ∈P 2 ||t 2 (α)|| • ∂ ∂ ϕ (t 2 α) • ϕ 2 (f)(x), . . . , ∂ ϕ (t 2 α) • ϕ 2 (f)(x) .
By assumption, ϕ is conservative on α and, thus,

∂ ϕ t 2 (α) • ϕ 2 (f)(x) ≤ ∂ ϕ s 2 (α) • ϕ 2 (f)(x) holds.
Moreover, using the differential properties satisfied by ∂ ϕ , one gets

∂ ϕ s 2 (α) • ϕ 2 (f)(x) ≤ ∂ ϕ (s 2 F).
One concludes by invoking the monotony of ∂ .

Complexity of polygraphic programs

In this section, we specialize polygraphic interpretations to polygraphic programs to get information on their complexity. In particular, we introduce additive polygraphic interpretations and use them as an estimation of the size of values. This way, we give bounds on the size of computations, with respect to the size of the arguments. We conclude this work with a characterisation of a class of polygraphic programs that compute exactly the FPTIME functions.

Additive functorial interpretations and the size of values

Definition 3.1.1. Let P be a polygraphic program. One says that a functorial interpretation ϕ of P is additive when, for every constructor 2-cell of arity n, there exists a non-zero natural number c such that, for every (x 1 , . . . , x n ) in ϕ(s 1 ), the following equality holds in N:

ϕ( )(x 1 , . . . , x n ) = x 1 + • • • + x n + c .
In that case, one denotes by γ the greatest of these numbers, i.e. :

γ = max c , ∈ P C 2 .
A polygraphic interpretation is additive when its functorial part is.

Example 3.1.2. The functorial interpretations we have built for the polygraphic programs D and F are additive. In both cases, γ is 1.

Additive functorial interpretations and the size of values

Lemma 3.1.3. Let ϕ be an additive functorial interpretation of a polygraphic program P and let t be a value with coarity 1. Then the following equality holds in N:

ϕ(t) = ∈P C 2 ||t|| • c .
Proof. Let us prove this result by induction on the size of the 2-path t. There is no degenerate value with coarity 1. If t is an elementary value with coarity 1, then t is a constructor 2-cell with arity 0. Since ϕ is additive, one has ϕ( ) = c . Moreover, ||t|| is 1 when = holds and 0 otherwise, yielding the equality one seeks. Now, let us fix a non-zero natural number N and assume that the result holds for every value with coarity 1 and size at most N. Let us fix a value t with coarity 1 and size N + 1. Then t admits a decomposition t = t 1 0 • • • 0 t n 1 , where is a constructor 2-cell with arity n and each t i , i ∈ {1, . . . , n}, is a value with coarity 1 and size at most N. As a consequence, for every constructor 2-cell , one has:

||t|| = ||t 1 || + • • • + ||t n || + 1 if = , ||t 1 || + • • • + ||t n || otherwise.
Finally, one computes:

ϕ(t) = ϕ( ) • ϕ(t 1 ) × • • • × ϕ(t n ) from the functorial relations of ϕ, = ϕ(t 1 ) + • • • + ϕ(t n ) + c since ϕ is additive, = ∈P C 2 ||t 1 || + • • • + ||t n || • c + c by induction hypothesis = ∈P C 2 ||t|| • c from previous remark.
Proposition 3.1.4. Let ϕ be an additive functorial interpretation of a polygraphic program P. Then, for every value t with coarity 1, the inequalities ||t|| ≤ ϕ(t) ≤ γ ||t|| hold in N. As a consequence, for every value t, one has ν(t) ≤ ϕ(t) ≤ γν(t), where ν is the functorial interpretation introduced in Example 2.1.6.

Proof. Let us assume that t is a value with coarity 1. From Lemma 3.1.3, one has:

ϕ(t) = ∈P C 2 ||t|| • c .
By additivity of ϕ and by definition of γ, one has 1 ≤ c ≤ γ for every constructor 2-cell . One concludes by using the following equality, that holds since t is in P C 2 :

||t|| = ∈P C 2 ||t|| .
When t 1 , . . . , t n are values with coarity 1 and when t = t 1 0 • • • 0 t n , one concludes thanks to the equalities ϕ(t) = ϕ(t 1 ), . . . , ϕ(t n ) and ν(t) = ||t 1 || , . . . , ||t n || .

Lemma 3.1.5. Let ϕ be an additive functorial interpretation of a polygraphic program P. For every value t with coarity 1, the equality ∂ ϕ t = ϕ(t) holds. As a consequence, for every value t with coarity n, one has

∂ ϕ t = µ n • ϕ(t).
Proof. Let us proceed by induction on the size of t. If is a constructor 2-cell with arity 0, then the equality holds by definition of ∂ ϕ . Now, let us fix a non-zero natural number N and assume that the result holds for every value with coarity 1 and size at most N. Let us consider a value t with coarity 1 and size N + 1. One decomposes

t into t = (t 1 0 • • • 0 t n ) 1 , with
a constructor 2-cell and where t i is a value with coarity 1 and size at most N, for every i ∈ {1, . . . , n}. Using the differential relations of ∂ ϕ , one gets:

∂ ϕ t = max ∂ ϕ (t 1 ), . . . , ∂ ϕ (t n ), ∂ ϕ ϕ(t 1 ), . . . , ϕ(t n ) .
The definition of ∂ ϕ gives:

∂ ϕ ϕ(t 1 ), . . . , ϕ(t n ) = max ϕ(t 1 ), . . . , ϕ(t n ), ϕ( ) ϕ(t 1 ), . . . , ϕ(t n ) .
Since ϕ is additive, ϕ( ) ϕ(t 1 ), . . . , ϕ(t n ) is greater than every ϕ(t i ), which is ∂ ϕ (t i ) by induction hypothesis applied to t i . Thus one gets the following equality and uses the functorial relations of ϕ to conclude:

∂ ϕ t = ϕ( ) ϕ(t 1 ), . . . , ϕ(t n ) .
Finally, let us consider a value t with coarity n. One denotes by (t 1 , . . . , t n ) the family of values with coarity 1 such that t = t 1 0 • • • 0 t n holds. One invokes the differential relations of ∂ ϕ to get the equality

∂ ϕ t = max ∂ ϕ (t 1 ), . . . , ∂ ϕ (t n ) .
One uses the induction hypothesis on each t i and concludes, thanks to the functorial relations satisfied by ϕ.

Proposition 3.1.6. Let ϕ be an additive functorial interpretation on a polygraphic program P. For every function 2-cell and every value t of type s 1 ( ), one has

∂ ϕ (t 1 ) = ∂ ϕ • ϕ(t).
Proof. Let us assume that has valence (m, n). One uses the differential relations of ∂ ϕ to produce:

∂ ϕ (t 1 ) = max ∂ ϕ t, ∂ ϕ • ϕ(t) .
But, by definition of ∂ ϕ , one has

∂ ϕ • ϕ(t) ≥ µ m • ϕ(t).
There remains to use Lemma 3.1.5 on t to get ∂ ϕ t = µ n • ϕ(t).

Notation 3.1.7. Let be a function 2-cell with arity m in a polygraphic program P, equipped with an additive functorial interpretation ϕ. Thereafter, we denote by M the map from N m to N defined by:

M (x 1 , . . . , x m ) = ∂ ϕ γx 1 , . . . , γx m .
The next result uses the map M and the size of the initial arguments to bound the size of intermediate values produced during computations, hence of the arguments of potential recursive calls.

Proposition 3.1.8. Let P be a polygraphic program, equipped with an additive, compatible and conservative functorial interpretation ϕ. Let be a function 2-cell and let t be a value of type s 1 . Then, for every 3-path F with source t 1 , the following inequality holds in N:

∂ ϕ (t 2 F) ≤ M • ν(t).

Cartesian polygraphic interpretations and the size of structure computations

Proof. The functorial interpretation ϕ is compatible and conservative: by Proposition 2.5.3, we know that ∂ ϕ (t 2 F) ≤ ∂ ϕ (t 1 ) holds. Since ϕ is additive, one may use Proposition 3.1.6 to produce the equality ∂ ϕ (t 1 ) = ∂ ϕ • ϕ(t). Furthermore, Proposition 3.1.4 gives ϕ(t) ≤ γν(t): one argues that ∂ ϕ is monotone to conclude.

Cartesian polygraphic interpretations and the size of structure computations

Here we bound the number of structure 3-cells that can appear in a computation. For that, we consider polygraphic interpretations that take special values on structure 2-cells. Definition 3.2.1. Let P be a polygraphic program. A functorial interpretation ϕ of P is said to be cartesian when the following conditions hold, for every 1-cells ξ and ζ:

ϕ ξ (x) = (x, x) and ϕ ξ,ζ (x, y) = (y, x).
A polygraphic interpretation is cartesian when its functorial part is cartesian and when its differential part sends every constructor and structure 2-cell to zero.

Proposition 3.2.2. If a functorial interpretation of a polygraphic program P is cartesian, then it is compatible with and conservative on all the structure 3-cells.

Proof. Let ϕ be a cartesian functorial interpretation of a polygraphic program P. We start by computing the values of ϕ and ∂ ϕ on the structure 2-paths, by induction on their size. This way, one proves that the following equalities hold, for any 1-path u and x ∈ ϕ(u), any 1-cell ξ and y ∈ ϕ(ξ):

ϕ u,ξ (x, y) = (y, x), ϕ ξ,u (y, x) = (x, y), ϕ u (x) = (x, x), ϕ u (x) = * .
Then, when u = * , all these 2-paths are degenerate, so that they are sent on 0 by the differential interpretation ∂ ϕ . Now, when u is non-degenerate, with x = (x 1 , . . . , x n ), one gets: With the same notations, we now check the conservativeness of ϕ with the structure 3-cells, i.e the compatibility of ∂ ϕ with them:

∂ ϕ u,ξ (x, y) = max {x 1 , . . . , x n , y} = ∂ ϕ ξ,u (y, x), ∂ ϕ u (x) = max {x 1 , . . . , x n } = ∂ ϕ u (
∂ ϕ (x, y) = max ∂ ϕ (x), y ≥ ∂ ϕ (x, y), ∂ ϕ (y, x) = max ∂ ϕ ( )(x), y ≥ ∂ ϕ (y, x), ∂ ϕ = ∂ ϕ ( ) = ∂ ϕ , ∂ ϕ = ∂ ϕ ( ) ≥ ∂ ϕ .
Definition 3.2.3. Let ϕ be a functorial interpretation of a polygraphic program P. We denote by ∂ S ϕ and call structure differential interpretation generated by ϕ the differential interpretation of P, over ϕ and into (N, +, 0), that sends every constructor and function 2-cell to zero and such that the following hold:

∂ S ϕ (x, y) = xy, ∂ S ϕ (x) = x 2 , ∂ S ϕ (x) =
x. Lemma 3.2.4. Let ϕ be a functorial interpretation of a polygraphic program P. If ϕ is both additive and cartesian, then ∂ S ϕ is strictly compatible with all the structure 3-cells of P. Proof. We start by computing ∂ S ϕ on the structure 2-paths, by induction on their size:

∂ S ϕ (x 1 , . . . , x n , y) = ∂ S ϕ (y, x 1 , . . . , x n ) = y • 1≤i≤n x i , ∂ S ϕ (x 1 , . . . , x n ) = 1≤i≤j≤n x i • x j , ∂ S ϕ (x 1 , . . . , x n ) = 1≤i≤n x i . Now, let us fix a constructor 2-cell
with arity n. Let us consider x = (x 1 , . . . , x n ) in ϕ(s 1 ). Since ϕ is additive, one notes that ϕ( )(x) > x 1 + • • • + x n holds. Then, given a y ∈ N -{0}, one checks that the following strict inequalities hold in N -{0}:

∂ S ϕ (x, y) = y • ϕ( )(x) > y • 1≤i≤n x i = ∂ S ϕ (x, y), ∂ S ϕ (x, y) = y • ϕ( )(x) > y • 1≤i≤n x i = ∂ S ϕ (x, y), ∂ S ϕ (x) = ϕ( )(x) 2 > 1≤i≤j≤n x i • x j = ∂ S ϕ (x), ∂ S ϕ (x) = ϕ( )(x) > 1≤i≤n x i = ∂ S ϕ (x).

Cartesian polygraphic interpretations and the size of structure computations

The following result gives sufficient conditions on a polygraphic interpretation such that one does not have to bother with the structure 3-cells to prove termination.

Proposition 3.2.5. If a polygraphic program admits an additive and cartesian polygraphic interpretation that is strictly compatible with every computation 3-cell, then it terminates.

Proof. Let (ϕ, ∂) be a polygraphic interpretation with the required properties. One applies Proposition 3.2.2 to get the compatibility of ϕ with structure 3-cells. Then Lemma 3.2.4 tells us that (ϕ, ∂ S ϕ ) is strictly compatible with structure 3-cells: hence Theorem 2.6.3 yields termination of P S 3 . Since ∂ sends every constructor and structure 2-cell to zero, one has ∂(s 2 α) = ∂(t 2 α) = 0 for every structure 3-cell α: thus (ϕ, ∂) is compatible with every structure 3-cell and, by hypothesis, strictly compatible with every other 3-cell. One applies Proposition 2.6.4 to conclude. Definition 3.2.6. Let P be a polygraphic program. One denotes by K the maximum number of structure 2-cells one finds in the targets of computation 3-cells:

K = max ||t 2 (α)|| P S 2 , α ∈ P R 3 .
Let ϕ be an additive functorial interpretation of P. For every function 2-cell with arity m, one defines S as the map from N m to N given by:

S (x 1 , . . . , x m ) = K • M 2 (x 1 , . . . , x m ).
The following lemma proves that, during a computation, if one applies a computation 3-cell, then the structure heat increase is bounded by a polynomial in the size of the arguments. Lemma 3.2.7. Let P be a polygraphic program, equipped with an additive, cartesian, compatible and conservative functorial interpretation ϕ. Let be a function 2-cell and t be a value of type s 1 ( ). Let f and g be 2-paths such that t 1 reduces into f which, in turn, reduces into g by application of a computation 3-cell α. Then, the following inequality holds in Z:

∂ S ϕ g -∂ S ϕ f ≤ S • ν(t).
Proof. Since ϕ is compatible and conservative, one can apply Proposition 2.6.7 on the 3-path from f to g, to get the following inequality:

∂ S ϕ g -∂ S ϕ f ≤ ∈P 2 ||t 2 (α)|| • ∂ S ϕ ∂ ϕ (f), . . . , ∂ ϕ (f) .
By definition of ∂ S ϕ , one has ∂ S ϕ = 0 except when is a structure 2-cell. Thus one gets:

∂ S ϕ g -∂ S ϕ f ≤ ||t 2 (α)|| • ∂ S ϕ ∂ ϕ (f), ∂ ϕ (f) + ||t 2 (α)|| • ∂ S ϕ ∂ ϕ (f) + ||t 2 (α)|| • ∂ S ϕ ∂ ϕ (f) = ||t 2 (α)|| • ∂ ϕ (f) 2 + ||t 2 (α)|| • ∂ ϕ (f) 2 + ||t 2 (α)|| • ∂ ϕ (f) ≤ ||t 2 (α)|| P S 2 • ∂ ϕ (f) 2 ≤ K • ∂ ϕ (f) 2 .
Finally, we recall that ϕ is additive, compatible and conservative: an application of Proposition 3.1.8 to the 3-path with source t 1 and target f yields ∂ ϕ (f) ≤ M • ν(t) and concludes the proof.

S (x) = x 2 , S (x) = x 2 , S (x, y) = (x + y -1) 2 .

The size of computations

Definition 3.3.1. Let P be a polygraphic program, with an additive polygraphic interpretation (ϕ, ∂).

For every function 2-cell with arity m, one denotes by P and by Q the maps from N m to N defined by:

P (x 1 , . . . , x m ) = ∂ γx 1 , . . . , γx m , Q (x 1 , . . . , x m ) = P (x 1 , . . . , x m ) • 1 + S (x 1 , . . . , x m ) .
The following result bounds the number of computation 3-cells in a reduction 3-path, with respect to the size of the arguments.

Proposition 3.3.2. Let P be a polygraphic program, equipped with an additive and cartesian polygraphic interpretation (ϕ, ∂) which is strictly compatible with every computation 3-cell. Let be a function 2-cell and t be a value of type s 1 ( ). Then, for every 3-path F with source t 1 , the following inequality holds:

|||F||| P R 3 ≤ P • ν(t).
Proof. If F is degenerate, then |||F||| P R 3 = 0 holds. Otherwise, the 3-path F decomposes this way:

F = H 0 2 G 1 2 H 1 2 G 2 2 • • • 2 G k 2 H k ,
where each G i is elementary in P R 3 and each H j lives in P S 3 . Hence |||F||| P R 3 = k. Since the polygraphic interpretation is cartesian, it is compatible with every structure 3-cell, so that one has ∂(s 2 H j ) ≥ ∂(t 2 H j ), for every j ∈ {0, . . . , k}. Since it is also strictly compatible with every computation 3-cell, one applies Proposition 2.4.3 to get the following chain of (in)equalities, for every i ∈ {0, . . . , k -1}:

∂(s 2 H i ) ≥ ∂(t 2 H i ) = ∂(s 2 G i ) > ∂(t 2 G i ) = ∂(s 2 H i+1 ).
By induction on i, one proves the following chain of (in)equalities:

∂(t 1 ) = ∂(s 2 G 1 ) > ∂(s 2 G 2 ) > • • • > ∂(s 2 G k ) > ∂(t 2 G k ).
Furthermore we have ∂(t 2 G k ) ≥ 0 and, consequently:

|||F||| P R 3 ≤ ∂(t 1 ).
Finally, let us bound ∂(t 1 ), which is equal to ∂ • ϕ(t) + ∂t, thanks to the differential relations of ∂. But (ϕ, ∂) is cartesian, yielding ∂t = 0, and Proposition 3.1.4 tells us that ϕ(t) ≤ γν(t) holds. One uses the definition of P to conclude.

The size of computations

Proposition 3.3.3. Let P be a polygraphic program, equipped with an additive and cartesian polygraphic interpretation (ϕ, ∂) which is strictly compatible with and conservative on every computation 3-cells. Let be a function 2-cell and let t be a value of type s 1 . Then, for every 3-path F with source t 1 , the following inequality holds:

|||F||| ≤ Q • ν(t).
Proof. If |||F||| = 0, then the inequality does hold. Otherwise, there exists a 3-cell that we can apply to the starting 2-path t 1 ; moreover, this is a computation 3-cell since no structure 3-cell can be applied to such a 2-path. Hence the 3-path F decomposes this way:

F = G 1 2 H 1 2 G 2 2 • • • 2 G k 2 H k ,
where each G i is elementary in P R 3 and each H j is in P S 3 . As a consequence, we have:

|||F||| = k + |||H 1 ||| + • • • + |||H k ||| . Furthermore k = |||F||| P R 3
holds and, thus, so does k ≤ P • ν(t) thanks to Proposition 3.3.2. We prove that the following inequality holds to conclude:

|||H 1 ||| + • • • + |||H k ||| ≤ k • S • ν(t) .
Towards this goal, let us fix an i ∈ {1, . . . , k}. Since ∂ S ϕ is strictly compatible with every structure 3-cell, one gets from Proposition 2.4.3:

|||H i ||| + ∂ S ϕ (t 2 H i ) ≤ ∂ S ϕ (s 2 H i ).
Furthermore, from Lemma 3.2.7, one knows that the following inequality holds:

∂ S ϕ (t 2 G i ) ≤ ∂ S ϕ (s 2 G i ) + S • ν(t).
Since t 2 G i = s 2 H i holds, one has:

|||H i ||| + ∂ S ϕ (t 2 H i ) ≤ ∂ S ϕ (s 2 G i ) + S • ν(t).
Or, written differently:

|||H i ||| ≤ ∂ S ϕ (s 2 G i ) -∂ S ϕ (t 2 H i ) + S • ν(t).
One sums this family of k inequalities, one for every i in {1, . . . , n}, to produce:

|||H 1 ||| + • • • + |||H k ||| ≤ k i=1 ∂ S ϕ (s 2 G i ) - k i=1 ∂ S ϕ (t 2 H i ) + k • S • ν(t).
By hypothesis, one has s 2 G 1 = t 1 , t 2 H k = t 2 F and, for every i ∈ {1, . . . , k}, t 2 H i = s 2 G i+1 , so that the following inequality holds:

|||H 1 ||| + • • • + |||H k ||| ≤ ∂ S ϕ (s 2 F) -∂ S ϕ (t 2 F) + k • S • ν(t).
Finally, one argues that both ∂ S ϕ (t 1 ) = 0 and ∂ S ϕ (t 2 F) ≥ 0 hold by definition of ∂ S ϕ to get the result.

Complexity of polygraphic programs

Example 3.3.4. Let us compute these bounding maps for the fusion sort function 2-cell of the polygraphic program F:

P (2x + 1) = 2x 2 + 1 and Q (2x + 1) = (2x 2 + 1) • 1 + (2x + 1) 2 .
Let us fix a list [i 1 ; . . . ; i n ] of natural numbers. One can check that, in F, this list is represented by a 2-path t such that ϕ(t) = ||t|| = 2n + 1. The polynomial P tells us that, during the computation of the sorted list (t), there will be at most 2n 2 + 1 applications of computation 3-cells. The polynomial Q bounds the total number of 3-cells of any type.

For example, when n is 2, one computes (t) by building a 3-path of size at most Q (5) = 234, containing no more than P (5) = 9 computation 3-cells. One can check that the 3-path presented in Example 1.4.8 is (way) below these bounds: it is made of seven 3-cells, six of which are of the computation kind.

Polygraphic programs and polynomial-time functions

Definition 3.4.1. Let P be a polygraphic program. A differential interpretation ∂ of P is polynomial when, for every function 2-cell , the map ∂ is bounded by a polynomial. A functorial interpretation ϕ of P is polynomial when ∂ ϕ is. A polygraphic interpretation is polynomial when both its functorial part and differential part are.

We denote by P the set of polygraphic programs which are confluent and complete and which admit an additive, cartesian and polynomial polygraphic interpretation that is conservative on and strictly compatible with their computation 3-cells.

As a consequence of previous results, the two polygraphic programs D, computing euclidean division, and F, computing the fusion sort of lists, are in P. We also introduce another example that we shall use thereafter. Proof. The polygraphic program N is orthogonal, hence locally confluent, and complete. Furthermore, the following hold:

n N, (m, n) = m + n, (m, n) = mn.
Then, one checks that the following polygraphic interpretation has all the required properties:

ϕ(n) = N -{0} , c = c = 1, ϕ( )(x, y) = x + y, ϕ( )(x, y) = xy, ∂ (x, y) = x and ∂ (x, y) = (x + 1)y.
Remark. So N computes addition and multiplication of natural numbers. As we have seen, it also computes duplication and permutation on them. As a consequence, for every polynomial P in N[x], one can choose a 2-path P in N such that P is P. Moreover, by induction, one proves that ϕ( P ) = P and that ∂ P is bounded by a polynomial in N[x].

Theorem 3.4.4. The polygraphic programs of P compute exactly the FPTIME functions.

Proof. The fact that a function computed by a polygraphic program in P is in FPTIME is a consequence of the results of Proposition 3.3.3. Indeed, it proves that the size of any computation of is bounded by Q applied to the size of the arguments: from the polynomial assumption and the definition of Q , this map is itself bounded by a polynomial. Moreover each 3-cell application modifies only finitely many 2-cells: hence the sizes of the 2-paths remain polynomial all along the computation. Furthermore, any step of computation can be done in polynomial time with respect to the size of the current 2-path. Indeed, it corresponds to finding a pattern and, then, replace it by another one: it is just a reordering of some pointers with a finite number of memory allocations. So, the computation involves a polynomial number of steps, each of which can be performed in polynomial time. Thus, the normalization process can be done in polynomial time.

Conversely, let f : Σ → Σ be a function of class FPTIME. This means that there exists a Turing machine M = (Σ, Q, q 0 , q f , δ) and a polynomial P in N[x] such that the machine M computes f and, for any word w of length n in Σ , the number of transition steps required by M to compute f(w) is bounded by P(n). We extend the polygraphic program N into P(M, P), by adding the following extra cells, adapted from the ones of the polygraphic Turing machine P(M) used in the proof of Theorem 1.5.2, in order to use P as a clock:

1. An extra 1-cell w. (b) Function 2-cells: the main : w ⇒ w for f, plus the modified q a , q ∈ Q and a ∈ Σ, now from n 0 w 0 w to w, plus an extra size function : w ⇒ n. both when δ(q 1 , a) = (q 2 , c, L)

both when δ(q 1 , a) = (q 2 , c, R) a q 2 b q f a q 0 q 1 a q 1 a q 2 b q 1 a q 2 q 1 q 2

One checks that P(M, P) is orthogonal and complete. We equip it with the polygraphic interpretation based on the one defined on N in the proof of Proposition 3. One checks that this polygraphic interpretation is additive, cartesian, polynomial, compatible with and conservative on all the computation 3-cells. Hence, P(M, P) is a polygraphic program in P. Furthermore, one has n N and w Σ . We also note that, among functions computed by P(M, P), one proves that : w → n is the length function. The four middle families of computation 3-cells of N are once again in bijection with the rules defining the transition relation of the Turing machine M. Hence, the configuration (q, a, w l , w r ) reduces into (q , a , w l , w r ) in k ∈ N steps if and only if, for any n ≥ k, one has: n 0 w l 0 w r 1 q a n -k 0 w l 0 w r 1 q a .

Finally, let us fix a word w of length n in Σ . The Turing machine computes f, so that (q 0 , , e, w) reduces into a unique configuration (q f , a, v, f(w)), after a finite number k of transition steps. Then we check the following chain of equalities, yielding = f:

(w) = q 0 P(n) 0 0 w = q f a P(n) -k 0 v 0 f(w) = f(w).

Future directions

Polygraphic programs -The definition we have chosen for this study stays close to the one of first-order functional programs. We shall explore generalization along different directions. We think that an important research trail concerns the understanding of the algebraic properties of the if-then-else construction in polygraphic terms. Towards this goal, we want to describe strategies as sets of 4-dimensional cells. The 3-paths will contain all the computational paths one can build when there is no fixed evaluation strategy, while the strategies and conditions will be represented by the 4-paths, seen as normalization processes of 3-paths. In particular, this setting shall allow us to internalize the test used to compute the merge function in the fusion sort algorithm, but also to describe conditional or probabilistic rewriting systems.

On another point, in the polygraphs we consider here, we have fixed a sublayer made of permutations, duplications and erasers, together with natural polygraphic interpretations for them. However, one can see them as a special kind of function 2-cells. Thus, we shall define a notion of hierarchical programs, where one builds functions level after level, giving complexity bounds for them modulo the previously defined functions. However, this does not prevent us to build modules that a programmer can freely use as sublayers, without bothering with the complexity of their functions: for example, a module that describes the evaluation and coevaluation. We think of this module system as a first possibility to integrate polymorphism into the polygraphic setting.

Removing duplication and erasure from the standard definition means that one moves from a cartesian setting to a monoidal one. According to a variant of André Joyal's paradox [START_REF] Lambek | Introduction to higher-order categorical logic[END_REF], this is necessary to describe functions such as linear maps on finite-dimensional vector spaces. Thus, one should be able to compute, for example, algebraic cooperations, such as the ones found in Jean-Louis Loday's generalized bialgebras [START_REF] Loday | Generalized bialgebras and triples of operads[END_REF], or automorphisms of C n , such as the universal Deutsch gate [START_REF] Nielsen | Quantum computation and quantum information[END_REF] of quantum circuits.

Going further, at this step, there will be no reason anymore to consider constructor 2-cells with one output only or values with no output. This way, one could consider algorithms computing, for example, on braids or knots. However, this also suggests to change our notion of function 2-cells to some kind of "polygraphic context", a notion of 2-path with holes whose algebraic structure has yet to be understood. In particular, this is the second solution we think of to describe polymorphic types and functions.

For all this research, we shall consider a more abstract definition of polygraphs: they are special higher-dimensional categories, namely the free ones. This formulation, though leading to a steeper learning curve, shall provide enlightenments about the possibilities one has when one wants to extend the setting. But, more importantly, this will make easier adaptation of tools from algebra for program analysis.

Analysis tools -In future work, we shall use other possibilities provided by polygraphic interpretations, together with other algebraic tools, to study the computational properties of polygraphs.

We restricted interpretations to be polynomials with integer coefficients. This is close to the tools considered in [START_REF]Algorithms with polynomial interpretation termination proofs[END_REF]. Following this last paper, a straightforward characterization of exponential-time (resp. doubly exponential-time) can be done by considering linear (resp. polynomial) interpretations for constructors, instead of additive ones. However, some studies are much more promising. First, to turn to polynomials over reals give some procedures to build interpretations (see [START_REF] Bonfante | Synthesis of quasiinterpretations[END_REF]) via Alfred Tarski's decidability [START_REF] Tarski | A decision method for elementary algebra and geometry[END_REF]. Second, we plan to consider differential interpretations with values in multisets (instead of natural numbers), to characterize polynomial-space computations.

  let rec sort = function | [] -> [] | x::[] -> x::[] | x::y::l -> let (l1,l2)=split(l) in merge(sort(x::l1),sort(y::l2))

1 . 3 ,

 13 A polygraphic program is a finite 3-polygraph P with one 0-cell, thereafter denoted by * , and such that its sets of 2-cells and of 3-cells respectively decompose into P 2 = P with the following conditions:

Example 1 . 3 . 2 . 3 .Example 1 . 3 . 3 .

 1323133 The following polygraphic program D computes the euclidean division on natural numbers (we formally define what this means later): 1. A computational model based on polygraphs 2. Apart from the fixed three structure 2-cells, it has two constructor 2-cells, : * ⇒ n for zero and : n ⇒ n for the successor operation, and two function 2-cells, : n 0 n ⇒ n for the minus function and : n 0 n ⇒ n for the division function. Its 3-cells are made of eight structure 3-cells, plus the following five computation 3-cells: The following program F computes the fusion sort function on lists of natural numbers lower or equal than some constant N ∈ N:

Example 2 . 1 . 3 .

 213 Let P be a polygraphic program with no constructor 2-cell and no function 2-cell. Then, given a non-empty part ϕ(ξ) of N -{0} for every 1-cell ξ, the following values extend ϕ into a functorial interpretation of P: ϕ ξ,ζ (x, y) = (y, x) and ϕ ξ (x) = (x, x).

Example 2 . 1 . 4 .

 214 The following values extend the ones of Example 2.1.3 into a functorial interpretation of the polygraphic program D of division:

Example 2 . 1 . 5 .

 215 For the polygraphic program F of fusion sort, we extend the functorial interpretation of Example 2.1.3 with the following values, where • and • stand for the rounding functions, respectively by excess and by default:

  Lemma 2.3.4 allows one to define a differential interpretation by giving its values on 2-cells.Example 2.3.5. The trivial functorial interpretation of a 3-polygraph P sends every 1-cell to some fixed one-element part * of N -{0} and every 2-path from u to v to the only possible map from ϕ(u) * to ϕ(v) * . Now, let us fix a family X of 2-cells in P. One can check that the map ||•|| X is the differential interpretation of P over the trivial interpretation and into (N, +, 0), sending a 2-cell to 1 if it is in X and 0 otherwise. Example 2.3.6. We consider the differential interpretation of the division polygraphic program D, over the functorial interpretation given in Example 2.1.4, into (N, +, 0), sending every constructor and structure 2-cell to zero and: ∂ (x, y) = y + 1 and ∂ (x, y) = xy + x, Example 2.3.7. For the polygraphic program F of fusion sort, we consider the differential interpretation, over the functorial interpretation of Example 2.1.5, into (N, +, 0), sending every constructor and structure 2-cells to zero and:

Example 3 . 1 . 9 .

 319 Applied to Example 1.3.3, Proposition 3.1.8 tells us that, given a list t, any intermediate value produced by the computation of the sorted list (t) has its size bounded by M (||t||) = ||t||. This means that recursive calls made during this computation are applied to arguments of size at most ||t||.

  x). Now, we fix a 1-path u, 1-cells ξ, ζ and a constructor 2-cell : u → ξ in P. Let us consider x ∈ ϕ(u) and y ∈ ϕ(ζ) and check that the following equalities hold, yielding the compatibility of ϕ on structure 3-cells: ϕ (x, y) = (y, ϕ(x)) = ϕ (x, y), ϕ (y, x) = (ϕ(x), y) = ϕ (y, x), 3. Complexity of polygraphic programs ϕ (x) = (ϕ(x), ϕ(x)) = ϕ (x), ϕ (x) = * = ϕ (x).

Example 3 . 2 . 8 .

 328 For the polygraphic program of Example 1.3.3, we have K = 1. The polynomials bounding the structure interpretation increase after application of one of the computation 3-cells of this polygraphic program are:

Definition 3 . 4 . 2 . 3 . 3 . 4 . 3 . 4 . 3 .

 342334343 Let us denote by N the polygraphic program with the following cells: 1. It has one 1-cell n.2. Its 2-cells are the three possible structure 2-cells plus: (a) Constructor 2-cells: for zero and for the successor. (b) Function 2-cells: for addition and for multiplication. Its 3-cells are the eight structure 3-cells plus the following computation 3-cells: Polygraphic programs and polynomial-time functions Proposition The polygraphic program N is in P and it computes the addition and multiplication of natural numbers.

2 .

 2 Extra 2-cells include the five new structure 2-cells plus: (a) Constructor 2-cells: the empty word : * ⇒ w and each letter a : w ⇒ w of Σ.

3 .

 3 Extra 3-cells include the new structure ones plus: (a) The computation 3-cells for the auxiliary function : a (b) Timed versions of the computation 3-cells for the Turing machine:

  4.3, extended with the following values:c = c a = 1, ϕ( )(x) = x, ϕ( q a )(x, y, z) = x + y + z, ϕ( )(x) = P(x) + x + 1, ∂ (x) = ∂ q a (x, y, z) = x, ∂(x)= ∂ P (x) + P(x) + x + 1.

  assumption, ϕ and ∂ are compatible with α, hence ϕ(s 2 α) ≥ ϕ(t 2 α) and ∂(s 2 α) ∂(t 2 α) hold. Then one applies Lemmas 2.1.7 and 2.3.8 to get ∂(s 2 F) ∂(t 2 F) and, when ∂ is strictly compatible with the 3-cell α, ∂(s 2

It has one 1-cell n, standing for the type of natural numbers.

Support -This work has been partially supported by ANR Inval project (ANR-05-BLAN-0267).

For each generalization of the notion of polygraphic program, such as the ones mentioned earlier, we shall adapt polygraphic interpretations in consequence. We think that, if these generalizations are done in an elegant way, this task will be easier. For example, if one considers "symmetric" values, i.e. values with inputs, one can use a third part of polygraphic interpretations we have not used here: ascending currents, described by a contravariant functorial part, such as in the original definition [START_REF]Termination orders for 3-dimensional rewriting[END_REF].

As pointed earlier, polygraphs are higher dimensional-categories. Philippe Malbos and the second author are currently adapting the finite derivation criterion of Craig Squier [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] to them, as was done before for 1-categories [START_REF] Malbos | For string rewriting systems the homotopical and homological finiteness conditions coincide[END_REF]. We think that this will lead us to a computable necessary condition to ensure that a function admits a finite, convergent polygraphic program that computes it.

The same collaboration has more long-term aims: using tools from homological algebra for program analysis. For example, the functorial and differential interpretations are special cases of, respectively, left modules over the 2-category of 2-paths (or bimodules, when there are ascending currents) and derivations of this same 2-category into the given module. Moreover, a well-chosen cohomology theory yields, in particular, information on derivations: thus, one can hope to get new tools such as negative results about the fact that a given algorithm lives in a given complexity class.

Cat -The main concrete objective of this project is to develop a new programming language, codenamed Cat. In this setting, one will build a program as a polygraph, while using the algebraic analysis tools we provide to produce certificates that guarantee several properties of the code, such as grammatical ones, computational ones or semantical ones. As in Caml [START_REF]The Caml Language, caml[END_REF], a Cat program will have two aspects: an implementation and an interface.

In the implementation, one builds the code, describing the cells and assembling them to build paths, i.e. building the data types, the functions, the computation rules and the evaluation strategies. Thanks to the dual nature of polygraphs, one shall be able to perform this using an environment that is either totally graphical, totally syntactical or some hybrid possibility between those.

The interface part contains all the information the programmer can prove on its code, in the form of certificates. These guaranteed properties will range from type information, as in Caml, to polygraphic interpretations proving termination or giving complexity bounds, to proofs of semantical properties in the form of polygraphic three-dimensional proofs [START_REF]The three dimensions of proofs[END_REF]. For all these certificates, we shall propose assistants, with tactics that automatize the simpler tasks and leave the programmer concentrate on the harder parts.

Finally, given such a polygraphic program, the question of evaluation arises. One can think of several solutions, whose respective difficulty ranges from "feasible" to "science-fiction": first, a compiler or an interpreter into some existing language, such as Tom [START_REF] Tom | loria.fr[END_REF], a task that has already been started; then, a distributed execution where each 2-cell is translated into a process, whose behaviour is described by the corresponding 3-cells; finally, concrete electronic chips dedicated to polygraphic computation.


Tieying Xu

Maria A Lizarralde-Iragorri

Olivier Français

Wassim El Nemer

Bruno Le Pioufle

APPLYING SUCCESSIVE MECHANICAL STRESSES ON CIRCULATING CELLS USING MICROFLUIDIC VASCULAR NETWORK TO ASSESS SICKLED RED BLOOD CELLS RIGIDITY

Keywords: Sickle Cell Disease, Red Blood Cell, Microfluidic, Successive Mechanical Stress

Thanks to their membrane elasticity and fluidity, red blood cells (RBCs) are capable to pass through the smallest microcapillaries while exchanging oxygen and CO2 with organs. For several blood disorders like sickle cells disease (SCD), RBCs lose their deformability leading to vaso-occlusions. To assess the deformability of RBC, successive mechanical stresses are applied in our device mimicking blood microcapillaries network, while RBCs circulating being monitored optically by microscopy. Normal and sickled RBCs behaviors are compared using such approach. This device could be a promising tool for the diagnostic of different blood disorders.

INTRODUCTION

Mature RBCs do not have any DNA-containing nucleus and show an important surface to volume ratio. Presenting a biconcave shape, cells have an average diameter of 8 µm and an average thickness of 2 µm, and their high capability to deform allows them to be squeezed and to transit through microcapillaries smaller than their own dimensions [START_REF] Steck | The organization of proteins in the human red blood cell membrane[END_REF]. In the case of sickle cell disease (SCD), because of the polymerization of abnormal hemoglobin S (HbS) [START_REF] Pauling | Sickle Cell Anemia, a Molecular Disease[END_REF], sickled cells become more rigid, leading to painful vaso-occlusive crisis. To compare RBCs of different pathological situations, in vitro experiments are carried out where successive mechanical stresses are induced on RBCs, using a microfluidic device mimicking vascular microcapillaries network. RBCs circulating behaviors are optically monitored, which allows to assess sickled red blood cells rigidity and cell deformability recovery.

THEORY

To realize a device mimicking microfluidic vascular capillaries network, applying the Poiseuille flow theory, the linear relationship between pressure and flow was taken into consideration: ΔP=Rh•Q, where ΔP corresponds to the pressure difference between inlet and outlet of the microcapillaries network. Rh represents the hydraulic resistance and Q represents the flow rate. As the lowest expected pressure ΔP, which allows maintaining RBC microcirculation, equals to 100 mbar and the corresponding Q equals to 100 μL•h -1 , the expected value of the hydraulic resistance for this microcapillaries network is required to be of the order of magnitude close to 3.6 × 10 -4 Pa•s•μm -3 [START_REF] Lizarralde Iragorri | A microfluidic approach to study the effect of mechanical stress on erythrocytes in sickle cell disease[END_REF].

EXPERIMENTAL

The mimicking microfluidic vascular capillaries network was realized by Polydimethylsiloxane (PDMS) replica molding procedure [START_REF] Xu | Characterization of red blood cell microcirculatory parameters using a bioimpedance microfluidic device[END_REF]. The SU-8 resin mold contains 3 layers: i) SU-8 2002 layer for microcapillaries network of the height equal to 2 µm; ii) SU-8 2005 layer for inlet and outlet zone of the network (height equal to 5 µm); iii) SU-8 2025 layer for large connection of network (height equal to 25 µm). The network contains 24 branches of microcapillaries in parallel. Each branch contains 10 microcapillaries in series. One single microcapillary has a symmetric structure that containing a restriction at the center to induce mechanical stress on RBC (length of 30 µm, cross section of 5 × 2 µm 2 ). At both side of the restriction, a wider section (length of 30 µm, cross section of 10 × 2 µm 2 ) followed by a big section (length of 20 µm, cross section of 20 × 2 µm 2 ) was designed as a buffer area for RBC recovering. The chosen dimensions need to take into account the expected value of the network hydraulic resistance.

The PDMS chip containing microcapillaries network was reversibly assembled above a quartz substrate. In order to ensure the single cell transiting within the restriction, RBCs suspension (2%) was introduced by depressurization of -250 mbar. Thanks to a thin film of parylene C (3.5 µm) covering external surface of PDMS chip, air bubbles were prevented during the whole experiment. RBCs circulating was recorded by a Phantom Miro M 320 S high-speed camera connected to an inverted AxioObserver Z1 microscope (Zeiss). The sampling duration τ was equal to 625 µs between 2 frames. The RBC transit time T was achieved by multiplying the sampling duration multiple and frames number n: T= τ•n.

RESULTS AND DISCUSSION

For normal RBCs (NA=71 cells in total), the mean value of transit time to pass through the 3 rd and the 7 th restriction in series are respectively 7.5 ms (µA3) and 8.13 ms (µA7), indicating a mean transit time increase ( ∆µ 𝐴𝐴 = µ 𝐴𝐴3 µ 𝐴𝐴7 -µ 𝐴𝐴3

) equals to 8.4%. For sickled RBCs (NS=73), the mean value of transit time to pass through the 3 rd and the 7 th µ 𝐴𝐴3 restriction equal to 7.54 ms (µS3) and 8.79 ms (µS7), with an increase ( ∆µ 𝑆𝑆 = µ 𝑆𝑆7 -µ 𝑆𝑆3 ) of 16.6%. The recovery of RBC

µ 𝑆𝑆3 µ 𝑆𝑆3
deformability after passing successive restrictions shows to be lower in the case of sickled cells.

CONCLUSION

Successive mechanical stress effect on RBCs of different pathological states was analyzed using our microcapillaries network chip. Clear evidence of lower recovery of the cell deformability, after transiting multiple restrictions, was demonstrated for sickled cells, using our microfluidic device. This device could be a diagnostic tool allowing in vitro analysis of RBC cycle in blood vascular microcapillaries system for patients of SCD or different blood disorders.

Figure 1 :

 1 Figure 1: A. Mimicking microfluidic vascular capillaries network; B. Successive restrictions in series; Histogram of transit time: C. for normal RBC transiting in 3 rd restriction; D. for sickled RBC transiting in 3 rd restriction; E. for normal RBC transiting in 7 th restriction; F. for sickled RBC transiting in 7 th restriction; Transit time delay histogram: G. for normal RBCs (NA=71); H. for sickled RBCs (NS=73).

ACKNOWLEDGEMENTS

The authors acknowledge the Labex LaSIPS (ANR-10-LABX-0040-Lasips), the "Ecole Doctorale EOBE" of Université Paris-Saclay, the "Institut d'Alembert" and the "CNRS" for project fundings.