Sorin Stratulat
email: sorin.stratulat@univ-lorraine.fr

Building explicit induction schemas for cyclic induction reasoning

, it has been shown how to transform any structural proof developed with the LKID system into a cyclic proof using the CLKID ω system. However, the inverse transformation was only conjectured. We provide a simple procedure that performs the inverse transformation for an extension of LKID with explicit induction rules issued from the structural analysis of CLKID ω proofs, then establish the equivalence of the two systems. This result is further refined for an extension of LKID with Noetherian induction rules. We show that Noetherian induction subsumes the two kinds of reasoning. This opens the perspective for building new effective induction proof methods and validation techniques supported by (higher-order) certification systems integrating the Noetherian induction principle, like Coq.

Introduction

(Mathematical) induction reasoning is known to be one of the most effective reasoning methods. Its distinctive feature is the use, during the proof process, of induction hypotheses representing 'not yet proved' formulas.

The induction hypotheses can be defined before their use, by explicit induction schemas that can be directly embedded in inference systems using explicit induction rules. On the other hand, the induction hypotheses can also be defined by need, at the moment of their use. In this case, the induction reasoning is schemata-free but should be performed at the proof level because the induction hypotheses can be (instances of) formulas positioned anywhere in the derivation.

The relation between the two kinds of induction reasoning was previously studied for Gentzen-style µ-calculus proof systems and proved equivalent, i.e., the proofs are convertible between systems. In [START_REF] Sprenger | On the structure of inductive reasoning: Circular and tree-shaped proofs in the µ calculus[END_REF], the explicit induction proofs are finite and the induction rules locally implement the Noetherian induction principle. The second kind of reasoning is captured by ω-regular proof trees that are finitely represented by stopping the development of the (sub-)derivations for nodes labelled with formulas already encountered in the derivation. The soundness of the method is ensured if the cyclic induction reasoning associated to each strongly connected component of the proof graph is well-founded.

We are interested to extrapolate the equivalence result for sequent-based systems that extend the Gentzen's LK system [START_REF] Gentzen | Untersuchungen über das logische Schließen[END_REF] to reason on inductively defined predicates [START_REF] Aczel | An introduction to inductive definitions[END_REF]. We focuss on two representative systems, proposed by Brotherston [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF]: i) the LKID structural system that integrates induction rules generalizing Noetherian induction reasoning by the means of schemas issued from the recursion analysis of (mutually defined) inductive predicates, and ii) the CLKID ω cyclic system, issued from LKID by replacing the induction rules with case-split rules. A main result of [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF] is that any LKID proof is convertible into a CLKID ω proof. However, the conversion in the other direction is only conjectured.

In this paper, we present a procedure that builds dynamically explicit induction schemas from the structural analysis of CLKID ω proofs. Firstly, we show the equivalence between CLKID ω and an extension of LKID, denoted by LKID ∼ , with induction rules that embed cyclic reasoning from existing CLKID ω proofs. The procedure is further refined to build Noetherian induction schemas from the productions defining new inductive predicate symbols attached to strongly connected components. LKID and CLKID ω , extended to deal with the new symbols, are shown equivalent. We conclude that Noetherian induction is sufficient to represent the structural and cyclic induction reasoning in this setting. Aside the theoretical and technical interests, this result can help developing i) effective sequent-based induction methods that combine the advantages of the two kinds of reasoning, and ii) automated techniques for their validation, supported by (higher-order) certification environments integrating the Noetherian induction principle, like Coq [START_REF]The Coq Reference Manual -version 8[END_REF].

The paper is structured in 6 sections. Section 2 gives the preliminaries for reasoning with sequent-based inference systems for classical first-order logic (FOL) with inductively defined predicates (FOL ID ), then presents the CLKID ω and LKID systems. The structural analysis of cyclic proofs is explained in Section 3. LKID ∼ is introduced in Section 4. The extension of LKID with Noetherian induction rules, denoted by LKID e , is presented in Section 5, as well as the procedure transforming CLKID ω proofs into LKID e proofs. As a running example, we consider 'P and Q' [START_REF] Wirth | Descente infinie + Deduction[END_REF]. The conclusions are presented in Section 6.

Syntax and sequent systems for FOL ID

Syntax. The logical framework is based on FOL ID using a standard (countable) first-order language Σ. The predicate symbols are labelled either as ordinary or inductive. We assume that Σ has P 1 , . . . , P n as inductive predicate symbols. The terms are defined as usual. By t, we denote a vector of terms (t 1 , . . . , t m ) of length m, the value of m being usually deduced from the context. New terms and formulas are built from replacing (free) variables by terms via substitutions. A substitution is a mapping from variables to terms, of the form {x 1 → t 1 ; . . . ; x p → t p }, written in a more compact form as {x → t}, where x is the vector of variables (x 1 , . . . , x p ) and t is the vector of terms (t 1 , . . . , t p ). An identity substitution consists only of mappings of the form x → x. ≡ denotes the syntactical equality. A term t is an instance of t ′ if there is a substitution σ such that t ≡ t ′ σ. Let F V (φ) denote the free variables of a given formula or set of formulas φ. We denote the instance of a formula ψ with σ by ψ[σ], where dom(σ) ⊆ F V (ψ). Also, given a multiset of formulas Ψ , Ψ [σ] denotes the set {ψσ|ψ ∈ Ψ }, where dom(σ) ⊆ F V (Ψ ).

Following [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF], a specification is the union of the finite inductive definition sets Φ Pi defining each P i (i ∈ [1..n]) and consisting of productions of the form

Q 1 (u 1 ), . . . Q h (u h ), P j1 (t 1 ), . . . , P jm (t m ) → P i (t) (1)
where i, j 1 , . . . j m ∈ [1.

.n] and Q 1 , . . . , Q h are ordinary predicate symbols.

The sequent-based inference system. The Gentzen's LK system [START_REF] Gentzen | Untersuchungen über das logische Schließen[END_REF], presented in Fig. 1, is extended with equality and unfold rules using the definitions of inductive predicates. The proof derivations are built from sequents of the form Γ ⊢ ∆, where Γ and ∆ are finite multisets of formulas, separated by commas. The comma is an associative and commutative operator which can be classically interpreted as a conjunction in the antecedent Γ , and as a disjunction in the succedent ∆; Γ ⊢ ∆ can also be interpreted in FOL as the clause C(Γ ⊢ ∆) ≡ ( F ∈Γ (¬F )) ∨ ( F ∈∆ F ). By abuse of notation, F V (Γ ⊢ ∆) denotes the set of free variables of Γ ⊢ ∆. The instance of the sequent Γ ⊢ ∆ with a substitution δ, denoted by

(Γ ⊢ ∆)[δ], is Γ [δ] ⊢ ∆[δ].
The inference system is built from inference rules. A rule is represented by a simple horizontal line that separates

The equality rules are given in Fig. 2. The (=L) rule replaces in Γ and ∆ occurrences of t by u, as well as of u by t. Assuming that (1) is the r-th production defining P i , the unfold rule applies on any sequent with a succedent formula P i (t ′ ) for which there is a substitution

(= R) Γ ⊢ t = t, ∆ Γ [{x → u; y → t}] ⊢ ∆[{x → u; y → t}] (= L) Γ [{x → t; y → u}], t = u ⊢ ∆[{x → t; y → u}]
σ such that P i (t ′ ) ≡ P i (t)[σ]: Γ ⊢ Q1(u1)[σ], ∆ . . . Γ ⊢ Q h (u h )[σ], ∆ Γ ⊢ Pj 1 (t1)[σ], ∆ . . . Γ ⊢ Pj m (tm)[σ], ∆ (PiRr) Γ ⊢ Pi(t ′ ), ∆
The CLKID ω system. It consists of the rules from Fig. 1 and Fig. 2, as well as the case-split rule representing a left-introduction operation for inductive predicate symbols: case distinctions (Case

P i ) Γ, P i (t ′ ) ⊢ ∆
where, for each production of the form (1), we define the case distinction

Γ, t ′ = t, Q 1 (u 1 ), . . . , Q h (u h ), P j1 (t 1 ), . . . , P jm (t m ) ⊢ ∆ (2)
such that, for any variable y from (1), we have

y ∈ F V (Γ ∪ ∆ ∪ P i (t ′ ))
(the variable y can be renamed to a fresh one, otherwise). The formulas P j1 (t 1 ), . . . , P jm (t m ) are said to be case-descendants of the active formula P i (t ′ ).

CLKID ω also includes the substitution rule:

Γ ⊢ ∆ (Subst) Γ [δ] ⊢ ∆[δ]
The CLKID ω proofs can be represented as finite graphs. Special nodes are the leaves and buds, representing terminal nodes, and some internal nodes referred to as companions. Definition 2.1 (Leaf, Bud). Given a derivation tree, by leaf we understand any sequent that is the conclusion of a 0-premise inference rule, for example (Ax) or (= R). A bud is a sequent that is not the conclusion of any rule. Definition 2.2 (Companion). Any internal node C in a derivation tree is said to be a companion for a bud B if C and B have the same sequent labelling. Definition 2.3 (CLKID ω pre-proof tree, Induction function). A CLKID ω pre-proof tree of a sequent S is a pair (D, R), where D is a finite derivation constructed with CLKID ω -rules and whose root is S. R is a defined induction function assigning a companion to every bud node in D. Definition 2.4 (Path in a pre-proof tree). A (finite or infinite) path in a pre-proof tree (D, R) is a sequence (S i ) 0≤i<α of sequents from D, for some α ∈ N ∪ {∞}, such that S i+1 is a premise of the rule applied on S i (resp. R(S i )) if S i is a non-bud (resp. bud) node.

A pre-proof is a proof if any infinite path satisfies some trace condition. Definition 2.5 (Trace, Progress point). Let (D, R) be a CLKID ω pre-proof tree and let (Γ i ⊢ ∆ i ) i≥0 be an infinite path from its graph. A trace following (Γ i ⊢ ∆ i ) i≥0 is a sequence (τ i ) i≥0 such that, for all i, we have:

1. τ i = P ji (t i ) ∈ Γ i ; 2. if Γ i ⊢ ∆ i is the conclusion of (Subst) then τ i = τ i+1 [δ],
where δ is the substitution associated with the rule instance; 3. if Γ i , t = u ⊢ ∆ i is the conclusion of (=L), there is a formula F and variables

x, y such that

τ i = F [{x → t; y → u}] and τ i+1 = F [{x → u; y → t}]; 4. if Γ i ⊢ ∆ i is the conclusion of a case-split rule then either a) τ i+1 = τ i or b)
τ i is the active formula of the rule instance and τ i+1 is a case descendant of τ i . In the latter case, i is said to be a progress point of the trace; 5. if Γ i ⊢ ∆ i is the conclusion of any other rule then τ i+1 = τ i .

An infinitely progressing trace is a trace with infinitely many progress points. Definition 2.6 (CLKID ω proof tree). A CLKID ω proof tree is any CLKID ω pre-proof tree (D, R) that satisfies the following global trace condition: for every infinite path (Γ i ⊢ ∆ i ) i≥0 in D, there is an infinitely progressing trace following some tail of the path

(Γ i ⊢ ∆ i ) i≥k , for some k ≥ 0.
The soundness of CLKID ω is defined as in [START_REF] Brotherston | A generic cyclic theorem prover[END_REF]. Let I be a non-empty set of interpretations of sequents. If I ∈ I, we write I |= S to mean that S is true under I. S is valid iff I |= S, for any I ∈ I. An ordinal trace function can be defined for a CLKID ω proof in order to interpret as ordinals the τ -values from the traces following paths from the CLKID ω proof. If I |= S i , there is I ′ ∈ I such that I ′ |= S i+1 and α ≤ α ′ , where α (resp. α ′ ) is the ordinal assigned to τ i under I (resp. τ i+1 under I ′ ). We have α < α ′ if i is a progress point. The ordinals are issued from the usual semantics of inductive predicates, which can be generated by sequences of approximants (P γ ) γ≥0 . The interpretation of the τ -value for ⊢ P (t) under I is the minimal γ such that ⊢ P γ (t) is true under I.

Theorem 2.7 (Soundness [START_REF] Brotherston | A generic cyclic theorem prover[END_REF]). Let us assume an ordinal trace function for a CLKID ω proof tree and I. If S is the root sequent, then S is valid.

The LKID system. It consists of the rules from Fig. 1 and Fig. 2 as well as the (Subst) and induction rules. The induction rules are left-introduction rules for predicate symbols. Compared to case-split rules, a formula F j is associated to some inductive symbol P j , then is instantiated following the schema: minor premises Γ, F j (t) ⊢ ∆ (Ind P j )

Γ, P j (t) ⊢ ∆
A minor premise is built from each production defining a predicate P i that is P j or mutually dependent with P j . The minor premise corresponding to (1) is

Γ, Q 1 (u 1 ), . . . Q h (u h ), G j1 (t 1 ), . . . , G jm (t m ) ⊢ F i (t), ∆ (3)
if (1) and Γ, P j (t) ⊢ ∆ do not share variables (otherwise, the variables from (1) can be renamed accordingly), and G j1 , . . . , G jm , F i are predicates associated to P j1 , . . . , P jm , P i , respectively. Γ, F j (t) ⊢ ∆ is called major premise. Definition 2.8 (LKID-proof ). A finite LKID derivation tree is a proof if all branches end in an axiom. Theorem 2.9 ( [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF]). Any LKID proof can be converted to a CLKID ω proof.

Structuring cyclic proofs

Any CLKID ω proof can be structured by transforming it into a (Subst)-free forest, then defining a well-founded ordering on its strongly connected components.

Converting proof trees to forests. A proof forest can be built from any CLKID ω proof tree by deleting its (Subst) steps. Before doing this, any bud S that is not the premise of a (Subst) step will become one by the following 'stuttering' transformation, where σ id is the identity substitution that instantiates the free variables from S: . . .

S . . . (rule) becomes

S ′ . . . S (Subst) S[σ id ] . . . (rule) S ′
Then, the subtree rooted by the premise S of any (Subst) rule that is not a bud node is detached from the proof tree to represent a new derivation tree; a copy of S is kept as a bud node and premise of the (Subst) rule, as below:

. . .

S (Subst) becomes S[δ]

. . .

S (new tree) (bud ) S (Subst) S[δ]
The premise of any (Subst) rule can now be deleted and a new induction function R ′ is defined. The conclusion S[δ] of (Subst) becomes a bud node for which R ′ (S[δ]) = (S ′ , δ), where S ′ is the companion referred to by R(S) in the CLKID ω tree if S is a bud node; otherwise, S ′ is the root of the new CLKID ω tree and labelled as S. S ′ is referred to as the (forest) companion of S[δ]. Definition 3.1 (CLKID ω pre-proof forest). A CLKID ω pre-proof forest of a sequent S is a pair (F, R ′ ), where R ′ is the new induction function and F is a set of finite derivation trees resulted by deleting the (Subst) rules from the CLKID ω proof tree of S.

Example 3.2 (The 'P and Q' example [START_REF] Wirth | Descente infinie + Deduction[END_REF]). Let us consider the productions for the inductive predicate N , as well as the mutually defined predicates P and Q:

→N (0) N (x) →N (s(x)) →P (0) P (x), Q(x, s(x)) →P (s(x)) →Q(x, 0) Q(x, y), P (x) →Q(x, s(y))
The sequent N (x) ⊢ P (x) is the root of the annotated CLKID ω pre-proof, where R(( * 1)) = R(( * 2)) = ( * ) and R(( †1)) = ( †).

(P R1) ⊢ P (0) (= L) x = 0 ⊢ P (x) N (x) ⊢ P (x) (*1) (Subst) N (x ′ ) ⊢ P (x ′ ) (**) (P R2),(Wk) N (s(x ′ )), N (x ′ ) ⊢ P (s(x ′ )) (= L) N (x), x = s(x ′ ), N (x ′ ) ⊢ P (x) (Case N ),(Wk) N (x), N (x) ⊢ P (x) (ContrL) N (x) ⊢ P (x) (*)
For lack of horizontal space, the rightmost branch of the pre-proof tree, annotated by (**), is developed separately below.

(QR1) N (u) ⊢ Q(u, 0) (= L) N (u), v = 0 ⊢ Q(u, v) N (x) ⊢ P (x) (*2) (Subst) N (u) ⊢ P (u) N (u), N (v) ⊢ Q(u, v) ( †1) (Subst) N (u), N (v ′ ) ⊢ Q(u, v ′ ) (QR2),(Wk) N (u), N (v ′ ) ⊢ Q(x, s(v ′ )) (= L) N (u), v = s(v ′ ), N (v ′ ) ⊢ Q(u, v) (Case Q) N (u), N (v) ⊢ Q(u, v) ( †) (Subst) N (x ′ ), N (s(x ′ )) ⊢ Q(x ′ , s(x ′ )) (**)
The premise of the (Subst) rule applied on (**) is not a bud and a new tree is generated. Finally, the pre-proof forest F is made of two trees:

(P R1) ⊢ P (0) (= L) x = 0 ⊢ P (x) ((*), {x → x ′ }) N (x ′ ) ⊢ P (x ′ ) (( †), {u → x ′ ; v → s(x ′ )}) N (v ′ ), N (s(x ′ )) ⊢ Q(x ′ , s(x ′ )) (P R2),(Wk) N (s(x ′ )), N (x ′ ) ⊢ P (s(x ′ )) (= L) N (x), x = s(x ′ ), N (x ′ ) ⊢ P (x) (Case N ),(Wk) N (x), N (x) ⊢ P (x) (ContrL) N (x) ⊢ P (x) (*) (QR1) N (u) ⊢ Q(u, 0) (= L) N (u), v = 0 ⊢ Q(u, v) ((*), {x → u}) N (u) ⊢ P (u) (( †),{v → v ′ }) N (u), N (v ′ ) ⊢ Q(u, v ′ ) (QR2),(Wk) N (u), N (v ′ ) ⊢ Q(u, s(v ′ )) (= L) N (u), v = s(v ′ ), N (v ′ ) ⊢ Q(u, v) (Case Q) N (u), N (v) ⊢ Q(u, v) ( †)
For each bud, the pair value computed by R ′ is displayed above the bud. △ Definition 3.3 (Path in a pre-proof forest). A (finite or infinite) path in the pre-proof forest (F, R ′ ) is a sequence (S i ) 0≤i<α of sequents from F, for some α ∈ N ∪ {∞}, such that S i+1 is a premise of the inference rule applied on S i (resp. S satisfying R ′ (S i ) = (S, δ)) in a non-bud (resp. bud) node.

A finite path (S i ) 0≤i≤n is bud-free (resp. companion-free) if no S j with j ∈ [0..n -1] is a bud (resp. companion).
The traces in pre-proof forests are defined similarly as for pre-proof trees. Let (F, R ′ ) be a CLKID ω pre-proof forest and (Γ i ⊢ ∆ i ) i≥0 a path in it. A (forest) trace following (Γ i ⊢ ∆ i ) i≥0 is a sequence (τ i ) i≥0 such that, for all i, the conditions from Definition 2.5 are satisfied. In addition, when

Γ i ⊢ ∆ i is a bud node for which R ′ (Γ i ⊢ ∆ i ) = (S, δ), we have τ i = τ i+1 [δ].
Lemma 3.4. G is a path (resp. trace, progress point) in a pre-proof tree iff it is also a path (resp. trace, progress point) in the corresponding pre-proof forest.

Proof. By the construction of pre-proof forests.

⊓ ⊔ Definition 3.5 (CLKID ω proof forest). A CLKID ω proof forest is any CLKID ω pre-proof forest (F, R ′ ) that satisfies the following global trace condition: for every infinite path (Γ i ⊢ ∆ i ) i≥0 in F, there is an infinitely progressing trace following some tail of the path (Γ i ⊢ ∆ i ) i≥k , for some k ≥ 0.

Theorem 3.6. Let us assume a CLKID ω proof tree based on an ordinal trace function and I. The corresponding CLKID ω pre-proof forest is a proof.

Proof. By Lemma 3.4 and the fact that the CLKID ω proof tree satisfies the global trace condition.

⊓ ⊔

Building the partition with ordered parts. Given a pre-proof forest F built from a proof tree T , we say that a node A is connected to a node B if there is a path from A to B. The companions found in each strongly connected component of the graph represented by F and identifying maximal cycles in the graph, will build a part for the partition P. P will also integrate the singleton containing the root sequent of T if it is not a companion, as well as the singletons built from the companions that are not included in any strongly connected component.

Example 3.7. The partition generated for the pre-proof forest built by Example 3.2 consists of only one part made of the two companions N (x) ⊢ P (x) and N (u), N (v) ⊢ Q(u, v). △ Definition 3.8 (dependency relation). Let π 1 and π 2 be two parts from a partition P. We say that π 2 depends on π 1 and write π 1 < P π 2 if, for any S 1 ∈ π 1 and S 2 ∈ π 2 , there is a path from S 2 to S 1 but no path from S 1 to S 2 .

Lemma 3.9. < P is a terminating ordering relation.

Proof. We show that < P is irreflexive, asymmetric and transitive.

irreflexivity. For any part π ∈ P and any two distinct sequents S 1 , S 2 ∈ π, there is a path from S 1 to S 2 but also a path from S 2 to S 1 . So, π < P π. -asymmetry. If π 1 < P π 2 then π 2 < P π 1 , for any distinct π 1 , π 2 ∈ P. Otherwise, the elements of π 1 and π 2 are in the same strongly connected component. -transitivity. Assume that π 1 , π 2 , π 3 ∈ P such that π 1 < P π 2 and π 2 < P π 3 .

Then there exist S 1 ∈ π 1 , S 2 ∈ π 2 and S 3 ∈ π 3 such that there are two paths leading S 1 to S 2 , and S 2 to S 3 , respectively. Their concatenation is a path leading S 1 to S 3 . On the other hand, there is no sequence followed by a trace leading S 3 to S 1 . Otherwise, S 1 , S 2 and S 3 would be in the same strongly connected component, hence in the same part. We conclude that π 1 < P π 3 .

< P is also terminating (well-founded) since P has a finite number of parts. ⊓ ⊔ 4 The LKID ∼ system

We define LKID ∼ as the extension of LKID with the (PInd)-rule: companions axioms S ∈ π (PInd π) S

The rule requires that S be a sequent from the part π included in a partition P computed for some CLKID ω forest proof. For each terminal node or companion N for which there exists a bud-and companion-free path leading a π-sequent to N , we will consider as premise for (PInd):

-N if it is an axiom, or -the axiom C(N ) ⊢ C(N ) if N is a companion ∈ π, or -the axiom C(N ′ ) ⊢ C(N ′ ) if N is a bud and R ′ (N ) = (N ′ , δ), N ′ ∈ π, or -N if it is a companion ∈ π, or -N ′ if N is a bud, R ′ (N ) = (N ′ , δ) and N ′ ∈ π.
Any LKID ∼ derivation is a proof if all branches end in an axiom.

Example 4.1. The LKID ∼ proof of N (x) ⊢ P (x) starts with the application of (PInd), issued from the structural analysis of the proof forest F from Example 3.2. According to Example 3.7, there is only one partition for F. The premises of (PInd) are built only from the axioms ⊢ P (0), N (u) ⊢ Q(u, 0), and C ⊢ C, where C is the clause interpreting each of the sequents

N (x ′ ) ⊢ P (x ′ ), N (v ′ ), N (s(x ′ )) ⊢ Q(x ′ , s(x ′ )), N (u) ⊢ P (u), and N (u), N (v ′ ) ⊢ Q(u, v ′ ). △ Theorem 4.2.
LKID ∼ and CLKID ω are equivalent.

Proof. The '⇒' part. We follow similar arguments as in [START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF]. The transformation of the (Ind) rule is described by Lemma 7.3.1. The (PInd π) rule is translated into the strongly connected component corresponding to the part π computed for a previous CLKID ω forest. As in the proof of Theorem 7.3.2, the set of strongly connected components of the resulted CLKID ω forest F is the disjoint union of the strongly connected components introduced by the (Ind) and (PInd) rules. Hence, Proposition 7.2.3 can be applied for F and conclude that it is a proof. The '⇐' part. Given a CLKID ω proof D, it is firstly transformed into a proof forest F, then into a successive applications of (PInd) rules using parts from F and starting with the root sequent of D. The resulted LKID ∼ derivation, denoted by E, is finite because i) for any application of a (PInd π) rule, the part π ′ of any companion from its premises is smaller (w.r.t. < P ) than π, and ii) < P is a terminating ordering, by Lemma 3.9.

⊓ ⊔

The LKID e system

Given the partition P for a CLKID ω proof, the LKID e system extends LKID to deal with a new predicate symbol P π defined for each part π ∈ P. The set Φ Pπ has a unique production of the form F (x) → P π (x), where F (x) is the conjunction formula S∈π C(S) and x is its vector of free variables. The other productions of Φ Pπ are of the form P π (s j ) → P π (t i ) or → P π (t k ). Productions using non-atomic premises have already been proposed by Martin-Löf [START_REF] Martin-Löf | Haupstatz for the intuitionistic theory of iterated inductive definitions[END_REF] for iterated inductive definitions. The conclusion of the (Ind) rule extended for P π is the sequent P π (x) ⊢ F (x) and the two rightmost premises are axioms (they are further omitted), the first derived from the production F (x) → P π (x) and the second as the major premise:

F (s j ) ⊢ F (t i ) ... ⊢ F (t k ) ... F (x) ⊢ F (x) F (x) ⊢ F (x) (Ind P π ) P π (x) ⊢ F (x)
The LKID e system also integrates an axiom rule for P π :

(Ax P π ) ⊢ P π (x)
The (NInd P π ) rule encodes the Noetherian induction. Defined below on the left of ≡, it is the abbreviation of the LKID e derivation on the right of ≡:

F (sj ) ⊢ F (ti)... ⊢ F (t k )... (NInd Pπ) ≡ ⊢ F (x) F (sj ) ⊢ F (ti)... ⊢ F (t k ))... (Ind Pπ) Pπ(x) ⊢ F (x) (Ax Pπ) ⊢ Pπ(x) (Cut) ⊢ F (x)
Definition 5.1 (LKID e -proof ). A finite LKID e derivation tree is a proof if all branches end in an axiom.

Generating the productions for P π . Each production for P π corresponds to an induction case of the induction schema built for ⊢ F (x), which is a composition of individual induction schemas built for the sequents ⊢ C(S), S ∈ π.

Building the individual induction schemas. Each node from the pre-proof forest will be decorated by a substitution. Any premise from a case-split rule, of the form (2), will be decorated by {x → t|(x → t) ∈ µ and x is a variable from t ′ }, where µ is the mgu of t ′ and t such that t ′ µ = tµ. In the following, we assume that t and t ′ are constructor terms built only from variables and free constructor symbols, i.e. there is no equality relation between two distinct constructor symbols. In this case, the mgu relation can be computed using syntactic unification algorithms [START_REF] Baader | Term Rewriting and All That[END_REF]. The other nodes will be decorated with identity substitutions that instantiate their free variables. Given the sequents S from π and B from a bud-free path starting with S, called cumulative path, we can build a unique cumulative substitution.

Definition 5.2 (Cumulative substitution). Given a cumulative path

(Γ i ⊢ ∆ i ) i∈[0..n] , its cumulative substitution θ is {σ 0 . . . σ n-1 | σ i is the substitution decorating (Γ i ⊢ ∆ i ), ∀i ∈ [0..n -1]}
Example 5.3. 0 and s are the free constructor symbols for naturals. The substitutions associated to the left and right premises of the (Case N ) rule are {x → 0} and {x → s(x ′ )}, and for (Case Q) are {v → 0} and {v → s(v ′ )}, respectively.

The cumulative substitutions computed for the cumulative paths leading the root sequents to the terminal nodes of the pre-proof forest built in Example 3.2 are: i

) {x → 0} for ⊢ P (0), ii) {x → s(x ′ )} for N (x ′ ) ⊢ P (x ′ ) and N (x ′ ), N (s(x ′ )) ⊢ Q(x ′ , s(x ′ )), iii) {v → 0} for N (u) ⊢ Q(u, 0), and iv) {v → s(v ′ )} for N (u) ⊢ P (u) and N (u), N (v ′ ) ⊢ Q(u, v ′ ). △ Lemma 5.4. If θ B
is the cumulative substitution of the cumulative path (S i ) 0≤i≤n leading S to B (i.e., S 0 ≡ S and S n ≡ B) i) the rules applied at each step i ∈ [0..n -1] can be reapplied to build a new path (S ′ i ) 0≤i≤n such that

S ′ 0 ≡ S 0 [θ B ], S ′ n ≡ B, ii) for any i ∈ [1..n -1]
, there is a substitution θ i such that S ′ i [θ i ] ≡ S i , and iii) the (case-split) rules do not instantiate free variables. Proof. We will perform by induction on the length of the path leading S 0 to B. If n = 0, then B ≡ S 0 and θ B is the identity substitution.

If n > 0, let us assume that the path p of length n and leading S 0 to B has the form S 0 , . . . , S n-1 , B. Also, let θ Sn-1 be the cumulative substitution for S 0 , . . . , S n-1 . By induction hypothesis, we assume that any path of length n -1 satisfies the property, in particular S 0 , . . . , S n-1 . So, the steps from S 0 , . . . , S n-1 can be reapplied to build the path S ′′ 0 , . . . , S ′′ n-1 such that S ′′ 0 ≡ S 0 [θ Sn-1 ], S ′′ n-1 ≡ S n-1 and for i ∈ [1..n-2], there is a substitution θ i such that S ′′ i [θ ′ i ] ≡ S i . Let σ be the substitution decorating S n and θ B the cumulative substitution for p. σ can be either an identity substitution, or an mgu substitution instantiating free variables from S n-1 . For the first case, θ B equals θ Sn-1 and the re-execution of the rule applied at the step n -1 of p on S ′′ n-1 generates B. In the second case, θ B is the substitution composition θ Sn-1 σ. The path (S ′ i ) 0≤i≤n is defined as The cumulative substitution is {x → s(x ′ )} and the new path is: (N (s(x ′ )) ⊢ P (s(x ′ ))), (N (s(x ′ )), N (s(x ′ )) ⊢ P (s(x ′ ))), (N (s(x ′ )), s(x ′ ) = s(x ′ ), N (s(x ′ )) ⊢ P (s(x ′ ))), (N (s(x ′ )), N (x ′ ) ⊢ P (s(x ′ ))), (N (x ′ ) ⊢ P (x ′ )). △

S ′ i ≡ S ′′ i [σ],
An induction schema for a sequent S is a collection of induction cases that attach a (potentially empty) set of sequents, called induction hypotheses, to an instance of S, called induction conclusion. .k]) defined on every (sub)vector given as argument to the conclusion of ( 4) is the conclusion of an individual induction case defined for ⊢ C ip (x ip ). For each of its attached induction hypotheses, there is a premise of (4) defined as follows. If the induction hypothesis is the sequent ⊢ C ir (t ir ) (r ∈ [1..k]), the premise is the induction conclusion of (4) for which the rth (sub)vector is replaced by t ir . The premises that replace distinct (sub)vectors are factorized into a single premise.

Example 5.8. P π12 is defined by the productions issued from the individual induction schemas for ⊢ C 1 (x) and ⊢ C 2 (u, v), computed at Example 5.7: → P π12 (0, u, 0), P π12 (x ′ , x ′ , s(x ′ )) → P π12 (s(x ′ ), u, 0), P π12 (u, u, v ′ ) → P π12 (0, u, s(v ′ )), and P π12 (x ′ , x ′ , s(x ′ )), P π12 (u, u, v ′ ) → P π12 (s(x ′ ), u, s(v ′ )). △ Applying the (NInd) rule on a part sequent. The proof of Γ ⊢ ∆ ∈ π i1...i k starts by applying a (Cut) using the conjunction formula of π i1...i k :

(∨L),(¬L),(Ax) Γ, C(Γ ⊢ ∆) ⊢ ∆ (∧L),(Wk) S∈πi 1 ...i k C(S), Γ ⊢ ∆ (the induction cases) (NInd P πi 1 ...i k ) ⊢ S∈πi 1 ...i k C(S) (Wk) Γ ⊢ S∈πi 1 ...i k C(S), ∆ (Cut) Γ ⊢ ∆
Each induction case is further transformed into the individual induction cases that built it, by firstly deleting the conjunction symbols from the antecedent using successive applications of (∧L) rules, then the conjunction symbols from the succedent using the (∧R) rule. The antecedent formulas from each new sequent, that are not induction hypotheses attached to the induction conclusion from the succedent, are deleted by the (Wk) rule. The induction step is summarized as:

Conclusions and perspectives

We have shown that structural and cyclic induction reasoning in FOL ID are convertible and are subsumed by Noetherian induction. Compared to LKID, LKID e can generate proofs that combine the advantages of structural and cyclic reasoning by the dynamic definition of new induction schemas. Our procedure transforms effectively cyclic to structural proofs and does not require unfolding operations as in [START_REF] Sprenger | On the structure of inductive reasoning: Circular and tree-shaped proofs in the µ calculus[END_REF] or as suggested in [START_REF] Brotherston | Cyclic proofs for first-order logic with inductive definitions[END_REF][START_REF] Brotherston | Sequent Calculus Proof Systems for Inductive Definitions[END_REF].

These results open the perspective for validating CLKID ω -like proofs by (higher-order) certification environments integrating the Noetherian induction principle, like Coq [START_REF]The Coq Reference Manual -version 8[END_REF], by using similar certification methodologies as for implicit induction [START_REF] Stratulat | Automated certification of implicit induction proofs[END_REF]. Also, it would be interesting to extend CLKID ω for integrating reductive-free cycles [START_REF] Stratulat | A unified view of induction reasoning for first-order logic[END_REF].

A The proof of Lemma 5.11 Let π be a part of the partition P from a proof forest F built from a CLKID ω proof tree T , based on the ordinal trace function f and the non-empty set of interpretations I.

By absurd, assume that (NInd P π ) is applied in some CLKID e derivation D with valid premises but false conclusion. The conclusion is ⊢ F (x)(≡ S∈π C(S)), hence there is a sequent S ∈ π that is false. By Definition 3.5, the definition of ordinal trace functions and Lemma 3.4, there is an infinite path S i≥0 of false sequents in F starting with S, and an infinitely progressing trace following some tail of S i≥k , for some k ≥ 0. Since F has a finite number of nodes, there is a companion S ′ that is infinitely often visited in the path. Since any companion from F is in a part of P, we consider π ′ ∈ P such that S ′ ∈ π ′ .

The rule (NInd P π ′ ) should be also applied in D, otherwise S ′ cannot occur infinitely in S i≥k . Its conclusion ⊢ F ′ (x ′ )(≡ S∈π ′ C(S)) is false. Let S k1 be the first occurence of S ′ in S i≥k and S k2 , with k 1 < k 2 , the occurence of the next visited companion S ′′ ∈ π ′ in S i≥k . Let also assume that the τ -value of S k1 and S k2 in the trace is α k1 and α k2 , respectively. There should be a premise of (NInd P π ′ ), built from a companion-free cumulative path ∈ F leading a false cumulative instance of S ′ to a false instance of S ′′ or some bud node whose companion is S ′′ , by Lemma 5.4. We denote by F ′ (t k2 ) ⊢ F ′ (t k1 ) the instance of the premise leading S k1 to S k2 and notice that both F ′ (t k2 ) and F ′ (t k1 ) are false. We associate to the term vectors t k1 and t k2 the weights α k1 and α k2 , respectively. We proceed similarly for S k2 as for S k1 , as well as for any future occurrence of companions from π ′ in S i≥k .

Let us define E ′ = {t p | S p is an occurrence of S ′ in S i≥k1 and F ′ (t p ) has C(S p ) as one of its conjuncts}. We have that (∀t p ∈ E ′ , ¬F ′ (t p ) ⇒ (∃t j ∈ E ′ , t j < t p ∧ ¬F ′ (t j )))

(5) i) by taking, for an arbitrary t p , the vector t j such that S j is the next occurrence of S ′ in S i≥k1 that follows S p for which there is a progress point between S j and S p , ii) by successively considering the companions from π ′ in S j≤i≤p , and iii) by using the definition of ordinal trace functions and the transitivity property of <. The Noetherian induction principle ∀φ, (∀m ∈ E, (∀k ∈ E, k < m ⇒ φ(k)) ⇒ φ(m)) ⇒ ∀p ∈ E, φ(p) can be applied on the contrapositive version of (5) when instantiating E by E ′ and φ by F ′ , to conclude that ∀p ∈ E ′ , F ′ (p). Contradiction since F ′ (p) is false, for any p ∈ E ′ . ⊓ ⊔

Fig. 2 .

 2 Fig. 2. The equality rules.

Example 5 . 5 .

 55 for any i ∈ [0..n -1], and S ′ n ≡ B. No instantiation of free variables is performed when the case-split rule is applied on S ′′ n-1 . ⊓ ⊔ Let us assume the cumulative path pre-proof forest given in Example 3.2, for which the sequents are decorated with substitutions (excepting the last sequent): (N (x) ⊢ P (x), {x → x}), (N (x), N (x) ⊢ P (x), {x → s(x ′ )}), (N (x), x = s(x ′ ), N (x) ⊢ P (x), {x → x; x ′ → x ′ }), (N (s(x ′ )), N (x ′ ) ⊢ P (s(x ′ )), {x ′ → x ′ }), (N (x ′ ) ⊢ P (x ′ )).

Definition 5 . 6 (Example 5 . 7 .

 5657 individual induction schema). Let S ∈ π (π ∈ P). For each companion-free cumulative path leading S to (a terminal node or companion) N , we build an induction case of the individual induction schema for ⊢ C(S) having:-⊢ C(S)[θ N ] as induction conclusion built with the cumulative substitution θ N , -⊢ C(S N )[δ] as induction hypothesis if N is a bud node for which R ′ (N ) = (S N , δ) and S N ∈ π, or ⊢ C(N ) if N is a companion from π.Considering the part from Example 3.7, let us denote byC 1 (x) (resp. C 2 (u, v)) the clause C(N (x) ⊢ P (x)) (resp. C(N (u), N (v) ⊢ Q(u, v))). By using the cumulative substitutions from Example 5.3, the induction cases of the individual induction schema for -⊢ C 1 (x) are: i) ⊢ C 1 (0), and ii) ⊢ C 1 (s(x ′ )) with the induction hypotheses⊢ C 1 (x ′ ) and ⊢ C 2 (x ′ , s(x ′ )); -⊢ C 2 (u, v) are: i) ⊢ C 2 (u,0), and ii) ⊢ C 2 (u, s(v ′ )) with the induction hypotheses ⊢ C 1 (u) and ⊢ C 2 (u, v ′

  ). △ Generating productions for new predicate symbols. Let π i1...i k be a part built on k(> 0) sequents S i1 , . . . , S i k , where i 1 , . . . , i k ∈ [1..k] is a permutation of the values from [1..k]. Let also C ip (x ip ) be C(S ip ) (p ∈ [1..k]) with x ip the vector of free variables from C(S ip ) and D 1 ip × . . . × D ji p ip the domain of C ip . The new inductive predicate symbol P πi 1 ...i k with the domain D 1 i1 × . . . × D

					ji 1 i1 × . . . ×
	D 1 i k × . . . × D	ji k i k is defined by the smallest set of productions of the form
		premises → P πi 1 ...i k (t 1 i1 , . . . , t	ji 1 i1 , . . . , t 1 i k , . . . , t	ji k i k )	(4)
	Each of the sequents ⊢ C ip (t 1 i1 , . . . , t	ji 1

i1 , . . . , t 1 ip , . . . , t ji p ip ) (p ∈ [1.

a sequent, called conclusion and written beneath it, from a (potentially empty) multiset of sequents, called premises and written above it. Side annotations may specify the name of the rule and its application conditions. Derivations are built by successive applications of inference rules and have a tree shape. When it is clear from the context, we use a double line instead of a simple line to mean that formulas may be permuted in the antecedent of the conclusion and one or several occurrences of the rules specified aside are successively applied.Γ ∩ ∆ = ∅ (Ax) Γ ⊢ ∆ Γ ′ ⊢ ∆ ′ Γ ′ ⊆ Γ, ∆ ′ ⊆ ∆ (Wk) Γ ⊢ ∆ Γ ⊢ F, ∆ Γ, F ⊢ ∆ (Cut) Γ ⊢ ∆ Γ ⊢ F, ∆ (¬L) Γ, ¬F ⊢ ∆ Γ, F ⊢ ∆ (¬R) Γ ⊢ ¬F, ∆ Γ, F ⊢ ∆ Γ, G ⊢ ∆ (∨L) Γ, F ∨ G ⊢ ∆ Γ, F, F ⊢ ∆ (contrL) Γ, F ⊢ ∆ Γ ⊢ F, F ∆ (contrR) Γ ⊢ F, ∆ Γ ⊢ F, G, ∆ (∨R) Γ ⊢ F ∨ G, ∆ Γ, F, G ⊢ ∆ (∧L) Γ, F ∧ G ⊢ ∆ Γ ⊢ F, ∆ Γ ⊢ G, ∆ (∧R) Γ ⊢ F ∧ G, ∆ Γ ⊢ F, ∆ Γ, G ⊢ ∆ (⇒ L) Γ, F ⇒ G ⊢ ∆ Γ, F ⊢ G, ∆ (⇒ R) Γ ⊢ F ⇒ G, ∆ Γ, F ⊢ ∆ x ∩ F V (Γ ∪ ∆) = ∅(∃L) Γ, ∃xF ⊢ ∆ Γ ⊢ F, ∆ x ∩ F V (Γ ∪ ∆) = ∅(∀R) Γ ⊢ ∀xF, ∆ Γ, F [{x → t}] ⊢ ∆ (∀L) Γ, ∀xF ⊢ ∆ Γ ⊢ F [{x → t}], ∆ (∃R) Γ ⊢ ∃xF, ∆Fig. 1. The LK rules.

{C1 . . . Cp ⊢ C | '⊢ C attaches ⊢ C1 . . . ⊢ Cp' is an individual case} (NInd Pπ i 1 ...i k ), (∧L),(∧R),(Wk) ⊢ Ci 1 (x 1 i 1 , . . . , x

Example 5.9. The LKID derivation of N (x) ⊢ P (x) from Example 3.2 starts as (Ax) N (x), P (x) ⊢ P (x) (Ax) N (x) ⊢ N (x), P (x) (¬L) N (x), ¬N (x) ⊢ P (x) (∨L) N (x), C1(x)(≡ ¬N (x) ∨ P (x))

(NInd P π12 ) is applied on ( †) using the productions from Example 5.8:

The derivations of its premises are

(Ax) leaf . . . (following the companion (comp.)-free cumulative paths with θ as cumulative substitution)

13

The derivation of C 1 , . . . , C p , Γ [θ] ⊢ ∆[θ] starts by executing the rules from the companion-free cumulative paths of the CLKID ω pre-proof forest leading Γ ⊢ ∆ to the terminal nodes and companions for which the cumulative substitution is θ, as shown in the proof of Lemma 5.4. We perform a case analysis on them.

The LKID e derivation for a leaf is (Ax). For any companion Γ j ⊢ ∆ j or bud whose companion Γ j ⊢ ∆ j is not in π i1...i k , the derivation is developed as for Γ ⊢ ∆. The sequent corresponding to any other node has in the antecedent a clause C that interprets the node; it is proved by decomposing C, as previously.

Example 5.10. The derivations of the individual induction cases ⊢ C 1 (0) and ⊢ C 2 (u, 0) from Example 5.9, after expansion to their clausal definition, are:

(Ax)

where the derivation of the leftmost sequent, denoted by (**), is

The derivation of C 1 (x ′ ), C 2 (x ′ , s(x ′ )), N (x ′ ) ⊢ C 1 (s(x ′ )) is done similarly. △ Lemma 5.11. (NInd) is locally sound and implements Noetherian induction. Theorem 5.12. LKID e and CLKID ω are equivalent.

Proof. The ' ⇒ ′ part. (Ind) using new predicate symbols is an instance of LKID's (Ind), hence translatable into CLKID ω . The application of (Ax P π ) on ⊢ P π (x) is translated to the application of (P π R) using the production S∈π C(S) → P π (x) which yields the sequent ⊢ S∈π C(S). By decomposing it using conveniently the (∧R), (∨R) and (¬R) rules, we get the sequents ⊢ S, S ∈ π. Each of them is proved by the CLKID ω (forest) proof of π. The ' ⇐ ′ part. By generating the partition P from the CLKID ω proof T , then applying recursively the procedure for developing the derivation of a part sequent starting with the root of T . The process terminates as < P is terminating.

⊓ ⊔ Corollary 5.13. Noetherian induction can represent structural and cyclic induction reasoning performed by LK extended with new inductive predicates.

Proof. By Theorems 4.2 and 5.12 since our procedure converts any CLKID ω proof to an LKID e proof using only (NInd)-based induction reasoning. ⊓ ⊔


Frédéric Lacour

Andrei Sabac

Michel Spajer
email: michel.spajer@univ-fcomte.fr

Nanostructuring Optical Waveguides by Focused Ion Beam Milling. Near-Field Characterization

Keywords: numbers: 84.40.Ik, 84.40.Fe Nanostructures, Photonic Band Gap, FIB milling, Scanning Near-field Optical Microscopy, Waveguide characterization

Nanostructures have become an attractive subject due to many applications, particularly the photonic bandgap effect observed in photonic crystals. Nevertheless, the fabrication of such structures remains a challenge because of accurate requirement concerning regularity, shape, hole depth etc. of the structure. E-beam lithography permits a good control of dimensional parameters but needs a 1-step fabrication process. In our work, we have to combine traditional strip-load waveguides (SiO2/SiON/SiO2 on Si) and nanostructures whose dimension are totally different. This imposes a 2-step process where waveguides and nanostructures are successively fabricated. We have at our disposal different ways to characterize these nanostructures. A direct aspect control during and after FIB treatment can be achieved by FIB and SEM imaging. Scanning near-field optical microscopy (SNOM) is currently the most effective way to test guiding confinement in such surface structures by detecting the evanescent field.

I. INTRODUCTION

Within the last two decades, the development of technology has permitted structure fabrication at a submicrometer scale. These nanostructures allow a new control of light, mainly after the significant progress made in understanding of photonic band gap (PBG) since the 1980s years [START_REF] Joannopoulos | Photonic Crystals, Molding the Flow of Light[END_REF]. Since then periodic nanostructures (with dimensions a hundred times smaller than the original waveguides) seem the best way to develop novel integrated optical devices which dimensions are a hundred times smaller than the original waveguides. Hunting the losses in such devices is a real challenge mainly for telecom application. Devices like waveguides or microcavities in photonic crystals (PhCs) have already been presented and demonstrated [START_REF] Chow | [END_REF]. Nevertheless, before all-PhCs components can be developed and replace presently used components, PhCs and classical optical devices will coexist for a certain time. In this perspective we were interested in fabricating and characterizing mixed devices, which combine both photonic structures or nanostruc-tures and classical waveguides.

The most common used PhCs are planar PhCs (lattice of holes in dielectric material or dielectric pillars in air), which are easier to fabricate than 3D-PhCs which theorically ensure the best control of light. 2D-PhCs have photonic band gap (PBG) in two directions, so light has to be confined in the third direction by a multilayer structure. Therefore high-index materials (AsGa, AlGaAs, Si etc.) have been used because of their large index difference with air which produces large photonic bandgap. Low-index materials like SiO 2 (n = 1.47 at λ = 900nm) which are the most common in integrated optics are generally not studied for PBG application, except for photonic fibers.

In this work, we fabricate and characterize photonic structures combined with typical waveguides in materials often used in integrated optics and MOEMS components [3], such as multilayer waveguides SiO 2 /SiON/SiO 2 on Si.

The first part is a theoretical study of the structures based on FDTD (Finite Difference Time Domain) calculation. These simulations demonstrate the feasibility of a PBG with low-index materials in specific conditions. Afterwards, we describe the fabrication of the samples in two steps : fabrication of the waveguides and of the photonic structures. We'll show in this part a novel way to fabricate PhCs using a Focused Ion Beam (FIB). Finally characterization by SNOM probing will be presented.

II. THEORETICAL STUDY

Numerical studies are carried out using three commercial software from RSoft. In a first step a study of infinite PhCs is performed by a PWE (Plane Wave Expansion) software (RSoft BandSolve) to find the PBG and to optimize the parameters of the nanostructure (hole size and period). In a second step electromagnetic field propagation in the nanostructures is numerically mapped by a FDTD calculation (RSoft F ullW ave). Rigorous analysis of geometrical parameters like hole depth or surface roughness requires 3D calculation, which demands too many computer ressource. Therefore, we shall limit our study to 2D calculation applied to a 2D equivalent structure, to describe the general behavior of the 3D structure. The basic structure studied is a triangular lattice of holes centered on the waveguide as shown in Fig. 1a. The equivalent 2D structure we chose is a vertical guiding slab with a lattice of infinite vertical holes centered inside.

The free waveguide properties (modes, propagation, losses...) are obtained by a BPM (Beam Propagation Method) software (RSoft BeamP rop).

a) b)

FIG. 1: Two studied nanostructures a) without defects b) with a line defect.

A. Photonic bandgaps calculation

For the wavelength λ = 900nm, effective index of the multilayer waveguide is calculated by the BPM software to be n ef f = 1.489. Our calculation gives complete photonic band gap in the case of triangular lattice for only one polarization (TM) (Fig. 2), for a hole diameter d between 0.65a, and 0.82a (a is the period of the lattice). Figure 2 shows the band diagram for d = 0, 7a. A TM PBG can be obtained for frequencies 0.473 < ( ω.a 2πc = a λ ) < 0.496. The fact that the PBG in TM mode is very narrow and that there is no complete band gap in the other polarisation can be explained by Afterwards we only consider holes of period a = 360nm and diameter d = 200nm. These values were chosen to fit with technological limitations (the ratio d/a can hardly exceed 0.7 in the milling process) and to obtain a bandgap in the wavelength range (around 700-980nm) given by the tunable laser (See IV).

B. FDTD Simulations

After determining the parameters of the hole lattice the combination of the nanostructures with the waveguide can be characterized by FDTD calculation.

Two structures were modelled: the first one is a complete lattice, in the second one a line of holes has been removed at the center of the waveguide ( Fig. 1b). It is expected that the lattice of holes without defects will behave like a mirror for wavelengths included in the photonic band gap.

Complete triangular lattice of holes

Light is injected in the equivalent planar waveguide wherein the hole lattice has been pierced according to the previous parameters. In a first step, transmission spectra have been calculated by injecting a pulse excitation in the direction ΓM . Two samples of this spectrum are presented in Fig. 3. Although PBG calculation exhibits no complete band gap for TE polarisation and a narrow one for TM polarisation, the spectrum shows a band gap for both polarisations. For TE polarisation a fall of transmission efficiency can be noticed for wavelengths between 848nm et 934nm. In TM polarisation a similar PBG exists for wavelengths between 800nm and 927nm.

It must be noticed that a partial band gap can exist for a given incidence, even if the crystal has no complete band gap (independent of the incidence). In the present case, the spectra of Fig. 3 correspond to the partial band gaps observed on the vertical line M of Fig. 2. It can be verified that the width given by FDTD is slightly smaller (×0.8) than the previous one as shown in table I. This discrepancy can probably be explained by the plane wave expansion of the guided mode: the direction of incidence is not limited to the waveguide axis . The fall of transmission increases with the number of periods in the propagation direction. We found that a minimum of ten periods is necessary to obtain a 0.1% transmission. For this example, 40 periods have been used.

Then, by launching continuous excitation and waiting for field stabilization in the structure, a mapping of each field (Ey, Hx and Hz for TE polarisation, Ex, Ez and Hy for TM polarisation) can be obtained as shown in Fig. 4. For λ = 800nm, light can pass through the lattice, but for λ = 900nm, light seems to be completely reflected.

Triangular lattice with a line defect

We carried out the same calculation for a triangular lattice of holes where one line is missing. Light propagation is always in the direction ΓM . Transmission spectrum shows that the band gap has been perturbed and that some peaks appear (See Fig. 5(a)). For a better coupling efficiency between optical waveguide and PBG waveguide of different width, a taper would be desirable (optical waveguide is 4µm wide and a line missing line is wide of one period of the lattice (360nm)). Nevertheless 2D FDTD calculation at the wavelength corresponding to the higher peak (λ = 800nm) exhibits a high confinement of light in the line defect (See Fig. 5 (b)). A calculation made at PBG wavelengths shows no light propagation in this line defect: the result is similar to Fig. 4 (b). Photonic crystal fabrication remains a challenge mainly due to the size and the depth of engraved holes. In our case, hole diameter is 200nm and the depth has to be more than 3µm to overlap the optical guided mode. Moreover, as optical waveguides have been fabricated beforehand, a good precision is needed to align correctly waveguides and nanostructures.

In a previous work [4], we have demonstrated the possibility of nanostructuring lithium niobate substrate by Focused Ion Beam (FIB) the dimension of which is less than 50nm. Other laboratories have obtained FIB patterns at submicrometer scale [6] with good optical properties [5,[START_REF] Bostan | Proceedings Symposium IEEE/LEOS (Benelux chapter[END_REF]. Furthermore the main advantage of FIB is the ability to drill holes directly from the sample surface and the direct control of the structures after milling.

A. Waveguide fabrication

Optical waveguides are an important part in the fabrication of the sample since they guide light to nanostructures and also provide optical confinement in the third dimension.

The optical waveguides (Fig. 6) we have chosen are multilayer waveguides (SiO 2 /SiON/SiO 2 ) deposited on a Si substrate. The three layers (SiO 2 , thickness: e 1 = 3µm, SiON : e 2 = 0.5µm and SiO 2 again: e 3 = 0.5µm) are deposited by PECVD process. This process allows a good control over the thickness and over the optical index of the different layers. After a lithographic masking the rib waveguides are etched by RIE process on the top SiO 2 layer.

For the chosen parameters, BPM calculation have shown that waveguides are single mode over the wavelength scale which will be used for near-field characterization (700 -950nm).

B. Nanostructuring waveguides with FIB

The fabrication process (See Fig. 7) is based on a direct etching of the sample substrate by FIB bombardement. The samples, on which multilayer waveguides have been previously fabricated, are chromium coated (< 150nm layer) by electron gun evaporation to avoid charging, and grounded with a conductive paste before introduction in the FIB vacuum chamber (< 10 -8 torr). Then the sample is milled using a FIB column (Orsay-Physics -LEO FIB4400). Ga + ion are emitted with a current of 2µA and accelerated by a voltage of 30kV . The probe current of the focused beam is 66pA or 115pA . The Gaussianshaped spot size is estimated to be 50nm in the best conditions. The ion beam scans the sample, the deflection field being controlled by a software to produce the desired pattern.

Several triangular lattice of circular holes with previously determined parameters (a = 360nm and d = 200nm) have been milled on the substrate. Fig. 8 shows two views of a 20 × 20 hole lattice fabricated by FIB. The cross section realized by FIB (Fig. 8 (b)) provides important information about the hole depth (which we expect to be more than 1µm deep), the surface aspect and the hole shape . Hole shape is not cylindrical as we first wanted but conical. The upper diameter at the surface is about 220nm and the bottom diameter 120nm. This kind of problem is a fundamental drawback of FIB milling due to material redeposition during the scanning process. More vertical sidewalls can be obtained by using reactive gases during the FIB process. We have characterized this fabricated nanostructures using two different methods. A transmission spectrum of those nanostructures has first been studied by measuring the ratio between intensities of injected light and recovered light at the waveguide extremity. The second method is an in-situ characterization of the nanostructures with a stand-alone near-field microscope working in detection mode. This technique has been employed by several laboratories, more specifically in the study of high electromagnetic confinement (See [11,12,13,14,15]).

A. Transmission spectrum

A tunable Titane-Sapphire Laser is used to scan a wavelength range from λ = 700nm to λ = 980nm. Its beam is injected into a polarization maintaining optical fiber which can be oriented to select TE or TM polarization. Light is injected directly in the optical waveguides from this fiber to limit the optical losses. Injection is controlled by collecting the guided mode from the end face of the waveguide by a microscope objective and a CCD camera (Fig. 10). The transmission spectrum exhibits variations of about 20% but does not show any clear photonic band gap. The reason seems to be the out-of-plane losses caused by the perforation of the waveguide which induces a coupling of the guided wave with radiation modes. Recent work [START_REF] Ferrini | [END_REF]9,10] has demonstrated that out-of-plane losses in planar PhCs depend on two principal parameters: they occur when the overlap between the guided mode and the nanostructures is not complete and when the sidewalls of holes are not vertical. From the cross-section of Fig. 8 (b) the tilt of the sidewall is about 2.5 o and the holes are deeper than the core layer but do not overlap the mode completely. Fig. 9 superimposes the hole profile and the BPM calculated optical mode. Reference [START_REF] Ferrini | [END_REF] demonstrates that a sidewall tilt bigger than 1 o may have disastrous consequences on the LiN bO 3 effect.

1,2µm

Even if a real PBG cannot be observed by transmission spectrum, we'll see that near-field characterization could show relevant information on these nanostructures.

B. Near-field characterization 1. Experimental setup

A stand-alone microscope has been used to characterize nanostructures on waveguides (Fig. 10). The evanescent wave on top of the structure is collected by an optical probe made of an optical fiber tapered by the pulling/heating method under CO 2 laser beam. Gluing the probe to a tuning fork ensures the usual distance control by shear-force feedback. The laser beam is modulated by a chopper and the optical signal measured by synchronous detection. Both topographic signal from feedback control and optical signal are recorded by a computer, which controls the XY scanning. its section (Fig. 11 (c)) show a minimum of intensity at the edges of waveguide, which matches with the theorical optical field intensity section calculated at constant distance by BPM calculation (Fig. 11 (e)).

Near-field characterization of a complete lattice

We have characterized at different wavelengths a lattice of 40 × 40 holes (diameter: d = 200nm, period: a = 360nm) pierced on the waveguide. Even if transmission spectra did not show any clear photonic band LiN bO 3 , light penetration into such structures have important variations with the wavelength. Two images (topographic and optical) at two wavelengths (Fig. 12), one in the theorical band gap (λ = 900nm, Fig. 12 (c)), the other out of the bandgap (λ = 850nm, Fig. 12 (b)) show two completely different behaviours. Topographic image (Fig. 12 (a) and (c)) exhibits periodic nanostructures (between white lines). Light propagates from top to bottom. Fig. 12 (b) shows a deep penetration of the light into the structure. For the other wavelength, Fig. 12 (c) shows a bright zone near the upper limit of the hole lattice but light decreases rapidly inside the lattice. The transmission efficiency (ratio output/input) of the lattice is five times greater at λ = 850nm than at λ = 900nm.

Fringes inside and in front of the lattice must be noticed: multiple reflections inside such structures and standing waves outside could explain this phenomenon.

Near-field characterization of a lattice with a line defect

A second type of structure (80 × 40 hole lattice with a line missing in its center) has been characterized. It can be considered as a photonic waveguide, in which the injection would require a taper to ensure an efficient connection to the conventional waveguide, as its width is 10 times smaller.

As in the previous part, penetration and propagation of light into the structure depends on the wavelength. Fig. 13 shows topographic and optical images at λ = 825nm which is outside the theoretical bandgap. On the topographic image the missing line is visible in the center of the waveguide. The optical signal exhibits a dark line located on the missing holes and two lines of bright dots on both sides. This result presents similarities with the numerical simulation Fig. 5 (b). These bright lines are completed by two diffracted beam which are guided in the SiON layer on both sides of the waveguide (Fig. 13(c)).

V. CONCLUSIONS

Direct FIB milling has shown some limits (hole shape, etching depth) which have caused imperfection in the fabricated photonic crystals. We are improving another similar way of fabricating such nanostructures: FIB is used only to engrave a 200-250nm thick metallic layer, which is considered as a mask for RIE or deep-RIE. A shorter milling time and a better aspect ratio are expected from this process.

In the present conditions the 2D approximation we used in FDTD simulation helped us to chose the wavelength domain in the characterization but the imperfect structures had no bandgap effect to be compared with the theoretical one. In spite of this difficulty the characterization of imperfect photonic structures is an example of the diagnosis delivered by near-field probing applied to complex 3D structures, the properties of which are not predicted by a 2D model. Despite the imperfection of the fabricated structures, the experimental and theoretical images of light propagation in a line-defect lattice present interesting similarities.

FIG. 2 :

 2 FIG. 2: Bandgap diagrams of a triangular hole lattice (n = 1.53)

FIG. 3 :

 3 FIG. 3: Transmission spectrum of 40 × 40 lattice of holes for TE and TM polarisation.

FIG. 4 :

 4 FIG. 4: Cartographies of Ey field for TE polarisation at λ = 800nm (a) (outside PBG) and λ = 900nm (b) (inside PBG) for 40 × 40 holes triangular lattice (a = 360nm, d = 200nm).

FIG. 5 :

 5 FIG. 5: (a) Transmission spectrum of 40 × 40 lattice of holes with a line defect for TE polarisation. (b) Ey field cartography (2D FDTD calculation) for λ = 800nm

FIG. 6 :FIG. 7 :

 67 FIG. 6: Description of the optical waveguides.

FIG. 8 :

 8 FIG. 8: (a) SEM image of a 20 × 20 lattice of holes on a waveguide. (b) FIB image of a cross section made by FIB milling of the same lattice. Measured depth: e = 1.20µm (view angle α = 30 o )

FIG. 9 :

 9 FIG. 9: Problems of fabricated structures. Superimposition of BPM calculated guided mode and structures.

FIG. 11 :

 11 FIG. 11: Near-field characterization of two bare waveguides. (a) Topographic image (40 × 40µm 2 ) (b) Corresponding optical image (c) Section of experimental optical image (d) Section of theorical optical image (BPM)

FIG. 12 :

 12 FIG. 12: Near-field characterization of hole lattice on the waveguide at two wavelengths ((b) λ = 850nm; (c) λ = 900nm). (a) Topographic image (5 × 5µm 2 ). (b), (c) Corresponding optical images.

FIG. 13 :

 13 FIG. 13: Near-field characterization of the hole lattice with a line defect on the waveguide at λ = 825nm (a) Topographic image (10 × 10µm 2 ). (b)Corresponding optical image. (c) Optical image (40 × 40µm 2 ) of the same structure. Measured angle of the diffracted beam θ = 18.8 o .

TABLE I :

 I Comparaison of obtained band gap between FDTD calculation (FullWave) and PWE method (BandSolve).

		BandSolve	FullWave
	TE ∆(a/λ) =	0.0495	0.0391
	TM ∆(a/λ) =	0.0795	0.0621
	TM complete PBG	∆(a/λ) = 0.023

Acknowledgments

Many thanks to Éloïse Devaux (INIST, Strasbourg) for her technical assistance and to Maria-Pilar Bernal, Matthieu Roussey, Nadège Bodin, Dominique Heinis for fruitful discussions.


A Bilbao-Guillerna

A Barrios

I Mancisidor

N Loix

J Muñoa

Control laws for chatter suppression in milling using an inertial actuator

Keywords: active damping, chatter suppression, inertial actuator, milling

In this paper an inertial actuator is used to design an active damper for chatter suppression in a milling process. Researchers usually use the Direct Velocity Feedback (DVF) technique to design the control law for the actuator. This DVF technique is widely used for its simplicity and leads to very good results. However, it can easily excite the structural modes of the actuator and make unstable the closed-loop system. A Virtual Passive Absorber (VPA) control law is proposed to avoid this drawback. This kind of controllers are less likely to excite the actuator since the control effort is focused on the problematic mode of the structure. The parameters of the VPA controller are chosen to reduce the real part of the frequency response function (FRF) of the structure, which is well known to be important to determine the stability region. Several practical experiments are performed to show the usefulness of the control laws comparing the performance of both of them. The VPA control is tested in a pair of practical milling processes as well.

Introduction

Self-excited or chatter vibrations are well known among milling machine manufacturers and users. Nowadays, chatter is one of the main limitations of milling processes. Machine tool chatter vibrations cause an unacceptable surface finish on the workpiece reducing the life of the tool and the mechanical components of the machine.

Chatter stability margin can be increased by adding a tuned vibration absorber to the structure [START_REF] Rivin | Enhancement of dynamics stability of cantilever tooling structures[END_REF][START_REF] Sims | Particle dampers for workpiece chatter mitigation[END_REF]. However, a passive absorber is not feasible in many machining processes where the dynamics of the system change according to the operation point and an active damper is needed [START_REF] Brecher | Electrohydraulic active damping system[END_REF][START_REF] Chung | Active damping of structural modes in high speed machine tools tools[END_REF][START_REF] Ganguli | Active damping of in machine -demonstration with a hardware-in-the-loop simulator[END_REF]. The use of an inertial actuator is a possible solution. An inertial actuator produces a reaction force on the host structure according to a designed control law.

Inertial actuators have been widely used to reduce vibrations in machining operations. Researchers usually use the well-known Direct Velocity Feedback (DVF) strategy in order to design the control law [START_REF] Ehmann | Comparison of control strategies for active vibration control of flexible structures[END_REF][START_REF] Huyanan | Vibration control strategies for proof-mass actuators[END_REF][START_REF] Preumont | Vibration Control of Active Structures. An Introduction[END_REF]. This technique has been mainly used due to its simplicity and leads to very good results, avoiding the appearance of chatter in many practical cases. However, some authors have proposed alternative control laws, which may lead to better results. One of these possible control laws is the Virtual Passive Absorber (VPA) control [START_REF] Huyanan | Vibration control strategies for proof-mass actuators[END_REF][START_REF] Juang | Robust controller designs for second order dynamics systems, a virtual passive approach[END_REF][START_REF] Pratt | Chatter control and stability of cantilever boring bar under regenerative cutting conditions[END_REF]. This control law is designed to make the inertial actuator behave as a typical passive damper. The main disadvantage of passive absorbers is that they are limited to reduce a unique mode of the system. However, a VPA control can be retuned to avoid a different mode and it can be designed to have larger mass ratios. In this paper we propose a VPA controller to increase the chatter stability margin in machining operations using an inertial actuator.

Despite its simplicity the DVF control requires some study in order to find the optimum value of the feedback gain. This is usually calculated from a root locus analysis if a model of the system is available. In most cases this value is found experimentally increasing its value until the closed-loop system is unstable. This study is necessary because a large value of the feedback gain excites the structural modes of the mass damper while a small value of it could lead to a not good enough reduction of the vibrations in the structure.

On the other hand, VPA control is more straightforward and it only requires a modal analysis of the system to be controlled. Many authors have proposed different ways of finding the optimum values of the parameters of the controller [START_REF] Hartog | Mechanical Vibrations[END_REF][START_REF] Nishimura | Active tuned mass damper[END_REF][START_REF] Preumont | Vibration Control of Active Structures. An Introduction[END_REF]. In this paper we have used the tuning methodology proposed by N. D. Sims in [START_REF] Sims | Vibration absorbers for chatter suppression: A new Analytical tuning methodology[END_REF]. Passive absorbers are typically tuned to reduce the magnitude of the frequency response function near a problematic mode. However, Sims proposed an alternative tuning methodology focused on decreasing the magnitude of the real part of it. This fact is really useful in machining operations, because it is well known that the chatter stability margin is given by the real part of the frequency response of the system. In [START_REF] Sims | Vibration absorbers for chatter suppression: A new Analytical tuning methodology[END_REF] the tuning method is presented as a new solution, which is easier to apply than other numerical and graphical approaches. The main novelty of this paper is to use these tuning equations and integrate them with the VPA to build an active damper for chatter suppression and provide an alternative control algorithm for an inertial actuator that leads to a larger stability range.

Another advantage of this control law is that an optimal tuning does not excite the structural modes of the actuator and guarantees the closed-loop stability without further analysis in the case of an structure with a unique mode. Structures with more than one mode require a more detailed study and probably a more complex control law. Some authors propose the use of a combination of different VPA controllers to manage this situation, where each of this controllers is tuned to avoid a different mode of the system.

We have tested both control laws mounting the actuator on different structures and found that the VPA control provides a larger chatter stability than the DVF control. Moreover, an experimental tuning was always required with the DVF control, while the parameters of the VPA controller were calculated directly from a modal analysis and the tuning equations described in [START_REF] Sims | Vibration absorbers for chatter suppression: A new Analytical tuning methodology[END_REF], which results to be faster. In this paper a comparison between both controls laws is presented emphasizing the advantages and disadvantages of each one of them. This paper is organized as follows. First, the inertial actuator is described and a model of it is developed. The different control laws are then explained. In the next section the experimental results are presented. In this section a couple of milling test are performed using the VPA control. Finally, conclusions end the paper.

Inertial actuator

An inertial actuator can be described as a reaction mass m a supported on a spring k a and a damper c a attached to a base (Fig. 1.a). According to an applied voltage V in the reaction mass is excited and it induces a force F a on the supporting base [START_REF] Preumont | Vibration Control of Active Structures. An Introduction[END_REF]. The dynamics of an inertial actuator can be modeled as the following transfer function

F a  s V in  s = G • m a s 2 m a s 2 c a sk a =g a s 2 s 2 2  a  a s a 2 (1)
where ω a is the natural frequency, ζ a the damping ratio and g a is the gain of the actuator. The actuator behaves as an ideal lineal force generator beyond a determined frequency ω p (Fig. 1.b). Another upper limitation in the bandwidth is included by the electromagnetic circuit. This means that the actuator can only be used as a force generator in this linear range. The task is to design an appropriate control law to the actuator in order to control structure vibrations. In this paper the actuator used to perform the practical applications is a model of Micromega Dynamics company [18]. This actuator is capable of applying an up to 900 N force on the host structure. The actuator is mounted on a Kistler dynamometer plate and excited by a chirp voltage signal with the aim of calculating its dynamics. Fig. 2 shows the FRF (Frequency Response Function) between the measured force and the applied Voltage. In Fig. 2 we can see that the actuator possesses an oscillation mode at low frequencies (around 8 Hz). This fact limits not only the bandwidth but also should be taken into account for stability consideration. This will be explained in detail in next section. The upper limitation of the linear range is found to be around 200 Hz. The actuator is modeled as in equation (1) by the following transfer function

F a  s V in  s = 65 s 2 s 2 16.76s2280 N V (2)
The identification is performed using a parameter estimator based on a least squares algorithm [START_REF] Ganguli | Active damping of in machine -demonstration with a hardware-in-the-loop simulator[END_REF].

Control laws

In this section the two different control laws considered in this paper will be explained in detail. First, the typical Direct Velocity Feedback control law is explained. Nowadays, most of the inertial actuators used for vibration control include this control law. This is due to its simplicity and good results. However, this type of controllers has some drawbacks which should be considered to guarantee the closed stability and sometimes they could limit the performance of the controller. The use of a Virtual Passive Absorber controller is proposed to avoid some of them. VPA control law is explained in the second part of this section. Finally, the advantages and disadvantages of both control laws are compared.

Direct Velocity Feedback

The main idea of this control law consists in a negative feedback of the velocity of the structure. The transfer function of the controller can be written as

( ) ( ) ( ) c v v V s g X s g s X s = - = -⋅ ⋅ & (3)
where ( ) c V s is the applied control input to the inertial actuator, s X  s is the velocity on the structure and

v g R + ∈
is the control gain. Considering that the actuator is working in the linear range, then the transfer function between the applied force on the structure and the control voltage input can be written as

F a  s= g a •V c  s=-g a • g v • s • X  s (4)
If the structure is modeled as a linear time invariant SISO system, the characteristic equation can be calculated as follows

1g v • g a • s •G  s=0 (5)
where G s  is the transfer function describing the structure to be controlled. Now if we consider a structure with a unique mode, equation ( 5) can be written as

1g v • g a • s • g s 2 2 n  n s n 2 =0 s 2 s  g v • g a • g 2  n  n  n 2 =0 (6)
The damping can be increased in equation ( 6) increasing the value of the feedback gain g v . The effect of the inertial actuator can be studied including its transfer function in previous characteristic equation

1g v • s • g a s 2 s 2 2 a  a s a 2 G  s=0 (7)
In this case the low frequencies dynamics of the actuator should be considered to guarantee closed-loop stability. In Fig. 3 a root locus analysis is performed for a unique mode structure including the actuator dynamics. It shows that the poles of the structure are damped increasing the feedback gain. However, the poles of the actuator become unstable for large values of g v . This means that for sufficiently large values of g v the close loop is unstable. The largest value of this gain that keeps the system stable could be calculated if we had a linear model of the structure. However, this is not always possible and the optimal value of the feedback gain g v is usually calculated experimentally. Initially it is chosen to be small and it is increased until the closed-loop system becomes unstable.

Virtual Passive Absorber

The second control law is designed to make the actuator behave as a typical passive vibration absorber. A passive absorber is usually used to attenuate any of the modes of a structure and it is tuned to work in that range. The state space equations of the controller can be written in the following way [START_REF] Huyanan | Vibration control strategies for proof-mass actuators[END_REF] 2

1 2 0 1 0 2 1 c c c c c c c c c c a c c c c x x y x x x u y M g x ω ζ ω µ ω ζ ω -          = ⋅ + ⋅          - -                = = - - ⋅         & && & & (8)
where y x = && is the acceleration on the structure,

c m M µ =
is the mass ratio between the controller mass m c and the system mass M. c ω and c ζ are the natural frequency and the damping ratio of the controller, respectively. In this case the measured acceleration is used as an input to the feedback controller. Then the controller output feeds the actuator. From (8) the transfer function of the VPA controller can be calculated as

( ) ( ) 2 2 2 2 ( ) 2 c c c c c a c c c M s G s g s s µ ζ ω ω ζ ω ω + = + + (9)
The characteristic equation of the closed-loop system for a linear time-invariant SISO system including the dynamics of the actuator can be calculated as

( ) ( ) ( ) 2 2 2 2 2 2 2 2 1 ( ) 0 2 2 c c c c a a a a a c c c M s s g s G s s s g s s µ ζ ω ω ζ ω ω ζ ω ω + + ⋅ ⋅ = + + + + (10)
The optimal values of c ω y c ζ can be directly calculated from passive absorbers optimization methods. These methods just require a model analysis of the host structure. If these parameters are not appropriately tuned a resulting passive absorber may still be stable, but the closed loop behavior may not be good enough. On the other hand, an inertial actuator with this kind of control law can be unstable if the parameters of the controller are not appropriately tuned due to the low frequency dynamics of the actuator. The most used techniques for absorber tuning can be found in [START_REF] Chung | Active damping of structural modes in high speed machine tools tools[END_REF][START_REF] Phan | Identification and Control of Mechanical Systems[END_REF][START_REF] Pratt | Chatter control and stability of cantilever boring bar under regenerative cutting conditions[END_REF]. In most of them the parameters of the absorber are chosen such that the magnitude of the frequency response is reduced around the problematic mode. The aim of this paper is to design a control law to reduce the chatter in a milling process. It is well known that the stability range is given by the real part of the FRF instead of the magnitude. Using a typical turning model for the chatter process, the stability limit can be calculated using

Nyquist Criterion [1] ( ) lim ( ) 1 1 j T s K b uG j e ω ω - - = - (11)
where G(s) is the tool transfer function between the cutting force and the displacement on the surface. Any value of the depth cut b > b lim makes the system unstable. The stability condition can be written as

[ ] ( ) lim 1 2 Re ( ) s c b K uG jω = - (12)
where c ω is the chatter frequency. According to equation [START_REF] Nishimura | Active tuned mass damper[END_REF] the stability is given by the real part of

G(ω). Since lim b R + ∈
only the frequency range that makes Re(uG(jω)) positive should be taken into account. u is used to denote the orientation coefficient and it is positive in an upmilling cutting process and negative in a downmilling process. This means that for a downmilling process the negative part of the FRF is considered to calculate the stability condition while for a upmilling process the positive real part of it is considered. Figure 4 shows a graphical representation of the relation between the real part and the resulting stability lobe for a downmilling process. From equation ( 12) it is clear that reducing the reducing the positive real part in an upmilling process or the negative part in a downmilling the chatter stability is increased. In this point one could think that the effort of the controller could be focused on this fact instead of reducing the magnitude. This kind of tuning for passive absorbers has been been considered by many authors before, but in [START_REF] Sims | Vibration absorbers for chatter suppression: A new Analytical tuning methodology[END_REF] Sims presents a new analytical solution for this problem. In this paper we use those results to tune the parameters of the VPA controller. The effect of the controller is that two equal peaks or troughs appear on the real part of the FRF around the tuned mode. The equations for the optimal parameters of the controller defined in ( 8) are obtained from the following equations ( )

2 2 2 2 2 2 2 1 c n n f µ µ µ ω ω µ + + +   = =     + (13)
( )

2 2 2 2 2 2 1 c p n f µ µ µ ω ω µ + - +   = =     + (14)
( )

3 8 1 µ ζ µ = + (15)
where the subscript n denotes a downmilling milling process, while the subscript p is used for an upmilling one and ω n is the structural frequency to be damped. In case there is more than one problematic mode, a possible solution is to use a set of different VPA controllers in parallel. Each of these controllers is tuned to attenuate a different mode of the structure. The resulting controller can be calculated as

( ) ( ) ( ( ) ( ) ( ) ( )2 2 ( ) ( ) ( )2 2 ( ) 2 i i i i i N c c c c c i i i i i a c c c M s G s g s s µ ζ ω ω ζ ω ω = + = + + ∑ ( 16
)
where N is the number of mode to attenuate. In this point we should remark that the tuning process is not as easy as in an unique mode case. A VPA controller excites the structural modes at lower frequencies. For this reason the tuning requires an experimental tuning, beginning with the mode of larger frequency which is not going to be affected for any other controller and continuing until the lower one is tuned. The experimental tuning is started from the theoretical values in equations ( 13)-( 15) and then they are slightly changed until two peaks or trough are observed in the real part of the FRF.

A comparison between both control laws

In this section the control laws are compared remarking the main advantages and disadvantages of both of them.

The main advantage of DVF control is its simplicity, since only a parameter has to be tuned. Despite this it leads to very good damping results. This fact makes this control law the most used one among researchers. Moreover, if there is not any kind of information about the system to be damped the experimental tuning is easier than in the VPA control, where a modal analysis is always required. On the other hand, with DVF finding theoretically the optimal value of the feedback gain is more difficult if a linear model of the system is not available. The VPA control just requires a modal analysis of the structure, which is easier to perform that finding a linear model. When a DVF is used a high-pass filter should be added in the control loop in order to minimize the effects of low frequency dynamics of the actuator. In addition, the closedloop can easily become unstable for sufficiently large values of the feedback gain. This can limit the performance of the controller in some cases.

The VPA control is designed to work in a particular frequency range. This makes the control less likely to affect the dynamics of the actuator and the high-pass filter is not needed in the control loop. In the particular case of chatter suppression the VPA control is focused on reducing the real part of the FRF, while the DVF consumes significant energy trying to reduce the whole frequency range including regions with no contribution to chatter. However, the VPA control has some disadvantages that should be taken into account. The parameters should be appropriately chosen in order to achieve the desired performance. Moreover, if the dynamics of the system change during the process, then the controller could no longer be the appropriate one and an adaptive law should be implemented [START_REF] Wu | Adaptive control using a vibration absorber controller[END_REF].

Experimental results

In this section some experimental results are presented. Two different structures are considered and both control laws are tested. The first structure is a unique mode workpiece fixed to the ground. In the second part of our tests the actuator is mounted on the ram of a milling machine. Both control laws are again tested for different ram outputs. Finally some milling processes are performed with the VPA control to show the usefulness of this control law.

Workpiece

First the DVF control law is tested on the workpiece. The structure is excited with an impact hammer and an accelerometer is attached on the surface of the structure to measure the acceleration. Fig 5 shows the magnitude of the FRF for different values of the feedback gain. The real part is shown in Fig. 6. As expected the vibration is reduced increasing g v . However, values larger than 400 lead to unstable results. Subsequently the VPA control law is tested on the workpiece. In this case is not very important to consider the upmilling or the downmilling case since we are not dealing with a milling process. However, the downmilling tuning is chosen for comparison. Fig. 7 displays the magnitude of the obtained FRF for different values of gain μ. The effect of the controller can be clearly seen in Fig. 8 where the real part is plotted. In this Figure we can see the appearance of two troughs around negative real part of the FRF. The optimal tuning is the one that makes these two troughs equal. Both Figures show that a larger damping is obtained increasing the value of μ. One could think to use very large values of this gain to obtain a better result. However, there are a few limitations for this. First, increasing this value the low frequency gain of the controller is increased as well. On the hand, the voltage input to the actuator can not take larger values )

c o n t r o l o f f g v = 1 0 0 g v = 2 0 0 g v = 4 0 0
than a determined value. This means that for sufficiently large values of μ the control signal can be saturated and then the control law could not be efficient enough. Moreover, increasing this gain the frequency range with negative real part is increased as well, while the positive peak is moved to a lower frequency (see Fig. 8). This is not be very important while the minimum in the negative real part is augmented, but for large values of μ the positive peak could reach the low frequencies where there are the structural modes of the actuator and make the whole process unstable. In practical situations, we should consider the magnitude of the oscillations on the structure to guarantee that the control signal remains inside the admissible voltage amplitude range for the actuator. We should check if the structural mode of the structure is near the modes of the actuator as well. If that happens then we should use small values of μ not exciting the dynamics of the actuator. Finally, both controllers are compared for their optimal tuning. Fig. 9 shows that using a DVF controller a larger reduction of the magnitude of the FRF in the whole range of frequencies is obtained, while the VPA results to be better increasing the minimum of the negative part of the FRF near the problematic mode of the structure. For this reason, the VPA seems to be more efficient for chatter considerations, where the real part of the FRF is used to determine the chatter stability.

Ram of a milling machine

Now the actuator is mounted on the ram of a milling machine. The dynamics of the ram change according to the operation point. For that reason the parameters of the VPA controller should be calculated for each operating point. The experiments are performed with the machine switched off to avoid further vibrations.

Fig. 11 shows the magnitude of the FRF for both control laws when the ram output is 1000mm. The DVF control has been used with the optimal feedback gain obtained from an experimental study. The VPA control has been tuned to avoid the main structural mode at 42 Hz. The real part of the FRF is plotted in 3 0 4 0 5 0 6 0 7 0 8 0 9 0 1 0 0 1 1 0 1 2 0 1 3 0 1 4 0 0 . 5 Looking in detail those two figures we can observe some of the advantages and disadvantages of control laws commented in section 3. The DVF control law attenuates the whole frequency range, but it excites the structural mode of the actuator. We can see that there is a small peak at low frequencies. Remember that in the identification performed to the actuator in section 2 the structural mode was found around 8 Hz. On the other hand, the VPA control has no effect on it. The drawback of the VPA control is that the response of secondary structural modes at lower frequencies are excited. We should look if the influence of these modes is relevant for chatter stability. Since we are tuning the controller for a downmilling process we just look at the negative real part and in this case stability is not lost due to these secondary modes. Another important conclusion is that the parameters of the VPA control have been calculated directly from the modal analysis using equations ( 14)-( 15) without further experimental tuning while the feedback gain of the DVF has to be calculated from an experimental tuning. Since a modal analysis is faster to perform that a manual tuning of a feedback gain, where several test should be performed until the optimal value is found, we can conclude that VPA control results to be more straightforward and easier to implement in this case. Other two tests are performed for different ram outputs. Fig. 13-16 show the FRFs for both cases. In these cases we can observe similar results. The DVF control excites the mode of the actuator, while the VPA control excites secondary modes. In both cases the VPA control results to be the best option to increase the chatter stability.

Milling Tests

Finally some milling tests are performed for VPA control. Tests have been performed for a 120 mm tool of 8 teeth with a radial immersion of 80 mm, a depth cut of 4.2 mm, 500 rpm and downmilling conditions. The material of the workpiece is steel F1140. In the first experiment the ram is chosen to operate in a region where the chatter is not very severe. Figure 17 shows the measured acceleration on the ram through time. The control signal to the actuator is plotted in Figure 18. In Figure 17 the improvement is not apparent, so a frequency analysis is performed and displayed in Figure 19. In this case the chatter frequency is 44.39 Hz and we can see that it is completely removed by the actuator when the control signal is applied. The tooth pass frequency is the one located at 66.7 Hz. Finally, another test is performed moving the ram to a another position where stiffness is reduced and stronger chatter is obtained. In this case the time domain signal is enough just to see the improvement with the VPA control law (Fig. 20). The frequency analysis of this signal shows that the chatter peak does not appear again (Fig. 22) when the control is applied (Fig. 21).

Conclusions

In this paper an active damper using an inertial actuator for chatter suppression is presented. Two different control laws are considered and compared. First the typical DVF control is explained. This control laws is widely used for active damping due to its simplicity. Different authors have proposed different type of which could lead to better results. We propose the VPA control using a tuning method focused in the real part of the FRF of the structure to be damped. This fact is found to be considerably useful to increase chatter stability. The VPA control law overcome some of the main drawbacks of the typical DVF control. The parameters of the VPA control can be directly calculated from a direct model analysis of the structure, while the DVF requires a manual tuning to guarantee the stability. In addition, the VPA control focuses its effect on the problematic mode and is less likely to excite the structural modes of the actuator, main drawback of the DVF control. Some practical tests have been performed showing that a theoretically tuned VPA control improves performance obtained with the DVF control. However, the VPA can not be directly implemented in some cases. When the dynamics of the structure change during the process then an unique VPA controller could not be valid and an adaptive law should be implemented. Moreover, if there are more than one mode to be damped then a more complex controller should be implement. One possible solution to be studied is a combination of different VPA controllers.

[1] Altintas Y., Manufacturing automation: Metal cutting mechanics, machine tool vibrations and CNC design, Cambridge university Press (2000).

Fig. 1

 1 Fig.1.a: Inertial actuator

Fig. 2 :

 2 Fig. 2: Experimental and modeled FRF of the inertial actuator

  e r i m e n t M o d e l

Fig. 3 : 6 R e a l a x i s I m a g i n a r y a x i s s t r u c t u r e a c t u a t o r

 36 Fig.3: Root locus analysis including the dynamics of the actuator

Fig. 4 :

 4 Fig.4: Relation between the real part and the stability lobe in a downmilling milling process.

Fig. 5 : 6 :

 56 Fig. 5: Magnitude of the FRF of the workpiece using the DVF Fig. 6: Real part of the FRF of the workpiece using the DVF

7 F 5 F

 75 r e q u e n c y ( H z ) R e s p o n s e M a g n i t u d e ( m • Nr e q u e n c y ( H z ) R e s p o n s e R e ( m • N -1

Fig. 7 : 8 :Fig. 9 : 10 :

 78910 Fig. 7: Magnitude of the FRF of the workpiece using the VPA control Fig. 8: Real part of the FRF of the workpiece using the VPA control

7 F 7 F 7 F 5 Fig. 12 .

 777512 Fig.[START_REF] Pratt | Chatter control and stability of cantilever boring bar under regenerative cutting conditions[END_REF]. In both Figures it is clear that the VPA achieves a better performance near the tuned mode. Looking in detail those two figures we can observe some of the advantages and disadvantages of control laws commented in section 3. The DVF control law attenuates the whole frequency range, but it excites the structural mode of the actuator. We can see that there is a small peak at low frequencies. Remember that in the identification performed to the actuator in section 2 the structural mode was found around 8 Hz. On the other hand, the VPA control has no effect on it. The drawback of the VPA control is that the response of secondary structural modes at lower frequencies are excited. We should look if the influence of these modes is relevant for chatter stability. Since we are tuning the controller for a downmilling process we just look at the negative real part and in this case stability is not lost due to these secondary modes. Another important conclusion is that the parameters of the VPA control have been calculated directly from the modal analysis using equations (14)-(15) without further experimental tuning while the feedback gain of the DVF has to be calculated from an experimental tuning. Since a modal analysis is faster to perform that a manual tuning of a feedback gain, where several test should be performed until the optimal value is found, we can conclude that VPA control results to be more straightforward and easier to implement in this case.

Fig. 11 : 12 :

 1112 Fig. 11: Magnitude of the FRF for a 1000mm ram output Fig. 12: Real part of the FRF for a 1000mm ram output

Fig. 13 : 14 : 8 F) 8 F 8 FFig. 15 :Fig. 16 :

 13148881516 Fig. 13: Magnitude of the FRF for 800 mm ram output Fig. 14: Real part of the FRF for 800 mm ram output

Fig. 17 : 8 F 2 ) c o n t r o l o f f c o n t r o l oFig. 19 :Fig. 20 : 2 Fig. 21 :

 17821920221 Fig.17: Acceleration measured in milling process 1 Fig.18: Control law in milling process 1

3 F) c o n t r o l o f f c o n t r o l o n c h a t t e r f r e q u e n c y 4 F

 34 r e q u e n c y ( H z ) V e l o c i t y ( m • s -1 r e q u e n c y ( H z ) V e l o c i t y ( m • s -1 ) c o n t r o l o f f c o n t r o l o n c h a t t e r f r e q u e n c y 4 t r o l l a w ( V )