Malika Auvray

Yann Kechabia

Gabriel Arnold

come

Providing proprioceptive feedback by means of vibrotactile stimuli: A way to improve body integration of a prosthetic arm

I. INTRODUCTION

Prosthetic arms allow amputees to perform a broad range of movements. However, these technologies still face some limitations. The lack of some active joints, the absence of sensory feedback, the complexity of the command, and the resulting cognitive load lead many amputated patients to stop using their prosthesis: 38% in [START_REF] Wright | Prosthetic usage in major upper extremity amputations[END_REF], 20% in [START_REF] Biddiss | Upper-limb prosthetics: critical factors in device abandonment[END_REF]. For those still using them, these issues limit the overall ease with the device and reduce their users' capabilities and autonomy [START_REF] Antfolk | Sensory feedback in upper limb prosthetics[END_REF]. In particular, the absence of sensory feedback forces amputees to rely on vision only. This results in slow and cognitively heavy processes, insufficient to appreciate physical interactions [START_REF] Antfolk | Sensory feedback in upper limb prosthetics[END_REF]. It has been underlined that one of the main requests from users is to have control mechanisms that require less visual attention [START_REF] Atkins | Epidemiologic overview of individuals with upper-limb loss and their reported research priorities[END_REF]. A promising way to achieve this goal consists in developing artificial tactile or vibro-tactile feedback. To do so, methodologies were borrowed from sensory substitution, that is, the projection of information from one deficient sensory modality to an intact one, as is commonly used in the field of assistive technologies for visual impairments [START_REF] Deroy | A crossmodal perspective on sensory substitution[END_REF][START_REF] Arnold | Individual differences in sensory substitution[END_REF][START_REF] Auvray | The perception of space and form recognition in a simulated environment: The case of minimalist sensory-substitution devices[END_REF].

Attempts to provide proprioceptive feedback were done both in invasive and non-invasive ways [START_REF] Riso | Strategies for providing upper extremity amputees with tactile and hand position feedback-moving closer to the bionic arm[END_REF]. In particular, previous studies coded proprioceptive cues by tactile feedback in the context of prosthetics. These studies focused on information about hand opening [START_REF] Witteveen | Vibro-and electrotactile user feedback on hand opening for myoelectric forearm prostheses[END_REF] and grasping force [START_REF] Dosen | Building an internal model of a myoelectric prosthesis via closed-loop control for consistent and routine grasping[END_REF][START_REF] Antfolk | A tactile display system for hand prostheses to discriminate pressure and individual finger localization[END_REF], useful for grasping tasks, location of the prosthetic hand [START_REF] Christiansen | Vibrotactile feedback of pose error enhances myoelectric control of a prosthetic hand[END_REF], and sense of position and motion, this time by inducing rotational skin stretch on the user's skin [START_REF] Wheeler | Investigation of rotational skin stretch for proprioceptive feedback with application to myoelectric systems[END_REF]. In the study reported here, the proprioceptive cue of wrist rotation was coded into vibro-tactile feedback. We investigated if this sensory feedback allows improving performance with a prosthetic arm. *Research supported by the labex SMART (ANR-11-LABX-65) and the Mission pour l'interdisciplinarité (CNRS, Auton, Sublima Grant). M.A., Y.K., N.J. are at Sorbonne Université, UPMC, CNRS, Institut des Systémes Intelligents et de Robotique (ISIR), Paris, France (e-mails: auvray@isir.upmc.fr, yannkechabia@gmail.com, jarrasse@isir.upmc.fr) G.A. is at the Company Caylar, Orsay, France (e-mail gabriel.arnold@caylar.net).

II. METHODS

Participants. Twenty three healthy participants completed the experiment (12 females, mean age: 23.4, ranging between 21 and 32 years). All the participants provided informed consent and were naive to the purpose of the experiment, which took approximately 30 min to complete.

Materials. The materials consisted of a prosthetic arm and a vibro-tactile bracelet. In order to control the prosthesis, two cutaneous electrodes, with an acquisition frequency of 10 Hertz, were used to receive the electromyographic signals.

The electrodes were placed on two muscles on the participants' arm: the flexor and the extensor. Whenever there was a muscle contraction, signals were generated, filtered, and amplified inside the electrode. The tactile feedback was given through a bracelet made of scratch on which 6 vibrators (Haptuator Mark II, Tactile Labs, Montreal, Canada) were equidistantly located, so that they were separated by a 30° angle (see Fig. 1).

Figure 1. Image of the experimental set-up

Procedure. The experiment was divided into four successive steps.

Step 1. Familiarization with the set-up. The participants were first trained to use the myoelectric command without feedback during a couple of minutes. Then, they were explained the functioning of the vibrotactile bracelet.

Step 2. Pre-test. The participants completed 2 successive series of 6 orientations to reach (12 trials in total). At the beginning of each trial, the participants received information about the starting orientation of the hand which was set at

Providing proprioceptive feedback by means of vibrotactile stimuli:

A way to improve body integration of a prosthetic arm* M. Auvray, Y. Kechabia, G. Arnold, and N. Jarasse 0°. Then, one of the 6 vibrators was activated, which corresponded to one of the 6 orientations to reach [-90°, -60°, -30°, 30°, 60°, 90°]. The participants were asked to perform a movement by pronosupination of the prosthesis' wrist by means of the myoelectric command, in order to reach the target orientation. The participants held a go-no-go button that they had to press just before initiating a movement and again once they reached the target orientation. At the end of each trial, the prosthesis was automatically repositioned at the 0° starting orientation.

Step 3. Learning phase. The participants had to complete 5 successive series of 6 orientations to reach (30 trials in total). The procedure was similar to step 2, except that, this time, the participants chose the orientations to reach. The 6 possible hand orientations were shown visually. The participants had to complete an entire grid of 6 orientations before completing the next grid. The participants' task was to move the prosthesis by pronosupination of the wrist so that their prosthesis and the corresponding image have the same orientation. In order to measure the influence of vision on learning, half of the participants completed step 3 with vision and the other half without. In the condition without vision, a cover fell back on the prosthesis during movement.

Step 4. Post-test. Identical to step 2.

III. RESULTS

IV. CONCLUSION

Our results show that training with a vibro-tactile feedback about wrist rotations allows improving participants' performance in terms of movement preparation time. Regarding spatial accuracy, our results does not show significant improvement after training. Although there was a numerical trend in this direction, more participants are needed to confirm this trend. In addition, our results do not allow for now concluding on the interest of vision during learning. Interestingly, the learning protocol used here allowed performance improvement in as few as 30 trials, which is promising for further attempts of providing proprioceptive feedback by means of tactile stimuli. Our next steps will involve testing our protocols with transhumeral amputees and extend our findings to additional artificial sensory feedbacks on proprioceptive information.

Figure 2 .

 2 Figure 2. Percentage of spatial error and Movement preparation time obtained in the conditions with vibration and vision (VV) and with vibration and no vision (VN). Two dependent variables were computed: Percentage of spatial error and Movement preparation time. Repeated measures ANOVAs were conducted on these two dependent variables with the factors Learning (pre-test versus post-test) and Visual condition (with vision versus without vision during the learning phase). Regarding the Percentage of spatial error, the analysis showed a significant effect of Visual condition [F (1, 22): 10.63, p<0.01], no effect of Learning, and no significant interaction between these two factors (both ps>0.05). Regarding Movement preparation time, the analysis showed a significant effect of Learning [F (1, 22): 5.22, p<0.05], no effect of vision, and no significant


Assia Mahboubi

Matthieu Piquerez

A First Order Theory of Diagram Chasing

Keywords: 2012 ACM Subject Classification Theory of computation → Logic and verification Diagram chasing, formal proofs, abelian categories, decidability Digital Object Identifier 10.4230/LIPIcs.CVIT.2016.23

This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order theory, and we study the models and decidability of this theory. The longer-term motivation of this work is the design of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers.

Introduction

Homological algebra [START_REF] Mac | Homology. Class. Math[END_REF][START_REF] May | A concise course in algebraic topology[END_REF] attaches and studies a sequence of algebraic objects, typically groups or modules, to a certain space, e.g., a ring or a topological space, in order to better understand the latter. In this field, diagram chasing is a major proof technique, which is usually carried out via a form of diagrammatic reasoning on abelian categories. Diagrams appear as early as in the introduction of Mac Lane's classic reference book [START_REF] Mac | Categories for the working mathematician[END_REF], while Riehl's textbook devotes a section to the art of diagram chase [START_REF] Riehl | Category Theory in Context[END_REF]Section 1.6]. Lawvere and Schanuel's pedagogical introduction to category theory [START_REF] Lawvere | Conceptual mathematics. A first introduction to categories[END_REF]Session 17] uses an entire session to discuss the role of graphs in diagrammatic categorical reasoning.

A diagram can be seen as a functor F : J → C, whose domain J, the indexing category, is a small category [START_REF] Riehl | Category Theory in Context[END_REF] sometimes also called the shape of the diagram [START_REF] May | A concise course in algebraic topology[END_REF]. Diagrams are usually represented as directed multi-graphs, also called quivers, whose vertices are decorated with objects of C, and arrows with morphisms. Paths in such graphs thus correspond to chains of composable arrows. Diagrams allow for visualizing the existence of certain morphisms, and to study identities between certain compositions of morphisms. In particular, a diagram commutes when any two paths with same source and target lead to identical composite. For instance, the commutativity of the diagram on Figure 1 asserts that morphism e is equal to the composition of morphisms a and b, denoted by b • a, as well as to the composition d • c. Commutativity of diagrams in certain categories can be used to state more involved properties, and diagram chasing essentially consists in establishing the existence, injectivity, surjectivity of certain morphisms, or the exactness of some sequences, using hypotheses of the "by diagram chasing", also called diagram chases. On paper, diagrams help conveying in a convincing manner proofs otherwise consisting of overly pedestrian chains of equations. The tension between readability and elusiveness may however become a challenge. For instance, diagram chases may rely on non-trivial duality arguments, that is, on the fact that a property about diagrams in any abelian category remains true after reversing all the involved arrows, although the replay of a given proof mutatis mutandis cannot be fulfilled in general. Motivated in part by the second author's experience in writing intricate diagram chases (see for instance [16, p.338]), this work aims at laying the foundations of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers. The present article discusses the design of a formal language for statements of properties amenable to proofs by diagram chasing, according to three objectives. The first is simplicity and expressivity: this language should be at the same time simple enough to be implemented in a formal library, and expressive enough to encompass the desired corpus of results. Then, duality arguments in proofs shall follow directly from a meta-property of the language. Finally, the corresponding proof system should allow for automating proofs of commutativity clauses. Observe for instance, that the commutativity of the square diagram of Figure 1 follows from that of the two triangle sub-diagrams: the concluding step in diagram chases usually amounts to a such a commutativity clause. Automating the mundane proofs of commutativity clauses amounts to studying a decision problem hereafter referred to as the commerge problem: Given a collection of sub-diagrams of a larger diagram which commute, must the entire diagram commute?

For this purpose, we introduce the two following formal languages.

▶ Definition 1. We define a many-sorted signature Σ with sorts the collection of finite quivers. Signature Σ has one function symbol restr m :

Q ′ →Q , of arity Q → Q ′ , per each quiver morphism m : Q ′ → Q between two quivers Q and Q ′ ,
m : Q ′ →Q , of arity Q → Q ′ , per each injective quiver morphism m : Q ′ → Q between two quivers Q and Q ′ ,
and one predicate symbol commute Q , on sort Q, for each finite acyclic quiver Q.

The thesis of the present article is that signature Σ fulfills the three above objectives. We validate this thesis by giving a first-order theory for diagrams in small and abelian small categories respectively. We state and prove a duality theorem and motivate the choice of Σ over the possibly more intuitive Σ by the automation objective.

The rest of the article is organized as follows. We first fix some vocabulary and notations in Section 2, so as in particular to make Definition 1 precise. Then, Section 3 introduces a theory for small categories and describes its models, Section 4 discusses duality, before Section 5 provides an analogue study for abelian categories. Finally in Section 6, we formalize and study the decidability of several variants of the commerge problem.

Preliminaries

In all what follows, N := {0, 1, . . . } refers to the set of non-negative integers. If k ∈ N, then [k] denotes the finite collection {0, . . . , k -1}. We denote card(A) the cardinal of a finite set A. We use the notation id for the identity map.

Quivers

In this section, we introduce some vocabulary and notations related to directed multi-graphs, also called simply graphs in some standard category theory textbooks [START_REF] Lawvere | Conceptual mathematics. A first introduction to categories[END_REF][START_REF] Mac | Categories for the working mathematician[END_REF]. In this article, we depart from these texts and use instead the term quiver.

▶ Definition 2 (General quiver, dual). A general quiver Q is a quadruple (V Q , A Q , s Q : A Q → V Q , t Q : A Q → V Q ) where V Q and A Q are two sets. The element of V Q are called the vertices of Q and the element of A Q are called arrows. If a ∈ A Q , s Q (a) is called the source of a and t Q (a) is called its target. The dual of a quiver Q is the quiver Q † := (V Q , A Q , t Q , s Q ),
which swaps the source and the target maps of Q.

▶ Definition 3 (Morphism, embedding, restriction). A morphism of quivers m :

Q → Q ′ , is the data of two maps m V : V Q → V Q ′ and m A : A Q → A Q ′ such that m V • s Q = s Q ′ • m A and m V • t Q = t Q ′ • m A . Such a morphism is called an embedding of quivers if moreover both m V and m A are injective. In this case we write m : Q → Q ′ . If A is a subset of A Q , the (spanning) restriction of Q to A denoted by Q| A is the quiver (V Q , A, s Q | A , t Q | A ). There is a canonical embedding Q| A → Q.
We denote by ∅ the empty quiver with no vertex and no arrow, and by S the set of quivers Q such that V Q and A Q are finite subsets of N. In this article, a quiver refers to an element of S. We use a non-cursive Q for elements of S, and a cursive Q for general quivers.

For the sake of readability, we use drawings to describe some elements of S, as for instance:

. . .

For a quiver Q denoted by such a drawing, the convention is that

V Q = [card(V Q )] and A Q = [card(A Q )].
From left to right, the drawn vertices correspond to 0, 1, . . . , card(V Q ) -1. Arrows are then numbered by sorting pairs (s Q , t Q ) in increasing lexicographical order, as in:

. . .

0 1 2 0 1 2 3
We also use drawings to denote embeddings. The black part represents the domain of the morphism, the union of black and gray parts represents its codomain. Here is an example of an embedding of the quiver .

. into the quiver drawn above. A path-quiver can be drawn as: If 0 ≤ k ≤ l are two integers, we denote by sp k,l : PQ k → PQ l the leftmost embedding of PQ k into PQ l , i.e., such that (sp k,l ) V (0) = 0. If k and l are clear from the context, we draw sp k,l as if k ̸ = 0 and as . if k = 0. Moreover, we denote by tp k,l : PQ k → PQ l the rightmost embedding of PQ k into PQ l , i.e., such that (tp k,l ) V (k) = l. The corresponding drawings are and . . Moreover, if P is a nontrivial path-quiver, we define st P : . . → P to be the embedding mapping the first vertex on the leftmost vertex of P and the second vertex on the rightmost vertex of P . We denote this embedding . . . If Q is a general quiver, a morphism of the form p : PQ k → Q, for some k, is called a path of Q from u to v of length k, where u := p(0) and v := p(k). If moreover p A is injective, it is called a trail [START_REF] West | Introduction to graph theory[END_REF]. A trail p such that p V (0

C V I T
) = p V (k) is called a cycle. Two paths p 1 : P 1 → Q, p 2 : P 2 → Q of Q have the same extremities if p 1 • st P1 = p 2 • st P2 .
We denote by BP Q , resp. BT Q , the set of pairs of paths, resp. of trails, of Q having the same extremities. Such a pair is called a bipath, resp. a bitrail.

A general quiver is acyclic if any path of this quiver is an embedding. The set of acyclic quivers in S is denoted by S.

We now recall the definition of a free category (see for instance [START_REF] Mac | Categories for the working mathematician[END_REF]Section II.7]).

▶ Definition 5 (Free category). For a general quiver Q, the free category over Q, denoted by ⟨Q⟩ is the category with objects Ob ⟨Q⟩ = V Q whose morphisms Hom ⟨Q⟩ (u, v), for two vertices u and v are the paths from u to v. The identity map from u to u is the empty path, and the composition is defined as the concatenation of paths.

Note that a morphism m of quivers induces a functor between the corresponding categories that we denote by Φ m . In the other direction, any small category C has an underlying quiver.

Diagrams

The purpose of this section is to introduce diagrams in a category, and to define what it means for a diagram to commute. We also introduce useful constructions later used for building new diagrams by restricting and pasting existing ones.

▶ Definition 6 (Diagram). For any category C and any quiver

Q, a diagram in C over Q is a functor from ⟨Q⟩ to C.
Definition 6 is actually a special case of D-shaped diagrams, for D a small category [START_REF] May | A concise course in algebraic topology[END_REF]. Thanks to the universal properties of free categories, it coincides with Mac Lane's Q-shaped diagrams in category C [13, Section II.7].

Let P be a path-quiver from vertex u to vertex v. To a diagram D : ⟨P ⟩ → C over P one can associate the corresponding composition of morphisms in the category C, which is an element of Hom C (D(u), D(v)). We denote this element comp(D). By convention, when the path-quiver P is trivial, comp(D) is the identity map id D(u) . ▶ Definition 7 (Pullback). Let Q, Q ′ be two quivers and let D be a diagram over Q. Let m : Q ′ → Q be a morphism of quivers. We define the pullback of D by m, denoted by m * (D),

as the diagram D • Φ m over Q ′ .
Note that term pullback here refers to pre-composition rather than to fiber products.

▶ Definition 8 (Commutative diagram). For any category C and any quiver

Q, a diagram D over Q is commutative if comp(p * 1 (D)
) and comp(p * 2 (D)) coincide for any two paths p 1 and p 2 in Q with same extremities, that is:

∀(p 1 , p 2 ) ∈ BP Q , comp(p * 1 (D)) = comp(p * 2 (D)). ▶ Definition 9 (Pushout configuration). Consider four quivers Q, Q 1 , Q 2 , Q ′ and four embed- dings m 1 : Q → Q 1 , m 2 : Q → Q 2 , m ′ 1 : Q 1 → Q ′ and m ′ 2 : Q 2 → Q ′ : Q Q 1 Q 2 Q ′ . m1 m2 m ′ 1 m ′ 2 This data is a pushout configuration if: m ′ 1 • m 1 = m ′ 2 • m 2 , Q ′ = Im(m ′ 1 ) ∪ Im(m ′ 2 ), (i.e., V Q ′ = Im(m ′ 1,V ) ∪ Im(m ′ 2,V ) and A Q ′ = Im(m ′ 1,A ) ∪ Im(m ′ 2,A )), Im(m ′ 1 • m 1 ) = Im(m ′ 1 ) ∩ Im(m ′ 2 ). In this case, the triple (Q ′ , m ′ 1 , m ′ 2 ) is called a pushout of (Q, Q 1 , Q 2 , m 1 , m 2 ). ▶ Remark 10. Any tuple (Q, Q 1 , Q 2 , m 1 , m 2 )
m * 1 (D 1 ) = m * 2 (D 2 )
then there exists a unique diagram

D ′ over Q ′ such that D 1 , resp. D 2 , is the pullback of D ′ by m ′ 1 , resp. m ′ 2 , i.e., D 1 = m ′ * 1 (D ′ ) and D 2 = m ′ * 2 (D ′ )
Proof. Immediate. ◀

Category congruences, path relations and quotient categories

We first introduce category congruences and quotients, following Mac Lane [13, Section II.8], and provide an important example thereof. However, we slightly depart from this reference by only considering the special case of quotients of categories by congruences, as it is the only one used in the present article.

P 1 = . . . . P 2 = . . . Q ′ = . . . . .

for any pair of objects A and B such that, for any objects A, B, C and any morphisms f, g ∈ Hom

C (A, B) and f ′ , g ′ ∈ Hom C (B, C), f ∼ g and f ′ ∼ g ′ =⇒ f ′ • f ∼ g ′ • g, where we write h ∼ h ′ if h and h ′ are in relation, i.e., (h, h ′ ) ∈ r E,F for some objects E and F . Such a relation is said complete if r A,B = Hom C (A, B)

Proof. Immediate. ◀

We now introduce relations on pairs of paths with same extremities in a general quiver: the ones that are induced from a congruence on the corresponding free category are of special interest.

▶ Definition 14. A relation between paths with same extremities in

Q is by definition a subset of BP Q . If r ⊆ BP Q is such a relation then, for (p, q) ∈ BP Q , we write p ∼ q if (p, q) ∈ r. Note that BP Q = A,B∈Ob ⟨Q⟩ Hom ⟨Q⟩ (A, B) 2 . Such a relation r is called a path relation if it is a category congruence on ⟨Q⟩. The complete path relation on Q, i.e., BP Q , is denoted by tot Q .
For instance, in a small category C the composition axiom induces a path relation on the underlying quiver Q. To be more precise, this relation is given by

{(p 1 , p 2 ) ∈ BP Q | comp(F • Φ p1 ) = comp(F • Φ p2 )}
where F is the canonical functor from ⟨Q⟩ to C. Following the usual notation of ideals, if r 0 , . . . , r l-1 are some relations between paths with same extremities, we denote by (r i | i ∈ [l]) the smallest path relation containing r 0 , . . . , r l-1 .

Let Q ′ be another general quiver and let m : Q → Q ′ be a morphism. If r ⊆ BP Q , we denote by m * (r) the relation induced by the image by m of r in BP Q ′ .

A finite characterization of commutative diagrams

Definition 8 about the commutativity of a finite diagram a priori relies on an infinite number of equations. In this section, we give an equivalent formulation based on the finite set BT Q .

▶ Lemma 15. Let Q be a quiver. The smallest path relation containing BT Q ⊆ BP Q is the total relation tot Q .
Proof. Denote this smallest path relation by r. It suffices to prove that any path is related with a trail. Let p be a path which is not a trail. Then p contains a nontrivial cycle, i.e., if we denote by ≫ the concatenation operator on paths, p = p 1 ≫ c ≫ p 2 for some paths p 1 and p 2 and some nontrivial cycle c. Since any cycle is a trail, the pair (c, c • . ) belongs to BT Q , where c • . is the path of length 0 based on c V (0). Hence p = p 1 ≫ c ≫ p 2 ∼ p 1 ≫ p 2 . This last past is strictly smaller, and we conclude by infinite descent. ◀

As a direct consequence of the previous lemma, we get the following proposition.

▶ Proposition 16. A diagram D over a finite quiver Q is commutative if and only if ∀(p 1 , p 2 ) ∈ BT Q , comp(p * 1 (D)) = comp(p * 2 (D)).

Many-sorted logic, categorical interpretation

We first recall a few basic definitions mostly pertaining to many-sorted logic, but instantiated to the signatures introduced by Definition 1, and we set the corresponding notations. Remember that signature Σ only differs from Σ by restricting the allowed sorts to the acyclic quivers and the allowed quiver morphisms to embeddings.

Let us first fix a countable set X, so that for each quiver Q in S (resp. in S), elements of the set X Q := X × {Q} are the variables of sort Q. A term of sort Q either is a variable of sort Q or has the form restr m : Q→Q ′ (t), with t a term of sort Q ′ , Q ′ a quiver and m : Q → Q ′ a morphism of quivers. When possible, we leave the sorts implicit and simplify the notation of symbol restr m : Q ′ →Q into restr m .

We denote the equality symbols by ≈, leaving sorts implicit. An atom is thus of the form s ≈ t with s and t two terms of the same sort, or of the form commute Q (t) with t a term of sort Q. We consider first-order many-sorted formulas and write the sort of quantifiers as a subscript, i.e.,

∃ Q x Q , ϕ and ∀ Q x Q , ϕ where Q ∈ S, x Q ∈ X Q and ϕ is a formula. We shorten ∀ Q x, ∀ Q y, P (x, y), resp. ∃ Q x, ∃ Q y, P (x, y), into ∀ Q x, y, P (x, y), resp. into ∃ Q x, y, P (x, y). We write ∃! Q y, P (y) for formula ∃ Q y, P (y) ∧ ∀ Q y 1 , y 2 , P (y 1 ) ∧ P (y 2 ) → y 1 ≈ y 2 . A formula with free variables x 1 , . . . , x n of respective sorts Q 1 , . . . , Q n is said to be of arity Q 1 × . . . Q n .
We now define standard, sometimes also called Tarskian [START_REF] Tarski | The semantic conception of truth and the foundations of semantics[END_REF], semantics for first-order theories on signatures Σ and Σ. We mostly follow classic presentations [START_REF] Hodges | A shorter model theory[END_REF] but adapted to the context of multi-sorted signatures.

▶ Definition 17 (Structures, models). A Σ-structure M, also called interpretation of Σ, is defined by: a collection of disjoint non-empty domain sets (M Q ) Q , indexed by the collection of (quiver) sorts; an interpretation of each function symbol restr m : Q ′ →Q , as a function restr M m : Q ′ →Q with domain M Q and codomain M Q ′ ; an interpretation of each predicate symbol commute Q , as a subset commute M Q of M Q . A given Σ-structure together with a variable assignment mapping any variable of sort Q to an element of domain M Q entail a truth value for any first-order formula ϕ on language Σ. If ϕ has no free variable, we write M |= ϕ if ϕ M is true and we say that ϕ is valid in M. A formula ϕ is satisfiable when there is a variable assignment which makes it true, and unsatisfiable in the opposite case. A model of a theory T on signature Σ is the interpretation of a Σ-structure such that every formula in T is true.

We also define analogue structures, interpretations, models for signature Σ.

The standard models of the signatures introduced in Definition 1 are actually diagrams in a certain category.

▶ Definition 18 (Categorical interpretation).

To each small category C, we associate an interpretation of Σ, resp. Σ, that we also denote by C, as follows:

To each sort Q we associate the set

C Q of diagrams in C over Q. restr m is interpreted as the function mapping a diagram D to the diagram m * (D). commute C
Q is the set of commutative diagrams in C over Q. We call such an interpretation a categorical interpretation of Σ, resp. Σ.

A theory for diagrams in small categories

This section introduces a theory whose models can be seen as categorical interpretations.

C V I T 2 0 1 6 23:8

A First Order Theory of Diagram Chasing

Axioms

We now introduce the different axioms of the theory. A formula F with free variables x 1 , . . . , x n is written F (x 1 , . . . , x n ) so as to clarify the sorts of each variable in the arity of F .

Existence and uniqueness of the empty diagram

EmptyEU :

∃! ∅ x, x ≈ x

Compatibility of restrictions

For any quivers Q, Q ′ , Q ′′ and morphisms m :

Q → Q ′ and m ′ : Q ′ → Q ′′ , we define: RestrComp m,m ′ : ∀ Q ′′ x ′′ , restr m (restr m ′ (x ′′ )) ≈ restr m ′ •m (x ′′ ).

Pushout

For any pushout configuration as in Definition 9, and using the same notations as this definition, we define the following formulas of arity

Q 1 × Q 2 × Q ′ : Cospan m ′ 1 ,m ′ 2 (x 1 , x 2 , x ′ ) : restr m ′ 1 (x ′ ) ≈ x 1 ∧ restr m ′ 2 (x ′ ) ≈ x 2 . PushoutEU m1,m2,m ′ 1 ,m ′ 2 : ∀ Q1 x 1 , ∀ Q2 x 2 , restr m1 (x 1 ) ≈ restr m2 (x 2 ) → ∃! Q ′ x ′ , Cospan m ′ 1 ,m ′ 2 (x 1 , x 2 , x ′ ).

Composition

The

Equality of nontrivial paths

For any two nontrivial path-quivers P 1 and P 2 , it is possible to choose in a canonical way a quiver Q ′ together with two embeddings m ′ 1 , m ′ 2 such that the following diagram forms a pushout configuration (as for instance on Figure 2): . .

P 1 P 2 Q ′ st P 1 st P 2 m ′ 1 m ′ 2
We thus define the following predicate of arity P 1 × P 2 :

EqPath P1,P2 (x 1 , x 2 ) : restr . . (x 1 ) ≈ restr . . (x 2 ) ∧ ∀ Q ′ x, Cospan m ′ 1 ,m ′ 2 (x 1 , x 2 , x) → commute(x) .

Identity

The following predicate, of arity . × . . , defines the identity map:

Id(x, y) : restr . . (y) ≈ x ∧ ∀ . . z, w, Comp(y, z, w) → EqPath(z, w) ∧ Comp(z, y, w) → EqPath(z, w)
and the following formula ensures the existence of identity maps.

IdE :

∀ . x, ∃ . . y, Id(x, y).

Note that Id(x, y) and IdE entail that restr . . (y) ≈ x.

Equality for general paths

For any nontrivial path-quiver P , we define the following formulas:

EqPath .,. (x, y) :

x ≈ y,

EqPath .,P (x, y) : ∃ . . z, Id(x, z) ∧ EqPath . .,P (z, y), EqPath P,. (x, y) : EqPath .,P (y, x).

Hence, we can see EqPath as a relation with arity any pair of path-quivers. We ensure this relation to be an equivalence relation by defining for any path-quivers P 1 , P 2 and P 3 the three formulas EqPathRefl P1 , EqPathSym P1,P2 and EqPathTrans P1,P2,P3 stating that the relation EqPath is respectively reflexive, symmetric and transitive.

We also make sure to enforce the properties of a category congruence. For this purpose, for any four path-quivers P 1 , P ′ 1 , P 2 , and P ′ 2 , of respective length k 1 , k ′ 1 , k 2 and k ′ 2 , we define the following formula where bound variables x 1 , x 2 , x ′ 1 , x ′ 2 respectively have sort P 1 , P 2 , P ′ 1 and P ′ 2 and the sort of

x ′′ i , i ∈ {1, 2}, is PQ ki+k ′ i . EqPathConcat P1,P2,P ′ 1 ,P ′ 2 : ∀x 1 , x 2 , x ′ 1 , x ′ 2 , EqPath(x 1 , x 2 ) ∧ EqPath(x ′ 1 , x ′ 2 ) ∧ restr . (x 1 ) ≈ restr . (x ′ 1 ) → ∀x ′′ 1 , x ′′ 2 , Cospan , (x 1 , x ′ 1 , x ′′ 1 ) ∧ Cospan , (x 2 , x ′ 2 , x ′′ 2 ) → EqPath(x ′′ 1 , x ′′ 2 ).

Commutativity

We relate commutativity and equality by the following formula:

ComEq : ∀ . . x, commute(x) → restr . . (x) ≈ restr . . (x).
For any quiver Q, the following formula provides an analogue of the notion of commutativity of diagrams via the characterization given in Proposition 16,

PathCom Q : ∀ Q x, (p1,p2)∈BT Q EqPath(restr p1 (x), restr p2 (x)) ↔ commute(x).
where we recall that BT Q denotes the (finite) set of pairs of trails of Q having the same extremities.

▶ Definition 19. Theory Tcat , over signature Σ, consists of the following formulas: Let us prove the other direction. Let Q be an acyclic quiver. By an abuse of the notations, if v ∈ V Q , resp. a ∈ A Q , we also denote by v, resp. a, the corresponding embedding v : . → Q, resp. a : . . → Q. Here is a crucial lemma for the proof of the theorem.

C V I T
▶ Lemma 21 (General pushout). Let M be a model of T cat . Let Q be an acyclic quiver, β V : V Q → M . and β A : A Q → M . . be two maps. Then the following statements are equivalent.

There exists an element

β of M Q such that, for any v ∈ V Q and any a ∈ A Q , restr M v (β) = β V (v) and restr M a (β) = β A (a).

For any a

∈ A Q , restr M . . (β A (a)) = β V (s Q (a)) and restr M . . (β A (a)) = β V (t Q (a)
). Moreover, when both statements hold, the element β is unique.

Proof. The fact that the first point induces the second one follows directly from RestrComp. Hence we focus on the other direction and on the uniqueness.

We proceed by induction on the structure of Q. In the case of an empty Q, the second point holds trivially. The first point and the uniqueness follows from EmptyEU.

Assume first that the lemma holds for some quiver Q 1 with no arrow. Let Q be the quiver Q 1 with an extra vertex v 0 . Let β V and β A be two maps as in the statement of the lemma, and β 1,V the restriction of β V to V Q1 . We have the following pushout configuration:

∅ Q 1 . Q m1 m2 m ′ 1 m ′ 2 =v0
Point 2 holds trivially. Let us prove the existence and uniqueness of an element β satisfying the property of Point 1. By induction, we get a unique β 1 ∈ M Q1 compatible with β 1,V and β A . Set

β 2 := β V (v 0 ). By EmptyEU, restr M m1 (β 1 ) = restr M m2 (β 2 ). Hence we can apply PushoutEU m1,m2,m ′ 1 ,m ′ 2 to get a unique element β ∈ M Q such that Cospan M m ′ 1 ,m ′ 2 (β 1 , β 2 , β).
From RestrComp and the induction hypothesis, it follows that for

β ′ ∈ M Q , Cospan M m ′ 1 ,m ′ 2 (β 1 , β 2 , β ′ ) is equivalent to restr M v (β ′ ) = β V (v) for any v ∈ V Q . This concludes the induction.
Assume more generally that the lemma holds for some acyclic quiver Q 1 . Let Q be an acyclic quiver obtained from Q 1 by adding one arrow a 0 . Let β V and β A be two maps as before and β 1,A the restriction of β A to A Q1 . Let m 1 : . . → Q 1 mapping the first point to s Q (a 0 ) and the second point to t Q (a 0 ). Let m 2 := st . . = .

. . Once again, we get a pushout configuration:

. . Q 1 Q m1 m2 m ′ 1 m ′ 2 :=a 0
Assume that Point 2 holds. By induction, we get a unique element β 1 ∈ M Q1 compatible with β V and β 1,A . Set β 2 := β A (a 0 ). We have already proven the lemma for the quiver . . . Hence we deduce that

restr M m1 (β 1 ) = restr M m2 (β 2 ).
We can apply PushoutEU as before to get Point 1 as well as the uniqueness part. This concludes the proof of the lemma. ◀

We now continue the proof of Theorem 20. Let M be a model of T cat . We define the general quiver Q associated to M by

V Q := M . , A Q := M . .
v ∈ V Q , Ψ(β)(v) = restr M v (β). for any a ∈ A Q , Ψ(β)(a)
is the path of length one with arrow restr M a (β). The image of Ψ is exactly the set of diagrams whose morphisms are paths of lengths one.

Let us now introduce another important map. Let A and B be two objects of C, and let p ∈ Hom C (A, B). Recall that p is just a path from A to B in Q. Let k be the length of p. By Lemma 21, there exists a unique element Θ(p

) ∈ M PQ k such that for each v ∈ V PQ k , restr M v (Θ(p)) = p(v), for each a ∈ A PQ k , restr M a (Θ(p)) = p(a)
. Relation EqPath M thus induces a relation r on morphisms of C. Moreover, EqPathRefl, EqPathSym, EqPathTrans and EqPathConcat, together with Lemma 21, make r a category congruence. We can hence define the category C := C/r. Now Ψ induces a map Ψ : M Q → C Q for any quiver Q, and we claim that Ψ induces a model isomorphism between M and C.

Let Q be any acyclic quiver. We first prove that Ψ is injective. Let P be a path-quiver and let β ∈ M P . We have to find an element γ ∈ M . . such that EqPath M P,. . (β, γ). If P has length one, this is trivial. If P has length zero, then by IdE, there exists γ such that Id M (β, γ). Moreover, by the definition EqPath .,. . and using the reflexivity of EqPath, we get EqPath M .,. . (β, γ). If P has length two, then by CompE, we can find an element γ such that

Let β, γ ∈ M Q such that Ψ(β) = Ψ(γ). For any vertex v ∈ V Q , Ψ(β)(v) = Ψ(γ)(v), i.e., restr M v (β) = restr M v (γ).
Comp(restr M . . . (β), restr M . . . (β), γ).
The commutativity of the triangle induces EqPath M . . .,. . (β, γ). For P with length k > 2, we proceed by induction on the length of P . Using EqPathTrans, it suffices to find γ over PQ k-1 such that EqPath M P,PQ k-1 (β, γ). To do so, we see P as the pushout of PQ 2 and PQ k-2 along m ′ 1 = : PQ 2 → P and m ′ 2 = : PQ k-2 → P . By the case k = 2, we can find γ 1 ∈ M . . such that EqPath(restr

M m ′ 1 (β), γ 1 ). We set γ 2 = restr M m ′ 2 (β).
In particular we have EqPath(γ 2 , γ 2 ). By EqPathConcat, we get EqPath(β, γ)

where γ ∈ M PQ k-1 is such that Cospan m ′ 1 ,m ′ 2 (γ 1 , γ 2 ,
γ), and the result follows. We have shown that Ψ induces a bijection between the corresponding domains. In order to conclude the proof, it remains to prove that Ψ commutes with function restr and with predicate commute. The commutativity with restr follows from the definition of Ψ and the formulas RestrComp.

The compatibility with the predicate commute can be reduced to the compatibility of EqPath via the formula PathCom and the characterization of commutativity given in Proposition 16. Let P 1 and P 2 be two path-quivers and β 1 ∈ M P1 and β 2 ∈ M P2 . These elements correspond to paths p 1 and p 2 in Q. Using the definitions of the different elements, we get the following chain of equivalences:

EqPath C (Ψ(β 1 ), Ψ(β 2 )) ⇔ comp C (Ψ(β 1 )) = comp C (Ψ(β 2 )) ⇔ comp C ( Ψ(β 1 )) ∼ comp C ( Ψ(β 2 )) ⇔ p 1 ∼ p 2 ⇔ EqPath(β 1 , β 2 ).
This concludes the proof of the theorem. ◀

Duality

Signatures of Definition 1 are tailored to enforce a built-in, therefore easy to prove, duality principle, which we now make precise. Recall from Definition 2 that duality is an involution on quivers, as well as on acyclic quivers. We define the dual of a formula over Σ as follows:

if m : Q → Q ′ is a morphism, then m † : Q † → Q ′ † is defined by m † V = m V and m † A = m A . if x = (x, Q) is a variable in X × S then x † := (x, Q † ), (restr m (x)) † := restr m † (x † ) and (commute Q (x)) † := commute Q † (x † ), (x ≈ y) † := x † ≈ y † , (∀ Q x, ϕ) † := ∀ Q † x † , ϕ † and (∃ Q x, ϕ) † := ∃ Q † x † , ϕ † , (ϕ ∧ ψ) † := ϕ † ∧ ψ † , etc. For Y a set of variables, Y † denotes {x † | x ∈ Y }. For any theory T , T † denotes {ϕ † | ϕ ∈ T }.
For M an interpretation of Σ over a set of variables Y , we define its dual model M † over Y † as:

M † Q := M Q † , for x ∈ Y † , x M † := (x † ) M . restr M † m := restr M m † and commute M † Q := commute M Q † ,
The duality involution also induces involutions respectively on formulas, theories and models over Σ.

▶ Example 22.

If C is a small category, then the dual interpretation C † is isomorphic to the model of the dual category, both with respect to Σ and to Σ.

▶ Theorem 23 (Duality theorem). Let ϕ be a formula with free variables included in Y ⊆ X ×S, resp. in Y ⊆ X × S, and let M be a model of Σ, resp. of Σ. Then

M |= ϕ ⇐⇒ M † |= ϕ † . Proof. The proof is direct. ◀ ▶ Remark 24.
The duality principle has some useful direct consequences: If ϕ is a valid, resp. satisfiable, resp. unsatisfiable, formula, then so is ϕ † . Let T be theory such that any model of T verifies T † . If ϕ is a valid, resp. satisfiable, resp. unsatisfiable, formula among models of T , so is ϕ † . We have the following reciprocal. Let T be a theory such that any model M of T verifies that M † |= T , then every model of T verifies T † .

The following fact follows directly from this last point, Theorem 20 and Example 22.

▶ Proposition 25. Models of T cat verify T † cat , and models of Tcat verify T † cat .

A theory for diagrams in abelian categories

We now introduce a theory whose models are diagrams in small abelian categories. We rely on the set of axioms given by Freyd in [START_REF] Freyd | Abelian categories. An introduction to the theory of functors[END_REF]. This reference is particularly well-suited for our purpose. Indeed, the author does not impose the homomorphisms between any two objects of an abelian category to form an abelian group, but this fact rather follows from the axioms.

Let us first formulate common notions of category theory in the languages introduced in Section 2.5. Here is a predicate of arity .

. which corresponds to monicity of a map in a category. The dual predicate to Mono(x) is named Epi(x).

Let Q be a quiver. We define the cone of Q as the quiver

cone(Q) := (V Q ⊔ {v 0 }, A Q ⊔ {a v | v ∈ V Q }, s cone(Q) , t cone(Q) ),

C V I T 2 0 1 6 Decidability of the commerge problem

In this section, we use the notations of Section 2.3. Let Q be a quiver, k ∈ N and, for each i ∈ [k], let Q i be a quiver and m i : Q i → Q be a morphism. We define the following formula:

Commerge m0,...,m k-1 : ∀ Q x, k-1 i=0 commute(restr mi (x)) → commute(x).
▶ Definition 29. Notations as above, the acyclic, resp. cyclic, commerge problem for morphisms, or embeddings, m 0 , . . . , m k-1 and for a theory T on language Σ, resp. Σ, is the problem of deciding the validity of Commerge m0,...,m k-1 in models of theory T .

We recall that a thin category is a category with at most one morphism between any pair of objects. Let tot Qi = BP Qi be the complete path relation on

Q i . Set r i := m i * (tot Qi ) for i ∈ [k]. Recall that (r i | i ∈ [k])
| i ∈ [k]) is a thin category. Proof. Set C := ⟨Q⟩/(r i | i ∈ [k]).
It is a model of T cat , resp. Tcat . Moreover, the canonical diagram D : ⟨Q⟩ → C verifies the premise of Commerge m0,...,m k-1 . If C is not thin, then there are two paths p and q in ⟨Q⟩ with the same extremities which are not in relation. Then comp(p * (D)) is the class of p in the quotient, which is different of the class of q, that is of comp(q * (D)). Hence D is not commutative.

For the other direction, by Theorem 20, it suffices to study diagrams in small categories. It is easy to check that any diagram D ′ over Q in a category C ′ which verifies the condition of Commerge m0,...,m k-1 factors through D, i.e., D ′ = F • D for some functor F : C → C ′ . If C is thin, then for any two paths p and q with same extremities in Q, we have: Proof. We proceed by reduction to an undecidability result, independently due to Adyan and Rabin [START_REF] Ivanovich | Algorithmic undecidability of problems of recognition of certain properties of groups[END_REF][START_REF] Michael | Recursive unsolvability of group theoretic problems[END_REF]. For B an arbitrary finite set and ⟨B⟩ the associated free monoid, let M be the finitely presentable monoid ⟨B | r = 1, r ∈ R⟩, for R a nonempty finite subset of ⟨B⟩ ∖ {1}. In particular, any finitely presentable group is of this form. Hence, by the Adyan-Rabin theorem, determining the triviality of M from B and R is undecidable. Let B, R and M as above. Let Q = ({v}, B ⊔ {e}, s Q , t Q ) be a quiver with one vertex and loops labeled by elements of B plus one loop e. To each element ρ ∈ R corresponds a path p ρ : PQ kρ → Q, for some k ρ ∈ N. Let Q ρ be a pushout of the morphisms . . : . . → PQ kρ and .

comp(p * (D ′ )) = F (comp(p * (D))) = F (comp(q * (D))) = comp(q * (D ′ )).
. . Let m ρ be the extension to Q ρ of p ρ obtained by mapping the new arrow onto e. Also set m e : . → Q which maps the loop on e. Now, ⟨Q⟩/ m * e (tot . ), (m * ρ (tot Qρ ) | ρ ∈ R) is the category associated to the monoid M . Hence this category is thin if and only if the monoid is trivial. The Adyan-Rabin theorem and Lemma 30 conclude the proof. ◀ C V I T 2 0 1 6

23:16 A First Order Theory of Diagram Chasing

We strengthen the previous proposition to the case of embeddings.

▶ Theorem 33. The cyclic commerge problem for embeddings and Tcat is undecidable.

Proof. Let B, R, M as in the proof of Proposition 32. Let Q be the quiver ({v}, B, s Q , t Q ) (note that we removed the arc e). If n ≥ 2, we define the quiver Qn as

Qn := {v i | i ∈ [n]}, {b i,j | b ∈ B, 0 ≤ i < j < n} ⊔ {e i,j | i, j ∈ [n]}, s Qn , t Qn where s Qn (b i,j ) = v i , s Qn (e i,j ) = v i , t Qn (b i,j ) = v j , t Qn (e i,j ) = v j .
We have a projection π : ⟨ Qn ⟩ → ⟨Q⟩, which maps b i,j on b and e i,j on id v , and a section ι : ⟨Q⟩ → ⟨ Qn ⟩ defined by mapping v onto v 0 and b onto b 0,n-1 • e n-1,0 , where, as usual, we denote in a same way an arrow and the corresponding path of length one.

For A any subset of A Qn , let m A : Qn | A → Qn be the canonical embedding, and let

r A := m A * (tot Qn | A ). Set r ′ := (r A | A ∈ A) for A ⊂ P(A Qn ) defined as the set containing A e := {e i,j | i, j ∈ [n]}, for i < j and b ∈ B, A b,i,j := { e 0,i if i ̸ = 0 , b i,j , e j,n-1 if j ̸ = n -1 , b 0,n-1 }.
We claim that π and ι induce an equivalence of category between ⟨Q⟩ and ⟨ Qn ⟩/r ′ . From the definition of A e , for any i, j, l ∈ [n], we have e i,j • e j,l ∼ e i,l and e i,i ∼ id i . Now the definition of A b,i,j , for b ∈ B and 0

≤ i < j < n, induces that e 0,i • b i,j • e j,n-1 ∼ b 0,n-1 .
These relations generate all r ′ , and they become equalities by applying the projection. Hence π * : ⟨ Qn ⟩/r ′ → ⟨Q⟩ is well-defined. Clearly π • ι is identity. Concerning the other direction, for b ∈ B and 0 ≤ i < j < n, we have

ι • π(b i,j ) = b 0,n-1 • e n-1,0 ∼ e 0,i • b i,j • e j,n-1 • e n-1,0 ∼ e 0,i • b i,j • e j,0 .
Hence we get a natural transformation η between the identity functor and ι • π * by setting

η i := e i,0 ∈ Hom ⟨ Qn ⟩/r ′ (i, ι • π(i) = v 0 )
. Since e i,0 is an isomorphism, we conclude that there is an equivalence of category between ⟨Q⟩ and ⟨ Qn ⟩/r ′ .

Recall that M is the finitely presentable monoid ⟨B | r = 1, r ∈ R⟩. Assume that n is greater than the longest word in R. To any word ρ Proof. Let M , B, R be as in the proof of Theorem 33. Consider the acyclic quiver The Adyan-Rabin theorem concludes the proof. ◀

= b 0 b 1 • • • b l-1 in R corresponds a subset A ρ := {e 0,l , b 0 0,1 , b 1 1,2 , . . . , b l-1 l-1,l } ⊆ A Qn . Let A ′ := A ∪ {A ρ | ρ ∈ R}. Then, ⟨ Qn ⟩/(r A | A ∈ A ′ ) is equivalent as a category to ⟨Q⟩/(π * (r Aρ ) | ρ ∈ R)
Q := ({v 0 , v 1 }, B, s Q , t Q ) where s Q (b) = v 0 and t Q (b) = v 1 for any b ∈ B. To a word ρ = b 0 b 1 • • • b l-1 with b 0 , . . . , b l-1 ∈ B,

Conclusion

We have shown that the many-sorted signature Σ is expressive enough to formulate a theory T cat whose models are exactly diagrams in small categories, as well as an extension T ab of T cat whose models are exactly diagrams in small abelian categories. Restricting sorts to acyclic quivers and morphisms to embeddings makes the commerge problem for T cat decidable, that is, one can decide when the commutativity of a given diagram follows from that of a given collection of sub-diagrams. Generalizing this study to monoidal categories [START_REF] Selinger | A survey of graphical languages for monoidal categories[END_REF] or more generally to higher category theory does not seem immediate. However, typetheoretic approaches have been successfully applied to devise a syntactic description of weak ω-categories [START_REF] Finster | A type-theoretical definition of weak ω-categories[END_REF] and of opetopes [START_REF] Ho | A sequent calculus for opetopes[END_REF], and both these works laid the foundations of prototype proof assistants.

The signatures and theories presented in this article are shaped by their subsequent usage as interfaces in a computer-aided tool for diagram chases. This tool eventually produces formal proofs of the corresponding theorems for a given mathematical structure. Interfaces should indeed be convenient enough to fullfil for concrete applications, e.g., abelian groups. This motivation explains some seemingly odd choices, including the use of a commutation predicate instead of the arguably more natural equivalence relation on paths.

A companion file [1] to this submission illustrates how to implement a deep embedding of formulas of Σ using the Coq proof assistant [START_REF]The coq proof assistant[END_REF]; its content should be easy to transpose to other proof systems. Theorem duality_theorem_with_theory expresses a general duality principle. It can be specialized, e.g., to any formalized definition of abelian categories, and the resulting instance of the theorem ensures that a formula of the language is valid for abelian categories if and only if its dual is valid. This companion file however does not provide any specific such formal definition of abelian categories. Theorem 31 results in a complete decision procedure for commutativity clauses. The optimizations that make it work on concrete examples however go beyond the scope of the present article.

Similar concerns about diagrammatic reasoning have motivated the implementation of the accomplished Globular proof assistant [START_REF] Bar | Globular: an online proof assistant for higherdimensional rewriting[END_REF], for higher-dimensional category theory. Based on higher-dimensional rewriting, it implements various algorithms for constructing and comparing diagrams in higher categories. It is geared towards visualization rather than formal verification. The closest related work we are aware of seem unpublished at the time of writing. Lafont's categorical diagram editor [START_REF] Lafont | A categorical diagram editor to help formalising commutation proofs[END_REF], based on the Unimath library [START_REF] Voevodsky | Univalent semantics of constructive type theories[END_REF] and Barras and Chabassier's graphical interface for diagrammatic proofs [START_REF] Chabassier | A graphical interface for diagrammatic proofs in proof assistants[END_REF] both provide a graphical interface for generating Coq proof scripts and visualizing Coq goals as diagrams. Himmel [START_REF] Himmel | Diagram chasing in interactive theorem proving[END_REF] describes a formalization of abelian categories in Lean [START_REF] Mendonça De Moura | The lean theorem prover (system description)[END_REF], including proofs of the five lemma and of the snake lemma, and proof (semi-)automation tied to this specific formalization. Duality arguments are not addressed. Monbru [START_REF] Monbru | Towards automatic diagram chasing[END_REF]

Figure 1

 1 Figure 1 Square diagram with a diagonal arrow

▶

  Definition 4 (Path-quiver). The path-quiver of length k, denoted by PQ k , is the quiver with k + 1 vertices and k arrows ([k + 1], [k], id, (i → i + 1)).

▶ Lemma 11 .

 11 has a pushout, and any two pushouts of the same tuple are isomorphic, see for instance Figure2.The next lemma allows to reduce the number of distinct diagrams involved in a formula. Let C be some category. Consider a pushout configuration as in Definition 9. Consider two diagrams D 1 and D 2 in C over Q 1 and Q 2 , respectively. If the pullback of D 1 by m 1 coincides with the pullback of D 2 by m 2 , i.e.,

Figure 2 A▶

 2 Figure2A pushout Q ′ of two path-quivers P1 and P2 with respect to stP 1 and stP 2 .

2

 2 for any pair of objects A and B. ▶ Proposition 13 (Quotient category). Given such a category congruence, the data Ob C/r := Ob C and Hom C/r (A, B) := Hom C (A, B)/r A,B define a category C/r called the quotient category of C by r.

  following predicate, of arity . . × . . × . . , describes composite of arrows: Comp(x, y, z) : ∃ . . . w, restr . . . (w) ≈ x ∧ restr . . . (w) ≈ y ∧ restr . . . (w) ≈ z ∧ commute(w) while the following one ensures the existence of compositions: CompE : ∀ . . x, y, restr . . (x) ≈ restr . . (y) → ∃ . . z, Comp(x, y, z).

  , s Q := restr M . . and t Q := restr M . . . Set C := ⟨Q⟩. Thanks to Lemma 21, to each acyclic quiver Q and to each element β ∈ M Q , we can associate a unique diagram Ψ(β) in C verifying: for any

C V I T 2 0 1 6 23: 12 A

 612 Let a be an arrow of Q. Then we have the relation Ψ(β)(a) ∼ Ψ(γ)(a). By definition of EqPath . .,. . , we validate the premise of ComEq, and thus the equality Ψ(β)(a) = Ψ(γ)(a), i.e., restr M a (β) = restr M a (γ). By the uniqueness part of Lemma 21, we get β = γ. First Order Theory of Diagram Chasing We now consider the surjectivity of Ψ. It suffices to prove that any morphism p ∈ Hom C (A, B), for any A, B ∈ Ob C , is in relation via r to a path of length one. Indeed, in such a case, for any diagram D in C over Q, one can find another diagram D ′ over Q whose morphisms are path of size one and such that any morphism of D is in relation with the corresponding morphism of D ′ . Hence the induced diagrams in C are equal. Moreover, D ′ is in the image of Ψ, and we would get the surjectivity.

  Mono(x) : ∀ . . . y, restr . . . (y) ≈ x ∧ commute(restr . . . (y)) ∧ commute(restr . . . (y))

▶

  which is the category of the monoid M . Hence the validity of Commerge (m A ) A∈A ′ is equivalent to the triviality of M . Once again, we conclude using Lemma 30 and the Adyan-Rabin theorem.◀ Theorem 34. The theory T cat is undecidable.

  for some l ∈ N, we associate the predicate of arity Q EqId ρ (x) :∃ PQ l y, i∈[l]restr ai (y) ≈ restr b i (x) ∧ EqPath .,PQ l (restr . (y), y)where, for i ∈ [l], a i : . . → PQ l maps the arc of . . onto the i-th arc of PQ l and, as usual, for b ∈ B, b : . . → Q maps the arc of ..onto the arc b ∈ A Q . If D is a diagram over Q in some category C, then EqId ρ (D) is equivalent to the fact that D(v 0 ) = D(v 1 ) and D(b l-1 ) • • • • • D(b 0 ) = id D(v0) .In particular, a diagram D : ⟨Q⟩ → C verifies ρ∈R EqId ρ (D) if and only if it factorizes through the category associated to the monoid M . Hence, the triviality of the monoid M is equivalent to the validity of the following formula in T cat :∀ Q x, ρ∈R EqId ρ (x) → commute(x).

6 23: 18 A

 618 also discusses automation C V I T 2 0 1 First Order Theory of Diagram Chasing issues in diagram chases, and provides heuristics for generating them automatically, albeit expressed in a pseudo-language.

2 0 1 6 23:4 A First Order Theory of Diagram Chasing

  with at least one vertex. Such a path-quiver is called nontrivial if it has at least two vertices.

	.	.	.	. . .	.

2 0 1 6 23:10 A First Order Theory of Diagram Chasing EmptyEU

  , CompE, IdE, ComEq, RestrComp m,m ′ for any pair of maps m and m ′ such that the codomain of m is the domain of m ′ , EqPathRefl P1 , EqPathSym P1,P2 , EqPathTrans P1,P2,P3 , EqPathConcat P1,P2,P3,P4 for any quadruple of path-quivers P 1 , P 2 , P 3 and P 4 , PathCom Q for any quiver Q. Theory T cat is defined as the restriction of Tcat to Σ. Models of T cat , resp. Tcat , are in fact exactly what we have called categorical interpretations.▶ Theorem 20. Every categorical interpretation of Σ, resp. Σ, is a model of T cat , resp. Tcat . Moreover, any model M of T cat , resp. Tcat , has an isomorphic categorical interpretation. We only prove the theorem for T cat , as the proof for Tcat is similar.If C is a small category, a routine check shows that the associated model C of Σ verifies the theory T cat . For instance,

	PushoutEU m1,m2,m ′ 1 ,m ′ 2 for a pushout configuration as in Definition 9,
	3.2 Models
	Proof.

the formulas PushoutEU follows from Lemma 11; IdE and CompE come from the existence of the identity map and the existence of the composition respectively; for two diagrams D 1 and D 2 respectively over path-quivers P 1 and P 2 , the formula EqPath P1,P2 (D 1 , D 2 ) corresponds to the relation comp(D 1 ) = comp(D 2 ), which is a path relation; ComEq and PathCom Q follow from Proposition 16.

  is the smallest path relation containing the r i for all i ∈ [k]. ▶ Lemma 30. Notations as above, the formula Commerge m0,...,m k-1 is valid for models of T cat , resp. Tcat , if and only if ⟨Q⟩/(r i

  The acyclic commerge problem for embeddings and T cat is decidable. Proof. By Lemma 30, it suffices to decide if ⟨Q⟩/(r i | i ∈ [k]) is a thin category. Since the set of paths in ⟨Q⟩ is finite, we can compute the relation (m i * (tot Qi ) | i ∈ [k]) extensively and check whether it is complete. ◀ ▶ Proposition 32. The cyclic commerge problem for morphisms and Tcat is undecidable.

	Hence Commerge m0,...,m k-1 is valid.	◀
	▶ Theorem 31.

Funding This work has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No. 101001995).

https://hal.science/hal-04266479 Full Version: https://arxiv.org/pdf/2311.01790.pdf

where s cone(Q) and t cone(Q) are extensions of s Q and t Q by s Q (a v ) = v 0 and t Q (a v ) = v. We define by i Q : Q → cone(Q) the corresponding embedding. If m : Q → Q ′ is a morphism of quivers, we get a canonical morphism cone(m) : cone(Q) → cone(Q ′ ).

Abusing the notations, if a is an arrow of Q, we also denote by a : . . → Q the corresponding morphism. We then introduce the usual notion of cones of diagrams by the following formula of arity Q × cone(Q).

We now formulate the notion of limit.

We also introduce the dual Colimit Q (x, y) := Limit † Q † (x, y). The introduction of monos, epis, limits and colimits allows to state Freyd's axioms of abelian categories [START_REF] Freyd | Abelian categories. An introduction to the theory of functors[END_REF]. First, we define zero objects and kernels of respective arity . and .

. × . . as follows:

Zero(x) : We also define Coker(x, y) := Ker † (x, y).

We define the category T ab , resp. Tab as the extension of T cat , resp. Tcat , by the following formulas.

ZeroE :

∃ Proof. The theory T cat implies its dual by Proposition 25. Moreover, ZeroE clearly implies its dual. Finally, the other axioms have their dual in the theory, by definition thereof. ◀ ▶ Remark 28. The theorem and the proposition also hold for theory Tab .


Danyaal Kaleel
email: d.m.kaleel@qmul.ac.uk

Benoit Clement
email: benoit.clement@ensta-bretagne.fr

Kaspar Althoefer
email: k.althoefer@qmul.ac.uk

A Framework to Design and Build a Height Controllable Eversion Robot

Keywords: robot design, eversion robot, vine robot

Eversion robots are used in many different environments for a variety of applications. However, the vast majority of these environments are land based and minimal work has been done on environments that are 3-dimensional (3D) such as in air or underwater. To be able to successfully operate in such environments, eversion robots need to be capable of operating in 3D, including adjusting their configuration along the vertical axis. This vertical motion for eversion robots has not been developed before. This paper proposes a design for an eversion robot that, when fully extended, is able to float in air, using varying amounts of helium to change its buoyancy and hence, the amount of lift force in the vertical direction. The robot in this paper consists of a fixed base, one main continuous everting chamber with a constriction at half its length to form two links and two actuation pouches, which are externally attached. Furthermore, the calculations for determining the quantity of helium required to generate a specific force to lift the robot a specified distance, for position changes is shown. Finally, a kinematic model of the robot shows how the robots link tip positions affect the shape and position of the robot.

I. INTRODUCTION

Robots constructed from soft materials can be applied to environments and be used in applications that traditional rigid robots cannot. This is due to their advantageous material properties of being flexible and deformable, which enable these robots to be adaptable to changes in their environment. An eversion robot is a soft robot, in the shape of a cylindrical tube, that extends in length from its tip by shifting pressurised body material through its inner body and pushing it out at its tip [START_REF] Blumenschein | Design, modeling, control, and application of everting vine robots[END_REF]. Eversion robots are able to extend in length from their tips using either pneumatic pressure, like those seen in [START_REF] Putzu | Plant-inspired soft pneumatic eversion robot[END_REF] or hydraulic pressure, like those seen in [START_REF] Takahashi | Eversion robotic mechanism with hydraulic skeleton to realize steering function[END_REF]. Eversion robots can extend themselves to reach a target [START_REF] Greer | A soft, steerable continuum robot that grows via tip extension[END_REF], they can retract themselves [START_REF] Jeong | A tip mount for transporting sensors and tools using soft growing robots[END_REF], and they can steer themselves [START_REF] Abrar | Highly manoeuvrable eversion robot based on fusion of function with structure[END_REF], over a horizontal plane with very little to no vertical movement, by bending their bodies in different directions [START_REF] Jitosho | Passive shape locking for multi-bend growing inflated beam robots[END_REF]. Typically, the environments in which these robots are seen to operate in are land-based environments, such as those seen in [START_REF] Suulker | Soft cap for eversion robots[END_REF], where the robot is on the ground and is only able to move on a 2-dimensional plane (2D).

This work was supported by the UK-France joint PhD programme jointly managed by the Defence Science and Technology Laboratory (DSTL) and the French MOD's Defence Innovation Agency (AID).

Eversion robot motion are fairly well documented in the literature for eversion robots that operate in 2D land-based environments. One of the few pieces of literature that investigates an eversion robot in a 3-dimensional (3D) environment is a paper that describes the development of an eversion robot for the exploration of a coral reef [START_REF] Luong | Eversion and retraction of a soft robot towards the exploration of coral reefs[END_REF]. This paper developed an eversion robot system that was capable of extending itself and retracting itself underwater [START_REF] Luong | Eversion and retraction of a soft robot towards the exploration of coral reefs[END_REF]. It used the surrounding water to enable extension and also provide neutral buoyancy [START_REF] Luong | Eversion and retraction of a soft robot towards the exploration of coral reefs[END_REF]. However, neither buoyancy control in the vertical direction nor horizontal steering was possible with this system. It instead relied on contact with its environment to change the direction at which it bends [START_REF] Luong | Eversion and retraction of a soft robot towards the exploration of coral reefs[END_REF]. Not relying on environmental contact and being able to choose the direction that the robot moves in is important for robotic applications. An essential movement to bring eversion robots into 3D environments, such as an underwater environment, is the robots ability to move in the vertical direction. In particular, its ability to change and remain at a specific depth underwater or height or altitude in air.

Therefore, this paper aims to 1) provide a possible design for an eversion robot that is capable of changing its depth through varying the internal concentrations of a lighter fluid (in this case helium) compared to the fluid that makes up its environment (in this case air), 2) provide calculations that enable researchers to determine the quantity of helium needed for a specific displacement in the vertical direction, 3) calculations that determine the force exerted with a specific quantity of helium, which are essential to the successful deployment of this type of eversion robot in environments that are fragile and delicate, and 4) a kinematic model to determine the shape and position of the eversion robot for a given link tip position, and providing researchers with a kinematic model to use as a comparison for the actual physical system. It is hoped that the work in this paper can further the development of eversion robots operating in 3D environments, especially underwater environments as we believe eversion robots will be beneficial for a number of underwater activities due to their inherent advantageous properties. These advantageous properties of using eversion robots underwater include creating very little disturbances or damage to the environment, due to having a friction-less extension movement with their environment [START_REF] Hawkes | A soft robot that navigates its environment through growth[END_REF], being compact and short for storage and travel, which could be useful if being deployed on a small ship and then growing into a large and long size [START_REF] Ataka | Modelbased pose control of inflatable eversion robot with variable stiffness[END_REF], which would be useful as bodies of water, such as the ocean, are vast and deep, and having a soft structure which enables them to morph their shape to suit their environment [START_REF] Greer | Robust navigation of a soft growing robot by exploiting contact with the environment[END_REF], which would be useful for moving through narrow passageways and crevices. These advantageous properties would enable eversion robots to be applied to many underwater applications including underwater search and rescue, underwater archaeology, underwater exploration of marine environments and underwater mine fields clearance [START_REF] Kaleel | Underwater eversion robot growth for underwater operations with an emphasis on underwater mine hunting[END_REF]. Although the purpose of this paper is to establish a first step for developing eversion robot depth or buoyancy control in an underwater environment, a floating eversion robot in air is a completely novel concept that has not been done before and so this paper provides a pivot on which researchers can be pointed in a useful direction to develop robots in this area also.

This paper is structured as follows: Section 2 proposes an eversion robot design, that would be capable of altering its vertical position, including the materials, dimensions and components. Section 3 presents the calculations for the quantity of helium required to generate the force needed to cause a specific vertical position change of the robot's link tips and the calculations for the force generated by this quantity of helium. Section 4 discusses a kinematic model that models the robots position for a given vertical displacement. Section 5 presents the conclusions and what future researchers can do to improve upon this work.

II. ROBOT DESIGN

The robot in this paper had two distinct main sections: a static rigid base and a soft flexible everting membrane with two buoyancy actuation pouches, as shown in Fig. 1. The everting body of the robot was connected to the base using the base's pneumatic fitting that supplies air to the everting body by screwing the excess plastic sheet material that makes up the everting body to this pneumatic fitting. Note that the eversion robot body is to be filled with air and the two actuation pouches are to be filled with varying amounts of helium to cause the robots shape and link positions to change.

A. Robot Base

The rigid fixed base, shown in Fig. 2, was made from an airtight plastic box, which has holes in for the pneumatic fittings. Rubber o-rings were placed on the female and male parts of the pneumatic fittings before they were connected to the base to prevent leaks. The pneumatic fittings were used for connecting an air supply to the everting section of the robot and a helium supply to the buoyancy actuation pouches. This was achieved using internal pneumatic tubes within the base of the robot to connect the air inlet with the air outlet and helium inlets with the helium outlets. To achieve the position shown in Fig. 1, the exploded view diagram of the base, shown in Fig. 2, is rotated by 90 degrees around the vertical axis.

B. Eversion Robot Body

According to the tests conducted by [START_REF] Gorjup | A low-cost, open-source, robotic airship for education and research[END_REF], helium has a lifting capability of 0.95 kg/cubic metre at room temperature. The materials that are used to construct the eversion robot were therefore chosen to be light to enable the helium to have an effect on the flotation height. The eversion robot body was made from thin plastic sheets that were heat welded together and the pneumatic pipes and altitude control pouches were made from rubber. The dimensions of the everting body of the robot are shown in Fig. 3. The two links of the robot were created by making a constriction in the robot using heat welding. This created a hinge between the links enabling bending while also allowing the robot to extend. The mass of links 1 and 2 were measured to be 0.084 kg and 0.038 kg. The mass of link 1 included the masses of the pneumatic tubes, the weight of the eversion robot body itself and the mass of the actuation pouch at tip of link 1 as these structures had their centres of mass concentrated on link 1. The mass of link 2 only included the mass of the actuation pouch at the tip of link 2.

III. CALCULATIONS FOR LIFT

To determine the quantity of helium required to generate the required force to lift the robot, we first have to consider the robot's initial position and the forces that influence the robot's position. The weight and lift forces of the links are shown in Fig. 3 and the initial position of the robot is shown in Fig. 4.

A. Modelling Assumptions

The first modelling assumption that has been made was that the weight and lift force that is concentrated over link 1 has no influence on the lift force generated at the tip of link 2 and the weight and lift force concentrated over link 2 has no influence on the lift force generated at the tip of link 1. The second modelling assumption is that the robots' length is the same as the distance from the ground to the origin of the robot, shown in Fig. 4. This helps in the following calculations to determine distance travelled to reach equilibrium. However, if the robot length was not the same as the distance of the origin of the robot to the ground, in that the robot was at a higher distance off the ground, then the distance at which equilibrium is achieved is vertically offset by a distance d, which is the distance to the tip of the second link at initial position. The final modelling assumption is that the eversion robot is assumed to be fully everted or extended when the helium is to be injected into the buoyancy actuation pouches.

B. Determining Quantity of Helium for Equilibrium

To achieve equilibrium of each link, shown in Fig. 5 and6, which is where the lifting force is equal to the weight of the robot causing the robot to float in the air without moving up or down, a certain quantity of helium is needed to generate this lifting force. To determine the quantity of helium required to lift links 1 and 2 to equilibrium, (1) can be used along with the known mass of link 1 and link 2 of the robot and the lifting capability of helium (LCH) from [START_REF] Gorjup | A low-cost, open-source, robotic airship for education and research[END_REF], which is 0.95 kg/m 3 .

Q = m/LCH ( 1
)
where Q is the quantity of helium in m 3 , m is the mass across the link in kg and LCH is the lift capability of helium, which is 0.95 kg/m 3 , according to [START_REF] Gorjup | A low-cost, open-source, robotic airship for education and research[END_REF].

Using the modelling assumptions above and the mass, m, across link 1 and 2, as 0.084 kg and 0.038 kg respectively, we can calculate Q for link 1 and 2 as Q 1 = 0.09 m 3 and Q 2 = 0.04 m 3 .

C. Determining Force Generated by Quantity of Helium at Equilibrium

To calculate the force produced by the quantity of helium at equilibrium, we know that at equilibrium the forces are balanced. In other words, the weight forces pulling the robot down equal the lift forces holding the robot up. With this information, we can calculate the force produced by the quantity of helium at equilibrium using (2):

F = m × g (2)
where F is the force produced by the amount of helium, m is the mass of the link in kg and g is the gravitational acceleration, which we have taken as an approximate value of 9.81 m/s 2 [START_REF] Di Giminiani | The effects of vibration on explosive and reactive strength when applying individualized vibration frequencies[END_REF]. For the robot design in this paper, we get a force for link 1, F 1 of 0.82404 N and a force for link 2, F 2 of 0.37278 N .

D. Determining the Quantity of Helium for a Specific Vertical Displacement

Since we know the quantity of helium that will produce the required force to achieve a known displacement, based on the definition of the robots position relative to the ground, shown in Fig. 4, 5 and 6, we can calculate the quantity of helium to get a displacement of n in the vertical direction. The equation for this calculation is shown using (3) below.

Q n = n/d × Q (3)
where n is the displacement in the vertical direction in m, Q n is the quantity of helium required to achieve n displacement in m 3 , d is the distance to equilibrium in m and Q is the quantity of helium to achieve equilibrium in m 3 . For example, if you wanted a displacement of n metres for link 1, you could use [START_REF] Greer | A soft, steerable continuum robot that grows via tip extension[END_REF].

Q n = n/0.615 × 0.09 (4)
If n is 0.1 m, then this tells you that the required quantity of helium to lift the robot by 0.1 m is 0.01 m 3 .

E. Determining the Force Produced by a Specific Quantity of Helium

Many applications involving eversion robots require the eversion robot to exert little force on the environment. Knowing the force output that the robot generates is useful to know as force can be controlled for. An application where force control is important, is search and rescue applications for earthquakes, such as those seen in [START_REF] Mishima | Development of a pneumatically controlled expandable arm for rescue searches in tight spaces[END_REF] and [START_REF] Whitman | Snake robot urban search after the 2017 mexico city earthquake[END_REF], where care must be taken to prevent debris from falling on top of someone. Another application where force control is important is pick and place, as seen in [START_REF] Stroppa | Human interface for teleoperated object manipulation with a soft growing robot[END_REF], where forces involved in moving objects must be considered. Equation [START_REF] Jeong | A tip mount for transporting sensors and tools using soft growing robots[END_REF] gives us a way to calculate the force exerted by the robot using the quantity of helium.

F n = Q n × g × LCH ( 5
)
where n is the displacement in the vertical direction in m, F n is the force exerted by the robot to achieve n displacement in N , Q n is the quantity of helium to achieve n displacement in m 3 , g is the gravitational acceleration on the Earth surface, which we have taken as an approximate value of 9.81 m/s 2 [START_REF] Di Giminiani | The effects of vibration on explosive and reactive strength when applying individualized vibration frequencies[END_REF] and LCH is the lift capability of helium, which is 0.95 kg/m 3 , according to [START_REF] Gorjup | A low-cost, open-source, robotic airship for education and research[END_REF].

IV. KINEMATIC MODEL FOR ROBOT POSITION

To verify the lift calculations above, a kinematic model, shown in Fig. 7, was developed.

A. Inverse Kinematics to Determine Required Bending Angles

Considering Fig. 7, we can calculate the desired angles of the links, q 1 and q 2 , using the desired position of the links in the y-direction and ( 6) and [START_REF] Jitosho | Passive shape locking for multi-bend growing inflated beam robots[END_REF].

q 1 = arccos(y 1 / -L 1 ) (6)
q 2 = arccos(y 2 / -L 2 ) (7)
where q 1 and q 2 are the desired angles of the links with respect to their initial position shown in Fig. 4, y 1 and y 2 are the desired position of the link tips in the vertical (y) direction and L 1 and L 2 are the lengths of the links.

B. Determining the Shape of the Robot

After obtaining the required angles, q 1 and q 2 , for a particular desired position, y 1 and y 2 , we can determine the shape of the robot using the forward kinematic equations shown in (8), ( 9), [START_REF] Hawkes | A soft robot that navigates its environment through growth[END_REF] and [START_REF] Ataka | Modelbased pose control of inflatable eversion robot with variable stiffness[END_REF].

x 1 = L 1 × sin(q 1 ) (8)
y 1 = -L 1 × cos(q 1 ) (9)
x 2 = L 1 × sin(q 1 ) + L 2 × sin(q 2 ) (10)
y 1 = -L 1 × cos(q 1 ) -L 2 × cos(q 2 ) (11)
where x 1 , y 1 , x 2 and y 2 are the x and y coordinate positions of the tips of links 1 and 2 with respect to a positive x and y axis shown in Fig. 7, L 1 and L 2 are the link lengths and q 1 and q 2 , are the angles of the links for a particular desired position.

C. Verification of Kinematic Model

The kinematic model was implemented in MATLAB [START_REF]The MatWorks, Inc[END_REF] to determine whether the shape of the robot was what was expected for the initial position of the robot, the equilibrium positions of links 1 and 2, and for equilibrium of both of the robots links. Comparing Fig. 8, which is the MATLAB plot of the initial position, to the expected initial position of the robot, shown in Fig. 4, shows that the kinematic model's calculated initial position of the robot is correct. Further, comparing the MATLAB plots produced, in Fig. 9, that shows the robot achieving equilibrium with the expected equilibrium positions, shown in Fig. 5 and6, further validates this kinematic solution. This affirmation of the kinematic model shows that it would make a good comparison for work involving a physical height controllable eversion robotic system.

V. CONCLUSIONS AND FUTURE WORK

The aim of this paper is to pave the way for motion control developments of eversion robots in 3D environments, which has not been done before. The paper started by proposing a potential design for a two-link eversion robot that is capable of altering the vertical height of its links using helium in externally mounted actuation pouches. A stand out feature of its design is the light weight materials used in its construction to enable helium to produce enough lifting force. Secondly, this paper showed the required calculations to determine the quantity of helium and the force that is generated from that quantity of helium that will result in a specified change to the vertical position of robots links. Lastly, this paper showed a kinematic model to determine the shape of the robot when given a vertical coordinate position for each of the two links. The work described in this paper is a first step towards developing an eversion robot that can alter its height using a lighter fluid in externally mounted actuation pouches.

Further work should look into testing a physical eversion robot prototype with the calculated quantities of helium for specific distances to see if they can be reached and compare it to the kinematic model in this paper, which is the ideal case. Additionally, an improved model for determining the quantity of helium is needed, that takes into account how the weight of link 1 and the lift force at the tip of link 1 affects the lift force needed to be generated at the tip of link 2 and vice versa. Lastly, a suitable controller needs to be developed to control eversion robots in 3D environments that can accommodate for all the different movements that eversion robots are capable of but also one that takes into account the complexity of the environment that the robot is moving through. A controller that uses reinforcement learning and artificial intelligence (AI) could be an ideal approach to investigate due to the highly nonlinear motion behaviour of eversion robots. Given that eversion robots are a type of continuum robot, continuum robot control systems should be investigated, such as [START_REF] Braganza | A neural network controller for continuum robots[END_REF]. Furthermore, a suitable model of the robot moving through its environment could be used for developing control strategies. One could look to underwater vehicle modelling such as [START_REF] Yang | Modeling of a complex-shaped underwater vehicle for robust control scheme[END_REF], for inspiration.

Fig. 1 .

 1 Fig. 1. Eversion Robot Design

Fig. 3 .

 3 Fig. 3. Forces that influence the robot and where these forces act based on the distance of the centre of mass, from the base, for distributed forces and based on the distance, from the base, for point forces.

Fig. 4 .

 4 Fig. 4. Robot's initial position in resting position.

Fig. 5 .

 5 Fig. 5. Robot's equilibrium position of first link with respect to the ground.

Fig. 6 .

 6 Fig. 6. Robot's equilibrium position of second link with respect to the ground.

Fig. 7 .

 7 Fig. 7. Kinematic chain diagram of robot

Fig. 10

 10 shows that solutions are also produced for random values of y 1 and y 2 between the values of -0.615 <= y 1 <= 0.615 and -0.565 m <= y 2 <= 0.565 m. These random values of y 1 and y 2 show that the model is not inclusive to only certain y 1 and y 2 values, such as those achieved at equilibrium and the initial position of the robot and that other positions of y 1 and y 2 can be achieved. Note that the 0.615 m and 0.565 m are the maximum lengths of the links and we are assuming that the robot is fully extended, when the actuation control pouches are being inflated with helium for height change. The vertical position coordinate values of y 1 and y 2 for determining the kinematic positions of the links shown in Fig. 8, 9 and 10 are shown in Tab. I.

Fig. 8 .

 8 Fig. 8. Initial position of robot determined using the kinematic model.

Fig. 9 .

 9 Fig. 9. Equilibrium position of robot determined using the kinematic model.

Fig. 10 .

 10 Fig. 10. Random positions of robot can be reached including positive, which have been determined using the kinematic model.

TABLE I VALUES

 I OF y 1 AND y 2 FOR DETERMINING THE KINEMATIC POSITIONS OF THE LINKS SHOWN IN FIG. 8, 9 AND 10

	Figure	y 1	y 2	Shows	Colour
	8	-0.615	-0.565	Initial Position	blue
	9	0	-0.565	Equilibrium of link 1 only	blue
	9	-0.615	0	Equilibrium of link 2 only	orange
	9	0	0	Equilibrium of links 1 and 2	yellow
	10	-0.515	-0.565	Random Link positions	blue
	10	-0.615	-0.360	Random Link positions	orange
	10	0.450	-0.365	Random Link positions	yellow

ACKNOWLEDGMENT

A special thank you to our collaborator Dr Adrian Baker from DSTL for his help on this project.