also emerged for the exploration of the affordances of VWs for language learning and acquisition, such as the NIFLAR, TILA and ARCHI21 projects and for the creation of teaching and learning materials (e.g. the AVALON, TALETE and CAMELOT projects). In 2010, the Euroversity Network was established with EU funding to bring together international scholars and researchers working with VWs in education for the sharing of best practice and with a clear focus on VWs for language learning. The EuroCALL-CALICO joint Virtual Worlds Special Interest Group was also founded around this time.

In a review of VW research in education up to 2008, [START_REF] Hew | Use of three-dimensional (3-D) immersive virtual worlds in K-12 and higher education settings: A review of the research[END_REF] found that initial studies had been descriptive and VWs had largely been used as communication spaces, experiential spaces and/or for simulation of space. The main topics of this initial research were the participants' affective domain, their learning outcomes or their social interaction (p. 46). Later research, reviewed by [START_REF] Kim | Between Purpose and Method: A Review of Educational Research on 3D Virtual Worlds[END_REF], indicated that studies on the use of VWs as simulation of space and communication places had increased more than those on VWs as experiential spaces. Indeed, more experimental research was being carried out, and an increasing number of studies started to focus on the use of VWs as spaces for communication, suggesting that users are naturally exposed to the target language through those environments and showing that research on education in VWs was becoming more mature (p. 15).

Over time, the interest of educational researchers in VWs has increasingly moved more towards finding an apt pedagogy for VWs. This is clearly noticeable in a review of educational research methods in desktop virtual world environments by [START_REF] Beck | Review of educational research methods in desktop virtual world environments: Framing the past to provide future direction[END_REF], who note that recent studies seem to have focused more on theory building research and advocate for more empirical research, leading to research studies on how the environment can be successfully used for learning. Their voice is echoed in contributions by leading researchers in the field of language teaching and learning in VWs, who see the need for establishing valid research approaches for these new environments and stand as testimony to a shift in the focus of research in VWs [START_REF] Panichi | Language Learning in Virtual Worlds -Research Issues and Methods[END_REF][START_REF] Sadler | Virtual Worlds, Telecollaboration, and Language Learning: From Theory to Practice[END_REF][START_REF] Zheng | Rethinking language learning: virtual worlds as a catalyst for change[END_REF][START_REF] Blin | Mondes virtuels et apprentissage des langues: vers un cadre théorique émergent[END_REF][START_REF] Wigham | A study of verbal and nonverbal communication in Second Life -the ARCHI21 experience[END_REF]. These spaces are now recognised as complex environments that need to be better understood if researchers want to tap into their educational potential, and this requires a drastic change of approach. The trend is quite clear: researchers in VWs are now showing an interest in looking at these environments through a different lens, which is able to incorporate the complexity of learning in VWs [START_REF] Boelstorff | Three real features for virtual worlds[END_REF][START_REF] Gregory | Learning in Virtual Worlds: Research and Applications (Issues in Distance Education)[END_REF].

This issue focuses on social virtual worlds that we define as 3D, synchronous, immersive, persistent, graphical environments with generative capabilities in which participants are copresent through their avatars and interact with each other and the world's contents. 2 The aim of the special issue is to systematically build on research in the field over the last 10 years and to provide a focus on what we consider to be the most salient and researchintensive aspect of language learning and teaching in VWs: interaction. The collection of papers in this special issue firstly documents how the mediation offered by social virtual worlds provides a rich landscape that supports different types of interaction and, secondly, showcases different approaches and methodologies to study these. As the different contributions illustrate, interaction in VWs for language learning and teaching is considered a multifaceted concept that includes, but is not limited to:  multimodal social interactions between participants via verbal and non-verbal modes (such as gestures, movement, proxemics) which are mediated by the virtual world environment and its communication channels;  avatar interactions with the virtual environment which allow for the learner not only to interact through the environment but also to become part of that environment and interact with its spatial elements;  interactions with linguistic and cultural content mediated by the target language, the other participants as well as the learning design and the virtual world environment and its tools.

These interactions are seen as a process, mediated by the multi-layered environment, and different interaction types need to be considered in relation to each other in order to provide a complete view of the social and interactional dimensions of language learning in social VWs. In the landscape in which language learner interaction takes place, the papers also underline how users are connected by verbal and visual interdependence in both individual and collaborative learning activities.

This special issue also aims to provide a timely state-of-the art discussion of how interaction can be captured, rendered and interpreted methodologically. We believe that to fully appreciate the potential of social VWs for language education we also require new ways of seeing and reading interactional data. Last but not least, in reviewing the field, in light of our own experiences as educators and researchers in VWs over the last 10 years, and of the papers presented in this issue (as well as the numerous original papers that we took into consideration when putting together this issue), we are convinced that the educational and research challenges that arise in such complex environments provide us with insights and understandings that may extend our current conceptualisations of interaction in face-to-face instruction as well [START_REF] Sadler | Language learning in Virtual Worlds: Research and practice[END_REF][START_REF] Dooly | Becoming little scientists: A case study of technologicallyenhanced project-based language learning[END_REF].

Peggy Hartwick contributes the first paper to the special issue and provides an overview of research in interaction in physical (real world) learning spaces and in three-dimensional virtual learning environments (3DVLEs). "Investigating research approaches: Classroombased interaction studies in physical and virtual contexts" guides the readers through key concepts and terminology related to the classroom context, interaction, classroom research approaches, and the implications of all of these for research design in VWs. Perhaps her most important enhancement to the discussion of this research area is the introduction of the following category in the study of interaction in SLA research: interactions between learners and the virtual spaces they inhabit and the tools they interact with. She also provides a very useful datavelliance observation matrix used in her own research that is designed to allow researchers to capture a number of details related to: learner interactional behaviour (including interactions with space or tools and how these connect to movement and gestures) teacher practice, other features of space, location in space, and task and activities. The foundation provided by this contribution also allows for a deeper understanding of the other articles that follow in this issue.

The spatial dimension of VWs is also central to Cristina Palomeque and Joan-Tomàs Pujolà's contribution to this special issue: "Managing multimodal data in virtual world research for language learning." Adopting a social semiotic approach to studying communication, the authors offer a multi-layered transcription method created to account for the multimodal nature of interactions in VWs and to describe how different communication modes or channels are used in combination to create meaning in-world. The proposed methodology allows the authors to structure data stemming from a college-level English for Tourism Purposes course during which sessions in Second Life were offered to volunteers who wished to work on their oral fluency. Of particular interest is the authors' attention to different analysis scales in their proposed methodology. Thus, macro-level information concerning the pedagogical sequence contextualises participants' interactions in the visual and verbal modes, as well as their interactions with the environment's interface at the micro level. After presenting the transcription method, Palomeque and Pujolà offer a discussion of the data management challenges that arise when working with multimodal interaction data. Although this discussion is illustrated with data stemming from a social virtual world, it will no doubt resonate with CALL researchers working with multimodal data collected in other environments.

In "Innovative assessment of aviation English in a virtual world: Windows into cognitive and metacognitive strategies," MoonYoung Park explores how the VW Second Life can play a role in training military air traffic control officers in South Korea by building a recreation of an existing helicopter air base, including a functional air traffic control tower and remote controlled helicopters. His research investigates two primary questions: What types of cognitive and metacognitive strategies are used by the participants in the virtual training environment? and How might those strategies be connected to subject performance in the simulated air traffic control tasks? Recording authentic interaction between helicopter pilots and air traffic controllers from the air base in question, and then importing those sound files into the VW, gave the participants access to a high level of authenticity while also requiring them to attend to the "live" virtual interaction with the virtual helicopters they were controlling. Kasumi Yamazaki's paper discusses acquisition of the target language, Japanese, in a virtual world environment. Her focus is on the development of communication skills where interaction through simulation tasks plays a key role in increasing awareness in learners of their learning and performance in the target language. The instructional approach used by Yamazaki is referred to as Computer Assisted Learning of Communication (CALC) where the focus is on learning through communication and the development of target language communication strategies. The results of her research indicate, in particular, that carefully designed language instruction which makes use of the immersive, situated, and experiential dimension of VWs leads to outcomes in target language acquisition. Specifically, in "Computer-Assisted Learning of Communication (CALC): A case study of Japanese learning in a 3D virtual world," Yamazaki discusses the acquisition of incidentally encountered vocabulary on the one hand, and of communicative competence, on the other, through the use of, in particular, persuasive talk, awareness of audience, and collaborative communication. This paper is an example of empirical research into language acquisition and communicative competence development through immersion carried out in a virtual world.

Following on the heels of numerous studies carried out in the field of Computer Mediated Communication (CMC) on the effect of anonymity on Foreign Language Anxiety (FLA), Sabela Melchor-Couto's "Virtual world anonymity and foreign language interaction" takes us one step further. CMC research has shown how the anonymity afforded by the technical medium can contribute to a lowering of the affective filter and have an effect on the users' interactional dynamics and on their learning. However, apart from a few studies showing that FLA levels are lower when oral interaction in the foreign language is established via VWs, research on the link between anonymity and FLA in VWs is still scarce. Thus, Melchor-Couto's study, conducted in Second Life with undergraduate students of Spanish as a Foreign Language, provides us with a much needed insight into the relationship between virtual world anonymity, FLA, personality profiles, and self-efficacy beliefs. With the aim of analysing whether Foreign Language virtual world interaction is beneficial for learners that present a specific personality profile, Melchor-Couto explores various facets of affective interaction in the virtual world, ranging from how the anonymity afforded by the virtual world environment interacts with the language learner's personality profile to how the perception of anonymity interacts with the learner's FLA profile and self-efficacy beliefs. The research study sheds further light on a field of VW research that is still underrepresented.

The collection of papers in this special issue underlines multiple types of interactions that occur in a social virtual world between social actors, participants and their avatars, avatars and their environment, and between participants and the linguistic and cultural content afforded by the learning design. Hartwick's paper foregrounds the importance of investigating the role played by the virtual space in future research on language learning in VWs. This virtual space provides learners with multimodal and multilayered possibilities of interaction that are going to require specific tools for its analysis (Palomeque & Pujolà). Further, learners' interactions via their avatars and with the environment itself affect the learners' learning experience and each learner's foreign language anxiety levels and selfefficacy, in unexpected ways (Melchor-Couto). On a different level, through the use of carefully designed simulation experiences, virtual world landscapes also lend themselves to the observation and assessment of learning and interactional linguistic competence required in specific fields of FL instruction. Interacting with and through the virtual environment can promote incidental FL learning (Yamazaki) and provide teachers and learners with authentic opportunities to design and perform tasks that promote strategic as well as linguistic competence (Park). In highlighting a range of different pedagogical and methodological approaches, this special issue aspires to document how social virtual worlds provide a rich and effective environment to support different types of interaction for language teaching and learning. We hope it will stimulate further research in the field of language learning and social virtual worlds. The Guest Editors wish to thank colleagues who contributed to this special issue by reviewing extended abstracts and papers. We also extend our thanks to Sylvie Thouësny, Alex Boulton and Françoise Blin for their advice and support during the preparation of this issue.

Guest Editors' Biographies

Ciara R. Wigham is Senior Lecturer in English and Applied Linguistics at Université Clermont Auvergne, France and a member of the Laboratoire de Recherche sur le Langage research unit. Ciara's research interests focus on multimodality in online language learning-teaching contexts. Her PhD investigated the interplay between verbal and nonverbal interaction to support verbal participation and production in a foreign language (https://tel.archivesouvertes.fr/tel-00762382). This was analysed from a socio-semiotic perspective of multimodality within the context of a Content and Language Integrated Learning course held in the synthetic world Second Life. Her current research investigates multimodal pedagogical communication in videoconferencing environments.

Luisa Panichi is Lecturer of English as a Foreign Language at the University of Pisa, Italy and has been involved in the use of virtual worlds in language education since 2007. Luisa was the coordinator for development under the EU funded AVALON and Euroversity Network projects which brought together international experts in the field of virtual world education and research. Luisa has published in the field of CALL, Language Awareness and Learner Advising. Her PhD (2015) examined Learner Participation in virtual world language learning (https://hydra.hull.ac.uk/resources/hull:11583). Luisa is currently training to become a professional counsellor in Transactional Analysis in the field of education and is increasingly interested in Educational Linguistics. Susanna Nocchi is Lecturer in Italian at the Dublin Institute of Technology, Ireland, where she teaches Italian language and culture and Italian history and literature. She is the current cochair of the EuroCALL Virtual Worlds and Serious Games Special Interest Group and the President of the Irish Association for Applied Linguistics. Susanna Nocchi's research interests focus on Computer Assisted Language Learning, particularly on Virtual Worlds and their potential for the teaching and learning of foreign languages. Her PhD thesis, investigating the affordances of virtual worlds for language learning, can be downloaded at http://doras.dcu.ie/21620/. Susanna Nocchi's more current research interest revolves around the role and development of Digital Literacies in education and in foreign language learning. Randall Sadler is an Associate Professor of Linguistics at the University of Illinois at Urbana-Champaign, where he teaches courses on telecollaboration and language learning, virtual worlds and language learning and the teaching of L2 reading and writing. He is also the Director of the Illinois Teaching English as a Second Language and ESL Programs. His main research area is on the role of technology in language learning, with a particular focus on how CMC and Virtual Worlds may be used to enhance that process. He has published in these areas in journals including the Journal of English for Academic Purposes, CALICO Journal, ReCALL, Language Learning & Technology, Computers & Education, ELT, and in numerous edited volumes. His latest book, Virtual Worlds, Telecollaboration, and Language Learning: From Theory to Practice is published by Peter Lang. He is also the co-owner of the EduNation Islands, which are located in the Virtual World of Second Life, where he may often be found in the guise of his avatar Randall Renoir.

From the early years of virtual world usage, the terminology adopted to label these virtual environments has varied. The term Virtual Worlds is one of the most commonly used and generally recognised by the industry, the public, the media and many researchers. For a discussion of the terminology, see[START_REF] Sadler | Virtual Worlds, Telecollaboration, and Language Learning: From Theory to Practice[END_REF][START_REF] Wigham | The interplay between non-verbal and verbal interaction in synthetic worlds which supports verbal participation and production in a foreign language[END_REF][START_REF] Panichi | Participation in language learning in virtual worlds[END_REF][START_REF] Nocchi | The affordances of virtual worlds for language learning[END_REF]

Acknowledgements


Eugene Ndiaye
email: eugene.ndiaye@telecom-paristech.fr

Tam Le
email: tam.le@riken.jp

Olivier Fercoq
email: olivier.fercoq@telecom-paristech.fr

Joseph Salmon
email: joseph.salmon@umontpellier.fr

Ichiro Takeuchi
email: takeuchi.ichiro@nitech.ac.jp

Safe Grid Search with Optimal Complexity

Popular machine learning estimators involve regularization parameters that can be challenging to tune, and standard strategies rely on grid search for this task. In this paper, we revisit the techniques of approximating the regularization path up to predefined tolerance in a unified framework and show that its complexity is O(1/ d √ ) for uniformly convex loss of order d > 0 and O(1/ √ ) for Generalized Self-Concordant functions. This framework encompasses least-squares but also logistic regression (a case that as far as we know was not handled as precisely by previous works). We leverage our technique to provide refined bounds on the validation error as well as a practical algorithm for hyperparameter tuning. The later has global convergence guarantee when targeting a prescribed accuracy on the validation set. Last but not least, our approach helps relieving the practitioner from the (often neglected) task of selecting a stopping criterion when optimizing over the training set: our method automatically calibrates it based on the targeted accuracy on the validation set.

Introduction

Various machine learning problems are formulated as minimization of an empirical loss function f plus a regularization function Ω whose calibration is controlled by a non negative hyperparameter λ. The choice of λ is crucial since it directly influences the generalization performance of the estimator, i.e., its score on unseen data sets. One of the most popular method in such a context is cross-validation, see [START_REF] Arlot | A survey of crossvalidation procedures for model selection[END_REF] for a detailed review. For simplicity, we investigate here the holdout version that consists in splitting the data in two parts: on the first part (training set) the method is trained for a pre-defined collection of candidates Λ T := {λ 0 , . . . , λ T -1 }, and on the second part (validation set), the best parameter is selected.

For a piecewise quadratic loss f and a piecewise linear regularization Ω (e.g., the Lasso estimator), [START_REF] Osborne | A new approach to variable selection in least squares problems[END_REF][START_REF] Rosset | Piecewise linear regularized solution paths[END_REF] have shown that the set of solutions follows a piecewise linear curve w.r.t. to the parameter λ. There are several algorithms that can generate the full path by maintaining optimality conditions when the regularization parameter varies. This is what LARS is performing for Lasso [START_REF] Efron | Least angle regression[END_REF], but similar approaches exist for SVM [START_REF] Hastie | The entire regularization path for the support vector machine[END_REF] or generalized linear models (GLM) [START_REF] Park | L1-regularization path algorithm for generalized linear models[END_REF]. Unfortunately, these methods have some drawbacks that can be critical in many situations:

• their worst case complexity, i.e., the number of linear segments, is exponential in the dimension p of the problem [START_REF] Gärtner | An exponential lower bound on the complexity of regularization paths[END_REF] leading to unpractical algorithms. Even in favorable cases, a complexity linear in p can be expensive to compute for large p.

• they suffer from numerical instabilities due to multiple and expensive inversion of ill-conditioned matrix. As a result, these algorithms may fail before exploring the entire path, a crucial issue whenever the regularization parameter decreases.

• they lack flexibility when it comes at incorporating different statistical learning tasks because they usually rely on specific algebra to handle the structure of the regularization and loss functions.

As far as we know, they apply to a limited number of cases and we are not aware of a general framework that bypasses these issues.

• they cannot benefit of early stopping. Following [START_REF] Bottou | The tradeoffs of large scale learning[END_REF], it is not necessary to optimize below the statistical error to reach good generalization property. Exact regularization path algorithms require maintaining optimality conditions when the hyperparameter varies, which is time consuming.

To overcome these issues, an approximation of the solution path up to accuracy > 0 was proposed and optimal complexity was proven to be O(1/ ) by [START_REF] Giesen | Approximating parameterized convex optimization problems[END_REF] in a fairly general setting. A noticeable contribution was proposed by [START_REF] Mairal | Complexity analysis of the lasso regularization path[END_REF], that come up with an algorithm whose complexity is O(1/ √ ) for the Lasso case. The later result was then extended by [START_REF] Giesen | Approximating concavely parameterized optimization problems[END_REF] to objective function that has a quadratic lower bound while providing a lower and upper bound of order O(1/ √ ). Unfortunately, these assumptions fail to hold for a large class of problems, including logistic regression or Huber loss.

Following such ideas, [START_REF] Shibagaki | Regularization path of crossvalidation error lower bounds[END_REF] have proposed, for classification problems, to approximate the regularization path on the hold-out cross-validation error. Indeed, the later is a more natural criterion to monitor when one aims at selecting a hyperparameter guaranteed to achieve the best validation error. The main idea is to construct an upper and lower bound on the validation error as simple functions of the regularization parameter. Hence by sequentially varying the parameters, one can estimate a range of parameter for which the validation error gap is smaller than an accuracy v > 0.

Contributions. We revisit the approximation of the solution and validation path in a unified framework under general regularity assumptions commonly met in machine learning. We encompass both classification and regression problems and provide a complexity analysis along with optimality guarantees. We discuss the relationship between the regularity of the loss function and the complexity of the approximation path. We prove that its complexity is O(1/ d √ ) for uniformly convex loss of order d > 0 (see (Bauschke and Combettes, 2011, Definition 10.5)) and O(1/ √ ) for the logistic loss thanks to a refined measure of its curvature throughout its Generalized Self-Concordant properties [START_REF] Sun | Generalized selfconcordant functions: A recipe for newton-type methods[END_REF]. Finally, we provide an algorithm with global convergence property for selecting a hyperparameter with a validation error v -close to the optimal hyperparameter from a given grid.

Notation. Given a proper, closed and convex func- Figure 1: Illustration of the approximation path for the Lasso at accuracy = y 2 2 /20. We choose λ max = X y ∞ and λ min = λ max /50. The shaded gray region shows the interval where any -path must lie. The exact path is computed with the LassoLars on diabetes data from sklearn.

tion f : R n → R ∪ {+∞}, we denote dom f = {x ∈ R n : f (x) < +∞}. If f is a twice continuously differ- entiable function with positive definite Hessian ∇ 2 f (x) at any x ∈ dom f , we denote z x = ∇ 2 f (x)z, z . The Fenchel-Legendre transform of f is the func- tion f * : R n → R ∪ {+∞} defined by f * (x * ) =
sup x∈dom f x * , x -f (x). The support function of a nonempty set C is defined as σ C (x) = sup c∈C c, x . If C is closed, convex and contains 0, we define its polar as σ • C (x * ) = sup σ C (x)≤1
x * , x . We denote by [T ] the set {1, . . . , T } for any non zero integer T . The vector of observations is y ∈ R n and the design matrix X = [x 1 , . . . , x n ] ∈ R n×p has n observations rowwise, and p features (column-wise).

Problem setup

Let us consider the class of regularized learning methods expressed as convex optimization problems, such as (regularized) GLM [START_REF] Mccullagh | Generalized Linear Models[END_REF]:

β(λ) ∈ arg min β∈R p f (Xβ) + λΩ(β) P λ (β) (Primal).
(1)

We highlight two important cases: the regularized least-squares and logistic regression where the loss functions are written as an empirical risk

f (Xβ) = i∈[n] f i (x i β)
with the f i 's given in Table 1. The penalty term is often used to incorporate prior knowledges by enforcing a certain regularity on the solutions. For instance, choosing a Ridge penalty [START_REF] Hoerl | Ridge regression: Biased estimation for nonorthogonal problems[END_REF]) Ω(•) = • 2 2 /2 improves the stability of the resolution of inverse problems while Ω(•) = • 1 imposes sparsity at the feature level, a motivation that led to the Lasso estimator [START_REF] Tibshirani | Regression shrinkage and selection via the lasso[END_REF]; see also [START_REF] Bach | Convex optimization with sparsityinducing norms[END_REF] for extensions to other structured penalties.

In practice, obtaining β(λ) , an exact solution to Problem ( 1) is unpractical and one aims achieving a prescribed precision > 0. More precisely, a (primal) vector β (λ) := β (λ, ) (we will drop the dependency in

Lasso Logistic regr. fi(z) (yi -z) 2 /2 log(1 + e z ) -yiz f * i (u) ((u -yi) 2 -y 2 i )/2 Nh(u + yi) V f * ,x (u) u 2 2 /2 w4( u 2 x / u 2) u 2 u Table 1: w 4 (τ ) = (1-τ ) log(1-τ )+τ τ 2 and Nh(x) = x log(x) + (1 -x) log(1 -x)
for readability) is referred to as an -solution for λ if its (primal) objective value is optimal at precision :

P λ (β (λ) ) -P λ ( β(λ) ) ≤ .
(2)

We recall and illustrate the notion of approximation path in Figure 1 as described by [START_REF] Giesen | Approximating concavely parameterized optimization problems[END_REF].

Definition 1 ( -path). A set P ⊂ R p is called an -path for a parameter range [λ min , λ max ] if ∀λ ∈ [λ min , λ max ], ∃ an -solution β (λ) ∈ P . (3)
We call path complexity T for Problem (1) the cardinality of the -path.

To achieve the targeted -precision in (2) over a whole path and construct an -path 1 , we rely on duality gap evaluations. For that, we compute c -solutions 2 (for an accuracy c < ) over a finite grid, and then we control the gap variations w.r.t. λ to achieve the prescribed -precision over the whole range [λ min , λ max ]; see Algorithm 1. We now recall the Fenchel duality (Rockafellar, 1997, Chapter 31):

θ(λ) ∈ arg max θ∈R n -f * (-λθ) -λΩ * (X θ) D λ (θ) (Dual). ( 4
)
For a (primal/dual) pair (β, θ) ∈ domP λ ×domD λ , the duality gap is defined as the difference between primal and dual objectives:

G λ (β, θ) = f (Xβ) + f * (-λθ) + λ(Ω(β) + Ω * (X θ)) .
and weak duality yields D λ (θ) ≤ P λ (β) and

P λ (β) -P λ ( β(λ) ) ≤ G λ (β, θ) , (5)
explaining the interest of the duality gap as an optimality certificate. Using (5), we can safely construct an approximation path for Problem (1) : if β (λ) is an -solution for λ, it is guaranteed to remain one for all parameters λ such that G λ (β (λ) , θ (λ) ) ≤ . Since the function λ → G λ (β (λ) , θ (λ) ) does not exhibit a simple dependence in λ, we rely on an upper bound on the gap encoding the structural regularity of the loss function (e.g., when f is strongly convex, we consider a 1-dimensional quadratic). This bound allows to control the optimization error as λ varies while preserving an optimal complexity on the approximation path.

1 note that such a path depends on exact solutions β(λ) 's 2 the c stands for computational in c Figure 2: Illustration of the construction of anpath for the Lasso on synthetic dataset generated with sklearn as X, y = make regression(n = 30, p = 150) at accuracy = y 2 2 /40 and c = /10. We choose λ max = X y ∞ and λ min = λ max /10 leading to a path complexity T = 6. For Lasso the bound is piecewise quadratic.

λ 0 = λ max λ 1 λ 2 λ 3 λ 4 λ 5 = λ min

Bounds and approximation path

Definition 2. Given a differentiable function f and x ∈ dom f , let U f,x (•) and V f,x (•) be non negative functions that vanish at 0. We say that f is U f,xconvex (resp. V f,x -smooth) at x when Inequality (6) (resp. ( 7)) is satisfied for any z ∈ dom f

U f,x (z -x) ≤ f (z) -f (x) -∇f (x), z -x , (6) V f,x (z -x) ≥ f (z) -f (x) -∇f (x), z -x . (7)
This extends µ-strong convexity and ν-smoothness [START_REF] Nesterov | Introductory lectures on convex optimization[END_REF] and encompasses smooth uniformly convex losses and generalized self-concordant ones.

Smooth uniformly convex case:

U f,x (z -x) = U( z -x ), V f,x (z -x) = V( z -x ),
where U(•) and V(•) are increasing from [0, +∞) to [0, +∞] vanishing at 0; see [START_REF] Azé | Uniformly convex and uniformly smooth convex functions[END_REF] [START_REF] Juditski | Primal-dual subgradient methods for minimizing uniformly convex functions[END_REF] or (Bauschke and Combettes, 2011, Ch. 10.2 and 18.5) for details.

Generalized self-concordant case: a C 3 convex function f is (M f , ν)-generalized self-concordant of or- der ν ≥ 2 and M f ≥ 0 if ∀x ∈ dom f and ∀u, v ∈ R n : ∇ 3 f (x)[v]u, u ≤ M f u 2 x v ν-2 x v 3-ν 2 .
In this case, (Sun and Tran-Dinh, 2017, Proposition 10) shows that one could write:

U f,x (y -x) = w ν (-d ν (x, y)) y -x 2 x , V f,x (y -x) = w ν (d ν (x, y)) y -x 2 x ,
where the last equality holds if d ν (x, y) < 1 for the case ν > 2. Closed-form expressions for w ν (•) and d ν (•) are recalled in Appendix for logistic and quadratic losses.

Approximating the duality gap path. Assume we have constructed primal/dual feasible vectors for a finite grid of parameters Λ T = {λ 0 , . . . , λ T -1 }, i.e., we have at our disposal (β (λt) , θ (λt) ) for all λ t ∈ Λ T . Let us denote G t = G λt (β (λt) , θ (λt) ), and for

ζ t = -λ t θ (λt) , ∆ t = f (Xβ (λt) ) -f (∇f * (ζ t )). For any function φ : R n → [0, +∞] that vanishes at 0, ρ ∈ R, we define Q t,φ (ρ) = G t +ρ • (∆ t -G t ) + φ(-ρ • ζ t ) . (8)
In the previous display, the G t and ∆ t represent a measure of the optimization error at λ t . The notation introduced in (8) will be convenient to write concisely upper and lower bounds on the duality gap. This is the goal of the next lemma which leverages regularity of the loss function f , as introduced in Definition 2. This provides control on how the duality gap deviates when one evaluates it for another (close) parameter λ.

Lemma 1. We assume that -λθ

(λt) ∈ dom f * and X θ (λt) ∈ dom Ω * . If f * is V f * -smooth (resp. U f * - convex) 3
, then for ρ = 1λ/λ t , the right (resp. left) hand side of Inequality (9) holds true

Q t,U f * (ρ) ≤ G λ (β (λt) , θ (λt) ) ≤ Q t,V f * (ρ) . (9)
Proof. Proof for this result and for other propositions and theorems are deferred to the Appendix.

The function φ, chosen as V f * (resp. U f * ) for the upper (resp. lower) bound, essentially captures the regularity needed to approximate the duality gap at parameter λ when using primal/dual vector (β (λt) , θ (λt) ) for λ t close to λ. When the function satisfies both inequalities, the tightness of the bound can be related to the conditioning U f * /V f * of the dual loss f * . Equality holds for the least-squares case (U

f * ≡ V f * ≡ • 2 2 /2),
which certifies the tightness of the bounds.

From Lemma 1, we have G λ (β (λt) , θ (λt) ) ≤ as soon as Q t,V f * (ρ) ≤ where ρ = 1λ/λ t varies with λ. Hence, we obtain the following proposition that allows to track the regularization path for an arbitrary precision on the duality gap. It proceeds by choosing the largest ρ = ρ t such that the upper bound in Equation (9) remains below and leads to Algorithm 1 for computing an -path.

3 we drop x in U f,x and write U f if no ambiguity holds.

Proposition 1 (Grid for a prescribed precision).

Given (β (λt) , θ (λt) ) such that G t ≤ c ≤ , for all λ ∈ λ t × 1 -ρ t ( ), 1 + ρ r t ( ) , we have G λ (β (λt) , θ (λt) ) ≤ where ρ t ( ) (resp. ρ r t ( )) is the largest non-negative ρ s.t. Q t,V f * (ρ) ≤ (resp. Q t,V f * (-ρ) ≤ ). Algorithm 1 training path Input: f, Ω, , c, [λmin, λmax] Initialization: t = 0, λ0 = λmax, Λ = {λmax} repeat Get β (λ t ) solving (1) for λ = λt to accuracy c < Compute ρ t ( ) = max{ρ s.t. Qt,V f * (ρ) ≤ } Set λt+1 = max(λt × (1 -ρ t ), λmin) Λ ← Λ ∪ {λt+1} and t ← t + 1 until λt ≤ λmin Return: {β (λ t ) : λt ∈ Λ}
Conversely, given a grid4 of T parameters Λ T = {λ 0 , . . . , λ T -1 }, we define Λ T , the error of the approximation path on [λ min , λ max ] by using a piecewise constant approximation of the map λ → G λ (β (λt) , θ (λt) ):

Λ T = sup λ∈[λmin,λmax] min λt∈Λ T G λ (β (λt) , θ (λt) ) . ( 10
)
This error is however difficult to evaluate in practice so we rely on a tight upper bound based on Lemma 1 that often leads to closed-form expressions.

Proposition 2 (Precision for a given grid). Given a grid of parameters Λ T , the set {β (λ) : λ ∈ Λ T } is an

Λ T -path with Λ T ≤ max t∈[T ] Q t,V f * (1 -λ t /λ t ) where for all t ∈ {0, . . . , T -1}, λ t is the largest λ ∈ [λ t+1 , λ t ] such that Q t,V f * (1 -λ/λ t ) ≥ Q t+1,V f * (1 -λ/λ t+1 ).
Construction of dual feasible vector. We rely on gradient rescaling to produce a dual feasible vector:

Lemma 2. For any β (λt) ∈ R p , the vector

θ (λt) = -∇f (Xβ (λt) ) max(λ t , σ • dom Ω * (X ∇f (Xβ (λt) ))
,

is feasible: -λθ (λt) ∈ dom f * , X θ (λt) ∈ dom Ω * . Remark 1. When the regularization is a norm, Ω(•) = • then σ • dom Ω * is the associated dual norm • * .
This choice guarantees that the duality gap G t and ∆ t converge to 0 when β (λt) converges to a solution β(λt) .

Finding ρ. Following Prop. 1, one needs to solve 1dimensional equations like Q t,V f * (ρ) = to obtain an -path. This can be done efficiently at high precision by numerical solvers if no explicit solution is available.

As a corollary from Lemma 1 and Proposition 2, we recover the analysis by [START_REF] Giesen | Approximating concavely parameterized optimization problems[END_REF]:

Corollary 1. If the function f * is ν 2 • 2 -
smooth, the left (ρ t ) and right (ρ r t ) step sizes defined in Proposition 1 have closed-form expressions:

ρ t = 2νδ t ζ t 2 + δ2 t -δt ν ζ t 2 , ρ r t = 2νδ t ζ t 2 + δ2 t + δt ν ζ t 2 ,
where δ t := -G t and δt := ∆ t -G t .

Discretization strategies

We now establish new strategies for the exploration of the hyperparameter space in the search for an -path.

For regularized supervised learning methods, it is customary to start from a large regularizer 5 λ 0 = λ max and then to perform iteratively the computation of β(λt+1) after the one of β(λt) , until the smallest parameter of interest λ min is reached. Generally, models are computing by increasing complexity which allows important speed-ups due to warm start [START_REF] Friedman | Pathwise coordinate optimization[END_REF], provided that the parameters λ's are close to each other. Knowing λ t we will provide recursive strategy constructing λ t+1 .

Adaptive unilateral. The strategy we call Unilateral consist in computing the new parameter as λ t+1 = λ t × (1ρ t ( )) as in Proposition 1.

Proposition 3 (Unilateral approximation path). Assume that f * is V f * -smooth. We construct the grid of parameters Λ (u) ( ) = {λ 0 , . . . , λ T -1 } by

λ 0 = λ max , λ t+1 = λ t × (1 -ρ t ( )) ,
and (β (λt) , θ (λt) ) s.t. G t ≤ c < for all t. Then, the set {β (λt)

: λ t ∈ Λ (u) ( )} is an -path for Problem (1).
This strategy is illustrated in Figure 2 on a Lasso example. It stands as a generic algorithm for computing an approximation path for loss functions satisfying the loose regularity assumption in Definition 2.

Adaptive bilateral. For uniformly convex functions, we can make a larger step by combining the information given by the left and right step sizes. Indeed, let us assume that we explore the parameter range from λ max to λ min . Starting from a parameter λ t , we define the next step, given by Proposition 1, λ t := λ t (1ρ t ). Then it exists λ t ≤ λ t such that λ r t := λ t (1+ρ r t ) = λ t . Thus a larger step can be done by using λ t = λ t × (1ρ t )/(1 + ρ r t ). However ρ r t depends on the (approximated) solution β (λ t ) that we do not know before optimizing the problem for parameter λ t when computing sequentially the grid points in 5 for the Lasso one often chooses λ0 = λmax := X y ∞ decreasing order i.e., λ t ≤ λ t . We overcome this issue in Lemma 3 by (upper) bounding all the constants in Q t ,V f * (ρ) that depend on the solution β (λ t ) , by constants involving only information given by β (λt) .

Lemma 3. Assuming f uniformly smooth yields ∇f (Xβ (λ t ) ) * ≤ R t , where R t := V * f -1 f (Xβ (λt) ) + 2 c ρ t ( ) . If additionally f is uniformly convex, this yields ∆ t ≤ ∆ t , where ∆ t := R t × U -1 f ( c ) as well as G λ (β (λ t ) , θ (λ t ) ) ≤ Q t ,V f * (ρ) ≤ Q t,V f * (ρ), where Q t,V f * (ρ) = c + ρ • ( ∆ t -c ) + V f * |ρ| • R t . Let us now define ρ (b) t ( ) = ρ t ( ) + ρr t ( ) 1 + ρr t ( )
, where ρ t ( ) is defined in Proposition 1 and ρr t ( ) is the largest non negative ρ such that Q t,V f * (ρ) ≤ in Lemma 3.

Proposition 4 (Bilateral Approximation Path). Assume that f is uniformly convex and smooth. We construct the grid

Λ (b) ( ) = {λ 0 , . . . , λ T -1 } by λ 0 = λ max , λ t+1 = λ t × (1 -ρ (b) t ( )) , and (β (λt) , θ (λt) ) s.t. G t ≤ c < for all t. Then the set {β (λt) : λ t ∈ Λ (b) ( )} is an -path for Problem (1).
Uniform unilateral and bilateral. Given the initial information from the initialization (β (λ0) , θ (λ0) ), we can build a (crude) uniform grid that guarantees an -approximation before solving any optimization problem. Indeed, by applying Lemma 3 at t = 0, we have G λ (β (λt) , θ (λt) ) ≤ Q 0,V f * (ρ). We can define ρ 0 ( ) (resp. ρ r 0 ( )) as the largest non-negative ρ s.t.

Q 0,V f * (ρ) ≤ (resp. Q 0,V f * (-ρ) ≤ ) and also ρ 0 ( ) = ρ 0 ( ) for Unilateral path, ρ 0 ( )+ ρ r 0 ( ) 1+ ρr 0 ( ) for Bilateral path. ( 11
)
Proposition 5 (Uniform approximation path).

Assume that f is uniformly convex and smooth, and define the grid

Λ (0) ( ) = {λ 0 , . . . , λ T -1 } by λ 0 = λ max , λ t+1 = λ t × (1 -ρ 0 ( ))
,

and ∀t ∈ [T ], (β (λt) , θ (λt) ) s.t. G t ≤ c < . Then the set {β (λt) : λ t ∈ Λ (0) ( )} is an -path for Problem (1)
with at most T grid points where

T = log(λ max /λ min ) log(1 -ρ 0 ( )) .
Remark 2. For cases such as the Lasso, an explicit value of β (λmax) can be obtained, say β (λ0) = 0, for λ 0 = X y ∞ . Since the uniform grid depends only on this initially known value β (λ0) , it can be computed prior any optimization solver is launched. Hence, this case is well suited for naive parallel computation over the grid of parameters.

Limitations of previous framework

Previous algorithms and analysis for computing anpath have been initially developed with a complexity of O(1/ ) [START_REF] Clarkson | Coresets, sparse greedy approximation, and the frank-wolfe algorithm[END_REF][START_REF] Giesen | Approximating parameterized convex optimization problems[END_REF] in a large class of problem. Nevertheless, data fitting functions arising in machine earning have often nicer regularities that must be exploited. This is all the more striking in the Lasso example where a better complexity in O(1/ √ ) was obtained by [START_REF] Mairal | Complexity analysis of the lasso regularization path[END_REF]; [START_REF] Giesen | Approximating concavely parameterized optimization problems[END_REF].

The relation between the complexity of the path and the regularity of the objective function remains unclear and previous methods do not apply to many machine learning problem. For instance, for the logistic regression, the dual loss f * is not uniformly smooth: so in order to apply the previous theory, one needs to restrict the solution on a (potentially badly pre-selected) compact set.

Let us consider the one dimensional toy example where

β ∈ R, X = Id and y = -1, f (Xβ) = log(1 + exp(β)). We have, ∇ 2 f (β) = exp(β)/(1 + exp(β)) 2 . Then for Problem (1), since P λ ( β(λ) ) ≤ P λ (0), we have | β(λ) | ∈ [0, log(2)
/λ] and a smoothness constant of the dual can be reasonably estimated as ν f * = (1 + exp(log(2)/λ)) 2 at each step. This leads to an unreasonable algorithm with tiny step sizes in Corollary 1, since for λ min = λ max /10 we already have ν f * ≈ exp(100). Also, note that the dual function is not polynomial; hence, the algorithm proposed by [START_REF] Giesen | Approximating concavely parameterized optimization problems[END_REF] can not be applied for the logistic loss.

Our proposed algorithm does not suffer from such limitations and we introduce a finer analysis that takes into account the regularity of the loss functions.

Complexity and regularity

Lower bound on the path complexity. For our method, the lower bound on the duality gap quantifies how close the proposed step in Proposition 1 is from the best possible step one can achieve for smooth loss functions. Indeed, at the optimal solution, we have G t = ∆ t = 0. Thus the largest possible step -starting at λ t and moving in decreasing order -is given by the smallest λ between λ min and λ t such that U f * (-ζ t × ρ) > . Hence, any algorithm for computing an -path with the duality gap for U f * -uniformly convex dual loss, have necessarily a complexity of order at least O(1/U -1 f * ( )).

Upper bounds. We remind that we write T for the complexity of our proposed approximation path i.e., the cardinality of the grid returned by Algorithm 1. In the following proposition, we propose a bound on the complexity w.r.t. the regularity of the loss function (details on the constants appearing in the following result are provided in Appendix).

Proposition 6 (Approximation path: complexity). For c < , there exists

C f ( c ) > 0 such that T ≤ log λ max λ min × C f ( c ) W f * ( -c ) ,
where for all t > 0, the function W f * is defined by

W f * =      V -1 f * , if f is uniformly convex and smooth √ •, if f is Generalized Self-Concordant
and uniformly-smooth.

Moreover, C f ( c ) tends to a finite constant C f when c goes to 0.

Validation path

To achieve good generalization performance, estimators defined as solution of Problem 1 require careful adjustment of the regularization parameter λ, to balance between data-fitting and regularization. A standard approach in machine learning to tune such a parameter is to select it by comparing the validation errors on a finite grid (potentially using K-fold cross-validation).

Unfortunately, it is often difficult to determine a priori the number of points in the grid or how they should be distributed to achieve low validation error, and practitioners often rely on rules of thumb for that task.

Considering the validation data (X , y ) (with n observations) and loss6 L, we define the validation error for β ∈ R p as

E v (β) = L(y , X β) . (12)
For selecting a hyperparameter, we leverage our approximation path to solve the bi-level problem arg min

λ∈[λmin,λmax] E v ( β(λ) ) = L(y , X β(λ) ) s.t. β(λ) ∈ arg min β∈R p f (Xβ) + λΩ(β) .
Recent works have addressed this problem by using gradient-based algorithms, see for instance Pe-dregosa (2016); [START_REF] Franceschi | Bilevel programming for hyperparameter optimization and meta-learning[END_REF] who have shown promising results in computational time and scalability w.r.t. multiple hyperparameters. However, they require assumptions such as smoothness of the validation function E v and non-singular Hessian of the inner optimization problem at optimal values which are difficult to check in practice since they depends on the optimal solutions β(λ) . Moreover, they can only guarantee convergence to stationary point.

In this section, we generalize the approach of [START_REF] Shibagaki | Regularization path of crossvalidation error lower bounds[END_REF] and show that with a safe and simple exploration of the parameter space, our algorithm has a global convergence property. The following conditions, on the validation loss and on the inner optimization objective, are assumed through the section:

A1 : |L(a, b) -L(a, c)| ≤ L(b, c) for ant a, b, c ∈ R n . A2 : The function β → P λ (β) is µ-strongly convex.
Note that the assumption on the loss function is verified for norms (regression) and indicator function (classification). Indeed, for any norm L(a, b) = ab , A1 corresponds to the triangle inequality. For the

0/1 -loss L(a, b) = 1 n n i=1
1 aibi<0 , and given any real values s, u and v, |1 us<0 -1 uv<0 | ≤ 1 sv<0 , one has

1 n n i=1 1 aibi<0 -1 n n i=1 1 aici<0 ≤ 1 n n i=1 1 bici<0 .
Definition 3. Given a primal solution β(λ) for parameter λ and a primal point β (λt) returned by an algorithm, we define the gap on the validation error between λ and λ t as λt) ) .

∆E v (λ t , λ) := E v ( β(λ) ) -E v (β (
(13)

Suppose we have fixed a tolerance v on the gap on validation error i.e., ∆E v (λ t , λ) ≤ v . Based on Assumption A1, if there is a region R λ that contains the optimal solution β(λ) at parameter λ, then we have

∆E v (λ t , λ) ≤ L(X β(λ) , X β (λt) ) ≤ max β∈R λ L(X β, X β (λt) ) .
A simple strategy consists in choosing R λ as a ball.

Lemma 4 (Gap safe region [START_REF] Ndiaye | Gap safe screening rules for sparsity enforcing penalties[END_REF]). Under Assumption A2, any primal solution β(λ) belongs to the Euclidean ball with center β (λt) and radius

r t,µ (λ) = 2 µ G λ (β (λt) , θ (λt) ) . ( 14
)
Such a ball relying on a duality gap evaluation has been recently proved useful to speed-up sparse optimization solvers. Their good performance comes from their ability to iteratively identify the sparsity structure of the optimal solutions, and are referred to as safe screening rules as they provide safe certificates for such structures [START_REF] El Ghaoui | Safe feature elimination in sparse supervised learning[END_REF][START_REF] Fercoq | Mind the duality gap: safer rules for the lasso[END_REF][START_REF] Shibagaki | Simultaneous safe screening of features and samples in doubly sparse modeling[END_REF][START_REF] Ndiaye | Gap safe screening rules for sparsity enforcing penalties[END_REF].

Since the radius in Equation ( 14) depends explicitly on the duality gap, we can sequentially track a range of parameters for which the gap on the validation error remains below a prescribed tolerance by controlling the optimization error.

Proposition 7 (Grid for prescribed validation error).

Under Assumptions A1 and A2, let us define

v,µ =      µ 2 × v X 2 (regression) µ 2 × x ( n v +1) β (λ t ) x ( n v +1) 2 (classification)
where

x ( n v +1) β (λ t ) x ( n v +1)
2 is the ( n v + 1)-th smallest value of

x i β (λ t ) x i 2 for i ∈ [n ]. Given (β (λt) , θ (λt) ) such that G t ≤ v,µ , we have ∆E v (λ t , λ) ≤ v for all λ ∈ λ t × 1 -ρ t ( v,µ ), 1 + ρ r t ( v,µ ) ,
where ρ t ( v,µ ), ρ r t ( v,µ ) are defined in Proposition 1. Remark 3. Considering the current regularization parameter λ t , we have

∆E v (λ t , λ t ) = E v ( β(λt) ) -E v (β (λt) ) ≤ v , Algorithm 2 v -path for Validation Set Input: f, Ω, v , [λ min , λ max ] Compute v,µ as in Proposition 7 Λ( v,µ ) = training path (f, Ω, v,µ , [λ min , λ max ]) Return: Λ( v,µ )
as soon as G t ≤ v,µ , which gives us a stopping criterion for solving the optimization problem on the training set (X, y) relative to the desired accuracy v on the validation set (X , y ). This point of view has the appealing property of relieving the practitioner from selecting the stopping criterion c while optimizing on the training set.

Algorithm 2 outputs a discrete set of parameters Λ( v,µ ) s.t. {β (λt) for λ t ∈ Λ( v,µ )} is an v -path for the validation error. Thus, for any λ in [λ min , λ max ], there exists

λ t ∈ Λ( v,µ ) such that E v (β (λt) ) -v ≤ E v ( β(λ) ) .
The following proposition is obtained by taking the minimum on both sides of the inequality.

Proposition 8. Under Assumptions A1 and A2, {β (λt) for λ t ∈ Λ( v,µ )} is an v -path for the error and

min λt∈Λ( v,µ ) E v (β (λt) ) - min λ∈[λmin,λmax] E v ( β(λ) ) ≤ v .

Numerical experiments

We illustrate our method on 1 -regularized least squares and logistic regression by comparing the computational times and number of grid points needed to compute an -path for a given range [λ min , λ max ].

We first consider the default grid in sklearn (Pedregosa et al., 2011) and glmnet [START_REF] Friedman | Regularization paths for generalized linear models via coordinate descent[END_REF] which is defined as λ t = λ max ×10 -δt/(T -1) (here δ = 3). Thanks to Proposition 2, we measure the approximation path error of the default grid of size T and report the times and numbers of grid points T needed to achieve a smaller approximation error. Our experiments were conducted on the following datasets: leukemia, available in sklearn and the climate data NCEP/NCAR Reanalysis [START_REF] Kalnay | The NCEP/NCAR 40-year reanalysis project[END_REF]. Results are reported in Figure 3 for both classification and regression problem. Our approach leads to a better approximation of the regularization path w.r.t. the default grid, as larger steps are obtain at each λ t . This often results in a significant gain in computating time.

The convergence of our method is illustrated for Elasatic Net in Figure 4 on synthetic databases generated with sklearn as a random regression problem make regression and make sparse uncorrelated (with low number of informative features) presented in [START_REF] Celeux | Regularization in regression: comparing bayesian and frequentist methods in a poorly informative situation[END_REF]. For a decreasing sequence of validation errors, we represent the hyperparameter selected by our algorithm and its corresponding safe interval. Note that, even if the validation curve is often non smooth and non convex, the output of the safe grid search converges to the global minimum as guaranteed in Proposition 8.

Generalized self-concordant functions

Proposition 9 [START_REF] Sun | Generalized selfconcordant functions: A recipe for newton-type methods[END_REF], Proposition 10). If (M f , ν)-generalized self concordant, then

w ν (-d ν (x, y)) y -x 2 x ≤ f (y) -f (x) -∇f (x), y -x ≤ w ν (d ν (x, y)) y -x 2 x ( 15
)
where the right-hand side inequality holds if d ν (x, y) < 1 for the case ν > 2 and where

d ν (x, y) := M f y -x 2 if ν = 2, ν 2 -1 M f y -x 3-ν 2 y -x ν-2 x if ν > 2, ( 16
)
and

w ν (τ ) :=            e τ -τ -1 τ 2 if ν = 2, -τ -log(1-τ ) τ 2 if ν = 3, (1-τ ) log(1-τ )+τ τ 2 if ν = 4, ν-2 4-ν 1 τ ν-2 2(3-ν)τ (1 -τ ) 2(3-ν) 2-ν -1 -1 otherwise. (17)
Remark 4. The dual of the logistic loss is Generalized Self-Concordant with 6.2 Proof of the bounds for the warm start error and approximation path error Lemma 1. We assume that -λθ

M f * = 1, ν = 4. -10 -8 -6 -4 -2 0
w ν (τ ) ν =2 ν =3 ν =4 ν =5 ν =6
(λt) ∈ dom f * and X θ (λt) ∈ dom Ω * . If f * is V f * -smooth (resp. U f * -convex),
then, for ρ = 1λ/λ t , the right (resp. left) hand side of Inequality (18) holds true

Q t,U f * (ρ) ≤ G λ (β (λt) , θ (λt) ) ≤ Q t,V f * (ρ). (18)
Proof. We recall that G t := G λt (β (λt) , θ (λt) ) and we denote for simplicity λt) , θ (λt) ) and Γ t := Ω(β (λt) ) + Ω * (X θ (λt) ) .

G λt λ := G λ (β (
By definition for any (β, θ)

∈ dom P λ × dom D λ we have G λ (β, θ) = f (Xβ) + f * (-λθ) + λ(Ω(β) + Ω * (X θ)), so the following holds 1 λ t [G t -f (Xβ (λt) ) -f * (-λ t θ (λt) )] = Γ t . (19)
Hence using Equality (19) in the definition of G λt λ , we have:

G λt λ = f (Xβ (λt) ) + f * (-λθ (λt) ) + λΓ t (19) = λ λ t G t + 1 - λ λ t [f (Xβ (λt) ) + f * (-λ t θ (λt) )] + f * (-λθ (λt) ) -f * (-λ t θ (λt) ).
Let us write the proof for the upper bound (the proof for the lower bound is similar). We apply the smoothness property and the Fenchel-Young Inequality ( 22) to the function f * (•) with z = -λθ (λt) and x = ζ t := -λ t θ (λt) to obtain

G λt λ ≤ λ λ t G t + 1 - λ λ t ∆ t + V f * ,ζt (λ t -λ)θ (λt) ,
where we have used the equality case in the Fenchel-Young Inequality (20) to get:

∆ t = f (Xβ (λt) ) + f * (ζ t ) + ∇f * (ζ t ), -ζ t = f (Xβ (λt) ) -f (∇f * (ζ t )) .
We conclude by noticing that

λ λt G t + 1 -λ λt ∆ t = G t + 1 -λ λt (∆ t -G t ).
Proposition 2 (Precision for a Given Grid). Given a grid of parameter Λ T , the set {β (λ) : λ ∈ Λ T } is an

Λ T -path and Λ T ≤ max t∈[T ] Q t,V f * (1 -λ t /λ t ) where for all t ∈ [T -1], λ t is the largest λ ∈ [λ t+1 , λ t ] such that Q t,V f * (1 -λ/λ t ) ≥ Q t+1,V f * (1 -λ/λ t+1 ).
Proof. From the upper bound G λ (β (λt) , θ (λt) ) ≤ Q t,V f * (1λ/λ t ) for all λ and λ t , and since one can partition the parameter set as [λ min , λ max ] = ∪ t∈[0:T -1] [λ t+1 , λ t ], we have

Λt ≤ max t∈[0:T -1] sup λ∈[λt+1,λt] min λt∈Λ T Q t,V f * (1 -λ/λ t ) ≤ max t∈[0:T -1] sup λ∈[λt+1,λt] min t ∈{t+1,t} Q t ,V f * (1 -λ/λ t ) .
where the last inequality holds since {λ t+1 , λ t } is a subset of Λ T . Let us define

∀λ ∈ [λ t+1 , λ t ], ψ t (λ) := min{Q t+1,V f * (1 -λ/λ t+1 ), Q t,V f * (1 -λ/λ t )} . The quantity Q t+1,V f * (1-λ/λ t+1 ) (resp. Q t,V f * (1-λ/λ t )
) is monotonically increasing w.r.t. λ (resp. decreasing), so sup λ∈[λt+1,λt] ψ t (λ) is reached for the largest λ satisfying

Q t,V f * (1 -λ/λ t ) ≥ Q t+1,V f * (1 -λ/λ t+1 ) .
Corollary 1. If the function f * is ν 2 • 2 -smooth, the left (ρ t ) and right (ρ r t ) step sizes defined in Proposition 1 have closed-form expressions:

ρ t = 2νδ t ζ t 2 + δ2 t -δt ν ζ t 2 , ρ r t = 2νδ t ζ t 2 + δ2 t + δt ν ζ t 2 , where δ t := -G t and δt := ∆ t -G t . Proof. If f * is ν 2 • 2 -smooth (which is equivalent to f is 1 2ν • 2 -strongly convex), we have from Lemma 1 G λ (β (λt) , θ (λt) ) ≤ Q t,V f * (ρ) = G t +ρ(∆ t -G t ) + νρ 2 2 ζ t 2 .
Hence we conclude by solving in ρ the inequality Q t,V f * (ρ) ≤ .

Useful convexity inequalities

Lemma 5 (Fenchel-Young inequalities). Let f be a continuously differentiable function. For all x, x * , we have

f (x) + f * (x * ) ≥ x * , x , (20)
with equalities if and only if x * = ∇f (x) (or equivalently x = ∇f * (x * )). Moreover, if f is U f,x -convex (resp.

V f,x -smooth) Inequality (21) (resp. Inequality ( 22)) holds true:

f (x) + f * (x * ) ≥ x * , x + U f,x (x -∇f * (x * )), (21)
f (x) + f * (x * ) ≤ x * , x + V f,x (x -∇f * (x * )). ( 22
)
Proof. We have from the U f,x -convexity and the equality f

(z) + f * (∇f (z)) = ∇f (z), z -f * (∇f (z)) + ∇f (z), x + U f,x (x -z) = f (z) + ∇f (z), x -z + U f,x (x -z) ≤ f (x).
We conclude by applying the inequality at z = ∇f * (x * ) and remark that ∇f (z) = x * . The same proof holds for the upper bound ( 22).

Applying Fenchel-Young Inequalities ( 21) and ( 22) give the following bounds.

Lemma 6. We assume that -λθ ∈ Dom(f * ) and X θ ∈ Dom(Ω * ). Then, the Inequality (23) (resp. ( 23))

provided that f is U f -convex (resp. V f -smooth). λ Ω(β, θ) + U f (Xβ -∇f * (-λθ)) ≤ G λ (β, θ) (23) λ Ω(β, θ) + V f (Xβ -∇f * (-λθ)) ≥ G λ (β, θ) (24)
where Ω(β, θ) = Ω(β) + Ω * (X θ) + β, -X θ .

Proof. We apply the Fenchel-Young Inequality ( 21) to obtain

G λ (β, θ) =f (Xβ) + f * (-λθ) + λ(Ω(β) + Ω * (X θ)) ≥ Xβ, -λθ + U f (Xβ -∇f * (-λθ)) + λ(Ω(β) + Ω * (X θ)) =U f (Xβ -∇f * (-λθ)) + λ Ω(β) + Ω * (X θ) + β, -X θ .
The same technique applies for the upper bound with the Fenchel-Young Inequality (22).

Remark 5. From the Fenchel-Young Inequality (20), we have Ω(β) + Ω * (X θ) ≥ β, X θ , so the lower bound is always non negative.

Variation of the loss function along the path Lemma 7. Let β (λt) (resp. β (λ t ) ) be an -solution at parameter λ t (resp. λ t ), then we have

1 - λ t λ t f (Xβ (λ t ) ) -f (Xβ (λt) ) ≤ G t + λ t λ t G t .
where G s := G λs (β (λs) , θ (λs) ) for s ∈ {t, t }. Moreover, the mapping λ → f (X β(λ) ) is non-increasing.

Proof. Since β(λ) is optimal at parameter λ, we have:

f (Xβ (λ) ) + λΩ(β (λ) ) -≤ f (X β(λ) ) + λΩ( β(λ) ) ≤ f (Xβ (λt) ) + λΩ(β (λt) ) . Moreover, f (Xβ (λt) ) + λΩ(β (λt) ) = λ λ t f (Xβ (λt) ) + λ t Ω(β (λt) ) + 1 - λ λ t f (Xβ (λt) ) ≤ λ λ t f (X β(λt) ) + λ t Ω( β(λt) ) + + 1 - λ λ t f (Xβ (λt) ) ≤ λ λ t f (Xβ (λ) ) + λ t Ω(β (λ) ) + + 1 - λ λ t f (Xβ (λt) ) .
The last inequality comes from the optimality of β(λt) at parameter λ t . Hence,

f (Xβ (λ) ) + λΩ(β (λ) ) -≤ λ λ t f (Xβ (λ) ) + λ t Ω(β (λ) ) + + 1 - λ λ t f (Xβ (λt) ) .
At optimality, = 0 and we can deduce that 1 -λ λt f (X β(λ) ) ≤ 1 -λ λt f (X β(λt) ), hence the second result.

Bounding the gradient along the path

We can furthermore bound the norm of the gradient of the loss when the parameter λ varies.

Lemma 8. For x ∈ Dom(f ), if f is V f,x -smooth, then writing V * f,x = (V f,x ) * for the Fenchel-Legendre transform, one has V * f,x (-∇f (x)) ≤ f (x) -inf z f (z) .
Proof. From the smoothness of f , we have

inf z f (z) ≤ inf z (f (x) + ∇f (x), z -x + V f,x (z -x)) = f (x) -(V f,x ) * (-∇f (x)) .
A direct application of Lemma 8 and Lemma 7 yields:

Lemma 9. Assume that f is uniformly smooth and let β (λ t ) (resp. β (λt) ) be an -solution at parameter λ t (resp. λ t ). Then for δ (λ t , λ t ) := λt+λ t λt-λ t , we have

V * f (-∇f (Xβ (λ t ) )) ≤ f (Xβ (λt) ) + δ (λ t , λ t ) .
At optimality = 0 and so δ (λ t , λ t ) = 0 and we have

V * f (-∇f (X β(λ t ) )) ≤ f (X β(λt) ).
Lemma 10. Assuming f is uniformly smooth and ρ

t ( ) = 1 -λ t λt , we have ∇f (Xβ (λ t ) ) ≤ R t . If in addition, f is uniformly convex, we have ∆ t ≤ ∆ t .
Proof. If f is uniformly smooth, from Lemma 9, we have:

V * f (-∇f (Xβ (λ t ) )) ≤ f (Xβ (λt) ) + δ (λ t , λ t ) ∇f (Xβ (λ t ) ) * ≤ V * f -1 f (Xβ (λt) ) + 2 ρ t ( ) =: R t
where the first line follows from Lemma 9 and the second follows from the fact that for

V f = V • • , we have V * f := (V f ) * = V * • • * and since λ t ≤ λ t , then δ (λ t , λ t ) ≤ 2 λ t /(λ t -λ t ) = 2 /ρ t ( ). Since f is convex, we have ∆ t := f (Xβ (λt) ) -f (∇f * (-λ t θ (λt) )) ≤ -∇f (Xβ (λt) ), ∇f * (-λ t θ (λt) ) -Xβ (λt) ≤ ∇f (Xβ (λt) ) * ∇f * (-λ t θ (λt) ) -Xβ (λt) ≤ ∇f (Xβ (λt) ) * × U -1 f (G λt (β (λt) , θ (λt) ))
where the two last inequalities comes from Holder inequality and Lemma 6.

Proof of the complexity bound

We denote T the cardinality of the grid returned by Algorithm 1 and let (ρ t ) t∈[0:T -1] be the set of step size needed to cover the interval [λ min , λ max ]. Using ρ t = 1 -λt+1 λt , we have log

λ max λ min = log T -1 t=0 λ t λ t+1 = T -1 t=0 log 1 1 -ρ t .
Hence, denoting ρ min ( ) = min t∈[0:T -1] ρ t , we have

T × ρ min ( ) ≤ log λ max λ min . (25)
Moreover, to simplify our analysis we will suppose that at each step λ t , we have solved the optimization problem with two measures of accuracy G t ≤ c and ∆ t ≤ c for c < . Also, we assume that we explore the parameter range in decreasing order. Then we recall from Lemma 1 that G

λ (β (λt) , θ (λt) ) ≤ Q t,V f * (ρ) which is smaller than as soon as V f * ,ζt (-ζ t • ρ) ≤ -c . Since ρ min ( ) = min t∈[0:T -1] ρ t = min t∈[0:T -1] sup{ρ : Q t,V f * (ρ) ≤ }, then ρ min ( ) ≥ min t∈[0:T -1] sup{ρ : V f * ,ζt (-ζ t • ρ) ≤ -c } . ( 26
)
Hence the complexity of the path is bounded as follows.

Proposition 6 (Complexity of the approximation path). For c < , there exists

C f ( c ) > 0 such that T ≤ log λ max λ min × C f ( c ) W f * ( -c ) ,
where for all t > 0, the function W f * is defined by

W f * =      V -1 f * , if f is uniformly convex and smooth √ •, if f is Generalized Self-Concordant
and uniformly-smooth.

Moreover, C f ( c ) tends to a finite constant C f when c goes to 0.

Proof. In the uniformly convex case, V f * ,ζt (-ζ t • ρ) = V f * (ρ ζ t * ), hence we can deduce from Equation ( 25) and (26) that

T ≤ 1 ρ min ( ) × log λ max λ min ≤ log λ max λ min × max t∈[0:N -1] ζ t * V -1 f * ( -c )
, so we just need to uniformly bound ζ s . By construction of the dual point Lemma 2, we have:

ζ t * = λ t max(λ t , σ • dom Ω * (X ∇f (Xβ (λt) )) ∇f (Xβ λt ) * ≤ ∇f (Xβ λt ) * ≤ R 0 , (27)
where the last inequality comes from Lemma 10.

For the Generalized Self-Concordant case, we first recall that the functions w ν (•) in Equation ( 17) are increasing and w ν (0) = 1/2. Then there exists a positive constant a ν such that w ν (τ ) ≤ 1 for τ ∈ [0, a ν ] (in fact a ν = 1 for the logistic regression). Thus, provided ρd ν (ζ t ) ≤ a ν , we can derive the bound V f * (-ζ t × ρ) ≤ ρ 2 ζ t 2 ζt . Like in the uniformly convex case, in order to get the complexity of the -path, we also need a uniform bound on ζ t ζt . By taking (6) on f * with x = ζ t and z = 0, we obtain Proposition 7 (Grid for a prescribed validation error). Suppose that we have solved problem (1) for a parameter λ t up to accuracy G λt (β (λt) , θ (λt) ) ≤ ξ( v , µ, X ), then we have ∆E v (λ t , λ) ≤ v for all λ ∈ λ t × 1ρ t (ξ( v , µ, X )), 1 + ρ r t (ξ( v , µ, X ))

where ρ t ( ) and ρ r t ( ) for > 0 are defined in Proposition 1.

Proof. We distinguish the two cases of interest: classification and regression.

• Case where the loss function is a norm:

we have max β∈B(β (λ t ) ,r)

L(X β, X β (λt) ) = max β∈B(β (λ t ) ,r)

X (ββ (λt) ) ≤ r λ,µ X where r λ,µ is the duality gap safe radius defined in Equation ( 14). Hence by using the bounds on the duality gap in Lemma 1, we can ensure ∆E v (λ t , λ) ≤ v for all ρ = 1λ/λ t such that Q t,V f * (ρ) ≤ µ 2 v 2 X 2 . • Case where the loss function is the indicator function: using the inequality -2ab ≤ (ab) 2b 2 for a = x i β and b = x i β (λt) and |x i (ββ (λt) )| ≤ r x i for all β ∈ B(β (λt) , r) we have:

-2(x i β)(x i β (λt) ) ≤ (r x i ) 2 -(x i β (λt) ) 2 .

Hence we obtain the following upper bound max β∈B(β (λ t ) ,r) L(X β, X β (λt) ) = max β∈B(β (λ t ) ,r)

1 n n i=1 1 (x i β (λ t ) )(x i β)<0 ≤ 1 n n i=1 1 |x i β (λ t ) |≤r x i .
By using the bound on the duality gap, we can ensure ∆E v (λ 0 , λ) ≤ v for all λ such that:

#    i ∈ [n] : ξ i := µ 2 x i β (λt) x i 2 ≤ Q t,V f * (1 -λ/λ t )    ≤ n v .
By denoting ξ (i) i∈[n] the (increasing) ordered sequence, we need the inequality to be true for at most the n v first values i.e., we choose λ such that:

Q t,V f * 1 - λ λ t < µ 2
x ( n v +1) β (λt) x ( n v +1) 2 .

  Exact: P λ ( β(λ) )Exact shifted: P λ ( β(λ) ) + Approximated: P λ (β (λ) )

  1 least-squares regression on climate data set NCEP/NCAR Reanalysis whith n = 814 observations and p = 73577 features. 1 logistic regression on leukemia data set with n = 72 observations and p = 7129 features.

Figure 3 :

 3 Figure 3: Computation of the approximation path at the same error than the default grid.

  Synthetic data set generated with sklearn as X, y = make sparse uncorrelated(n = 30, p = 50).

  Synthetic data set generated with sklearn as X, y = make regression(n = 500, p = 5000).

Figure 4 :

 4 Figure4: Safe selection of the optimal hyperparameter for Elastic Net regression when the targeted accuracy v on the validation set (30% of the observations) is refined. The range of parameters investigated is generated by Algorithm 2 (with bilateral path) between λ max = X y ∞ and λ min = λ max /100. Note that for loose precision, suboptimal parameter are identified, but better and better candidates are found as the accuracy v decreases.

Figure 5 :

 5 Figure 5: Illustration of the functions in self concordant bounds Equation (17)

  w ν (-d ν (ζ t )) ζ t 2 ζt = U f * ,ζt (-ζ t ) ≤ f * (0)f * (ζ t ) -∇f * (ζ t ), -ζ t = f (∇f * (ζ t )) = f (Xβ (λt) ) -∆ t ≤ f (Xβ (λt) ) + c ≤ f (Xβ (λ0) ) + 2 c ρ 0 ( ) + c =: R0where we used the inequality case of Fenchel-Young Inequality and the fact thatf * (0) =inf f = 0. This shows that ψ(ζ t ) := U f * ,ζt (-ζ t ) ≤ R0 .Since the function ψ is continuous, then its level set is closed i.e., {z ∈ R n : ψ(z) ≤ R0 } is closed. Recalling Equation (27), we have ζ t * ≤ R 0 . Then we haved ν (ζ t ) ≤ sup z∈H f d ν (z) =: B f where H f := {z ∈ R n : ψ(z) ≤ R0 } ∩ {z : z * ≤ R 0 } is a compact set.Since the function w ν (•) is increasing, we havew ν (-B f ) ζ t 2 ζt ≤ w ν (-d ν (ζ t )) f ) . Thus, provided ρd ν (ζ t ) ≤ āν , we can derive the bound V f * (ζ t × ρ) ≤ ρ 2 ζ t2ζt . Whence ρ min ( ) ≥ min t of the validation error bounds

we assume a decreasing order λt+1 < λt, reflecting common practices for GLM, e.g., for the Lasso.

the data-fitting terms might differ from training to testing; for instance for logistic regression one would use the 0/1 -loss for validation but optimize the logistic function at training.

Acknowledgements

This work was supported by the Chair Machine Learning for Big Data at Télécom ParisTech. TL acknowledges the support of JSPS KAKENHI Grant number 17K12745.


Abderrahman Mokni
email: abderrahman.mokni@mines-ales.fr

Marianne Huchard
email: huchard@lirmm.fr

Christelle Urtado
email: christelle.urtado@mines-ales.fr

Vauttier + Sylvain
email: sylvain.vauttier@mines-ales.fr

Yulin Zhang
email: yulin.zhang@u-picardie.fr

Formal rules for reliable component-based architecture evolution

Keywords: software architecture evolution, component reuse, consistency checking, coherence checking, evolution rules, formal models, abstraction level, B formal language

Software architectures are the blueprint of software systems construction and evolution. During the overall software lifecycle, several changes of its architecture may be considered (e.g. including new software requirements, correcting bugs, enhancing software performance). To ensure a valid and reliable evolution, software architecture changes must be captured, verified and validated at an early stage of the software evolution process. In this paper, we address this issue by proposing a set of evolution rules for software architectures in a manner that preserves consistency and coherence between abstraction levels. The rules are specified in the B formal language and applied to a three-level Adl that covers the three steps of software development: specification, implementation and deployment. To validate our rules, the approach is tested on a running example of Home Automation Software.

Introduction

The great importance of evolution and maintenance in software systems engineering has been noticed over more than two decades ago. According to a highly cited survey conducted by Lientz and Swanson in the late 1970s [START_REF] Lientz | Characteristics of application software maintenance[END_REF], it has been proven that software maintenance represents the main part of a software lifecycle in terms of cost and time. In particular, this high fraction relates to componentbased software engineering that tackles the development of complex software architectures (thanks to modularity, abstraction and reuse). Indeed, an ill mastered software system maintenance or a misconception during its evolving process may lead to serious architectural mismatches and inconsistencies. A famous problem that software architecture evolution is subject to is erosion. Introduced by Perry and Wolf [START_REF] Perry | Foundations for the study of software architecture[END_REF] in 1992 and studied over many years [START_REF] De Silva | Controlling software architecture erosion: A survey[END_REF], erosion can be defined as the deterioration or violation of architectural design decisions by the software implementation. It is usually due to software aging and an undisciplined evolution of its architecture. While a lot of work was dedicated to architectural modeling and evolution, there is still a lack of means and techniques to tackle architectural inconsistencies, and erosion in particular. Indeed, almost existing Adls hardly support the whole life-cycle of a component-based software and it often creates a gap between design and implementation, requirements and design or even both. These gaps make evolution harder and increase the risk of nonconformance between requirements, design and implementation hence leading to erosion. In previous work [START_REF] Zhang | Architecture-centric component-based development needs a three-level ADL[END_REF][START_REF] Zhang | A three-level component model in component-based software development[END_REF], we proposed Dedal, an Adl that supports the full lifecycle process of component-based software systems. Dedal proposes to model architectures at three abstraction levels that correspond to the three steps of software development: specification, implementation and deployment. However, at this stage the Adl handles evolution in an adhoc manner and lacks rigorous support for reliable and automatic software evolution. In this paper, we propose a set of evolution rules specified using the B formal language [START_REF] Abrial | The B-book: Assigning Programs to Meanings[END_REF] to automatically handle forward and reverse evolution among Dedal levels in a reliable way. We also show how evolution can be simulated at an early stage using the proposed rules, anticipating and preventing inconsistencies. The remainder of this paper is outlined as follows: Section 2 discusses related work. Section 3 gives a brief overview of Dedal architecture levels and their formalization. Section 4 presents the three-level evolution approach, illustrated by some evolution rules. Section 5 gives the simulation of an evolution scenario example using the proposed rules. Finally, Section 6 concludes the paper and discusses future work.

Related work

Over the two past decades, a wide area of related work has addressed the problem of software evolution. Indeed, many Adls have been proposed [START_REF] Medvidovic | A classification and comparison framework for software architecture description languages[END_REF]. Examples include C2SADL [START_REF] Medvidovic | ADLs and dynamic architecture changes[END_REF], Wright [START_REF] Allen | A formal basis for architectural connection[END_REF], Rapide [START_REF] Luckham | Specification and analysis of system architecture using rapide[END_REF], ACME [START_REF] Garlan | ACME: An architecture description interchange language[END_REF], Darwin [START_REF] Magee | Dynamic structure in software architectures[END_REF] and π-ADL [START_REF] Oquendo | {Pi-ADL}: An architecture description language based on the higherorder typed pi-calculus for specifying dynamic and mobile software architectures[END_REF]. While "box-and-line" seems to be the easiest way to represent architectures for practitioners [START_REF] Shaw | Formulations and formalisms in software architecture[END_REF], this notation is informal and leads to ambiguity and imprecision. For this reason, the use of a formalism and its integration into an Adl is crucial. To cope with software evolution and particularly dynamic change, existing Adls use several kinds of formal ground depending on their application domain. For instance, C2SADL uses event-based processes to model concurrent systems while Dynamic-Wright lies on CSP [START_REF] Hoare | Communicating sequential processes[END_REF], a process algebra formalism to support the specification and analysis of interactions between components. ACME, which was basically designed to define a common interchange language for architecture design tools, is based on first-order logic. The Adl was extended with Plastik [START_REF] Joolia | Mapping ADL specifications to an efficient and reconfigurable runtime component platform[END_REF] to support dynamic reconfiguration of architectures. π-ADL was designed for concurrent and mobile systems. It lies on π-calculus [START_REF] Milner | A calculus of mobile processes[END_REF], a higher-order logic formalism to model and evolve the behavior of the architectures. C2SADL, Pi-ADL, ACME and Dynamic-Wright support dynamic recon-figuration of architectures. However, they lack analysis support for the evolution activity and hardly cover the whole lifecycle of component-based software. In our work, we propose a solution for the simulation and verification of software architecture evolution using B [START_REF] Abrial | The B-book: Assigning Programs to Meanings[END_REF] formal models. The choice of B is motivated by its rigorism (first-order logic) and its expressiveness that enables modeling concepts in a reasonable easy way. The B formal models correspond to the definitions of our three-level Dedal Adl that covers the whole lifecycle of a software system (i.e. specification, implementation and deployment). Hence, we address both static and dynamic evolution by proposing change rules at each of the three abstraction levels of our Adl.

Overview of Dedal

Dedal abstraction levels

Dedal is a novel Adl that covers the whole life-cycle of a component-based software. It proposes a three-step approach for specifying, implementing and deploying software architectures as a reuse-based process(cf. Figure 1). To illustrate the concepts of Dedal, we propose to model a home automation software (Has) that manages comfort scenarios. Here, it automatically controls the building's lighting and heating in function of the time and ambient temperature.

For this purpose, we propose an architecture with an orchestrator component that interacts with the appropriate devices to implement the desired scenario.

The abstract architecture specification is the first level of software architecture descriptions. It represents the architecture as imagined by the architect to meet the requirements of the future software. In Dedal, the architecture specification is composed of component roles, their connections and the expected global behavior. Component roles are abstract and partial component type specifications. They are identified by the architect in order to search for and select corresponding concrete components in the next step. The instantiated architecture assembly describes software at runtime and gathers information about its internal state. The architecture assembly results from the instantiation of an architecture configuration. It lists the instances of the component and connector classes that compose the deployed architecture at runtime and their assembly constraints (such as maximum numbers of allowed instances). Component instances document how component classes in an architecture configuration are instantiated in the deployed software. Each component instance has an initial and current state defined by a list of valued attributes. Figure 2-c shows an instantiated architecture assembly for the Has example.

Dedal formal model

Dedal is enhanced by a formal model using the B specification language. The proposed model covers all Dedal concepts and includes rules for substitutability and compatibility among each level as well as the rules that govern interrelations between the different levels (cf. Figure 3). These rules, which were discussed in previous work [START_REF] Mokni | Towards automating the coherence verification of multi-level architecture descriptions[END_REF], are the basis for controlling the evolution process. Indeed, evolution needs a subtyping mechanism to manage change locally (at the same abstraction level) and then, inter-level rules to propagate change to the other levels.

Fig. 3. Component interrelations in Dedal

For the sake of simplicity, we present in For instance, the concept of component is specialized into compRole at the specification level and the concept of architecture is specialized into configuration at the configuration level. This model is used to set generic evolution rules which are specialized for each of the three abstraction levels of Dedal. An evolution scenario is presented in Section 5 as an illustration.

The formal evolution approach

In this section, we present our approach to handle multi-level software evolution as a reuse-based process. The objective of this approach is twofold: (1) capture software change and control its impact on architecture consistency and, (2) propagate change between multiple architecture levels to preserve global coherence.

The approach is formal model-based since it relies on the formal models of our three-level Adl and uses consistency and coherence properties and a set of evolution rules (cf. Figure 4). The approach is also dynamic in the sense that it performs analysis and simulates change on executable models. The formal models may be generated through a Mde (Model Driven Engineering) process where the source models are textual or graphical (UML profile) descriptions of Dedal. Since the transformation is not tooled yet, this issue is out of the scope of the present paper. The evolution management is composed of three main activities: consistency analysis, inter-level coherence analysis and evolution rules triggering. In the re-Fig. 4. The formal evolution process mainder, we present the foundations and the mechanisms of each of these three activities.

Architecture consistency analysis

Taylor et al. [START_REF] Taylor | Software architecture: Foundations, Theory, and Practice[END_REF] define consistency as an internal property intended to ensure that different elements of an architectural model do not contradict one another. Usually, this property includes five sorts of consistency: name, interface, behavior, interaction and refinement consistency. Some properties such as parameters, names and interfaces are taken into account by adding constraints in the definition of our architectural formal model [START_REF] Mokni | Towards automating the coherence verification of multi-level architecture descriptions[END_REF]. In our approach, we focus on three main properties: name consistency, connection consistency, which includes interaction and compatibility between components, and architecture completeness.

Name consistency. This property ensures that each component belonging to the architecture holds a unique name and hence avoids conflicts when selecting components.

Connection consistency. This property ensures that all architecture connections are correct and satisfy compatibility between both sides (i.e. a required interface is always connected to a compatible provided one). In addition, connection consistency stipulates that the architecture graph is consistent (i.e. each component is connected to at least another one).

Architecture completeness. This property ensures that the architecture realizes all its functional objectives. From an internal point of view, completeness is satisfied when all the required services in the architecture are met. Structurally, it means that all the required interfaces are connected to a compatible provided one.

When a change occurs, the analyzer checks all the aforementioned properties and notify the evolution manager in case a violation is detected. Then, the adequate evolution rules are triggered to reestablish architecture consistency.

The properties are defined using B, a first order set-theoretic formalism and hence analysis is performed using a B model checker.

Inter-level coherence properties

Coherence analysis is managed using inter-level rules (cf. Figure 5). These rules are defined to check whether a configuration conforms to its specification or a software instantiation is coherent with its configuration. Coherence between specification and configuration. A specification is a formal description of software requirements that is used to guide the search for suitable concrete component classes to implement the software. An architecture definition is coherent when all component roles are realized by component classes in the configuration. This results in a many-to many relation. Indeed, several component roles may be realized by a single component class while, conversely, a composition of component classes may be needed to realize a single role. Formally:

implements ∈ conf iguration ↔ specif ication ∧ ∀ (Conf, Spec).(Conf ∈ configuration ∧ Spec ∈ specification ⇒ (Conf, Spec) ∈ implements ⇔ ∀ CR.(CR ∈ compRole ∧ CR ∈ spec components(Spec) ⇒ ∃ CL.(CL ∈ compClass ∧ CL ∈ config components(Conf) ∧ (CL,CR) ∈ realizes)))
Coherence between configuration and assembly. Coherence between configuration and assembly levels is satisfied when all the classes of the configuration are instantiated at least once in the architecture assembly and, conversely, all instances of the assembly are instances of the component classes of the configuration. Formally:

instantiates ∈ assembly → conf iguration ∧ ∀(Asm, Conf ).(Asm ∈ assembly ∧ Conf ∈ conf iguration ⇒ ((Asm, Conf ) ∈ instantiates ⇔ ∀ CL.(CL ∈ compClass ∧ CL ∈ conf ig components(Conf ) ⇒ ∃ CI.(CI ∈ compInstance ∧ CI ∈ assm components(Asm) ∧ (CI, CL) ∈ comp instantiates)) ∧ ∀ CI.(CI ∈ compInstance ∧ CI ∈ assm components(Asm) ⇒ ∃ CL.(CL ∈ compClass ∧ CL ∈ conf ig components(Conf ) ∧ (CI, CL) ∈ comp instantiates)) ))
Coherence analysis comes after consistency checking returns a positive result. Indeed, it is necessary that software system descriptions are consistent at all abstraction levels before checking coherence between them. When a change occurs at any level, this may result in erosion or drift (for instance, some higher level decisions are violated or not taken into account by the lower level). The evolution manager is then notified about the detected incoherence and propagates the change to the incoherent levels using the adequate evolution rules.

Specifying evolution rules

An evolution rule is an operation that changes a target software architecture by the deleting, adding or substituting of one of its constituent elements (components and connections). These rules are specified using the B notation and each rule is composed of three parts: the operation signature, preconditions and actions. Architecture specification evolution. Evolving an architecture specification is usually a response to a new software requirement. For instance, the architect may need to add new functionalities to the system and hence add some new roles to the specification. Moreover, a specification may also be modified during the change propagation process to preserve coherence and keep an up-to-date specification description of the system that may be implemented in several ways. The proposed evolution rules related to the specification level are the addition, deletion and substitution of a component role and the addition and deletion of connections. The following role addition rule is an example of evolution rules at specification level: Architecture configuration evolution. Change can be initiated at configuration level whenever new versions of software component classes are released. Otherwise, an implementation may also be impacted by change propagation either from the specification level, in response to new requirements, or from the assembly level, in response to a dynamic change of the system. Indeed, a configuration may be instantiated several times and deployed in multiple contexts. At configuration level, there is a need for two more evolution rules: the connection and the disconnection of the exposed services. Indeed, a component class used in a configuration may hold more provided interfaces than the component role that it implements. These extra interfaces may be left unconnected. On the contrary, a specification sets by definition the requirements, and hence the provided interfaces of all roles must be connected to keep the architecture consistent. As an example of evolution rule at configuration level, we list the following component class substitution rule: Architecture assembly evolution. Since the architecture assembly represents the software at runtime, evolving software at assembly level is a dynamic evolution issue. Several kinds of change may occur at runtime. For instance, dynamic software change may be needed due to a change in the execution context (e.g. lack of memory, CPU). Unanticipated changes are one of the most important issues in software evolution. Indeed, some software systems have to be self-adaptive to keep providing their functions despite environmental changes. This issues are handled by the evolution manager which monitors the execution state of the software through its corresponding formal model. It then triggers the assembly evolution rules to restore consistency when it is violated. These rules include component instance deployment, component instance removal, component instance substitution, component instance connection / disconnection and service connection / disconnection. As an example of dynamic evolution rule, we state the following component instance addition rule:

replaceClass(config, oldClass, newClass) = PRE oldClass ∈ compClass ∧ newClass ∈ compClass ∧ config ∈ configuration ∧ oldClass ∈ config components(config) ∧ /*

Implementing an evolution scenario

To illustrate the use of evolution rules, we propose to evolve the Has architecture by adding of a new device that manages the building's shutters. The evolution simulation is performed using ProB [START_REF] Leuschel | ProB: An automated analysis toolset for the b method[END_REF], an animator and model checker of B models. Once the formal models corresponding to the three architecture descriptions are successfully checked, we use the ProB solver to trigger change as a goal to reach. In the remainder, we give some details about the example instances and the different steps of the evolution process. Initially, the instantiation of the formal Has specification is as follows: The change is requested by the execution of the the role addition operation that takes as arguments the HAS spec Has architecture specification and the Shutter (cr6) component role.

Intra-level change

addRole(HAS spec, cr6)

The change process is initiated by setting a goal. When the goal cannot be reached, the change process rolls back to the initial state of the architecture. In this case, the goal is to add a Shutter to the Has specification while maintaining architecture consistency (as defined in Section 4):

GOAL == changeOperation = ADDIT ION ∧ selectedRole = cr6 ∧ selectedSpec = HAS spec ∧ specif ication consistency
The change entails the disconnection of all servers, the deletion of the old orchestrator (cr4), the addition of the new orchestrator (cr4a) and finally the connection of all servers. These operations are automatically generated by the ProB solver:

disconnect(HAS spec, (cr4, rintILight), (cr1, pintILight)) disconnect(HAS spec, (cr4, rintIT ime), (cr2, pintIT ime)) disconnect(HAS spec, (cr4, rintIT herm1), (cr3, pintIT herm)) disconnect(HAS spec, (cr4, rintICon), (cr5, pintICon)) deleteRole(HAS spec, cr4) generateAddRole(HAS spec, cr4a) connect(HAS spec, (cr4, rintILight), (cr1, pintILight)) connect(HAS spec, (cr4, rintIT ime), (cr2, pintIT ime)) connect(HAS spec, (cr4, rintIT herm1), (cr3, pintIT herm)) connect(HAS spec, (cr4, rintICon), (cr5, pintICon)) connect(HAS spec, (cr4a, rintIShutter), (cr6, pintIShutter))

Propagating change to other levels

Once the change is successfully achieved at the specification level, the propagation rules are triggered in the other levels to attempt to restore coherence with the new specification architecture.

Propagating change to the HAS configuration. To restore conformity with the new Has specification, the new configuration must realize the added Shutter role and its connection to the orchestrator device to perform the new required behavior. In the given example, the solution is to search for a concrete component class that realizes the Shutter role and can be connected to a compatible orchestrator class. Initially, the Has configuration (illustrated by Figure 7) is formally instantiated as follows: Again, we use the ProB solver giving it the following goal to restore coherence property with the new Has specification:

GOAL == selectedConf ig = HAS conf ig ∧ conf iguration consistency ∧ specConf igCoherence
We note that specConfigCoherence is the conformity rule defined in Section 4 to check conformity between a specification and a configuration.

A potential solution generated by the solver is: Propagating change to the HAS assembly. In the same way, change is propagated to assembly level by disconnecting and deleting the instance of the old AndroidOrchestrator and by creating, deploying and connecting an instance of the new added Shutter device. The solver is given the following goal:

GOAL == selectedAssembly = HAS assembly ∧ assembly consistency ∧ assemblyConf igCoherence

The assemblyConfigCoherence is the defined property to check coherence between an assembly and a configuration (cf. Section 4). The solution generated by the solver is as follows:

unbind(HAS assembly, (ci4, rintILampInst), (ci1, pintILampInst1)) unbind(HAS assembly, (ci4, rintIIntensityInst), (cl1, pintIItensity1Inst)) unbind(HAS assembly, (ci4, rintILampInst), (ci2, pintILampInst2)) unbind(HAS assembly, (ci4, rintIIntensityInst), (ci2, pintIItensityInst2)) unbind(HAS assembly, (ci4, rintIClockInst), (ci1, pintIClockInst)) unbind(HAS assembly, (ci4, rintIT herm2Inst), (ci3, pintIT herm2Inst)) unbind(HAS assembly, (ci4, rintIConInst), (ci3, pintICon2Inst)) removeInstance(HAS assembly, ci4) deployInstance(HAS assembly, ci4a, cl4a, {}) bind(HAS assembly, (ci4a, rintILamp2Inst), (ci1, pintILampInst1)) bind(HAS assembly, (ci4a, rintIIntensity2Inst), (ci1, pintIItensityInst1)) bind(HAS assembly, (ci4a, rintIClockInst), (ci1, pintIClockInst)) bind(HAS assembly, (ci4a, rintILamp2Inst), (ci2, pintILampInst2)) bind(HAS assembly, (ci4a, rintIT herm3Inst), (ci3, pintIT herm2Inst)) bind(HAS assembly, (ci4a, rintICon2Inst), (ci3, pintICon2Inst)) bind(HAS assembly, (ci4a, rintIIntensity2Inst), (ci1, pintIItensityInst2)) bind(HAS assembly, (ci4a, rintIShutterInst), (ci6, pintIShutterInst))

At this stage, change is simulated and verified semi-automatically since the models are instantiated manually. Moreover, a manual checking is needed to validate the proposed evolution rules. A perspective is to fully automate the evolution management process and to study the scalability of the solver to timely handle complex goals.

Conclusion and future work

In this paper, we proposed a set of rules to evolve software architectures. These rules defined as a B formal model of our three-level Dedal Adl that covers the whole lifecycle of software systems. Our approach enables simulation and early validation of software evolution at design time (specification and implementation) as well as runtime (deployment). At this stage, the proposed consistency properties and evolution rules are checked and validated using a B animator and model checker. As a future work, we aim to extend the use of the proposed evolution rules in order to consider the semantics of changes. Another perspective is to generate multiple candidate evolution paths that can be evaluated using some criteria (e.g. quality of service, cost, change priority) as proposed by Barnes et al. [START_REF] Barnes | Evolution styles: foundations and models for software architecture evolution[END_REF]. We are also considering several MDE techniques to develop an eclipse-based environment for Dedal that automatically manages software architecture evolution.

Fig. 1 .

 1 Fig.1. Dedal overall process[START_REF] Zhang | A three-level component model in component-based software development[END_REF]

Figure 2 -

 2 a shows a possible architecture specification for the Has. In this specification, five component roles are identified. A component playing the Orchestrator role controls four components playing the Light, Time, Thermometer and CoolerHeater roles.

Fig. 2 .

 2 Fig. 2. Architecture specification, configuration and assembly of HAS

Figure 2 -

 2 Figure 2-b shows a possible architecture configuration for the Has example as well as an example of an AirConditioner composite component and its inner configuration. As illustrated in this example, a single component class may realize several roles in the architecture specification as with the AirConditioner component class, which realizes both Thermometer and CoolerHeater roles. Conversely, a component class may provide more services than those listed in the architecture specification as with the Lamp component class which, provides an extra service to control the intensity of light.The instantiated architecture assembly describes software at runtime and gathers information about its internal state. The architecture assembly results from the instantiation of an architecture configuration. It lists the instances of the component and connector classes that compose the deployed architecture at runtime and their assembly constraints (such as maximum numbers of allowed instances). Component instances document how component classes in an architecture configuration are instantiated in the deployed software. Each component instance has an initial and current state defined by a list of valued attributes. Figure2-cshows an instantiated architecture assembly for the Has example.

Fig. 5 .

 5 Fig. 5. Coherence between architecture levels

  addRole(spec, newRole) = PRE spec ∈ arch spec ∧ newRole ∈ compRole ∧ newRole ∈ spec components(spec) ∧ /* spec does not contain a role with the same name*/ ∀ cr.(cr ∈ compRole ∧ cr ∈ spec components(spec) ⇒ comp name(cr) ¬ comp name(newRole)) THEN spec servers(spec) := spec servers(spec) ∪ servers(newRole) || spec clients(spec) := spec clients(spec) ∪ clients(newRole) || spec components(spec) := spec components(spec) ∪ {newRole} END;

  The old component class can be substituted for the new one (verified by the component substitution rule)*/ newClass ∈ config components(config) ∧ (oldClass, newClass) ∈ class substitution THEN config components(config) := (config components(config) -{oldClass}) ∪ {newClass} || config clients(config) := (config clients(config)clients(oldClass)) ∪ clients(newClass) END

  deployInstance(asm, inst, class, state) = PRE asm ∈ assembly ∧ class ∈ compClass ∧ /* The instance is a valid instantiation of an existing component class*/ inst ∈ compInstance ∧ class = comp instantiates(inst) ∧ inst ∈ assm components(asm) ∧ /* The state given to the instance is a valid value assignment to the attributes of the instantiated component class*/ state ∈ P (attribute value) ∧ card(state) = card(class attributes(class)) ∧ /* The maximum number of allowed instances of the given component class is not already reached*/ nb instances(class) < max instances(class) THEN /*initial and current state initialization*/ initiation state(inst) := state || current state(inst) := state || /*updating the number of instances and the assembly architecture*/ nb instances(class) := nb instances(class) + 1 || assm components(asm) := assm components(asm) ∪ {inst} || assm servers(asm) := assm servers(asm) ∪ servers(inst) || assm clients(asm) := assm clients(asm) ∪ clients(inst) END;

Figure 6

 6 Figure 6 illustrates the old architecture specification and the evolved one.

Fig. 6 .

 6 Fig. 6. Evolving the HAS specification by role addition

Fig. 7 .

 7 Fig. 7. Change propagation to HAS configuration

Table 1 a

 1 generic formal model covering the underlying concepts of Dedal. COMPS ∧ comp name ∈ component → COMP NAMES ∧ comp interfaces ∈ component P(interf ace) ∧ /* A client (resp. server)is a couple of a component and an interface */ client ∈ component ↔ interface ∧ server ∈ component ↔ interface ∧ /* A connection is a relation between a client and a server */ connection ∈ client ↔ server ∧ /* An architecture has a set of components and connections */

	MACHINE Arch concepts
	INCLUDES Basic concepts
	SETS
	ARCHS; COM P S; COM P N AM ES
	VARIABLES
	architecture, arch components, arch connections, component,
	comp name, connection, comp interf aces, client, server
	arch clients, arch servers
	INVARIANT
	/* A component has a name and a set of interfaces */
	component ⊆

architecture ⊆ ARCHS ∧ arch components ∈ architecture → P(component) ∧ arch connections ∈ architecture → P(connection) /* Arch clients (resp. arch servers) lists the connected clients(reps. servers) within an architecture */ arch clients ∈ architecture → P (client) ∧ arch servers ∈ architecture → P (server) Specific B notations: ↔: relation : injection P(<set>): powerset of <set>

Table 1 .

 1 Formal specification of underlying concepts