Silvio Silvio Ghilardi
email: silvio.ghilardi@unimi.it

It Ghilardi

Luigi Santocanale
email: luigi.santocanale@lis-lab.fr.

Free Heyting Algebra Endomorphisms: Ruitenburg's Theorem and Beyond

Keywords: Heyting algebra, Ruitenburg's Theorem, Sheaf Duality, Bounded Bisimulations, Free algebra endomorphisms

come

Introduction

Unification theory investigates the behavior of substitutions from a syntactic point of view: substitutions are in fact key ingredients in various algorithms commonly used in computational logic. Taking an algebraic point of view, substitutions can be seen as finitely generated free algebra homomorphisms: in fact, such a homomorphism µ : F(x 1 , . . . , x n ) -→ F(y 1 , . . . , y m ) is uniquely determined by an n-tuple of terms t 1 (y 1 , . . . , y m ), . . . , t n (y 1 , . . . , y m ) and acts by associating with any term u(x 1 , . . . , x n ) the term u(t 1 /x 1 , . . . , t n /x n ) obtained by substitution. If free algebras are intended not as 'absolutely free algebras', but as 'free algebras in an equational class E', the same correspondence between homomorphisms and substitutions works, provided terms are intended as equivalence classes of terms modulo E and substitutions themselves are taken 'modulo E'.

The above correspondence between free algebra homomorphisms and substitutions is the starting point for the algebraic approaches to E-unification theory, like for instance [START_REF] Goguen | What is unification? A categorical view of substitution, equation and solution[END_REF][START_REF] Ghilardi | Unification through projectivity[END_REF], where structural information about homomorphisms of finitely generated (and also finitely presented) algebras is widely exploited. In this paper, we want to draw the attention on a surprising behavior that such homomorphisms can have in some algebraic logic contexts. Such behavior is unexpectedly similar to that of functions between finite sets.

To explain what we have in mind, let us recall that an infinite sequence a 1 , a 2 , . . . , a i , . . . ultimately periodic if there are N and k such that for all s 1 , s 2 ≥ N , we have that s 1 ≡ s 2 mod k implies a s 1 = a s 2 . If (N, k) is the smallest (in the lexicographic sense) pair for which this happens, then N and k are, respectively, the index and the period of the ultimately periodic sequence { a i } i . Thus, for instance, an ultimately periodic sequence with index N and period 2 looks as follows a 1 , . . . , a N , a N +1 , a N , a N +1 , . . .

A typical example of an ultimately periodic sequence is the sequence of the iterations { f i } i of an endo-function f of a finite set. Whenever infinitary data are involved, ultimate periodicity comes often as a surprise. Ruitenburg's Theorem is in fact a surprising result stating the following: take a formula A(x, y) of intuitionistic propositional calculus (IP C) (by the notation A(x, y) we mean that the only propositional letters occurring in A are among x, y -with y being, say, the tuple y 1 , . . . , y n ) and consider the sequence { A i (x, y) } i≥1 so defined:

A 1 := A, . . . , A i+1 := A(A i /x, y) (1)
where the slash means substitution; then, taking equivalence classes under provable bi-implication in (IP C), the sequence { [A i (x, y)] } i≥1 is ultimately periodic with period 2. The latter means that there is N such that

⊢ IP C A N +2 ↔ A N . (2)
An interesting consequence of this result is that least (and greatest) fixpoints of monotonic formulae are definable in (IP C) [START_REF] Mardaev | Least fixed points in Grzegorczyk's Logic and in the intuitionistic propositional logic[END_REF][START_REF] Mardaev | Definable fixed points in modal and temporal logics : A survey[END_REF][START_REF] Ghilardi | Fixed-point elimination in the intuitionistic propositional calculus[END_REF]: this is because the sequence (1) becomes increasing when evaluated on ⊥/x (if A is monotonic in x), so that the period is decreased to 1. Thus the index of the sequence becomes a finite upper bound for the fixpoint approximations convergence: in fact we have, ⊢ IP C A N (⊥/x) → A N +1 (⊥/x) and ⊢ IP C A N +1 (⊥/x) → A N +2 (⊥/x) by the monotonicity of A, yielding ⊢ IP C A N (⊥/x) ↔ A N +1 (⊥/x) by (2).

Ruitenburg's Theorem was shown in [START_REF] Ruitenburg | On the period of sequences (a n (p)) in intuitionistic propositional calculus[END_REF] via a, rather involved, purely syntactic proof. The proof has been recently formalized inside the proof assistant coq by T. Litak, see https://git8.cs.fau.de/redmine/projects/ruitenburg1984 .

In this paper we supply a semantic proof, using duality and bounded bisimulation machinery.

Bounded bisimulations are a standard tool in non classical logics [START_REF] Fine | Logics containing K4. II[END_REF] which is used in order to characterize satisfiability of bounded depth formulae and hence definable classes of models: examples of the use of bounded bisimulations include for instance [START_REF] Shavrukov | Subalgebras of diagonalizable algebras of theories containing arithmetic[END_REF][START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF][START_REF] Visser | Uniform interpolation and layered bisimulation[END_REF][START_REF] Ghilardi | Best solving modal equations[END_REF].

Duality has a long tradition in algebraic logic, see e.g. [START_REF] Esakia | Topological Kripke models[END_REF] for the case of Heyting algebras. Indeed, many phenomena look more transparent whenever they are analyzed in the dual categories. This especially happens when dualities can convert coproducts and colimits constructions into more familiar 'honest' products and limits constructions. The duality we use to tackle Ruitenburg's Theorem, firstly described in [START_REF] Ghilardi | Model completions, r-Heyting categories[END_REF], see also [START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF], realizes this conversion. It has a mixed geometric/combinatorial nature. In fact, the geometric environment shows how to find relevant mathematical structures (products, equalizers, images,...) using their standard definitions in sheaves and presheaves; on the other hand, the combinatorial aspects show that such constructions are definable, thus meaningful from the logical side. In this sense, notice that we work with finitely presented algebras, and our combinatorial ingredients (Ehrenfeucht-Fraissé games, etc.) replace the topological ingredients which are common in the algebraic logic literature (working with arbitrary algebras instead). Duality, although not always in an explicitly mentioned form, is also at the heart of the finitarity results for E-unification theory in [START_REF] Ghilardi | Unification in intuitionistic logic[END_REF][START_REF] Ghilardi | Best solving modal equations[END_REF][START_REF] Ghilardi | Unification, finite duality and projectivity in varieties of Heyting algebras[END_REF].

The paper is organized as follows. In Section 2 we show how to formulate Ruitenburg's Theorem in algebraic terms and how to prove it via duality in the easy case of classical logic (where index is always 1). This Section supplies the methodology we shall follow in the whole paper. We introduce in Section 3 the required duality ingredients for finitely presented Heyting algebras, leading to the statement of the duality Theorem. The full proof of this theorem appears in the following Section 4. We show then, in Section 5, how to extend the basic argument of Section 2 to finite Kripke models of intuitionistic logic. This extension does not directly give Ruitenburg's Theorem, because it supplies a bound for the indexes of our sequences which is dependent on the poset a given model is based on. Using the ranks machinery introduced in Section 6, this bound is made uniform in Section 7, thus finally reaching our first goal. Having established Ruitenburg's Theorem, we wonder how general this ultimately periodic behavior is among the finitely generated free Heyting algebra endomorphisms and, in Section 8, we supply a counterexample showing that this behavior fails whenever at least two free generators are moved by the endomorphism. In the final Section 9, we prove that, whenever an endomorphism is ultimately periodic, its period can be bound as a function of the number of the free generators only. This observation is used to provide bounds of periods of free algebra endomorphisms in locally finite varieties of Heyting algebras. We present concluding remarks and some open problems in the last Section.

Most of the material of this paper was presented at the conference AiML 18, see the reference [START_REF] Ghilardi | Ruitenburg's theorem via duality and bounded bisimulations[END_REF]; the content of the last two Sections as well as a strengthening of the duality theorem of [START_REF] Ghilardi | Model completions, r-Heyting categories[END_REF], however, are novel.

The Case of Classical Logic

We explain our methodology in the much easier case of classical logic. In classical propositional calculus (CP C), Ruitenburg's Theorem holds with index 1 and period 2, namely given a formula A(x, y), we prove that

⊢ CP C A 3 ↔ A (3)
holds (here A 3 is defined like in (1)).

2.1. The algebraic reformulation. First, we transform the above statement (3) into an algebraic statement concerning free Boolean algebras. We let F B (z) be the free Boolean algebra over the finite set z. Recall that F B (z) is the Lindenbaum-Tarski algebra of classical propositional calculus restricted to a language having just the z as propositional variables.

Similarly, morphisms µ :

F B (x 1 , . . . , x n ) -→ F B (z) bijectively correspond to n-tuples of equivalence classes of formulae A 1 (z), . . . , A n (z) in F B (z): the map µ corresponding to the tuple A 1 (z), . . . , A n (z) associates with the equivalence class of B(x 1 , . . . , x n ) in F B (x 1 , . . . , x n ) the equivalence class of B(A 1 /x 1 , . . . , A n /x n ) in F B (z).
Composition is substitution, in the sense that if µ : F B (x 1 , . . . , x n ) -→ F B (z) is induced, as above, by A 1 (z), . . . , A n (z) and if ν :

F B (y 1 , . . . , y m ) -→ F B (x 1 , . . . , x n ) is induced by C 1 (x 1 , . . . , x n ), . . . , C m (x 1 , . . . , x n ), then the map µ • ν : F B (y 1 , . . . , y m ) -→ F B (z) is induced by the m-tuple of formulas C 1 (A 1 /x 1 , . . . , A n /x n ), . . . , C m (A 1 /x 1 , . . . , A n /x n ).
How to translate the statement (3) in this setting? Let y be y 1 , . . . , y n ; we can consider the map µ A : F B (x, y 1 , . . . , y n ) -→ F B (x, y 1 , . . . , y n ) induced by the n + 1-tuple of formulae A, y 1 , . . . , y n ; then, taking in mind that in Lindenbaum algebras identity is modulo provable equivalence, the statement (3) is equivalent to

µ 3 A = µ A . (4)
This raises the question: which endomorphisms of F B (x, y) are of the kind µ A for some A(x, y)? The answer is simple: consider the 'inclusion' map ι of F B (y) into F B (x, y) (this is the map induced by the n-tuple y 1 , . . . , y n ): the maps µ : F B (x, y) -→ F B (x, y) that are of the kind µ A are precisely the maps µ such that µ • ι = ι, i.e. those for which the triangle

F B (x, y) F B (x, y) ✲ µ F B (y) ι ✠ ι ❅ ❅ ❅ | commutes.
It is worth making a little step further: since the free algebra functor preserves coproducts, we have that F B (x, y) is the coproduct of F B (y) with F B (x) -the latter being the free algebra on one generator. In general, let us denote by A[x] the coproduct of the Boolean algebra A with the free algebra on one generator (let us call A[x] the algebra of polynomials over A).

Recall that an algebra is finitely presented if it is isomorphic to the quotient of a finitely generated free algebra by a finitely generated congruence. For Boolean algebras, being 'finitely presented' is equivalent to being 'finite'. Yet, we should keep mind in the following Sections that this equivalence fails for Heyting algebras-so the two notions are in general distinct. A slight generalization of statement (4) now reads as follows:

• let A be a finitely presented Boolean algebra and let the map µ :

A[x] -→ A[x] commute with the coproduct injection ι : A -→ A[x] A[x] A[x] ✲ µ A ι ✠ ι ❅ ❅ ❅ |
Then we have

µ 3 = µ . (5)
2.2. Duality. The gain we achieved with statement (5) is that the latter is a purely categorical statement, so that we can re-interpret it in dual categories. In fact, a good duality may turn coproducts into products and make our statement easier -if not trivial at all. Finitely presented Boolean algebras are dual to finite sets; the duality functor maps coproducts into products and the free Boolean algebra on one generator to the two-elements set 2 = { 0, 1 } (which, by chance is also a subobject classifier for finite sets). Thus statement (5) now becomes

• let T be a finite set and let the function f : T ×2 -→ T ×2 commute with the product projection π 0 :

T × 2 -→ T T × 2 T × 2 ✲ f T π 0 ❅ ❅ ❅ | π 0 ✠ Then we have f 3 = f . (6)
In this final form, statement ( 6) is now just a trivial exercise, which is solved as follows. Notice first that f can be decomposed as π 0 , χ S (incidentally, χ S is the characteristic function of some Let us illustrate theses cases by thinking of f as an action of the monoid of natural numbers on the set A × 2, that is, as one-letter deterministic automaton:

S ⊆ T × 2). Now, if f (a, b) = (a, b) we trivially have also f 3 (a, b) = f (a, b); suppose then f (a, b) = (a, b ′ ) = (a, b). If f (a, b ′ ) = (a, b ′ ), then f 3 (a, b) = f (a, b) = (a, b ′ ),
(a, b) (a, b) (a, b ′ ) (a, b) (a, b ′ )
On each connected component of the automaton, the pair index/period is among (0, 1), (0, 2), [START_REF] Alberucci | The modal µ-calculus hierarchy over restricted classes of transition systems[END_REF][START_REF] Alberucci | The modal µ-calculus hierarchy over restricted classes of transition systems[END_REF]. We can compute the global index/period of f by means of a max /lcm formula: (1, 2) = (max{ 0, 0, 1 }, lcm{ 1, 2 }).

Duality for Heyting Algebras

In this Section we supply definitions, notation and statements from [START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF] concerning duality for finitely-presented Heyting algebras.

A partially ordered set (poset, for short) is a set endowed with a reflexive, transitive, antisymmetric relation (to be always denoted with ≤). A poset P is rooted if it has a greatest element, that we shall denote by ρ(P ). If a finite poset L is fixed, we call an L-evaluation or simply an evaluation a pair P, u , where P is a rooted finite poset and u : P -→ L is an order-preserving map.

Evaluations restrictions are introduced as follows. If P, u is an Levaluation and if p ∈ P , then we shall denote by u p the L-evaluation ↓ p, u • i , where ↓ p = { p ′ ∈ P | p ′ ≤ p } and i : ↓ p ⊆ P is the inclusion map; briefly, u p is the restriction of u to the downset generated by p.

Evaluations have a strict relationship with finite Kripke models: we show in detail the connection. If L, ≤ is P(x), ⊇ (where x = x 1 , . . . , x n is a finite list of propositional letters), then an L-evaluation u : P -→ L is called a Kripke model for the propositional intuitionistic language built up from x. 1 Given such a Kripke model u and an IPC formula A(x), the forcing relation u |= A is inductively defined as follows:

u |= x i iff x i ∈ u(ρ(P )) u |= ⊥ u |= A 1 ∧ A 2 iff (u |= A 1 and u |= A 2 ) u |= A 1 ∨ A 2 iff (u |= A 1 or u |= A 2 ) u |= A 1 → A 2 iff ∀q ≤ ρ(P ) (u q |= A 1 ⇒ u q |= A 2 ) .
We define for every n ∈ ω and for every pair of L-evaluations u and v, the notions of being n-equivalent (written u ∼ n v). We also define, for two L-evaluations u, v, the notions of being infinitely equivalent (written u ∼ ∞ v).

Let u : P -→ L and v : Q -→ L be two L-evaluations. The game we are interested in has two players, Player 1 and Player 2. Player 1 can choose either a point in P or a point in Q and Player 2 must answer by choosing a point in the other poset; the only rule of the game is that, if p ∈ P, q ∈ Q is the last move played so far, then in the successive move the two players can only choose points p ′ , q ′ such that p ′ ≤ p and q ′ ≤ q. If p 1 , q 1 , . . . , p i , q i , . . . are the points chosen in the game, Player 2 wins iff for every i = 1, 2, . . . , we have that u(p i ) = v(q i ). We say that -u ∼ ∞ v iff Player 2 has a winning strategy in the above game with infinitely many moves; -u ∼ n v (for n > 0) iff Player 2 has a winning strategy in the above game with n moves, i.e. he has a winning strategy provided we stipulate that the game terminates after n moves; -u ∼ 0 v iff u(ρ(P )) = v(ρ(Q)) (recall that ρ(P ), ρ(Q) denote the roots of P, Q). Notice that u ∼ n v always implies u ∼ 0 v, by the fact that L-evaluations are order-preserving. We shall use the notation [v] n for the equivalence class of an L-valuation v via the equivalence relation ∼ n .

The following Proposition provides an elementary recursive characterization of the relations ∼ n , n ≥ 1. Keeping the above definition for ∼ 0 as base case for recursion, the Proposition supplies an alternative recursive definition for these relations. Proposition 1. Given two L-evaluations u : P -→ L, v : Q -→ L, and n > 0, we have that u ∼ n+1 v iff ∀p ∈ P ∃q ∈ Q (u p ∼ n v q ) and vice versa.

When L = P(x 1 , . . . , x n ), so L-evaluations are just ordinary finite Kripke models over the language built up from the propositional variables x 1 , . . . , x n , the relations ∼ n are related to the implicational degree of formulas. For an IPC formula A(x), its implicational degree d(A) is defined as follows:

(i):

d(⊥) = d(x i ) = 0, for x i ∈ x; (ii): d(A 1 * A 2 ) = max[d(A 1 ), d(A 2 )], for * = ∧, ∨; (iii): d(A 1 → A 2 ) = max[d(A 1 ), d(A 2 )] + 1. One can prove [23] that: (1) u ∼ ∞ v holds precisely when (u |= A ⇔ v |= A)
holds for all formulae A(x); (2) for all n, u ∼ n v holds precisely when (u |= A ⇔ v |= A) holds for all formulae A(x) with d(A) ≤ n. That is, two evaluations are ∼ ∞ -equivalent iff they force the same formulas and they are ∼ n -equivalent iff they force the same formulas up to implicational degree n. Let us remark that, for (1) to be true, it is essential that our evaluations are defined over finite posets.

The above discussion motivates a sort of identification of formulae with sets of evaluations closed under restrictions and under ∼ n for some n. Thus, bounded bisimulations (this is the way the relations ∼ n are sometimes called) supply the combinatorial ingredients for our duality; for the picture to be complete, however, we also need a geometric environment, which we introduce using presheaves.

A map among posets is said to be open iff it is open in the topological sense (posets can be viewed as topological spaces whose open subsets are the downward closed subsets); thus f : Q -→ P is open iff it is order-preserving and moreover satisfies the following condition for all q ∈ Q, p

∈ P p ≤ f (q) ⇒ ∃q ′ ∈ Q (q ′ ≤ q & f (q ′ ) = p) .
Let us recall that open surjective maps are called p-morphisms in the standard non classical logics terminology.

Let P 0 be the category of finite rooted posets and open maps between them; a presheaf over P 0 is a contravariant functor from P 0 to the category of sets and function, that is, a functor H : P op 0 -→ Set. Let us recall what this means: a functor H : P op 0 -→ Set associates to each finite rooted poset P a set H(P ); if f : Q -→ P is an open map, then we are also given a function H(f ) :

H(P ) -→ H(Q); moreover, identities are sent to identities, while composition is reversed, H(g • f ) = H(f ) • H(g).
Our presheaves form a category whose objects are presheaves over P 0 and whose maps are natural transformations; recall that a natural transformation ψ : H -→ H ′ is a collections of maps ψ P : H(P ) -→ H ′ (P ) (indexed by the objects of P 0 ) such that for every map f : Q -→ P in P 0 , we have

H ′ (f ) • ψ P = ψ Q • H(f ).
Throughout the paper, we shall usually omit the subscript P when referring to the P -component ψ P of a natural transformation ψ.

The basic example of presheaf we need in the paper is described as follows. Let L be a finite poset and let h L be the contravariant functor so defined:

• for a finite poset P , h L (P ) is the set of all L-evaluations;

• for an open map f :

Q -→ P , h L (f ) takes v : P -→ L to v • f : Q -→ L.
The presheaf h L is actually a sheaf (for the canonical Grothendieck topology over P 0 ); we won't need this fact, 2 but we nevertheless call h L the sheaf of L-evaluations (presheaves of the kind h L , for some L, are called evaluation sheaves).

Notice the following fact: if ψ : h L -→ h L ′ is a natural transformation, v ∈ h L (P ) and p ∈ P , then ψ(v p ) = (ψ(v)) p (this is due to the fact that the inclusion ↓ p ⊆ P is an open map, hence an arrow in P 0 ); thus, we shall feel free to use the (non-ambiguous) notation ψ(v) p to denote ψ(v p ) = (ψ(v)) p . 2 The sheaf structure becomes essential for instance when one has to compute images -images are the categorical counterparts of second order quantifiers, see [START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF].

The notion of bounded bisimulation index (b-index, for short)3 takes together structural and combinatorial aspects. We say that a natural transformation ψ :

h L -→ h L ′ has b-index n if, for every v : P -→ L and v ′ : P ′ -→ L, we have that v ∼ n v ′ implies ψ(v) ∼ 0 ψ(v ′ ).
The following Proposition lists basic facts about b-indexes. In particular, it ensures that natural transformations having a b-index compose.

Proposition 2. Let ψ : h L -→ h L ′ have b-index n;
then it has also b-index m for every m ≥ n. Moreover, for every k ≥ 0, for every v : P -→ L and v ′ :

P ′ -→ L, we have that v ∼ n+k v ′ implies ψ(v) ∼ k ψ(v ′ ).
Proof. Suppose that ψ has b-index n; we prove by induction on k that

∀v, v ′ if v ∼ n+k v ′ then ψ(v) ∼ k ψ(v ′ ) ( * ) k For k = 0, ( * ) k is just the definition of ψ having b-index n. Suppose that ( * ) k holds for some k. Let v, v ′ be such that v ∼ n+k+1 v ′ .
We shall prove that (let P, P ′ be the domains of v, v ′ respectively)

∀p ∈ P ∃p ′ ∈ P ′ ψ(v) p ∼ k ψ(v ′ ) p ′ (the converse statement is similar). Fix p ∈ P . Since v ∼ n+k+1 v ′ , there is p ′ ∈ P ′ such that v p ∼ n+k v ′ p ′ .
Using the inductive assumption and the naturality of ψ, we obtain:

ψ(v) p = ψ(v p ) ∼ k ψ(v ′ p ′ ) = ψ(v ′ ) p ′ as wanted.
We are now ready to state duality theorems. As it is evident from the discussion in Section 2, it is sufficient to state a duality for the category of finitely generated free Heyting algebras; although it would not be difficult to give a duality for finitely presented Heyting algebras, we just state a duality for the intermediate category of Heyting algebras freely generated by a finite bounded distributive lattice (this is quite simple to state and is sufficient for proving Ruitenburg's Theorem).

Theorem 3. The category of Heyting algebras freely generated by a finite bounded distributive lattice is dual to the subcategory of presheaves over P 0 having as objects the evaluations sheaves and as arrows the natural transformations having a b-index.

We present a full proof of the above Theorem in the next section.

It is important to notice that in the subcategory mentioned in the above Theorem, products are computed as in the category of presheaves. This means that they are computed pointwise, like in the category of sets: in other words, we have that (h

L × h L ′ )(P ) = h L (P ) × h L ′ (P ) and (h L × h L ′ )(f ) = h L (f )×h L ′ (f )
, for all P and f . Notice moreover that h L×L ′ (P ) ≃ h L (P ) × h L ′ (P ), so we have h L×L ′ ≃ h L × h L ′ ; in addition, the two product projections have b-index 0. The situation strongly contrasts with other kind of dualities, see [START_REF] Esakia | Topological Kripke models[END_REF] for example, for which products are difficult to compute. The ease by which products are computed might be seen as the principal reason for tackling a proof of Ruitenburg's Theorem by means of sheaf duality.

As a final information, we need to identify the dual of the free Heyting algebra on one generator: Proposition 4. The dual of the free Heyting algebra on one generator is h 2 , where 2 is the two-element poset { 0, 1 } with 1 ≤ 0. Indeed, we shall see in the next Section that h 2 is dual to the Heyting algebra freely generated by the distributive lattice D(2), the lattice of downsets of the chain 2. Since D(2)-which is a three element chain-is the free distributive (bounded) lattice on one generator, a standard argument proves that the Heyting algebra freely generated by the distributive lattice D( 2) is itself free on one generator.

Proof of the Duality Theorem

We present in this Section a proof of Theorem 3. The reader interested in Ruitenburg's Theorem might wish to proceed directly to Section 5. While the material in this Section is adapted from [START_REF] Ghilardi | Model completions, r-Heyting categories[END_REF], Theorem 16, generalizing the duality to some subvarieties of Heyting algebras, is new.

With each L-evaluation u : P -→ L and each n ∈ ω we associate the set T ype n (u) of ∼ n -equivalence classes, T ype n (u) := { [u p ] n | p ∈ P }-where we recall that [u p ] n denotes the ∼ n -equivalence class of u p . An important, although simple, fact is given by the following proposition: Proposition 5. For a finite poset L and n ∈ ω, there are only finitely many equivalence classes of L-evaluations with respect to ∼ n .

Proof. This is evident for n = 0. For n > 0, we argue by induction as follows. By Proposition 1, we have that u ∼ n v iff T ype n-1 (u) = T ype n-1 (v), hence there cannot be more non ∼ n -equivalent L-evaluations than sets of ∼ n-1 equivalence classes.

Let S(h L ) be the set of subpresheaves S of h L satisfying the following condition for some n ≥ 0

∀u : P -→ L, ∀v : Q -→ L (u ∈ S P & u ∼ n v ⇒ v ∈ S Q ) . (7)
When the condition above holds, we say that n is a b-index for S. Notice that the choice of the naming b-index is consistent with the one used in the previous Section. Indeed, for S ⊆ h L , let χ : h L -→ h 2 be defined by χ P (u)(p) = 1 if and only if u p ∈ S ↓p . If n is a b-index for S, then χ is a natural transformation and n is a b-index for χ. Indeed, h 2 is a subobject classifier for subpresheaves that are sheaves for the canonical topology, see p.95 of [START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF].

The definition of S(h L ) can be given in a slightly different way by introducing the relations ≤ n . We put:

(i) v ≤ 0 u iff v(ρ) ≤ u(ρ); (ii) v ≤ n+1 u iff ∀q ∈ Q ∃p ∈ P (v p ∼ n u q ).
Lemma 6. S(h L ) can be equivalently defined as the set of subpresheaves S of h L satisfying the following condition for some n ≥ 0

∀u : P -→ L, ∀v : Q -→ L (u ∈ S P & v ≤ n u ⇒ v ∈ S Q ) . (8)
Proof. Let us call (for the time being) S ′ (h L ) the set of subpresheaves S of h L satisfying condition [START_REF] Frittella | Fixed-point theory in the varieties Dn[END_REF]. Clearly, S ′ (h L ) ⊆ S(h L ). For the converse, take S ∈ S(h L ) having b-index n; in order to show that S ∈ S ′ (h L ), we show that it satisfies [START_REF] Frittella | Fixed-point theory in the varieties Dn[END_REF] for n + 1. Let in fact u, v be such that u ∈ S P and v ≤ n+1 u. Then (considering the root of the domain of v) we know that there is

p ∈ P such that v ∼ n u p ; since S is a subpresheaf of h L , u p ∈ S ↓p and finally v ∈ S Q because n is a b-index for S.
Whenever a subpresheaf S satisfies condition (8) relative to n, we say that S has b ≤ -index n. Notice that, from these definitions, if S has b ≤index n, then it also has b-index n, and if S has b-index n, then it has b ≤ -index n + 1. It can be shown that S has a b-index n iff it has b ≤ -index n: however, we won't use this result, since it depends on a construction (the 'grafting construction', see p.77 of [START_REF] Ghilardi | Model completions, r-Heyting categories[END_REF]) which is not available if we move from the variety of Heyting algebras to one of its subvarieties. Depending on the context, we shall make use or not of the equivalent definition for S(h L ) supplied by Lemma 6.

Let, for every u : P -→ L and n ∈ ω,

(↓ n u) Q := { v : Q -→ L | v ≤ n u } .
The next Lemma is an immediate consequence of Lemma 6.

Lemma 7. ↓ n u is the least subpresheaf of h L having b ≤ -index n such that u ∈ F (P ). A subpresheaf of S of h L has b ≤ -index n if and only if, for each u : P -→ L with u ∈ S P , ↓ n u ⊆ S.
In particular ↓ n u ∈ S(h L ), for each u : P -→ L. Notice that the map

[u] n → ↓ n u ,
is well defined (actually, it is also injective) and so, by Proposition 5 and for fixed n ∈ ω, there exists only a finite number of presheaves of the form

↓ n u. Since S = u∈S P ↓ n u , when S ∈ S(h L ) has b ≤ -index n, it follows that: Lemma 8. Every S ∈ S(h L ) of b ≤ -index n is a finite union of elements of the form ↓ n u.
Recall that Sub(h L ) denotes the Heyting algebra of subpresheaves of h L .

Proposition 9. S(h L ) is a sub-Heyting algebra of Sub(h L ).

Proof. It is easily seen that if S and T have b-index n, then both S ∩ T and S ∪ T have b-index n. Next, consider the standard characterization of implication in subpresheaves:

(S → T ) P = { u ∈ (h L ) P | ∀h : Q -→ P (u • h ∈ S Q ⇒ u • h ∈ T Q ) } .
Notice that, for any h :

Q -→ P and u ∈ (h L ) P , we have that u • h ∼ ∞ u p , where p is h(ρ(Q)); as a consequence, since every U ∈ S(h L ) has a b-index, we have u • h ∈ U Q iff u p ∈ U ↓p for every U ∈ S(h L ).
Thus, the following is an equivalent description of the implication

(S → T ) P = { u ∈ (h L ) P | ∀p ∈ P (u p ∈ S ↓p ⇒ u p ∈ T ↓p ) } . (9)
From this description it easily follows that if

S, T ∈ Sub(h L ) have b-index n, then S → T has b-index n + 1.
Let D(L) denote the distributive lattice of downward closed subsets of L and recall that D(L) is the Birkhoff dual of the poset L, see [START_REF] Birkhoff | Rings of sets[END_REF][START_REF] Davey | Introduction to lattices and order[END_REF]. Notice that there is a lattice embedding ι L : D(L) -→ S(h L ) associating with a downward closed subset d of L, the subpresheaf

ι L (d) P := { u : P -→ L | u(ρ(P )) ∈ d } .
Thus, for p ∈ P and u ∈ h L (P ), we have

u p ∈ ι L (d) ↓p iff u(p) ∈ d.
We shall prove that S(h L ) is the free Heyting algebra generated by the finite distributive lattice D(L) with ι L as the canonical embedding.

Lemma 10. The image of ι L generates S(h L ) as a Heyting algebra.

Proof. Clearly, the elements of S(h L ) having b ≤ -index 0 are exactly the elements of the image of ι L . Now consider an element having b ≤ -index n + 1; by Lemma 8, it is a finite union of elements of the kind (↓ n+1 u). We can express such elements in terms of elements having b ≤ -index n as follows:

(

↓ n+1 u) = p∈dom(u), v ∼nup ( (↓ n v) → v ≤nw (↓ n w) ) . (10)
Notice that all intersections and unions involved in the above formula are finite. Indeed, we have already observed that there are only finitely many elements of the kind

↓ n w. Moreover, if v 1 ∼ n v 2 , then ↓ n v 1 =↓ n v 2 and also v 1 ≤ n w if and only if v 2 ≤ n w. As a consequence, (↓ n v 1 ) → v 1 ≤nw (↓ n w) equals (↓ n v 2 ) → v 2 ≤nw (↓ n w).
Let us verify equation [START_REF] Ghilardi | Unification in intuitionistic logic[END_REF]. Suppose that z ≤ n+1 u and let v : Q -→ L be arbitrary with the property that v ∼ n u p , for every point p in the domain of u. We show that z ∈ (↓ n v) → {w|v ≤nw} (↓ n w) using [START_REF] Ghilardi | Unification through projectivity[END_REF]. Let q be a point in the domain of z such that z q ≤ n v. From z ≤ n+1 u we conclude that there exists p such that z q ∼ n u p . Consequently, v ≤ n z q , otherwise z q ∼ n v and so v ∼ n u p , contradicting the choice of v. Therefore z q ∈ ↓ n z q ⊆ v ≤nw (↓ n w). Vice versa, suppose that z ≤ n+1 u. It follows that there is a point q in the domain of z such, that for every point p in the domain of u, z q ∼ n u p . We check that z ∈ (↓ n z q ) -→ zq ≤nw ↓ n (w). This is clear as z q ∈ (↓ n z q ) and z q ∈ zq ≤nw (↓ n w).

This proves equation [START_REF] Ghilardi | Unification in intuitionistic logic[END_REF] and ends the proof of the Lemma.

The following statement is an immediate consequence of the finite model property:

Lemma 11. Every finitely presented Heyting algebra embeds into a product of finite Heyting algebras.

Recall that, by Birkhoff duality, monotone maps f : M -→ L between finite posets M, L bijectively (and naturally) correspond to bound-preserving lattice homomorphism f -1 = D(f ) : D(L) -→ D(M ). Therefore, for f : M -→ L, we define a map

ev f : S(h L ) -→ D(M ) by putting, for X ∈ S(h L ), ev f (X) := { p ∈ M | f p ∈ X ↓p } . (11)
Proposition 12. The map ev f is a Heyting algebra morphism and makes the following diagram commute:

D(L) S(h L ) ✲ ι L D(f ) ❅ ❅ ❅ ❅ ❅ | D(M ) ❄ ev f
Consequently, S(h L ), together with ι L as the canonical embedding, is a free Heyting algebra generated by the finite distributive lattice D(L).

Proof. Let us verify first that the above diagram commutes. For each d ∈ D(L),

ev f (i L (d)) = { p ∈ M | f p ∈ i L (d) ↓p } = { p ∈ M | f p (p) ∈ d } = { p ∈ M | f (p) ∈ d } = D(f )(d) .
To see that ev f is a Heyting algebra homomorphism, we have, for example,

ev f (S → T ) = { p ∈ M | f p ∈ (S → T ) ↓p } = { p ∈ M | ∀q ∈↓ p (f pq ∈ S ↓q ⇒ f pq ∈ T ↓q ) } = { p ∈ M | ∀q ≤ p (f q ∈ S ↓q ⇒ f q ∈ T ↓q ) } = ev f (S) → ev f (T ) .
Notice also that, in view of Lemma 10, ev f is the unique Heyting algebra morphism g : S(h L ) -→ D(M ) with the property that g • i L = D(f ). Therefore, we have argued that every bounded lattice morphism g = D(f ) :

D(L) -→ D(M )
, where M is a finite poset, extends uniquely to the Heyting algebra morphism ev f : S(h L ) -→ D(M ). By a standard argument, the same universal property holds with respect to the bound-preserving lattice homomorphisms g : D(L) -→ H, where now H is a sub-Heyting algebra of a product of finite Heyting algebras of the form D(M ). In particular, using Lemma 11, we can take (H, g) to be (F, η), the free Heyting algebra algebra generated by the distributive lattice D(M ). Then, by combining the universal properties of (ι L , S(h L )) and of (F, η), it follows that S(h L ) and F are isomorphic.

Let HD be the category of Heyting algebras freely generated by a finite distributive lattice and let M H be the subcategory of presheaves over P 0 having as objects the evaluations sheaves and as arrows the natural transformations having a b-index. We want to show that HD is dual to M H .

We define the following functor T H :

M H HD op h L S(h L ) h M S(h M ) T H f f -1 =T H (f )
where S(h N ) is as in Lemma 10 and f -1 is the inverse image function.

Lemma 13.

(i): T H is a well defined functor. (ii): T H is essentially surjective.

Proof. By Proposition 12, S(h L ) is a Heyting algebra freely generated by a finite distributive lattice and every such Heyting algebra is isomorphic to one of that form. Hence T H is well defined on objects and essentially surjective. Clearly T H preserves compositions and identities. We need to show that for any subpresheaf D of h M with a b-index, f -1 (D) has a b-index and that f -1 is a Heyting algebra morphism. The latter follows from the fact that f -1 : Sub(h M ) -→ Sub(h L ) is a Heyting algebra morphism and that S(h L ), S(h M ) are sub-Heyting algebras of the Heyting algebras of subpresheaves Sub(h L ), Sub(h M ), respectively.

Let n be a b-index of D and m a b-index of f . We shall show that f

-1 (D) has b-index n + m. Let v ∈ f -1 (D) and v ′ be such that v ∼ n+m v ′ . By Proposition 2, f (v) ∼ n f (v ′ ). Since f (v) ∈ D and D is ∼ n -closed, it follows that f (v ′ ) ∈ D and then v ′ ∈ f -1 (D).
Recall from Proposition 12 that, for u : P -→ L, ev u is the unique Heyting algebra morphism S(h L ) -→ D(P ) such that D(u) = ev u • ι L . Conversely, given a Heyting algebra morphism α : S(h L ) -→ D(P ), we define an L-evaluation α : P -→ L as the dual of the distributive lattice morphism α • ι L . By the definition of α, the diagram

D(L) S(h L ) D(L) ι L D(α) α
commutes and therefore, by the universal property of ev, we deduce the following relation:

ev α = α . (12)
The two maps α → α u → ev u , yield a bijective correspondence between the Heyting algebra morphisms α : S(h L ) -→ D(P ) and the L-evaluations u ∈ h L (P ) which is natural in P . This immediately follows from the chain of natural isomorphisms POS(P, L) ≃ DLATT(D(L), D(P )) ≃ HA(S(h L ), D(P )) ,

where the first natural isomorphism is Birkhoff duality between the category of finite posets and the category of finite distributive lattices, and the second is by freeness of S(h L ), Proposition 12. Let h L , h M be objects of HD, µ : S(h L ) -→ S(h M ) be a morphism of Heyting algebras. For each P ∈ P 0 , we define

µ * P : h M (P ) -→ h L (P )
as follows:

µ * P (u) := ev u • µ , for each u ∈ h M (P ). Note that by the above correspondence, it is immediate that µ * P (u) ∈ h L (P ) and that µ * : h M -→ h L is a natural transformation. Moreover Proposition 14. With the notation as above, we have 12)-that, for any α : S(h L ) -→ D(M ), ev α = α and so, in particular, ev µ * P (u) = ev evu•µ = ev u • µ. Therefore, for X ∈ S(h L ) and u : P -→ M , we have ev µ * P (u) (X) = ev u (µ(X)) and therefore, according to the previous observation, we have µ * P (u) ∈ X iff ev µ * P (u) (X) = P iff ev u (µ(X)) = P iff u ∈ µ(X) P .

(i) µ * P (u) ∈ X P iff u ∈ µ(X) P , for X ∈ S(h L ) and u ∈ h M (P ); (ii) µ * : h M -→ h L is a morphism in M H ; (iii) µ = (µ * ) -1 = T H (µ * ); (iv) f = (f -1 ) * , for any morphism f : h M -→ h L in M H .

Proof. Ad (i). Observe that, for any

v ∈ h M (Q) and Y ∈ S(h L ), ev v (Y ) = Q iff, for all q ∈ Q, v q ∈ Y ↓q , iff v ρ(Q) ∈ Y ↓ρ(Q) iff v ∈ Y Q . Recall now-see equation (
Ad (ii). We need to show that the transformation µ * has a b-index. Let n ∈ ω be the maximum of the b-indexes of sets of µ(X) where X is of the kind ι L (d) for some d ∈ D(L). Notice that there are only finitely many such X's and, moreover, for w, w ′ ∈ h L we have w ∼ 0 w ′ iff w, w ′ belong to the same such X's. For any u ∈ h M (P ) and v ∈ h M (Q) such that u ∼ n v and for X = ι L (d), we have

µ * Q (v) ∈ X Q by (i) v ∈ µ(X) Q u ∈ µ(X) P µ *
P (u) ∈ X P where the horizontal lines above stand for logical equivalences. Thus µ * Q (v) ∼ 0 µ * P (u) and µ * has b-index n. Ad (iii). Using (i), we have, for any X ∈ S(h L ) and v ∈ h M (P ),

v ∈ (µ * P ) -1 (X) µ * P (v) ∈ X v ∈ µ(X) P i.e. µ = (µ * ) -1 .
Ad (iv). Let v ∈ h M (P ), p ∈ P and d ∈ D(L). Then, we have

(f -1 ) * P (v)(p) ∈ d by the definition of ι L , (f -1 ) * ↓p (v p ) ∈ ι L (d) ↓p using (i), v p ∈ (f -1 (ι L (d))) ↓p f ↓p (v p ) ∈ ι L (d) ↓p f P (v)(p) ∈ d
Since P , v, p and d were arbitrary f = (f -1 ) * .

Thus we have :

Theorem 15 (Duality Theorem). The functor T H : M H -→ HD op is an equivalence of categories.

Proof. Lemma 13 shows that T H is a functor which is essentially surjective and by Lemma 14(ii-iv) T H is full and faithful, i.e. T H is an equivalence of categories.

For some applications in Section 9, we shall need a duality theorem for some subvarieties. Call a variety V of Heyting algebras finitely approximable if every finitely generated free V -algebra embeds into a product of finite Valgebras.

We can extend the above duality Theorem to finitely approximable subvarieties as follows. Take one such subvariety V and let P V 0 be the category of finite rooted posets P such that D(P ) ∈ V. Let HD V be the category of V-algebras freely generated by a finite distributive lattice and let M H V be the subcategory of presheaves over P V 0 having as objects the evaluations sheaves and as arrows the natural transformations having a b-index. We have:

Theorem 16 (Duality Theorem for Finitely Approximable Subvarieties). For every finitely approximable variety V of Heyting algebras, HD V is dual to M H V .

Proof. By reading back the proof of Theorem 15, it is immediately realized that Lemma 11 is the only specific fact on Heyting algebras we used. When this Lemma is replaced by the assumption that V is finitely approximable, the same chain of arguments yields a proof of Theorem 16.

Indexes and Periods over Finite Models

Taking into consideration the algebraic reformulation from Section 2 and the information from Section 4, we can prove Ruitenburg's Theorem for (IP C) by showing that all natural transformations from h L × h 2 into itself, commuting over the first projection π 0 and having a b-index, are ultimately periodic with period 2. Spelling this out, this means the following. Fix a finite poset L and a natural transformation ψ :

h L × h 2 -→ h L × h 2 having a b-index such that the diagram h L × h 2 h L × h 2 ✲ ψ h L π 0 ❅ ❅ ❅ | π 0
✠ commutes; we have to find an N such that ψ N +2 = ψ N , according to the dual reformulation of (2). From the commutativity of the above triangle, we can decompose ψ as ψ = π 0 , χ , were both π 0 : h L × h 2 -→ h L and χ : h L × h 2 -→ h 2 have a b-index; we assume that n ≥ 1 is a b-index for both of them. We let such ψ = π 0 , χ and n be fixed for the rest of the paper.

Notice that for (v, u) ∈ h L (P ) × h 2 (P ), we have

ψ k (v, u) = (v, u k )
where we put u 0 := u and u k+1 := χ(v, u k ) .

Since P and L are finite, it is clear that the sequence { ψ k (v, u) | k ≥ 0 } (and obviously also the sequence

{ u k | k ≥ 0 }) must become ultimately periodic.
We show in this section that, for each finite set P and for each (v, u) ∈ h L (P ), the period of the sequence { ψ k (v, u) | k ≥ 0 } has 2 as an upper bound, whereas the index of { ψ k (v, u) | k ≥ 0 } can be bounded by the maximum length of the chains in the finite poset P (in the next section, we shall bound such an index independently on P , thus proving Ruitenburg's Theorem).

Call (v, u) ∈ h L (P ) 2-periodic (or just periodic4 ) iff we have ψ 2 (v, u) = (v, u); a point q ∈ P is similarly said periodic in (v, u) iff (v, u) q is periodic. We shall only say that p is periodic if an evaluation is given and understood from the context. We call a point non-periodic if it is not periodic (w.r.t. a given evaluation).

Lemma 17. Let (v, u) ∈ h L (P ) and p ∈ P be such that all q ∈ P , q < p, are periodic. Then either (v, u) p is periodic or ψ(v, u) p is periodic. Moreover, if (v, u) p is non-periodic and u 0 (p) = u(p) = 1, then u 1 (p) = χ(u, v)(p) = 0.

Proof. We work by induction on the height of p (i.e. on the maximum ≤chain starting with p in P ). If the height of p is 1, then the argument is the same as in the classical logic case (see Section 2).

If the height is greater than one, then we need a simple combinatorial check about the possible cases that might arise. Recalling the above definition (13) of the 2-evaluations u n , the induction hypothesis tells us that there is M big enough so that so for all k ≥ M and q < p, (u k+2 ) q = (u k ) q .

Let ↓ ↓ p = { q ∈ P | q < p }. We shall represent (u k ) p as a pair a k x k , where a k = u k (p) and x k is the restriction of (u k ) p to ↓ ↓ p.

Let us start by considering a first repeat (i, j) of the sequence { a M +k } k≥0 -that is i is the smallest i such that there is j > 0 such that a M +i+j = a M +i and j is the smallest such j. Since the a M +n can only take value 0 or 1, we must have i + j ≤ 2. We show that the sequence { (u M +k ) p } k≥0 has first repeat taken from (0, 1), (0, 2), (1, 1), [START_REF] Alberucci | The modal µ-calculus hierarchy over restricted classes of transition systems[END_REF][START_REF] Birkhoff | Rings of sets[END_REF] .

This shall imply in the first two cases that (v, u) p is periodic or, in the last two cases, that ψ(v, u) p is periodic. To our goal, let x = x M and y = x M +1 (recall that we do now know whether x = y).

Notice that, if j = 2, then i = 0 and a first repeat for { (u k ) p } k≥M , is (0, 2), as in the diagram below

a x b y a x .
Therefore, let us assume j = 1 (so i ∈ { 0, 1 }). Consider firstly i = 0: The last statement of the Lemma is also obvious in view of the fact that if a = b = 1, then x = y = 1, so p is periodic.

Corollary 18. Let N P be the height of P ; then ψ N P (v, u) is periodic for all (v, u) ∈ h L (P ).

Proof. An easy induction on N P , based on the previous Lemma.

Ranks

Ranks (already introduced in [START_REF] Fine | Logics containing K4. II[END_REF]) are a powerful tool that goes hand in hand with bounded bisimulations; in our context the useful notion of rank is given below. Recall that ψ = π 0 , χ and that n ≥ 1 is a b-index for ψ and χ.

Let (v, u) ∈ h L (P ) be given. The type of a periodic point p ∈ P is the pair of equivalence classes

[(v p , u p )] n-1 , [ψ(v p , u p )] n-1 . ( 14
)
The rank of a point p (that we shall denote by rk(p)) is the cardinality of the set of distinct types of the periodic points q ≤ p. Since ∼ n-1 is an equivalence relation with finitely many equivalence classes, the rank cannot exceed a positive number R(L, n) (that can be computed in function of L, n).

Clearly we have rk(p) ≥ rk(q) in case p ≥ q. Notice that an application of ψ does not decrease the rank of a point: this is because the pairs [START_REF] Ghilardi | Ruitenburg's theorem via duality and bounded bisimulations[END_REF] coming from a periodic point just get swapped after applying ψ. A nonperiodic point p ∈ P has minimal rank iff we have rk(p) = rk(q) for all non-periodic q ≤ p. Lemma 19. Let p ∈ P be a non-periodic point of minimal rank in (v, u) ∈ h L (P ); suppose also that (v, u) is constant on the set of all non-periodic points in ↓ p. Then we have ψ m (v, u) q 0 ∼ n ψ m (v, u) q 1 for all m ≥ 0 and for all non-periodic points q 0 , q 1 ≤ p.

Proof. We let Π be the set of periodic points of (v, u) that are in ↓ p and let Π c be (↓ p) \ Π . Let us first observe that for every r ∈ Π c , we have

{ [(v s , u s )] n-1 , [ψ(v s , u s )] n-1 | s ≤ r, s is periodic} = { [(v s , u s )] n-1 , s , u s )] n-1 | s ≤ p, s is periodic}
(indeed the inclusion ⊆ is because r ≤ p and the inclusion ⊇ is by the minimality of the rank of p). Saying this in words, we have that "for every periodic s ≤ p there is a periodic

s ′ ≤ r such that (v s , u s ) ∼ n-1 (v s ′ , u s ′ ) and ψ(v s , u s ) ∼ n-1 ψ(v s ′ , u s ′ )"
; also (by the definition of 2-periodicity), "for all m ≥ 0, for every periodic s ≤ p there is a periodic s ′ ≤ r such that ψ m (v s , u s ) ∼ n-1 ψ m (v s ′ , u s ′ )". By letting both q 0 , q 1 playing the role of r, we get: Fact. For every m ≥ 0, for every q 0 , q 1 ∈ Π c , for every periodic s ≤ q 0 there is a periodic s ′ ≤ q 0 such that ψ m (v s , u s ) ∼ n-1 ψ m (v s ′ , u s ′ ) (and vice versa).

We now prove the statement of the theorem by induction on m; take two points q 0 , q 1 ∈ Π c .

For m = 0, (v, u) q 0 ∼ n (v, u) q 1 is established as follows: as long as Player 1 plays in Π c , we know (v, u) is constant so that Player 2 can answer with an identical move still staying within Π c ; as soon as it plays in Π, Player 2 uses the above Fact to win the game.

The inductive case ψ m+1 (v, u) q 0 ∼ n ψ m+1 (v, u) q 1 is proved in the same way, using the Fact (which holds for the integer m + 1) and observing that ψ m+1 is constant on Π c . The latter statement can be verified as follows: by the induction hypothesis we have ψ m (v, u) q ∼ n ψ m (v, u) q ′ , so we derive from Proposition 2 ψ m+1 (v, u) q ∼ 0 ψ m+1 (v, u) q ′ , for all q, q ′ ∈ Π c ; that is, ψ m+1 is constant on Π c .

Ruitenburg's Theorem

We can finally prove: Theorem 20 (Ruitenburg's Theorem for IPC). There is N ≥ 1 such that we have ψ N +2 = ψ N .

Proof. Let L be a finite poset and let R := R(L, n) be the maximum rank for n, L (see the previous section). Below, for e ∈ L, we let |e| be the height of e in L, i.e. the maximum size of chains in L whose maximum element is e; we let also |L| be the maximum size of a chain in L. We make an induction on natural numbers l ≥ 1 and show the following: (for each l ≥ 1) there is N (l) such that for every (v, u) and p ∈ dom(v, u) such that l ≥ |v(p)|, we have that ψ N (l) (v p , u p ) is periodic. (It will turn out that N (l) is 2R(l -1) + 1). Once this is proved, the statement of the Theorem shall be proved with N = N (|L|).

If l = 1, it is easily seen that we can put N (l) = 1 (this case is essentially the classical logic case).

Pick a p with |v(p)| = l > 1; let N 0 be the maximum of the values N (l 0 ) for l 0 < l: 5 we show that we can take N (l) to be N 0 + 2R.

Firstly, let (v, u 0 ) := ψ N 0 (v, u) so all q with |v(q)| < l are periodic in (v, u 0 ). After such iterations, suppose that p is not yet periodic in (v, u 0 ). We let r be the minimum rank of points q ≤ p which are not periodic (all such points q must be such that v(q) = v(p)); we show that after two iterations of χ, all points p 0 ≤ p having rank r become periodic or increase their rank, thus causing the overall minimum rank below p to increase: this means that after at most 2(Rr) ≤ 2R iterations of ψ, all points below p (p itself included!) become periodic (otherwise said, we take Rr as the secondary parameter of our double induction).

Pick p 0 ≤ p having minimal rank r; thus we have that all q ≤ p 0 in (v, u 0 ) are now either periodic or have the same rank and the same v-value as p 0 (by the choice of N 0 above). Let us divide the points of ↓ p 0 into four subsets:

E per := { q | q is periodic } E 0 := { q | q ∈ E per & ∀q ′ ≤ q (q ′ ∈ E per ⇒ u 0 (q ′ ) = 0) } E 1 := { q | q ∈ E per & ∀q ′ ≤ q (q ′ ∈ E per ⇒ u 0 (q ′ ) = 1) } E 01 := { q | q ′ ∈ E per ∪ E 1 ∪ E 0 } .
Let us define frontier point a non-periodic point f ≤ p such that all q < f are periodic (clearly, a frontier point belongs to E 0 ∪ E 1 ); by Lemma 17, all frontier points become periodic after applying ψ. Take a point q ∈ E i and a frontier point f below it; since q also has minimal rank and the hypotheses of Lemma 19 are satisfied for (v, u) q , we have in particular that ψ m (v, u 0 ) q ′ = ψ m (v, u 0 ) f for all m ≥ 0 and all non-periodic q ′ ≤ q, and hence ψ(v, u 0 ) q is periodic too.

Thus, if we apply ψ, we have that in (v, u 1 ) := ψ(v, u 0 ) all points in E per ∪ E 0 ∪ E 1 become periodic, together with possibly some points in E 01 . The latter points get in any case u 1 -value equal to 0. This can be seen as follows. If any such point gets u 1 -value equal to 1, then all points below it get the same u 1 -value. Yet, by definition, these points are above some frontier point in E 1 and frontier points in E 1 get u 1 -value 0 by the second statement of Lemma 17.

p 0 • E 0 E 1 E 01 E per ψ =⇒ p 0 • E ′ 0 E ′ per ψ =⇒ p 0 • E ′′ per Figure 1.
Iterating twice ψ to make p 0 periodic If p 0 ∈ E 0 has become periodic, we are done; we are also done if the rank of p 0 increases, because this is precisely what we want. If p 0 has not become periodic and its rank has not increased, then now all the non-periodic points below p 0 in (v, u 1 ) have u 1 -value 0 (by the previous remark) and have the same rank as p 0 . Thus, they are the set E 0 computed in (v, u 1 ) (instead of in (v, u 0 )) and we know by the same considerations as above that it is sufficient to apply ψ once more to make them periodic.

Figure 1 illustrates the main step of the proof, the double iteration of ψ to turn p 0 into a periodic point. Notice that some crucial arguments used in the above proof (starting from the induction on |e| itself) make essential use of the fact that evaluations are order-preserving, so such arguments are not suitable for modal logics.

A Non-Ultimately Periodic Endomorphism

Ruitenburg's Theorem, interpreted over finitely generated free Heyting algebras, says that any endomorphism of such algebras

µ : F H (x 1 , . . . , x n ) -→ F H (x 1 , . . . , x n )
is ultimately periodic with period 2, in case it fixes all free generators but one. One may ask whether this is a peculiar property of the endomorphisms fixing all free generators but one or whether this can be extended to all endomorphism: we show by a counterexample that there exists endomorphisms of the free algebra over two generators which are not periodic.

To describe our counterexample we first introduce a variant (R, ≤) of the Rieger-Nishimura ladder. This is the poset so described:

-R = {n ∈ Z | n ≥ -1}; -n ≤ m iff either n = -1 or (n ≥ 0 and either n ≤ m -2 or n = m). It is not difficult to see that ≤ is a reflexive, transitive, antisymmetric relation (actually, (R, ≤) differs from Rieger-Nishimura only for the presence of the bottom element -1, see Figure 2).

Let us consider the Heyting algebra D(R) of downsets of (R, ≤). We show that this is generated by the two downsets a = {-1} and b = {0, -1}. To see

Proof. Let F for the time being be the above mentioned finitely presented algebra. Since, within D(R), the downset {-1} is a least non trivial element (so ¬{-1} = ∅) and {-1} ⊆ {0, -1}, it is clear that D(R) satisfies the equality [START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF] for a := {-1} and b := {0, -1}. Also, D(R) is generated by the two elements {0, -1} and {-1}; as a consequence, the function q : F -→ D(R) mapping the equivalence class of the free generator b to {0, -1} and the equivalence class of the free generator a to {-1} is a Heyting algebras quotient. To show that this quotient map is also injective, we use the same technique we adopted for showing that S(h L ) is the free algebra over the distributive lattice D(L): since F embeds into a product of finite Heyting algebras (like any finitely presented Heyting algebra, see Lemma 11), it is sufficient to show that any morphism h : F -→ D(P ) (for a finite poset (P, ≤)) factors through q. This follows from the following statement on finite Kripke models: (iv) if all p ′ < p force b and there is p ′ < p forcing only b, then f (p) := 2; (v) in all remaining cases, f (p) := { f (p ′ ) | p ′ < p }. Notice that the above analysis is exhaustive: since a → b is true everywhere, there cannot be points forcing only a and not b. Similarly, since ¬¬a is true everywhere, for every p there must be p ′ ≤ p forcing a: this fact is used when checking that f as defined above is open.

Lemma 23. There is an endomorphism of D(R) which is not ultimately periodic.

Proof. The endomorphism is the inverse image f -1 along the open map f : (R, ≤) -→ (R, ≤) so defined:

f (n) := -1 (for n < 2) f (n) := n -2 (for n ≥ 2) .
It is evident that f -1 is not ultimately periodic: this comes from the fact that we have f (n) = n -2 for all n ≥ 2.

To lift the endomorphism of Lemma 23 to the level of the free algebra on two generators, we first show that D(R) is a projective algebra: Lemma 24. D(R) is a projective Heyting algebra.

Proof. We might use for the proof of this Lemma the general results from [START_REF] Ghilardi | Unification in intuitionistic logic[END_REF], however we prefer to supply a direct proof. Let F H (a, b) be the free Heyting algebra on two generators and let q : F H (a, b) -→ D(R) be the homomorphism mapping the free generator b to {0, -1} and the free generator a to {-1}: what we have to produce is a section of q, namely a morphism s in the opposite direction such that q • s = id. Taking into consideration Lemma 22 and turning the existence of s into logical terms, what we need is a substitution σ such that the formulae

σ(¬¬a ∧ (a → b)) ¬¬a ∧ (a → b) → (a ↔ σ(a)) ¬¬a ∧ (a → b) → (b ↔ σ(b))
are provable in intuitionistic logic (here σ(a), σ(b) must be formulae over the propositional variables a, b). The required substitution in fact exists and can be taken to be

a -→ ¬¬a → a, b -→ ((¬¬a → a) → b) → b
as it can be easily checked.

Theorem 25. There is an endomorphism of the free Heyting algebra on two generators which is not ultimately periodic.

Proof. Let f : D(R) -→ D(R) be the morphism defined in Lemma 23, so f i+p = f i for no i ≥ 0 and p ≥ 1. Let q : F H (a, b) -→ D(R) and s : D(R) -→ F H (a, b) as in the proof of Lemma 24, so q•s = id. Let g := s•f •q and suppose that g i+p = g i . Then s•f i+p •q = s•f i •q and, by precomposing with s and postcomposing with q, f i+p = f i , contradiction.

Bounds for Periods

We fix, in this Section, a finite poset L and a natural transformation ψ : h L -→ h L . We shall pay a particular attention to the case where ψ is the dual of an endomorphism of a finitely generated free algebras. This happens exactly when ψ has a b-index and when L is of the form P(x), ⊇ for a finite set x (so D(L) is a free distributive lattice).

As we saw, ψ might not be ultimately periodic but, on the other hand, all components ψ P of ψ are such (because the P are finite posets). We show that the period of ψ P can be uniformly bounded depending on the sole cardinality of L (and not on the cardinality of P ). More precisely, we have the following statement: Proposition 26. Let ℓ be the cardinality of L. For each finite set P and each v ∈ h L (P ), the period of the sequence { ψ k P (v) | k ≥ 0 } has ℓ! as an upper bound.

The Proposition is an immediate consequence of Lemma 27 below, for which we need to define a few concepts.

For a point p ∈ P , we let the view set of p (w.r.t. v, ψ) be the set { ψ k (v)(p) | k ≥ 0 } and, for S ⊆ P , we let the view set of S (w.r.t. v, ψ) be the union of the view sets of the p ∈ S.

Our claim follows from the following:

Lemma 27. For v ∈ h L (P ), the period of the sequence { ψ k (v) | k ≥ 0 } has as an upper bound K!, where K is the cardinality of the view set of P .

Proof. We argue by induction on the height of P . If such an height is 1, then P contains only the root and the period is bounded by K ≤ K!. Suppose that the height of P is greater than 1 and let p be the root of P . Then, let ↓ ↓ p := { q ∈ P | q < p } and let M be the cardinality of the view set of ↓ ↓ p. By the induction hypothesis, for any q ∈↓ ↓ p, M ! is an upper bound for the period of the sequence { ψ

k (v q ) | k ≥ 0 }. Since the lcm of many copies of M ! is M !, the restriction of { ψ k (v) | k ≥ 0 } to ↓ ↓ p has period M !.
Thus, for s large enough, we have ψ s+M ! (v q ) = ψ s (v q ) for all q ∈↓ ↓ p. Let a be maximal (w.r.t. the partial order of L) in the view set of ↓ ↓ p (w.r.t. v, ψ s ). Without loss of generality (that is, up to increasing s a bit), we can suppose that there is q 0 ∈↓ ↓ p such that ψ s (v)(q 0 ) = a.

Consider now the set { ψ s+k•M ! (v)(p) | k ≥ 0 } and let N be its cardinality. If, for some k, ψ s+k•M ! (v)(p) belongs to the view set of ↓ ↓ p, then, for all q ∈↓ ↓ p,

ψ s+k•M ! (v)(q) ≤ ψ s+k•M ! (v)(p), and in particular a = ψ s (v)(q 0 ) = ψ s+k•M ! (v)(q 0 ) ≤ ψ s+k•M ! (v)(p). It follows that a = ψ s+k•M ! (v)(p)
, by the maximality of a. Therefore the set { ψ s+k•M ! (v)(p) | k ≥ 0 } intersects the view set of ↓ ↓ p at most in the singleton { a } and, consequently, we have M + N -1 ≤ K, where K is the cardinality of the view set of the whole P . We clearly have that ψ s becomes periodic in at most N • (M !) steps (with period bounded by this number) and the claim follows from the inequality N

• (M !) ≤ K! below. Lemma 28. For M, N ≥ 1, we have N • (M !) ≤ (M + N -1)!. Proof. The case N = 1 is obvious, so we suppose that N > 1. Since M ≥ 1, N ≤ M + N -1 and therefore N • M ! ≤ (M + N -1)M ! ≤ M !(M + 1)(M + 2) . . . (M + N -1) = (M + N -1)! ,
where for the last equality we have used that M + N -1 > M .

The following result is an immediate consequence of Proposition 26: Proposition 29. Let a finitely generated free Heyting algebra homomorphism µ : F H (x 1 , . . . , x n ) -→ F H (x 1 , . . . , x n ) be ultimately periodic; then its period is bounded by 2 n !.

Remark 30. Let us point out that the bound given in Proposition 26 strictly depends on h L (P ) being a set of monotone functions. Observe that, when the bound has been constructed in the proof of Lemma 27, the function ψ P : h L (P ) -→ h L (P ) has been decomposed as ψ P ( y, x) = (g( y), f ( y, x)), where y is a vector of elements of L indexed by ↓ ↓ p and x ∈ L; moreover ψ is applied to pairs ( y, x) such that y ≤ x for each y ∈ y. If we give away the latter constraint on the order, it is easy to see that the bound does not hold anymore. This happens, even when ψ is recursively defined on the height of P (so that all of its restrictions ψ p are of the form g • π 1 , f for some g :↓ ↓ p -→↓ ↓ p and for some f : L ↓ ↓p × L -→ L). Consider the following example. Let P be the chain { 1, . . . , n } and let L = { 0, 1 }, so we can identify arbitrary functions from P to L with words on the alphabet { 0, 1 } of length n. For x ∈ { 0, 1 }, let ψ 1 (x) := 1x. Suppose that, for i < n, we have defined ψ i : { 0, 1 } i -→ { 0, 1 } i so that ψ i is a bijection of period/order 2 i . We can list then { 0, 1 } i = { w 0 , . . . , w 2 i -1 } with w j = ψ j i (0, . . . , 0), j = 0, . . . , 2 i -1. Define then

ψ i+1 (w j , x) := (h i (w j ), x) , j < 2 i -1 , (h i (w j ), 1 -x) , j = 2 i -1 .
This recursive construction yields ψ n of period 2 n and, in particular, the factorial bound 2! for the period does not apply.

A subvariety V of Heyting algebras is said to be locally finite iff the finitely generated free V-algebras are all finite (we shall indicate with F V (x 1 , . . . , x n ) the free V-algebra on the generators x 1 , . . . , x n . Obviously, a locally finite subvariety is also finitely approximable, hence Theorem 16 applies to it. Since all results in this section trivially apply also to finitely approximable varieties and since the endomorphisms between finitely generated free Valgebras are ultimately periodic (by the finiteness of these algebras), we obtain:

Theorem 31. Let V be a locally finite variety of Heyting algebras. Every endomorphism µ : F V (x 1 , . . . , x n ) -→ F V (x 1 , . . . , x n ) is ultimately periodic and its period is bounded by 2 n !.

The interesting point is that the above bound is uniform with respect to all varieties V. However it is not in general tight, as we shall remark in the final section by considering as V the variety of Boolean algebras.

Conclusions and Open Problems

Ruitenburg's Theorem exhibits a particular finitistic behaviour of onevariable substitutions in the Intuitionistic Propositional Calculus. Willing to provide a semantical proof of this theorem, we have studied more general substitutions, which, algebraically, can be identified with endomorphisms of finitely generated free Heyting algebras. The proof of Ruitenburg's Theorem as well as some additional remarks on periods of iterated substitutions have been achieved using the semantical apparatus given by the sheaf theoretic duality for finitely presented Heyting algebras [START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF].

Using these semantical tools, sheaf duality and bounded bisimulations, we found upper bounds for the index and the period of sequences of iterated substitutions. The bounds so found are not optimal. For example, the proof of Theorem 20 yields a bound for the index which is non elementary as a function of the implication degree of an IPC formula. On the other hand, the bound that can be extracted from the syntactic computations in [START_REF] Ruitenburg | On the period of sequences (a n (p)) in intuitionistic propositional calculus[END_REF] is linear w.r.t. the implicational degree and the number of propositional variables of a formula. The syntactic computations in [START_REF] Ghilardi | Fixed-point elimination in the intuitionistic propositional calculus[END_REF] for fixpoints convergence also yield tighter bounds.

While the semantical approach has been successful for providing a proof of Ruitenburg's Theorem, it remains open whether similar approaches can yield finer bounds.

Other open problems arise from inspecting the results presented in this paper. Firstly, although we were able to show that periodicity fails for twovariable substitutions, it is still an open problem to characterize or to decide periodicity for abitrary substitutions in IPC (the only sufficient condition known is the one supplied by Ruitenburg's Theorem-namely the fact that all-but-one variables are fixed).

Secondly, concerning the upper bounds we found, notice that Proposition 29 provides bounds for periods of free Heyting algebra endomorphisms in locally finite subvarieties; being able to bound their indexes might also be interesting. In particular, it is not clear whether indexes are sensitive to the number of generators of a free algebra or, similarly to what happen for fixpoint approximants in some lattice varieties, see [START_REF] Frittella | Fixed-point theory in the varieties Dn[END_REF], they are uniform in a fixed variety. Corollary 18 can be used to argue that this is the case in varieties of Heyting algebras of bounded height-see e.g. the varieties bd n in [START_REF] Chagrov | Modal logic, volume 35 of Oxford Logic Guides[END_REF]Prop. 2.38]-yet there are locally finite varieties of Heyting algebras-notably, the variety of Gödel/Dummet algebras-whose Kripke models might be of unbounded height.

Coming back to the period, let us also notice that the upper bound provided by Proposition 29 is not in general tight. To see why, consider free Boolean algebras: a morphism f : F B (x 1 , . . . , x n ) -→ F B (x 1 , . . . , x n ) corresponds, via duality, to a function f : 2 n -→ 2 n . Now, estimating an upper bound for the periods of functions from the set [k] := { 1, . . . , k } (where in our case k = 2 n ) to itself can be reduced to estimating an upper bound for the period (or order) of permutations of [k]. Indeed, if i and p are such that f i+p = f i , then the restriction of f to f i ([k]) is a permutation of f i ([k]) which can be extended to a full permutation of the set [k] of equal period p. Now, an upper bound for all these periods is lcm(1, . . . , k) for which we have 2 k-1 ≤ lcm(1, . . . , k) ≤ 3 k [6] and, asymptotically, lcm(1, . . . , k) ∼ e k (by the prime number theorem). On the other hand, using Stirling approximation, k! ∼ √ 2πk( k e ) k . It is an open problem whether the bound 2 n ! can be made tighter by considering locally finite varieties of Heyting algebras other than Boolean algebras; it is not clear either how the bound can vary below 2 n ! depending on the locally finite subvariety V.

Finally, most of the techniques used here for Heyting algebras are also the tools for studying modal logics in [START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF]. While we can expect that periodicity phenomena of substitutions do not arise for the basic modal logic K, they surely do for locally tabular modal logics. Considering also the numerous results on definability of fixpoints, see e.g. [START_REF] Sambin | An effective fixed-point theorem in intuitionistic diagonalizable algebras[END_REF][START_REF] Alberucci | The modal µ-calculus hierarchy over restricted classes of transition systems[END_REF], these phenomena are likely to appear in other subsystems of modal logics. As far as we know, investigation of periodicity phenomena in modal logics is a research direction which has not yet been explored and where the bounded bisimulation methods might prove their strength once more.

  otherwise f (a, b ′ ) = (a, b) (there are only two available values for b!) and even in this case f 3 (a, b) = f (a, b).

  If x = y, then we have a repeat at (0, 1). Also, if a = 1, then the mappings x and y are uniformly 1 (since evaluations are order-preserving maps and we have 1 ≤ 0 in 2): again, x = y and (0, 1) is a repeat. So let us assume x = y and a = 0. If c = a, then we have the repeat (0, 2) as above. Otherwise c = 1, so x = 1. We cannot have d = 1, otherwise 1 = x = y. Thus d = 0 = a, and the repeat is (1, 2). Finally, consider i = 1 (so a = b and j = 1): We have two subcases: b = 1 and b = 0. If b = 1, then a = 0 and x = 1 = y: we have a repeat at (1, In the last subcase, we have b = 0, a = 1 and now if d = 0 we have a repeat at (1, 2) and if d = 1 we have a repeat (1, 1) (because d = a = 1 implies y = 1 and x = 1).

↓ 6 → (↓ 3 ∨ ↓ 4 )Figure 2 .

 6342 Figure 2. The modified Rieger-Nishimura ladder

  (*) : for every finite Kripke model over P validating ¬¬a ∧ (a → b) there is an open map f : (P, ≤) -→ (R, ≤) preserving the evaluation of a, b. Property (*) is easily checked by defining f (p) (p ∈ P ) by induction on the height of p. In detail: (i) f (p) := -1 if p forces both a, b; (ii) f (p) := 0 if p forces only b; If p forces neither a nor b, then (iii) if all p ′ < p force both a and b, then f (p) := 1;

However, let us notice that, according to our convention, a P ( x), ⊇ -evaluation is such that, for p, q ∈ P if p ≤ q then u(p) ⊇ u(q); in standard logical literature, see e.g.[START_REF] Chagrov | Modal logic, volume 35 of Oxford Logic Guides[END_REF], the opposite order on P is used, namely an evaluation is such that u(q) ⊆ u(p), for q ≤ p.

This is called 'index' tout court in[START_REF] Ghilardi | Sheaves, Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics[END_REF]; here we used the word 'index' for a different notion, since Section 1.

From now on, 'periodic' will mean '2-periodic', i.e. 'periodic with period 2'.

It is easily seen that we indeed have N0 = N (l -1).


Alaa Hijazi

Eric Bideaux

Pascal Venet

Guy Clerc

Keywords: Boost converter, PI controller, sliding mode, supercapacitor

This paper presents a DC/DC converter with supercapacitor stack for a trolleybus. After the description of transportation application, the performances of the system are studied by testing different control strategies. The comparison of SMC (Sliding mode Control) and PI controller on a developed test bench have shown the benefit of SMC in this type of application.

I. INTRODUCTION

DC to DC converters are more and more used in applications that required converting DC voltage from one level to another one.

Conventionally, PID controllers are used to control power converters [START_REF] Arulselbi | Design of PID controller for boost converter with RHp zero[END_REF] [2] [START_REF] Mingzhi | Nonlinear PID in digital controlled buch converters[END_REF]. However, these controllers, which are based on linearization techniques [START_REF] Rashid | Power electronics handboos[END_REF] [START_REF] Forsyth | Modelling and control of DC-DC converters[END_REF], fails to perform satisfactory constrained specifications under large perturbation variations [START_REF] Racirah | Comparative Study Of Proportional-Integral Sliding Mode, and Fuzzy Logic Controllers for Power Converters[END_REF].

Sliding mode control (SMC) of power converters is an important alternative for controlling such systems, due to their capability to control nonlinear system and to provide robust stability and performance [START_REF] Rashid | Power electronics handboos[END_REF] [START_REF] Utkin | Sliding mode control and optimization[END_REF] [8] [START_REF] Malesani | Performance optimization of Cuk converters by sliding-mode control[END_REF]. The SMC has becoming an attractive subject in the field of the control of power electronic converters. The objectives of must research work are to simplify the design, to improve robustness, to reduce the number of components, and to prevent the chattering phenomena which is the origin of high frequency oscillations along the sliding surface. The SMC for power converters is an old subject. Early works on the development of SMC for DC-DC Controllers appear in 1983 [10] [11] . This work shows the application of SMC to various topologies of second order DC-DC converters. A general method to synthesize SMC for most topologies of DC-DC converters is proposed in [START_REF] Mattavelli | General-purpose sliding-mode controller for DC/DC converter applications[END_REF]. This study shows clearly the robustness of SMC toward load and parameters variation. The study of several sliding surfaces has been conducted in [START_REF] Cortes | Robust sliding mode control for the boost converter[END_REF], particularly surfaces that do not depend on the load current. Several studies ( [START_REF] Mattavelli | General-purpose sliding-mode controller for DC/DC converter applications[END_REF] [14] [START_REF] Iannelli | Dithering for sliding mode control of DC/DC converters[END_REF] [START_REF] Tan | Adaptive feedforward and feedback control schemes for sliding mode controlled power converters[END_REF] [17] [START_REF] Siew-Chong Tan | A Fixed-Frequency Pulsewidth Modulation Based Quasi-Sliding-Mode Controller for Buck Converters[END_REF]) have been interested with the problem of fixing the frequency of SMC. The solutions proposed consist of adding some triangular waveforms or adaptive hysteresis band to the sliding surface. Another works deals with eliminating the steady state error by adding an integral term in the sliding surface [19] [20].

However, despite being a popular research subject, SMC is still rarely applied in practical DC-DC converters [START_REF] Siw-Chong Tan | General Design Issues of Sliding-Mode Controllers in DC-DC converters[END_REF]. So our goal in this paper is to explore the benefit of application of SMC in industrial application concerning the supply of trolleybus via supercapacitors stack associated with DC-DC converter.

The supply system of trolleybus consists of two parallel DC-DC converters (Fig. 1). The first converter (Trolleybus converter) regulates the voltage of the bus Vb to 330 Volts while the other one (Supercapacitors converter) manages the energy transfer between supercapacitors and trolleybus. When the voltage of trolleybus is more than 350 Volts, the supercapacitors will be charged. When the voltage decreases fewer than 310 Volts, the supercapacitors discharges to insure the continuity of the supply of the auxiliary of trolleybus (pump, air compressor, fans). The supercapacitors voltage must be always between 120 and 300 Volts. In this paper, we will focus on the discharge phase of supercapacitors. As the voltage of trolleybus is greater than the voltage of supercapacitors, our study is limited to the study of the control of boost converter.

Due to its simplicity, boost converters are widely present in applications that need to increase voltage. However because of its non-minimum phase structure, the control of boost converter is more complicated than buck converter [START_REF] Kapat | A Current-Controlled Tristate Boost Converter With Improved Performance RHP Zero Elimination[END_REF]. This paper deals with the application of sliding mode control to a boost converter, which is used for supplying a trolleybus with supercapacitors, during power micro-cuts. For many systems, in the trolley, such as electric air compressor, these cuts of electrical supply are very critical. Implementing an auxiliary energy source in the trolley improves the system reliability and decrease the energy consumption by recovering the braking energy. The electrical micro-cuts can take place during very short time, thus the importance of the dynamic performance of the controller.

In the second section, we present the theoretical study, concerning the synthesis of SMC and PI controller for boost converter. In the third section, the developed prototype is presented. Finally, the fourth section is dedicated to emphasize Improvement of the performance of DC/DC converter used for transportations applications.

Test of different control strategies the advantages and the drawbacks of the SMC by comparing the PI controller and the SMC structure performances. Fig. 2 shows the circuit of a boost converter. It consists of a DC input voltage E, which represents the voltage of the supercapacitors, the smoothing inductor L, the controlled switch S, the freewheeling diode D, the filter capacitor C and finally the load, which is modeled by the resistor R. Assuming that the circuit is in continuous conduction mode, which means that the inductors current never falls to zero, the mathematical model of boost converter can now be easily deduced by applying Kirchhoff's laws. The model of boost converter in continuous conduction mode is:

Trolleybus DC/DC converter

Supercapacitors & DC DC converters

Motors + Auxiliaries

II. THEORETICAL STUDY OF SMC AND PI CONTROLLER

A. Mathematical model of a boost converter

C dV dt 1 u i i , L di dt E 1 u V , (1)
Where u is the switch state or the switch duty cycle in the case of average model, V and i are respectively the output voltage and the inductor current of the boost converter.

B. Sliding mode controller for boost converter 1) Introduction

The sliding mode control is a robust control, which is based on the concept of changing the controller in relation with the system state, in order to obtain the desired response. The sliding mode control is a bang-bang controller that switches abruptly between two states. The idea is to divide the state space by a boundary called sliding surface, which defines two subspaces corresponding to two possible states of the controller. Stabilization on the sliding surface is obtained by switching S each time a boundary decision trajectory is crossed. In order to have a stable equilibrium point, three conditions must be satisfied (figure 3): attractiveness condition, sliding condition and stability condition. The control should aim to make the surface attractive. Regardless the position of the system in state space, the control should insure that the system moves toward the surface (attractiveness). Once the surface is reached, we must ensure that the system slides over the surface (sliding condition). Finally, we should verify that the equilibrium point is stable, so the system goes toward the equilibrium point (stable condition).

For boost converter, we choose the sliding surface as a linear combination of the state variables (iL,Vb) :

S K V V K i I (2)
Where V and Iref are the output voltage and inductor current reference, 𝐾 and 𝐾 constants ∈ 𝑅 .

The reference current I depends on the operating point, so that :

I V i E (3)
where 𝑖 .

The reference current is dynamic and it tends toward I corresponding to the equilibrium state (V , I ). Replacing I by its value from (3) in the expression of the commutation surface (2), we obtain:

S K V V K i K V V R. E K K V R. E V K i K V (4)
Writing this last equation in a new coordinate system (x V V , x i I ), we have:

S K x K x (5)
3

In SMC, we usually determine u as following:

u 1 if S ∆ 0 if S ∆
Where S is the sliding surface. ∆ is an hysteresis band added to limit the switching frequency.

2) Calculation of system parameters Referring to the work presented in [START_REF] Hijazi | Sliding mode control of boost converter: Application to energy storage system via supercapacitors[END_REF] , to insure the stability of equilibrium point the gain of controller must respect this condition:

K K RCE V L V RE (6)
The inequality [START_REF] Racirah | Comparative Study Of Proportional-Integral Sliding Mode, and Fuzzy Logic Controllers for Power Converters[END_REF] provides general information about region where stability of the system is insured. However, the choice of these parameters has a great influence on the performance of the system and especially when the system presents large variation around operating point.

Let us write the model of boost converter (1) in the state space (x , x ) where the equilibrium point (V , I ) is the origin. We obtain:

C dx dt 1 u x I x V R , L dx dt E 1 u x V , (7)
The existence condition of sliding mode implies that both S and S will tend to zero when t tend to infinity. The existence condition of the sliding mode is deduced by taking V S as a Lyapunov function and by proving then that SS 0 (when S → 0), the fulfillment of this inequality ensures the existence of sliding mode around the commutation surface.

By calculating 𝑆𝑆 to be negative for u=0 and 1, we can deduce that the sliding region is limited by the following inequalities:

⎩ ⎪ ⎪ ⎨ ⎪ ⎪ ⎧ x K RC K L x K C K E L V L K V RC I C 0 K x RC K E L V K RC 0 (8)
Depending on whether or not the system intercepts the sliding surface in the sliding zone, the dynamic performance of the system can be affected as we can see from the figure 4. Let A(𝑥 , 𝑥 ) be the intersection of the system dynamics with the commutation surface and B(𝑥 , 𝑥 ) the limit of sliding part as shown in (Fig. 4). Supposing that at 𝑡 0 the output voltage is equal 𝑉 and the current in the inductor is zero. As at 𝑡 0 the surface 𝑆 will be negative, then 𝑢 1 and we obtain:

⎩ ⎪ ⎨ ⎪ ⎧ C dx dt x V R , L dx dt E. (9)
By solving these two equalities taking into account initial conditions, we obtain:

x V e V .

(

) 10
This equation represents the dynamic of the system before intercepting the surface at the point A. From 𝑆 0 and from [START_REF] Bilalovic | Buck converter regulator operating in the sliding mode[END_REF] we deduce the coordinate of point A:

x V e V .

(

) 11
Solving this last equation we can obtain 𝑥 function of the parameters of the converter and controller.

From the equation of the commutation surface and the limit of sliding zone defined by (8), we deduce the coordinate of point B, we have:

x K K K V RC I C K E L V L 1 C K K K K RC 1 L . ( 12
)
We can now deduce that the system intercepts the commutation surface in the right part if the controller parameters are selected in such a way that:

‖𝑂𝐴‖ ‖𝑂𝐵‖. ( 13
)
On the other side, the theoretical approach of sliding control makes the assumption that the hysteresis band is null and by consequence the frequency is infinite which is not practically possible due to the characteristic and limitation of circuit components.

In addition to the hysteresis band ∆, the gains of controller have great influence on the operating frequency. Based on the state of the switch and looking to figure 5, we can deduce the rise time "𝑡 " and fall time "𝑡 " :

𝑡 2∆ 𝑆 (14) 𝑡 2∆ 𝑆 (15)
From these equations and the expression of sliding surface (5), we can deduce the expression of the hysteresis band function of the controller and circuit parameters:

∆ 1 2f 1 A B (16)
Where A and B are equal to:

𝐴 1 K L E V K RC (17) 𝐵 1 K V REC V RC K E L V L (18)

C. PI controller for boost converter

As in the case of SMC, we choose in this paragraph to synthesize a PI control of boost converter by means of two loops (current and voltage loop). This improves dynamic performance and robustness of the system. In fact, the presence of a right hand plan zero (RHPZ) in the transfer function of the boost make its control by a single voltage loop inadequate and complicated in some cases [START_REF] Mitchell | Tricks of the Trade: Understanding the Right-Half-Plane Zero in Small-Signal DC-DC Converter Models[END_REF] [START_REF] Forsyth | Modelling and control of DC-DC converters[END_REF]. The structure of the control is shown in figure 6. The corrected error between the reference voltage and the measured voltage serves as a reference for the inner current loop which generates the duty cycle for the converter. C 1 and C 2 are respectively the controllers for outer and inner loop. G1 and G2 are respectively the transfer function for outer and inner loop. H 1 and H 2 are respectively the gain of current and voltage sensor.

The transfer function G1 and G2 are obtained from linearization of the converter model ( 1) around an equilibrium point (𝛼 , 𝑅). To obtain the transfer function G1 and G2, we refer to the works presented in [START_REF] Ferrieux | Alimentations à découpage convertisseurs à résonance[END_REF]. We have:

𝐺 𝑠 𝐼 𝑠 𝛼 𝑠 2𝑉 𝑅 1 𝛼 1 𝑅𝐶 2 𝑠 1 𝐿 𝑅 1 𝛼 𝑠 𝐿𝐶 1 𝛼 𝑠 (19)
𝐺 𝑠 𝑉 𝑠 𝐼 𝑠

1 𝛼 𝑅 2 1 𝐿 𝑅 1 𝛼 𝑠 1 𝑅𝐶 2 𝑠 (20)
The terms x correspond to small variation of the term x. 𝛼 is the duty cycle.

The analysis of transfer functions shows the presence of a zero in the right part of the complex plane, the pulsation of this zero is equal to:

𝜔 𝑅 1 𝛼 𝑒 𝐿 (21)
This unstable zero is present in all the converters that indirectly store the energy. These converters first store the energy in the inductor, then returns it to the load. If the dynamics of the change of duty ratio compared to a disturbance is very fast, naturally the inductor limits the current rise. So the current in the inductor will not be able to increase at the same speed as the duty cycle. This automatically leads to a voltage drop and therefore to oscillations.

The zero adds a phase shift of 90 º to the transfer function. If the zero appears close to the cutoff frequency, it has a negative effect on the phase margin of the system by reducing this latter, which affects the stability and causes the system to To overcome this problem, we should limit the dynamic variation of the duty cycle. As it's shown in [START_REF] Bassot | Switch-Mode Power Supply: Spice Simulations and Practical Designs[END_REF], the bandwidth of the system must be limited to 30 % of the RHP (Right Half Plane) zero pulsation.

III. PROTOTYPE MODEL

To compare SMC and PI controller, we have developed a test bench, which consists of a DC power supply feeding a resistive load and a reversible converter that manages the energy stored in 8 supercapacitors connected in series (figure 7). This configuration allows maintaining the DC bus voltage constant, in case of load variation or electrical cuts of DC power supply. This test bench is therefore close to the structure of the power system of the trolleybus, where we have two type of alimentation: the primary source from the catenaries and the secondary one from supercapacitors. Control of the converter is done through a DSPACE 1104 card. The connection between the converter and the card is done via optic fiber. The voltage and current of the supercapacitor and the load has been measured. The currents are measured with a LEM current sensor. The voltages are measured based on a voltage divider, associated with an isolated amplifier.

The measured current and voltage are connected to the ADC inputs of the DSPACE system and scaled to 0-5 V. A simple hysteresis control is adopted for buck converter.

The parameter of the converters is summarized in table 1.

IV. RESULTS AND DISCUSSION

In the case of SMC, both the controller's gain and the hysteresis band are chosen to obtain switching frequency above 5 kHz and a good dynamic performance. The synthesis of PI correctors must be around the critical point in terms of stability, which corresponds in the case of boost converter to the minimum input voltage and maximum load.

The correctors have been designed to obtain:  A response time for the inner loop about 1.5 ms  A phase margin for external loop 60 ° and a cutoff frequency of about 30 % of the pulsation of RHPZ (to avoid the adverse effect of the RHPZ).

We have utilized the toolbox Sisotool from Matlab@Mathworks in order to synthesize the controllers and we obtain:

𝐶 𝑠 822.01 1 0.0025s s (22)
𝐶 𝑠 165.05 1 0.00048𝑠 𝑠

The open loop diagram of the voltage loop is presented in the figure 8. The switch control of SMC is done from the digital output of the DSPACE using TTL voltage level.

In order to compare the performances of the controllers, we have realized a series of test that simulate the variation of the load or a DC power supply interruption. In this case, the supercapacitors provide electrical power to the load via the boost converter. The reference voltage for Vb in this case is equal to 40 V. Several test campaigns were made in order to compare the control laws in different conditions. The first one consists of varying the load from 20 to 5 Ω. The results obtained for two voltage levels are shown figure 9 and 10. We can notice the excellent dynamic performance of SMC compared to PI controller. The SMC allows the system to reach the reference voltage, very quickly (between 0.1 and 0.5 ms) without oscillations. With the PI controller, the bus voltage reference is reached more slowly (between 7 and 10 ms). This implies a voltage drop of several volts. We can also remark the non-linear aspect of SMC. Its performance is not influenced by a change of the operating point. However, control by sliding mode has two drawbacks: the static error and the variable switching frequency of the converter. In fact, a maximum static error of 2% was observed for a voltage across the supercapacitors equal to 10 V (V b equal 39.2 instead of 40 V). Increasing the order of the controller by adding an integrator can cancel this error. The switching frequency varies between 4.5 and 14 kHz.

After having tested the performance of controllers in different conditions characterizing the load variations, we illustrate in second test campaign, the performances of the controllers, in the case of loss of the alimentation. These tests have the advantage to illustrate the performance of controllers, based on an initial state far from the equilibrium point. We can remark that the power supply voltage is 43 V and the objective of the controllers is to regulate the output DC voltage to 40 V when the output voltage decreases below this limit. The results

Figure 1 :

 1 Figure 1 : Architecture of the trolleybus alimentation supply.

Figure 2 :

 2 Figure 2 : Schematic of boost converter.

Figure 3 :

 3 Figure 3 : Sliding mode condition.

Figure 4 :

 4 Figure 4 : Sliding mode with (a) and without overshoot (b).

Figure 5 :

 5 Figure 5 : Sliding regime with hysteresis band.

Figure 6 :

 6 Figure 6 : two loop control structure

Figure 7 Figure 8 :

 78 Figure 7 : experimental prototype.

  results show the excellent dynamic performance of SMC. The bus voltage has stabilized after 1 ms without overshoot in the case of SMC. The PI controller needs 10 ms to reach the same voltage.

FrequencyFigure 11 :

 11 Experimental results for power supply cut with a supercapacitors voltage equal to 10 V (a : PI, b : SMC).

Figure 12 :

 12 Experimental results for power supply cut with a supercapacitors voltage equal to 20 V (a : PI, b : SMC).

Figure 9 :

 9 Experimental results for a variation of load from 20 to 5  and for a supercapacitors voltage equal to 10 V (a : PI, b : SMC).

Figure 10 :

 10 Experimental results for a variation of load from 20 to 5  and for a supercapacitors voltage equal to 20 V (a : PI, b : SMC).

Table 1 : Converter's parameters.

 1

	Parameter name	Symbol	Value
	Input voltage	E	10-20 V
	Output voltage	V b	4 0 V
	Capacitor	C	1600 μF
	Inductor	L	160 μH
	Load resistance	R	5-20 Ω

Table 2 and

 2 3 summarizes the conclusions obtained concerning the controller comparison.

Table 2 : Summary of the comparison between SMC and

 2

	PI.
		P I	S M C
	Rapidity	-	+
	Robustness	-	+
	Non linearity	-	+
	Static error	+	-
	Constant	+	-
	frequency

Table 3 : Comparison between the performance of SMC and PI.

 3 In other side, it has been shown that the boost converter controlled by SMC is penalized by the steady state error and the variation of switching frequency. These drawbacks can be resolved by introducing an integral term in the sliding surface and by adapting the hysteresis band with the operating point.

		P I	S M C
	Maximum	16 ms	1 ms
	response time
	Maximum Steady	No error	2 %
	state error
	Maximum	10 V	No oscillation
	Amplitude of
	oscillation
	Switching	No variation	Between 5 and 14
	Frequency		kHz
	variation
		V. CONCLUSION
	In this paper, the comparison between SMC and PI control has
	been realized for a boost converter used in supercapacitors
	stack for transportation applications. A test bench have been
	developed and presented. The different tests have shown
	clearly the advantage of SMC toward a classical PI controller.
	The results show that the SMC allows having a fast response
	with no oscillation.