Fabien Benureau
email: fabien.benureau@gmail.com

Pierre-Yves Oudeyer
email: yves.oudeyer@inria.fr

Diversity-Driven Selection of Exploration Strategies in Multi-Armed Bandits

We consider a scenario where an agent has multiple available strategies to explore an unknown environment. For each new interaction with the environment, the agent must select which exploration strategy to use. We provide a new strategy-agnostic method that treat the situation as a Multi-Armed Bandits problem where the reward signal is the diversity of effects that each strategy produces. We test the method empirically on a simulated planar robotic arm, and establish that the method is both able discriminate between strategies of dissimilar quality, even when the differences are tenuous, and that the resulting performance is competitive with the best fixed mixture of strategies.

I. MOTIVATION

We are given a black-box that takes inputs and produces outputs. We know the values the inputs can take, but we do not know which inputs produce which outputs. We do not even know which outputs can be produced. We are given the opportunity to sample the black-box a limited number of times. In this context, we propose to investigate the following question: how much diversity of outputs can be produced with the limited access we have?

This question defines an exploration problem. Here, the objective is to discover what outputs the black-box is capable to deliver. To answer such a problem is to provide an exploration strategy, i.e. a method that selects which inputs to experiment with on the black box, in order to produce a diversity of outputs.

In this paper, we interest ourselves with a scenario where we have multiple exploration strategies available, whose internal operational details are not specified, and we must select, for each available interaction with the environment-i.e., the black box-, which exploration strategy to use to generate the inputs to execute.

Stated differently, we have several exploration black-boxes and one environmental black-box, and we want to know which exploration black-box to use on the environmental black-box at each interaction, so as to maximize the diversity of the effects produced by the environmental black-box.

Two salient points are present in our problem statement. We consider exploration problems rather than learning ones. And we establish an objective of diversity, not one of control or of prediction or of fitness or of reward optimization. We briefly motivate these two stances in the following sections.

A. Diversity and Exploration

Behavioural diversity is a factor of individual robustness when facing an evolving environment. It ensures that the next time the environment changes some of the behaviours will remain relevant. At the population level, behavioural diversity provides variability even in the absence of genetic diversity.

This point was recently heeded by the evolutionary robotics community, which was facing, amongst others, two specific challenges: early convergence, when the evolutionary process would get trapped in local minima because of a deceptive fitness function, and bootstrapping problems where the first generation fails to produce rewarding behaviour, hence stalling the evolutionary process. The then solution, staging the fitness function [START_REF] Gomez | Incremental evolution of complex general behavior[END_REF][START_REF] Kodjabachian | Evolution and development of neural controllers for locomotion, gradient-following, and obstacle-avoidance in artificial insects[END_REF][START_REF] Urzelai | Incremental robot shaping[END_REF]-a method similar to reward shaping in reinforcement learning [START_REF] Dorigo | Robot shaping: developing autonomous agents through learning[END_REF][START_REF] Maja | Reward functions for accelerated learning[END_REF]-, was deemed impractical because requiring problem-specific fitness functions.

The solution came from replacing or modifying the fitness function to encourage behavioural diversity in the population of candidate solutions [START_REF] Delarboulas | Open-ended evolutionary robotics: An information theoretic approach[END_REF][START_REF] Doncieux | Beyond black-box optimization: a review of selective pressures for evolutionary robotics[END_REF][START_REF] Gomez | Sustaining diversity using behavioral information distance[END_REF][START_REF] Lehman | Exploiting open-endedness to solve problems through the search for novelty[END_REF][START_REF] Mouret | Encouraging behavioral diversity in evolutionary robotics: An empirical study[END_REF][START_REF] Trujillo | Discovering several robot behaviors through speciation[END_REF], a method proposed first in the classical evolutionary algorithm domain [START_REF] Goldberg | Simple genetic algorithms and the minimal, deceptive problem[END_REF][START_REF] Sareni | Fitness sharing and niching methods revisited[END_REF].

In infants, actively fostering diversity in our interaction with the environment through exploratory behaviour is pivotal: it allows to discover and investigate new phenomena and affordances before they are detected as such. For Eleanor Gibson [START_REF] Gibson | Exploratory behavior in the development of perceiving, acting, and the acquiring of knowledge[END_REF], babies are not endowed with the abilities to perceive affordances, but must spend their first years discovering affordances in their environment. For instance, children do not already know that mirror are special objects proposing unique and salient interactions. Instead they must discover their affordance through an unrealed exploration of their environment. This point is important: studying exploratory behaviours on their own-rather than in the context of a learning problemcan shed light on how problems are discovered in the environment in the first place, before they are acknowledged as learning activities.

One could argue that, after noticing the mirror particular nature, the exploratory behaviour of the child in front of the mirror is in fact highly structured, and follows the child-asa-scientist paradigm [START_REF] Gopnik | Scientific thinking in young children: Theoretical advances, empirical research, and policy implications[END_REF][START_REF] Gweon | Stretching to learn: Ambiguous evidence and variability in preschoolers exploratory play[END_REF][START_REF] Schulz | Serious fun: Preschoolers engage in more exploratory play when evidence is confounded[END_REF]. But as Cook points out, more ecological explanations are also available: "selective exploration of confounded evidence is advantageous even if children explore randomly (with no understanding of how to isolate variables)" [7, p. 352]. Therefore the mere production of behavioural diversity is a useful tool in broad and specific exploration.

One other reason to investigate exploration independently from learning: exploration can happen without learning. For instance, a robot randomly producing movements does not exhibit learning, yet exhibit an exploratory behaviour. Similarly, a robot following mindlessly the left wall of a maze explores the maze, and does it successfully to boot. And many vacuum robots available today explore their environment without learning them. In all those examples, exploration is present because the behaviour creates access to (new) information about the environment. That the information is not remembered or exploited is not an exploration issue, it is a learning one.

B. More Than One Exploration Strategy

Different environments lend themselves to different exploration strategies. In simple environments, doing random actions will be as effective as any other strategy. In more complex contexts, more elaborate strategies are needed.

The field of computational intrinsic motivation has developed an abundance of different motivational drives such as novelty, surprise, prediction error, predictive information or competence progress (see [START_REF]Intrinsically Motivated Learning in Natural and Artificial Systems[END_REF][START_REF] Oudeyer | Intrinsic motivation systems for autonomous mental development[END_REF] for reviews). Each of these drives express preferences over what is interesting in the world, and define specific exploration strategies.

Moreover, exploration, for a robot, may be possible through different means: asking for social guidance, observing a peer, or opting for self-exploration. Each of those venues may not be always available, and some, e.g. social guidance, may only be available for infrequent use.

This suggests that robots should be endowed with different exploration strategies to tackle complex environments. Furthermore, we argue that one should resist hiding the choice these strategies represent under a larger, monolithic, opaque exploration strategy. Indeed such a strategy would need to handle simultaneously how, what and possibly when to explore, three aspects which may need to be specifically mediated by other components of behaviour.

Therefore, agents having multiple available exploration strategies are justified. In this article, we propose a strategyagnostic method to select which strategy to choose in function of the empirical behaviour of each of them.

II. PROBLEM A. Environment

An environment, is formally defined as a function f from M to S. M is the motor space, a bounded hyperrectangle of R m , and represents a parameterization of the movements the robot can execute. S is the sensory space; it is a subset of R s . Effects and goals1 (desired effects) are elements of S.

A task is defined as a pair (f, n) with f : M → S the environment and n the maximum number of samples of f allowed, i.e. the number of inputs the exploration strategy can try on the environment.

B. Exploration

An exploration strategy evaluates the function f , n times, providing a sequence of elements of S, x 0 , x 1 , ..., x n-1 . Each x i is evaluated as y i = f (x i ), and y i is observed by the exploration strategy before x i+1 is chosen.

In order to evaluate the exploration strategy, we use an exploration measure C, that takes the behavioural trace of the agent as input, i.e., the actions executed and effects produced:

{(x i , y i )} 0≤i<n .
A common objective of the experimenter is to evaluate if the agent has obtained knowledge of all the possibilities of the environment. A good proxy for this is to evaluate the set of effects the agent was able to produce during the exploration. In other words, how well the image of f , f (M )-the reachable space-was sampled.

Since we do not assume that the agents have knowledge of the exploration problem they are examined under, or that they have knowledge of the exploration measures that are used to evaluate their behaviour, and since agents may explore the environment for their own purposes, and self-evaluate their behaviour according to their own metrics, the choice of an exploration measure is necessarily arbitrary. This consideration is not present for instance in reinforcement learning, where the cumulative reward defines an objective motivation for the agent, and an objective evaluation for the experimenter. In an exploration context, it is the responsibility of the experimenter to justify the interest and relevance of the selected exploration measure.

In this work, we select a diversity measure to evaluate the exploration. The importance of diversity for the development of humans and animals was argued above. And behavioural diversity has proven itself empirically in the field of evolutionary robotics. Absent an objective environmental reward for the agent's behaviour, and absent an assumption that the agent possesses specific learning abilities, encouraging diversity in behaviour is relevant in multiple ways. First, it does not put tight constraints on the form the behaviour of the agent. Second, it prepares the agent for future problems: an agent with a diverse behavioural repertoire is likely to also have high amounts of diverse knowledge and skills.

The diversity measure concerns itself only with the sensory part of the behaviour: {y i } 0≤i<n . It is defined as a coverage measure. Given τ > 0, the diversity of the exploration C({y i } 0≤i<n ) is defined as the volume (more precisely the Lebesgue measure) of the union of the n hyperballs of R s with y 0 , y 1 , ..., y n-1 as a centres, and radius τ .

C τ ({y i } 0≤i<n = n i=0 B(y i , τ )
with B(y i , τ ) the hyperball of radius τ and centre y i .

In evolutionary robotics, other measures of diversity such as sparseness [START_REF] Lehman | Exploiting open-endedness to solve problems through the search for novelty[END_REF] or entropy [START_REF] Delarboulas | Open-ended evolutionary robotics: An information theoretic approach[END_REF] have been used.

III. ILLUSTRATING THE PROBLEM

In this section, we illustrate the problem on a specific example, that will serve as the experimental setup for the method, exposed in the next section.

We consider an idealized robotic arm on a two-dimensional plane, made up of an open chain of 20-joints linked by segments of 1/20th of a meter each, so that the total length of the arm is one meter. The angles of the joints are restricted to values between -150 and 150 degrees. The angles of the joints are the inputs: they uniquely define the posture of the arm, and therefore, the position of the end-effector, which corresponds to the environmental feedback. Let's remark that only the final position of the end-effector, corresponding to the angle inputed in absolute value, is returned by the environment (i.e. there is no posture dependence between two consecutive samples).

A. A Tale of Two Exploration Strategies

Despite the simplicity of the arm setup, it is not a trivial problem, and this is exacerbated since we cannot assume any knowledge about the arm.

The most simple strategy, random motor babbling (RMB), samples the motor space randomly. Here the RMB strategy (Figure 1) is inefficient: indeed, the redundancy2 of the arm is heterogeneously distributed in the sensory space (the endeffector position space). In particular, the redundancy is high near the origin, and order of magnitude lower on the edge of the reachable space. Because the RMB strategy is precisely an Fig. 1. Random motor babbling is not an efficient exploration strategy with a high number of joints.

estimator of the heterogenity of the redundancy, it rarely ever explores the edges of the reachable space.

A goal babbling strategy is (usually) better suited for exploring the arm setup. We will consider a random goal babbling (RGB) strategy [START_REF] Baranes | Intrinsically motivated goal exploration for active motor learning in robots: A case study[END_REF][START_REF] Rolf | Online goal babbling for rapid bootstrapping of inverse models in high dimensions[END_REF], that picks a goal at random in the square [-1, 1] × [-1, 1], and translate it to a tentative Fig. 2. Random goal babbling can a very efficient strategy-if the inverse model is well chosen. Each exploration is done over 5000 timesteps. In each case, the last five postures of the exploration are displayed.

motor command that tries to put the end-effector as close as possible of the goal.

To translate a goal into a motor command, we need an inverse model. As in this paper, we are only interested in relative performance: we choose a simple inverse model. Our inverse model, when given a goal, finds the nearest effect available in the observed data, retrieves the motor command that produced it, applies a small perturbation to it, and returns the perturbed command for execution of the exploration strategy. The magnitude of the perturbation is parametrized by the perturbation coefficient d: the perturbation is randomly chosen between ±d times the legal joint range. For instance (here 300 • ), if d = 0.05, the motor command is perturbed by a random value chosen in ±15 • on each joint.

Choosing d appropriately is not trivial. In Figure 2, the RGB exploration of three different values of d is shown. The d = 0.05 case results in a good exploration. But d = 0.001 creates degenerated clusters: the perturbation is too low to create enough sensory variability. A contrario, d = 0.5 creates too much variability, and is only marginally better than the RMB exploration of Figure 1.

Let's imagine now that we are given two strategies to explore the arm setup. One is the RMB strategy, and the other is a RGB strategy, with unknown d. We don't assume any knowledge of either strategy. How can we dynamically decide, for each interaction with the black-box, which exploration strategy to choose to maximize the coverage of the exploration over the reachable space?

B. Inverse Model

Given a goal, the inverse model finds the nearest neighbour in the observed effects and applies a small perturbation on its corresponding motor command.

Formally, M is an closed hyperrectangle of R m , and as such it is the Cartesian product of m closed intervals:

M = m-1 m=0 [a i , b i ]
Given an motor command x = {x 0 , x 1 , ..., x m-1 } in M , a perturbation of x is defined by:

PERTURB d (x) = {random(max(a j , x j -d(b j -a j )), min(x j + d(b j -a j ), b j ))} 0≤j<m

IV. METHOD

A. Effect Diversity

Choosing which strategy to employ at each step of the exploration faces three main challenges:

1) Interdependence: an exploration strategy effectiveness may depend on another strategy; goal babbling relies

Algorithm 1: INVERSE d (y g , E) Data: • d ∈ [0, 1], a perturbation ratio. • E = {(x t , y t )} 0≤t<N ∈ (M × S)
N , past observations.

• y g ∈ S, a goal. Result:

• x ∈ M a motor command.

Find (x i , y i ) in E so that y i is the the nearest neighbour of y g in {y t } 0≤t<N . x = PERTURB d (x i ) on motor babbling to bootstrap the exploration. Given the inverse model currently used, this is even more true, as goal babbling's performance depends heavily the sensorimotor attractors in which it expands, and thus on the location of the observations produced early in exploration by motor babbling.

2) Dynamical Value: the usefulness of a strategy may change rapidly. Motor babbling is useful in the beginning of the exploration, but its usefulness drops quickly. 3) Agnosticity: since an exploration strategy might be arbitrarily complex, and possibly involve, in turn, other exploration strategy, an adaptive strategy should not rely on knowledge of the internal workings of the strategies amongst which it must choose.

Interdependence does not have to be handled directly, but it implies that even strategies that did poorly in the past must be re-evaluated regularly as the exploration progresses. The dynamical nature of the contribution of each strategy means that performance data becomes obsolete quickly: evaluations should be done over short-term time windows. Agnosticity implies the contributions of the strategies have to be evaluated only from the observations the strategies produce. We introduce a measure that matches those constraints now.

A strategy that produces effects over areas that have already been explored is of little use for exploration. We introduce an online diversity measure that evaluates, each time a strategy is used, how much diversity is created, with regards to already observed effects.

In order to do that, we rely on the diversity measure introduced in section II, based on the union of disks centred on observed effects. Although we reuse the coverage measure here out of convenience, the two measures do not have to have any relationship with one another. The measure is adapted to evaluate a single effect: the diversity of a new observed effect is the increase in diversity, i.e., the increase in the covered area.

Definition 1: Given a set of effects E = {y 0 , y 1 , ..., y n-1 }, and a coverage threshold τ in R + , the diversity of a new effect y n relative to E is defined as:

div τ (y n , E) = C τ (E ∪ {y n }) -C τ (E)
The diversity of a strategy, in turn, is the averaged diversity of the effects it produced, over a given time window.

Definition 2: Given a set of strategies s 0 , s 1 , ..., s q-1 , and a set of observed effects E = {y 0 , y 1 , ..., y n }, we have for a given strategy s j a subsequence y j 0 , y j 1 , ..., y j nj of the effects produced by motor commands emanating from the strategy. Given a time window w in N + , we define the diversity of strategy s j as:

div τ,w (s j , E) =        1 w w i=0 div τ (y j nj -i , E) if n j > 0 0 otherwise with w = min(w, n j ).

B. Multi-Armed Bandits

As expressed above, the problem we tackle shares similarities with the Multi-Armed Bandit problem (MAB) [START_REF] Robbins | Some aspects of the sequential design of experiments[END_REF]. The exploration strategies are the bandits, amongst which the agent must choose to create diversity. However, the feedback received is a sensory feedback from the environment, which cannot be used as is in the MAB setting.

Using the diversity measure of a strategy introduced above, we can now evaluate the contribution of each strategy to the exploration. We now have a classic MAB problem: we choose between a finite number of different strategies with different diversity scores, and after choosing one we receive a feedback signal from the chosen strategy from which we compute an updated score.

The classic MAB problem considers only bandits that are independent from one another (choosing one does not affect the value of the others), and stationary (the distribution of rewards of the bandit does not change). A variation of the problem, the adversarial (also called non-stochastic or nonstationary) MAB, removes the stationary and interdependence assumptions: an adversary is free to choose arbitrary rewards for each bandit at each timestep.

In practice, a significant portion of the published literature on the adversarial MAB problem only removes the stationary assumption. In other words, the problem takes place in the oblivious opponent model: the actions of the adversary, i.e. the rewards for each bandit at each timestep, are decided before the game starts. This is the case in [START_REF] Whittle | Restless bandits: Activity allocation in a changing world[END_REF] and [START_REF] Auer | The nonstochastic multiarmed bandit problem[END_REF], who investigate rewards that can arbitrarily change. [START_REF] Garivier | On upper-confidence bound policies for nonstationary bandit problems[END_REF] presents abruptly changing environments, where all bandits' reward distributions change at specified timesteps. [START_REF] Cesa | Prediction, Learning, and Games[END_REF][156][157][158][159][160][161][162][163][164][165][166][167][168][169] provides a treatment of the nonoblivious case.

Recently, [START_REF] Lopes | The strategic student approach for lifelong exploration and learning[END_REF] introduced the Strategic Student Problem that tries to capture the issues involved when learning multiple tasks at the same time. A student has to learn multiple topics (maths, chemistry, history, etc.), and has limited resources (time) to do so. How should he allocate his study time between topics in order to maximize its mean grade at the end of the semester? A possibility is to consider the problem as a MAB problem where the bandits are learning tasks. Interestingly, the works of [START_REF] Baranes | Intrinsically motivated goal exploration for active motor learning in robots: A case study[END_REF] on goal babbling can be understood in this perspective: each region of the goal space is a different topic, whose improvement is empirically measured through competence progress during learning, and the exploration strategy must decide how to distribute its action given those learning feedback signals.

The strategic student problem also considers another related problem: a student has one topic to learn, but several possible learning strategies. Which one should he choose? Is a mixture of several strategies better than employing the best one all the time? This is the problem of learning how to learn [START_REF] Schmidhuber | On learning how to learn learning strategies[END_REF]. [START_REF] Baram | Online choice of active learning algorithms[END_REF] explored such a problem and showed that a dynamically selected mixture of three active learning strategies outperformed any pure strategy. [START_REF] Konidaris | Sensorimotor abstraction selection for efficient, autonomous robot skill acquisition[END_REF] demonstrated that empirically evaluating and selecting among different small state space representations specific to a task during learning was effective and avoided a large task space when learning was unfeasible. The work of [START_REF] Sao | Active choice of teachers, learning strategies and goals for a socially guided intrinsic motivation learner[END_REF] investigates robots dynamically choosing between asking a teacher for a demonstration or doing self-exploration on their own. [START_REF] Jauffret | From self-assessment to frustration, a small step toward autonomy in robotic navigation[END_REF] proposes a method where a robot can self-assess, and has a frustration drive. When frustrated, the robot can opt to choose social help to improve its performance. In the context of reinforcement learning, [START_REF] Hester | Learning exploration strategies in model-based reinforcement learning[END_REF] develops an algorithm that can evaluate dynamically which exploration strategy brings the most rewards. These exploration strategies are driven by extrinsic and intrinsic motivations: maximizing rewards, reducing variance, seeking novelty, seeking unexplored states (a binary novelty), and seeking or avoiding particular features of the state representation. [START_REF] Clement | Multiarmed bandits for intelligent tutoring systems[END_REF] uses the framework of the Strategic Student Problem to create a tutoring system that actively personalizes the sequence of activities to each student, by tracking their performance and identifying which exercises and modalities make the student progress faster. The works of [START_REF] Baram | Online choice of active learning algorithms[END_REF], [START_REF] Sao | Active choice of teachers, learning strategies and goals for a socially guided intrinsic motivation learner[END_REF] and [START_REF] Hester | Learning exploration strategies in model-based reinforcement learning[END_REF] are singular because they combine deciding how to learn, and deciding what to learn, using a hierarchical approach. The learning strategy is selected first (how), and then it chooses what input to sample (what).

Learning performance typically exhibits diminishing returns, and [START_REF] Lopes | The strategic student approach for lifelong exploration and learning[END_REF] shows that, in the strict case, this allows to express the mean performance across tasks as a submodular function [START_REF] Krause | Submodular function maximization[END_REF]. [START_REF] Nemhauser | An analysis of approximations for maximizing submodular set functions[END_REF] has proven that with non-decreasing submodular function, the greedy strategy is guaranteed to be no worse than 1 -1 e ≈ 0.63 times the optimal solution for maximizing the function. Of course, not all set of learning tasks exhibit a submodular structure. Still, it suggests that a good-enough performance might be obtained through simpleenough algorithm in practice. [START_REF] Lopes | The strategic student approach for lifelong exploration and learning[END_REF] and [START_REF] Hester | Learning exploration strategies in model-based reinforcement learning[END_REF] advocate the use of the EXP4 algorithm [START_REF] Auer | The nonstochastic multiarmed bandit problem[END_REF] rather than a greedy algorithm, as a more robust approach.

Compared to these works, our approach distinguishes itself on two fronts: first, we are selecting exploration strategies to improve exploration, rather than exploration or learning strategies to improve learning. The resulting strategy is another exploration strategy. Second, we are using diversity to transform the feature vector of the sensory feedback into a scalar that can be adequately interpreted as a reward. To our knowledge, this is the first work to do that in the context of a Multi-Armed Bandit problem.

C. Adaptive Strategy

The ADAPT algorithm chooses strategies proportionally to their diversity. To allow for constant re-evaluation of the strategies, even those with low diversity, the algorithm chooses a strategy at random α percent of the time, with α > 0. Algorithm 2 formally describes this.

Additionally, in order to foster initial experimentation with each strategy, the diversity measure is overestimated at the beginning of the exploration. For a given strategy s j , instead of considering the set E j = {y 0 , y 1 , ..., y nj }, we consider the set E = {y -k , y -k+1 , ..., y 0 , ..., y n }, with k in N + . The set {y -k , y -k+1 , ..., y -1 } is composed of fictitious points only available to the selecting strategy, that generate hyperballs that do not overlap with the observed effects. That way, the diversity of the strategy is overestimated during the w + k first times it is selected. This also avoids having the first strategy selected unfairly preferred because it created the first observation, thus receiving the diversity of a full hyperball volume. We will use k = 1 in all strategies.

V. RESULTS

Figure 3, the results of the strategy are displayed. In all three learner configurations, the ADAPT algorithm identifies and uses the correct strategies. When d = 0.001, the goal babbling strategy is inefficient in the beginning, and motor babbling is overwhelmingly used. Motor babbling diversity declines continually during the exploration, and in the later stage, is comparable to goal babbling. As a result, after 4000 timesteps, the two strategies are used roughly equally.

When d = 0.05, goal babbling and motor babbling produce the same diversity at the beginning, but goal babbling declines more slowly than motor babbling. As a result, goal babbling is used more and more as the exploration progresses, as it should be.

When d = 0.5, motor and goal babbling behave similarlyif d had been equal to 1.0, they would be the same strategy.

Algorithm 2: ADAPT(w, τ ) Input:

• s 0 , s 1 , ..., s q-1 , strategies.

• E = {y 0 , y 1 , ..., y n-1 }, a set of effects.

• τ , coverage threshold.

• w, time window.

• α, ratio of random choice. Result:

• s j , chosen strategy if RANDOM() < α then choose a random strategy. else choose a strategy s j proportionally to its diversity diversity τ,w (s j , E).

During the early phase of the exploration, the ADAPT algorithm does not distinguish between the two strategies. But in the later phase, goal babbling is able to provide an edge, however small, that is detectable by the ADAPT algorithm. Goal babbling usage dominates after 1500 timesteps, and is used 80% of the time after 4000 timesteps. While the algorithm works qualitatively, it remains to be seen if this translates quantitatively. Figure 4 compares the error of the ADAPT algorithms with fixed-ratio strategies, where the motor babbling strategies is chosen with probability p, and the goal babbling with probability 1 -p.

When goal babbling is much worse than motor babbling (d = 0.001) or when it is much better (d = 0.05), the ADAPT algorithm manages performance on par with the best fixed mixture of strategies. When goal and motor strategy behave similarly, the adapt strategy is more conservative than the best case. This stems from the early stage of the exploration, when the motor babbling and goal babbling strategies are both effective, and hence both significantly used.

VI. DISCUSSION

The ADAPT algorithm we proposed, and the corresponding adaptive strategy we implemented demonstrate how a choice of multiple exploration strategies can be exploited to explore an unknown environment. The diversity measure is, in many ways, rather crude, but it shows that discriminating between exploration strategies is definitely possible, and, advantageous. The general idea behind this work is not particularly new.

Its application to a diversity measure is, however. In fact, since exploration, as explained, does not make the typical assumption about the agents capabilities-it does not assume the agent is capable (or willing) to make predictions, nor to exert (or demonstrate) control over the environment-the method we presented extends the applicability of the Multi-Armed Bandits to situations where learning or reward signals are not present. And it does so without requiring to design a problem-specific reward function.

Our work could be criticized for the simplicity of the environment that is used, and that's a valid point. Yet, we chose to present this method on a simple setup here to avoid the reader having to suspend his intuition, or suspect interference from the robot complex dynamics into the results. The extreme simplicity of our inverse model is also a deliberate choice in this regard. We are currently preparing experiments on a real robot actuated through dynamical motor primitives to reproduce the results in a more complex scenario.

From the experiments we conducted, it is unclear how the ADAPT algorithm will scale with the number of strategies. As more strategies are available, either more time will have to be devoted to exploratory sampling of bad strategies, or strategies will be less accurately evaluated overall. This is the classic exploration/exploitation trade-off. The ADAPT algorithm performs well when strategies behave distinctly, and better than random with similar strategies. Each graph displays the performances of fixed mixtures of the two strategies, with the performance of the adaptive strategy added as a dotted line (its standard deviations in displayed in light colour as well). Experiments were repeated 25 times. Note that not all the y-axis of the graphs begin at zero. hours for running simulations were graciously provided by the MCIA Avakas cluster.

SOURCE CODE

The complete source code behind the experiments and the figures is open source and available at: fabien.benureau.com/code/icdlepirob2015.html

  with the function random(a, b) drawing a random value in the interval [a, b] according to a uniform distribution. d is the perturbation parameter, and the only parameter of the inverse model, that we can now express in Algorithm 1.

Fig. 3

 3 Fig. 3. T he ADAPT algorithm correctly selects the best strategy in all three contexts. For each learner, three graphs are shown: the spread graph with the coverage area (τ = 0.02), the diversity graph giving the diversity measure of each strategy in function of the timesteps, and the usage graph, showing how the strategies are effectively used. For the usage graph, the data at time t shows the percentage of use averaged over the surrounding 100 timesteps (50 before, 50 after).

Fig. 4 .

 4 Fig. 4.

We assume that S is known by the exploration strategy, but nothing prevents S to be set equal to R s

Considering a subset of the sensory space B, the redundancy of B is defined as the volume (more generally, the Lebesgue measure) of the set of motor commands whose effect belong to B, i.e. {x|f (x) ∈ B} with f the environment feedback function (see section II-A)).[START_REF] Lenarcic | On the quantification of robot redundancy[END_REF] provides an algorithm to quantify the redundancy of rigid, multijoint robotic arms, but the computation is only tractable for a small number of joints.

ACKNOWLEDGMENTS

This work was partially funded by the ANR MACSi and the ERC Starting Grant EXPLORERS 240 007. Computing


Emilio Jesús

Gallego Arias
email: emilio.gallego_arias@mines-paristech.fr

Olivier Hermant
email: olivier.hermant@mines-paristech.fr

Pierre Jouvelot
email: pierre.jouvelot@mines-paristech.fr

A Taste of Sound Reasoning in Faust

Keywords: DSP, audio, program verification, theorem proving

We address the question of what software verification can do for the audio community by showcasing some preliminary design ideas and tools for a new framework dedicated to the formal reasoning about Faust programs. We use as a foundation one of the strongest current proof assistants, namely Coq combined with SSReflect. We illustrate the practical impact of our approach via a use case, namely the proof that the implementation of a simple low-pass filter written in the Faust audio programming language indeed meets one of its specification properties.

The paper thus serves three purposes: (1) to provide a gentle introduction to the use of formal tools to the audio community, (2) to put forward programming and formal reasoning paradigms we think are well suited to the audio domain and (3) to illustrate this approach on a simple yet practical audio signal processing example, a low-pass filter.

Introduction

Formal program verification is gaining strong support in the computer programming world with projects such as the CompCert certified C compiler [START_REF] Leroy | Formal verification of a realistic compiler[END_REF], with more and more tools such as the Coq 1 proof assistant striving to ease the development of correctness proofs for hopefully the every-day programmer.

While there has been some work in the mathematical correctness of DSP -see for instance [START_REF] Neelakantan | Higherorder functional reactive programming without spacetime leaks[END_REF][START_REF] Brunel | A core quantitative coeffect calculus[END_REF] for type-based techniques, and [START_REF] Souari | Design and verification of a frequency domain equalizer[END_REF][START_REF] Ghafari | Formal Verification of Real-time Data Processing of the LHC Beam Loss Monitoring System: A Case Study[END_REF] for approaches using theorem proving -formal verification is still largely absent in the DSP and Computer Music (CM) communities. Yet, users and musicians are always striving for ever better sound experience and audio realism. Thus, ensuring the adequacy between an intended audio specification, for instance some sort of a limited-bandwidth filtering, 1 coq.inria.fr and its actual implementation, along with other key properties such as robustness [START_REF] Chaudhuri | Continuity and Robustness of Programs[END_REF] or Bounded-Input Bounded-Output (BIBO) stability, is warranted. Too often, the only correctness test performed is to check that "it sounds about right", which is a methodology that clearly deserves some improvements.

The overall goal of our paper is to provide a case for the introduction of tools and best practices dedicated to the formal mathematical reasoning about audio/sound application programs. We illustrate this vision via the use of Coq/SSReflect for the Faust audio language2 . We introduce a new framework for mathematically reasoning about Faust audio programs. We show how simple properties can be already proven for some Faust filtering applications using such an approach, thus paving the way to the future introduction of dedicated proof techniques for audio processing systems.

This paper is structured as follows. In Section 2, we introduce the Coq proof assistant and its SSReflect extension, which we use all along. Section 3 describes the Faust language core, using a low-pass filter as an example, while Section 4 provides a Coq implementation. We introduce in Section 5 a specific logic that will help reasoning about Faust programs. We finally put these tools into good use in Section 6, where we show how the low-pass filter can be proven equivalent to its specification. We discuss future work and conclude in Section 7.

A Coq/SSReflect Tour

Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development[END_REF]] is a software development environment in which programmers can write functional programs and prove properties about them. Coq's programming language Gallina is very similar to other functional programming languages like Ocaml, but with some added restrictions (in particular, all Coq pro-grams must terminate) and a more advanced type system. Coq is a strongly-typed language; in particular, a type is understood as a property P , and an expression e of type P , written e : P, is the proof for P .

SSReflect [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF] is a proof language and extensive library built on top of Coq. It promotes a structured style of programming and facilitates proof development by profiting from the fact that many properties of interest can be expressed as programs of type boolean.

Recursive Definitions We will illustrate some basics of the SSReflect's proof language by proving a toy property over a toy programming language. We first load some required libraries:

Require Import ssrfun ssrbool eqtype ssrnat.

The Abstract Syntax Tree (AST) of our toy programming language is defined in Coq with the Inductive command:

Inductive exp : Type := | cst : nat Ñ exp | mul : exp Ñ exp Ñ exp. Notation "' n" := (cst n).
Notation "a ˆb" := (mul a b).

which declares the recursive (so-called inductive) type exp with two constructors, cst for embedding natural integer constants, and mul for the multiplication of two expressions. Coq provides support to declare convenient notations such as ˆfor the multiplication operation.

Recursive functions are declared in Coq using the Fixpoint command. Then, the value of an expression in our toy language is defined by recursion over its structure: We can run our program with the Eval command:

Eval compute in eval ('2 ˆ('0 ˆ'3)).
which will display, as expected, 0. Going one step further, Ocaml code can be generated automatically from Coq programs, providing reasonably efficient and provably-correct implementations of the specified algorithms. Proving Properties Following upon our previous simple test, assume we want now to prove the following, 0-absorbing property, named eval0eB: all expressions e that contain a '0 subexpression evaluate to 0. We can write a boolean function mem_exp that checks if '0 occurs in an expression e easily 3 :

Fixpoint mem _ exp m e := match e with | ' n => n == m | e1 ˆe2 => mem _ exp m e1 || mem _ exp m e2 end.
Theorem eval0eB is rephrased now as: for all expressions e, if mem_exp 0 e is true, then eval e is 0. Let's begin by proving an easier property for constant expressions; it is stated here in Coq as Lemma eval0cB, followed by its proof:

Lemma eval0cB :
forall n, mem _ exp 0 ('n) Ñ eval ('n) == 0. Proof. by move=> n /=; exact. Qed.

In addition to programming in Gallina, we can also use automated program building procedures called tactics. We can use an interactive proof editor such as Proof General of CoqIDE to step from Proof to Qed; after each tactic (terminated by a .), the current proof state is displayed. The proof state consists of a set of hypotheses e : t (the "context") and a goal g which should be seen as a stack of properties p 0 ->....->p n ->g. Most SSReflect tactics tac can perform context manipulation operations before and after running. tac: x will remove a named hypotheses x : p from the context, pushing p to the goal before tac is run; tac => x will pop the top of the goal after tac is run, naming it x. Thus, if p 0 ->A is the current goal, move=> x will add x : p 0 to the context. Plenty of additional operations can be performed in addition to moving.

The previous proof started with the documentation-only Proof command, getting the goal:

forall n, mem _ exp 0 ('n) Ñ eval ('n) == 0.
with an empty context. The first step is to move n to the context with move=> n /=. The /= switch asks Coq to perform partial evaluation of the goal, resulting in a new goal n == 0 Ñ n == 0, which the exact tactic solves. Finally, Qed checks that the proof is correct, and, as for all previous function and type definitions, eval0cB is added to the global context for further use.

Moving then to our full theorem, we state: Here, the proof starts by performing induction on the structure of expressions. The induction tactic elim operates on the top of the goal, which in this case is the expression e. The base and inductive subgoals are generated, displayed as: We must prove each goal separately (theand + symbols indicate a new proof step). The base case is dealt with by first using Lemma eval0cB from the global context with the apply tactic (the by so-called "closing tactical" ensures that the current goal is finished). In the inductive case, the goal includes the facts that eval0eB is true on each subexpression, named here e and e0 by Coq. We first move e and e0, renamed e1 and e2, to the context, each followed by its induction hypotheses H i , before performing a partial evaluation. After the move, we have the following proof state:

subgoal 1 (ID 18) is: forall n : nat, mem _ exp 0 (' n) Ñ eval (' n) == 0 subgoal 2 (ID
e1 : exp H1 : mem _ exp 0 e1 Ñ eval e1 == 0 e2 : exp H2 : mem _ exp 0 e2 Ñ eval e2 == 0 ============================ mem _ exp 0 e1 || mem _ exp 0 e2 Ñ eval e1 * eval e2 == 0
The top of the goal is a boolean disjunction, on which we can perform case analysis using the case tactic with the orP view. Each of the two resulting cases happen to be the premise of the induction hypotheses, H1 and H2; thus the disjunctive pattern [/ H1|/H2] will rewrite the goal to:

eval e1 == 0 Ñ eval e1 * eval e2 == 0
and similarly for e2. The pattern /eqPÑ will rewrite eval e1 to 0 in the goal obtaining a goal of 0 * eval e2 == 0. This particular step is paradigmatic of the "proof by rewriting" technique: from a property a = b, we can replace all a terms occurring in the goal by b. The final step of the proof is again by rewriting, this time using the mul0n and muln0 lemmas part of the ssrnat library, with type mul0n : forall x, 0 * x = 0 and symmetrically. Rewriting Magic SSReflect's emphasis on boolean expressions fosters proof by rewriting in arithmetic proofs. For instance, in the following lemma:

Lemma leq _ 2add :

forall (x y : nat), x <= y Ñ x + x <= y + y. Proof. by move=> x y xy; rewrite leq _ add. Qed.

the proof, where "; " combines proof steps, is done by rewriting with the leq _ add lemma, provided by the ssrnat library, of type:

leq _ add : forall (m1 m2 n1 n2 : nat), m1 <= n1 Ñ m2 <= n2 Ñ m1 + m2 <= n1 + n2
How could that happen? Equalities do not seem to occur in the conclusion of leq _ add, but they have actually just been removed by the pretty printer. In fact, the exact conclusion is a boolean equality, namely m1 + m2 <= n1 + n2 = true, as the resulting type of the <= operator is boolean. Thus, x + x <= y + y = true can be easily matched and rewritten to true with proper bindings of leq _ add variables, leading to the goal

true = true.
Going Further It is obviously impossible to give a complete overview of SSReflect in two pages. In particular, SSReflect advocates particular conventions and coding styles that we did not fully follow for the sake of space and pedagogy. In particular, the idiomatic proof for Theorem eval0eB is:

by elim=> //= ? IH1 ? IH2 /orP [/ IH1|/IH2] /eqP Ñ ; rewrite ?(mul0n, muln0).

The Mathematical Components library is a companion project to SSReflect, and includes extensive libraries about finite groups, algebra, number theory and more, which have been used to formally prove significant large theorems like the Four Color or Feit-Thompson theorems.

The Faust Audio Language

Faust-which stands for "Functional Audio Stream" -is a DSP language [START_REF] Orlarey | Syntactical and semantical aspects of Faust[END_REF]]. Faust's main focus is the fast development of efficient digital audio programs, and has been used in live performances and offline and online audio applications, such as FaustLive [START_REF] Denoux | FAUSTLIVE, Just-In-Time Faust Compiler[END_REF] or moForte4 . It has also been used in other signal processing contexts [START_REF] Barkati | Faustine: A Vector Faust Interpreter Test Bed for Multimedia Signal Processing -System Description[END_REF].

Framework Faust programs are structured in two layers. The high-level layer is a macro language corresponding to an untyped, full-fledged functional language. It is used to generate programs written in the Core Faust syntax, where only a few primitives are available. In order to deal with the real-time constraints imposed by audio processing, Faust programs are then optimized and compiled towards an efficient language; Faust's main compiler generates C++ code, while alternative backends can now generate other formats, such as asm.js code.

While the core language is unpractical for writing real applications, it contains enough primitives for the rest of this paper. Moreover, it enjoys a strong type system and operational semantics. For a more precise description of Faust syntax and semantics, we refer the reader to [START_REF] Jouvelot | Dependent vector types for data structuring in multirate Faust[END_REF].

Semantics Signal processors are Faust's key components. A signal is a (potentially infinite) stream of amplitude values. In the discrete case, we can represent signals as functions from (discrete) time to real numbers. Formally, we write S for the function space N Ñ R. We assume that signals have amplitude 0 when time is negative. Signal processors from i inputs to o outputs are functions in S i Ñ S o , and every valid Faust program can be interpreted as a function of this type. We use "semantics brackets" to denote the function that maps a Faust program to its mathematical interpretation. For instance, the delay processor, which delays its input signal by 1 audio sample, is denoted as:

delay piqpnq " ipn ´1q.
The first argument i is the signal to be delayed, and n represents time. Then, delay will simply return the sample from i corresponding to the previous time value.

Core Faust For the purposes of this paper, we focus on a minimal but functional subset of Faust consisting of three particular signal processor-building blocks: primitives, composition, and feedback.

Examples of primitive signal processors are +, which takes as input two signals and outputs a signal with amplitude the sum of the input signal amplitudes, or * (c), that scales the amplitude by a constant factor c. Formally:

` pi 1 , i 2 qpnq " i 1 pnq `i2 pnq ˚pcq pi 1 qpnq " c ˚i1 pnq. We write f : g for the composition of signal processors f and g: f : g piq " g p f piqq.

The interesting construction is feedback, written as f " g. In this case, f is assumed be a processor from two signals to one, and g, a unary signal processor. Then, f " g represents the 1delay feedback loop through g. f " g piq " f p g p f " g p delay piqqq, iq.

Note that the definition of the semantics of feedback is recursive. For example, the Faust program + " sin is depicted in Figure 1.

A Simple Low-Pass Filter For the rest of the paper, we will work with a simple low-pass filter written in Faust as:

smooth(c) = * (1 ´c) :+ " * (c).
smooth is intended to be used with a coefficient c in the interval r0, 1s. If c is 0, then the filter has no effect, whereas as we increase c the cutoff frequency decreases, with a limit case of c " 1, that outputs a constant signal. The filter first multiplies the input amplitude by 1 ´c, then to perform 1-sample additive feedback with coefficient c. Its block diagram with c " 0.9 is drawn in Figure 2.

While this filter may not be very adequate for audio, due to its frequency response curve, it is useful for instance for smoothing control parameters, and for other applications with highfrequency components. A key property of filters is stability. That is to say, we expect smooth's output amplitude to remain in bounds that depend on the input. An excessive amount of feedback could cause the filter to behave badly.

Formalizing Faust in Coq

In the previous section, we described a core subset of Faust on paper. In this section, our goal will be to replicate this description inside a mechanized framework, Coq. This will enable us to later mechanically reason about Faust programs, avoiding a lot of potential error sources and getting strong confidence on the soundness of our reasoning.

Overview Mechanized reasoning about programs requires to encode their behavior or semantics in the particular theorem prover of choice. In a sense, this is equivalent to defining an interpreter ; however the idiosyncrasy of theorem proving often makes the process quite different from writing a regular interpreter or compiler for our language.

Once the semantic representation is in place, we can wonder whether two programs have the same behavior (read: semantics), what happens when the input does not meet certain criteria, etc.

The concrete tasks we need to complete in order to start reasoning about Faust programs in Coq are: a) define a representation of Faust syntax in Coq; b) define a representation for signals, or streams, in Coq; c) write a function that takes a program's AST and returns a stream processor.

Once this is done, we can start proving! However, a key point in theorem proving is how convenient will it be to write proofs. We would have a hard time justifying formalized reason-ing if we needed thousand of hours and lines of proof to perform trivial reasoning. We will address this point in Section 5, while devoting the rest of this one to explain how Faust is embedded into Coq. All the Coq code and examples can be downloaded from https: //github.com/ejgallego/mini-faust-coq/.

Faust AST in Coq We will encode the syntax of the program using an algebraic or inductive data type. ADT (Abstract Data Types) are one of the most powerful features of Coq, allowing the user to define new richly-typed datatypes. In Section 2, we saw an example of an ADT for expressions. Here, we will make use of an extra feature known as indexed or dependently-typed ADT. Thus, we will encode Faust expressions using the fterm datatype, which carries additional information about the number of input and output signals of the program:

Inductive fterm : nat Ñ nat Ñ Type := | mult : num Ñ 1 1 | plus : 2 1 | comp : 1 1 Ñ 1 1 Ñ 1 1 | feed : 2 1 Ñ 1 1 Ñ 1 1 where "i o" := (fterm i o).
Notation "'+" := plus. Notation "' * (c)" := (mult c). Notation "f : g" := (comp f g).

Notation "f ~g" := (feed f g).

Thus, a program of type i o will exactly go from i to o channels. Note that the constructors that correspond to the primitives enforce this requirement. In particular two signal processors can be composed only if they have the right types; thus no ill-typed Faust program can be built. We also define some notations to make display nicer.

Now, we can define our simple low-pass filter as follows:

Def smooth c : 1 1 := ' * (1 ´c) : '+ ~' * (c).

Streams in Coq Once we have defined the syntax of our Faust programs, the next step is to define their semantics. We will encode signals as finite-length sequences of reals. We could have used several other representations, but it is beyond the scope of this paper to discuss the advantages of this particular definition.

We will index signals by their length, using the SSReflect type n.´tuple R, the type of sequences of exactly n reals. We write ' S _ n for n.´tuple R to shorten notation. Signal processors are encoded using regular Coq functions:

Notation "'S _ n" := (n.´tuple R). Notation "'SP(i,o)" := (@ n, 'S _ n^i Ñ 'S _ n^o).

For instance, the type for signals with three samples is ' S _ 3. A signal processor (of type "'SP(i,o)") must be able to process signals of arbitrary length; thus we quantify the second definition on all lengths n. We write ' S _ n^k for k copies of ' S _ n, e.g., ' S _ n^2 is (' S _ n * 'S _ n). Interpretation Function With both syntax and semantics in place, we can define a function linking the two worlds. In our case, a Faust expression of type i o will be interpreted by a Coq function of type @ n, 'S _ n^i Ñ 'S _ n^o. Our interpreter I will thus have type:

I : i o Ñ 'SP(i, o)
Given a program f, the resulting function I f is effective, that is to say, given input signals, it computes the corresponding output ones. In particular, I f n formally corresponds to the semantic brackets introduced in Section 3, restricted to the first n samples of the signal. We write f |n for this truncated semantics. How is I defined? Definition for primitives and composition is straightforward; the most interesting case is the feedback:

Definition I _ feedback f g n i := iter n (fun fb => f (g (x0 :: fb), i)) [::].
where x0 is the initial value for the feedback loop, usually 0, and iter n f x is the function that applies f n times to x.

Note that this function outputs a signal of size n when the input is of size n, and does so by computing the feedback for n steps. The reader familiar with signal processing will notice that this implementation is extremely inefficient, as it may take quadratic time even for simple programs! Indeed, the goal of our interpretation is not to achieve efficiency, but to have a convenient representation of the semantics in order to reason about it. Usually, efficient implementations are not very well-suited for reasoning and vice-versa. The usual remedy when we care about efficiency inside Coq is to define two implementations, and prove them equivalent [START_REF] Dénès | A refinement-based approach to computational algebra in COQ[END_REF].

First Steps in Proving With those ingredients, we can start reasoning about programs. For instance, a proof of the fusion property of the multiplication stream processors is:

( * Fusion of mult * ) Lemma multF : I (' * (a) : ' * ( b)) = I (' * (a * b)). Proof.
apply: val _ inj; case: i => s /= _ . by elim: s => //= x s Ñ ; rewrite mulrCA mulrA. Qed.

The proof is straightforward, by induction, associativity, and commutativity of the multiplication operator of the real numbers. However, some amount of boilerplate is necessary to set up the induction, task that can get tricky with more complex programs. Indeed, this inductive proof method is common to most proofs; thus we will identify common patterns and will define higher-level reasoning principles that allow us to prove things with less effort in the next section.

Structured Reasoning: A Sample Logic

As we just saw in Section 4, the Coq semantics allow us to state -and attempt to provealmost any property imaginable about Faust programs. However, in most cases, reasoning can be repetitive, long and error-prone. That is the price we have to pay for accessing such a power.

A key observation is that proofs of certain classes of properties share common parts, while only a minor part of the proof actually depends on the property. As we saw in the previous fusion case, the relevant part of the proof is less than 10% of its total code. Imagine a property ϕ, supposed to hold for all samples of a signal. Then, it is enough to define ϕ as a predicate over one sample, and we can "automatically" lift the predicate over signals, checking that ϕ holds for all time.

Indeed, to illustrate the principles of highlevel structured reasoning over programs, we will focus on such "sample-level" properties in this section. While we will sacrifice quite a bit of expressivity, by limiting our language to onesample statements, this will still be enough to carry out proofs of stability and will significantly facilitate our proofs, allowing us to proceed in a short and structured way. Sample-level Properties For our purposes, a predicate over a sample is a function from reals to booleans, ϕ, ψ P R Ñ B, or, in Coq, P, Q : R Ñ bool. Then5 , we say a property ϕ holds for a signal s if @n.ϕpsrnsq; that is, for all time moments n, the sample meets ϕ. In Coq, we can use the all function for sequences, thus writing all P s. For instance, the property that a signal is bound by the interval ra, bs is defined as ϕpxq " x P ra, bs, or in Coq as

P := fun x => x \in '[a,b].
It makes sense to extend our properties to signal processors. In this case, we would like to relate properties over input signals with properties over the output signals. Given sample-level properties (ϕ, ψ) and input and output signals (i, o), a reasonable statement could be: "if the input signal i satisfies ϕ, then o should satisfy ψ."

If we think of our previous "being in an interval" property, its extension to signal processors allows us to capture stability. Indeed, we can precisely state now: "if the input signal is bounded, then the output signal will be too." Judging the Sampling The previous relation between input and output signals and their properties constitutes an instance of a "high-level" reasoning principle. It is highly convenient thus to encode the fact that a signal processor satisfies the property as a "judgment." Our judgments will be of the form, tϕu f tψu, with intended interpretation tϕu f tψu such that, for all input signals with samples satisfying ϕ, all the output samples of f satisfy ψ. Formally: tϕu f tψu ðñ @i.p@t.ϕpiptqqq ùñ p@t, ψp f qpiqptqq the Coq version is expressed in a slightly different way, using all:

Definition '[[ { P } f { Q } ]] := @ n (i : 'S _ n), all i P ==> all (I f n) Q.
In the case of i input and o output signals, judgements are extended pointwise to use one predicate per signal: tϕ 1 , . . . , ϕ i u f tϕ 1 , . . . , ϕ o u .

Reasoning Rules Now, we'd like to have a system of rules to determine when a judgment is valid without resorting to analyzing its semantics.

The standard way to achieve this goal is to introduce a "logic", or a set of rules to infer validity of judgments, and, by extension, of their intended properties. The form of a rule is

A 1 . . . A n B
meaning that, if A 1 , . . . , A n are valid, then B also is. This way, we can hopefully reduce validity checking for B to smaller problems.

The rules of our particular system for samplelevel reasoning are shown in Figure 3. Rule Prim is an example of a base rule, stating that a judgment about a primitive is valid if its semantics is. Rule Comp allows to reduce the verification of composition to the verification of its individual parts; a judgment about composition is valid if there are valid judgments about the individual signal processors such that the property of the output of f implies the required property for the input stream of g.

The Feed rule is quite similar to the composition rule: the internal state of the feedback should obey an invariant θ, and samples from the feedback output should be compatible with the requirements of g's input. We also require that the initial value x 0 satisfies ψ. Now, all that remains is to check that the rules are sound, that is to say that validity of the premises implies the validity of the conclusion, and we can reason using the newly defined logic: Theorem 5.1 (Soundness). For any program f of type i o, if tϕ 1 , . . . , ϕ i u f tψ i , . . . , ψ o u is derivable, tϕ 1 , . . . , ϕ i u f tψ i , . . . , ψ o u is valid.

Proof. We proceed by induction on the derivation. The base case is the Prim rule, and proof is immediate. For Comp soundness automatically follows by induction hypotheses. For Feed , we apply induction on the length of the input signal, plus induction hypotheses.

Case Study: Filter Stability

As a case study, we will verify that the smooth filter of Section 3 is stable, that is, if the input amplitude is bounded, the output amplitude is.

Assume a well-formed interval ra, bs, including 0, and c P r0, 1s. In Coq: then, we will prove: ti P ra, bsu smoothpcq to P ra, bsu @i 1 , i 2 , p@t.ϕ 1 pi 1 ptqq ^ϕ1 pi 2 ptqqq ùñ p@t.ψpi 1 ptq `i2 ptqqq tϕ 1 , ϕ 2 u `tψu Prim tϕu f tθu tθu g tψu tϕu f : g tψu Comp |ù ψpx 0 q tθ, ϕu f tψu tψu g tθu tϕu f " g tψu Feed which can be proved using the libraries by: by rewrite ?itv _ boundlr /= ?ler _ wpmul2r ?ler _ subr _ addr ?add0r ?Hrc ?(itvP Hi).

The next step is to apply Feed , choosing θpsq " s P ra ˚c, b ˚cs. Then, we apply Prim twice to get the obligations for + and * (c): where have introduces a local lemma, and solved by: by rewrite itv _ boundlr /= ?ler _ wpmul2r ?(itvP Hi) ?Hrc.

We have chosen to prove the arithmetic obligations manually, but we should remark that there exists tools that can prove this kind of results automatically. The full derivation is in Figure 4.

Conclusion

We presented a case for the use of developerassisted formal reasoning tools in the field of computer music and, more generally, audio DSP. We gave a quick tour of the Coq/SSReflect environment, which we believe can be particularly well fitted to reach such a vision. We applied our approach to the Faust audio signal processing, providing a formal semantics for its core and detailing how a property of a filter can be proven using a specific logic designed for Faust. Future work will tackle other applications in the audio processing domain to assess our tool, together with the development of specific DSP mechanisms within Coq/SSReflect (tactics, tacticals, or even a dedicated DSP library). We would also be interested in seeing how our system can be of help to prove more foundational theorems such as the Shannon Sampling Theorem.

Fixpoint

  eval (e : exp) : nat := match e with | ' n => n | e1 ˆe2 => eval e1 * eval e2 end.

Figure 1 :

 1 Figure 1: Simple Feedback in Faust

Figure 2 :

 2 Figure 2: The smooth Low-Pass Filter

  Hypothesis (Hab : a <= b). Hypothesis (H0ab : 0 \in '[a, b]). Hypothesis (Hrc : c \in '[0, 1]).

Figure 3 :

 3 Figure 3: A simple logic for Faust program verification

H1:

  i1 \in '[( a * c), (b * c)] H2 : i2 \in '[( a * (1 ´c)), (b * (1 ´c))] ============================ i1 + i2 \in '[a, b] solved by: have Ha: a = a * c + a * (1 ´c) by rewrite ´mulrDr addrC addrNK mulr1. have Hb: b = b * c + b * (1 ´c) by rewrite ´mulrDr addrC addrNK mulr1. by rewrite itv _ boundlr /= Ha Hb ! ler _ add ?(itvP H1) ?(itvP H2).

Hi

  : i \in '[ a, b] ============================ i * c \in '[( a * c), (b * c)]

http://faust.grame.fr

www.moforte.com/

From now on, we will interchangeably use Coq and mathematical notation where no confusion can arise, omitting double definitions.

Acknowledgements

We want to thank Yann Orlarey and Arnaud Spiwack for their insightful comments. Partial funding for this research was provided by the ANR FEEVER Project.


Hughes-Jehan Vibert
email: hughes-jehan.vibert@justice.gouv.fr

Benoit Pin
email: benoit.pin@mines-paristech.fr

Pierre Jouvelot
email: pierre.jouvelot@mines-paristech.fr

Aligning legivoc Legal Vocabularies by Crowdsourcing

legivoc is the first Internet-based platform dedicated to the diffusion, edition and alignment of legal vocabularies across countries. Funded in part by the European Commission and administered by the French Ministry of Justice, legivoc offers a seamless path for governments to disseminate their legal foundations and specify semantic bridges between them. We describe the general principles behind the legivoc framework and provide some ideas about its implementation, with a particular focus on the state-of-the-art tools it includes to help crowdsource the alignment of legal corpora together.

Introduction

legivoc 1 (all in lower case) is an Internet-based database platform dedicated to the management of multiple legal information terminologies, with a particular focus on vocabularies and their alignments [START_REF] Hughes-Jehan | Legivoc -Connecting law in a changing world[END_REF]. The system is designed to be used both interactively and also as an automated Web service, interoperable with other document management tools or international legislation or translation systems, via a dedicated Application Programing Interface (API).

The main goals of legivoc are: [START_REF] Von | Human Computation[END_REF] to provide access, within a unique framework and using a general formalism, to (ultimately) all the legal vocabularies of the Member States of the European Union; [START_REF] Deterding | Gamification using game-design elements in non-gaming contexts[END_REF] to foster the use of best practices regarding the encoding of these vocabularies using Internet standards such as the Simple Knowledge Organization System (SKOS) and Uniform Resource Identifier (URI); [START_REF] Pilos | European Commission machine translation and public administrations[END_REF] to encourage the creation of alignment information between these vocabularies, helping provide bridges between judicial systems based on different laws and languages.

The French Ministry of Justice spearheads the project, partly funded by the European Commission and the Ministries of Justice of the Czech Republic, Spain, Finland, France, Italy and Luxembourg. ARMINES and MINES ParisTech are the lead scientific advisors and implementation specialists for the legivoc project.

legivoc is intended to be used directly by law and judicial experts, for instance when dealing with cross-border legal issues or planning new legislative regulations. For such a purpose, knowing how a legal notion in a given vocabulary relates to similar ones in other countries, a so-called alignment is a key asset. We show how legivoc can be extended so that entering such information is a very intuitive operation, with the idea of relying on crowdsourcing efforts (where dedicated individuals perform useful tasks for the community, as in Wikipedia) to enrich its vocabularies.

The rest of this paper is structured as follows. In Section 2, we provide a brief introduction to legivoc structure and typical use cases. Section 3 focuses on the alignment process, which intends to build upon international crowdsourcing efforts to enrich the legivoc database. Section 4 outlines the communication capabilities embedded within legivoc, for use by the systems that want to take advantage of it. We conclude in Section 5.

legivoc 1.01

legivoc materializes as a Web site providing a state-of-the-art multilingual system for the creation, edition and alignment of international legal vocabularies (see Figure 1 for the site page).

User Interface and Capabilities

In its current (6/2015) state, legivoc enables registered users to access the legal vocabularies of 13 Member States plus Switzerland, in addition to a global one managed by Eurovoc2 . These vocabularies exist in multiple languages; these translated versions have been either provided by the Member States themselves or automatically translated via the European Commission MT@EC multilingual service [START_REF] Pilos | European Commission machine translation and public administrations[END_REF].

Words in vocabularies are considered as SKOS concepts. They can be (1) visualized in various forms (text, dendogram, SKOS source), (2) edited, (3) related to more or less abstract concepts or (4) aligned to similar concepts in other vocabularies (see Section 3). Figure 2 illustrates part of a typical display of a concept, here the one of "civil law"; it was obtained, after a search for "droit civil" in legivoc, via the French version of the Eurovoc vocabulary, identified by its International Standard Organization (ISO) code eu, followed by its legivoc number, 523.

Technological Foundations

legivoc is built on top of plinn 3 , an open-source collaborative infrastructure developed at ARMINES and MINES ParisTech. This environment, based on the Zope multi-purpose Web framework system, provides sophisticated ways to manage documents in various formats, with a particular emphasis on users' access rights, for security purposes, and workflows, to enforce best practices. The existing legal vocabularies provided by the State Members use various formats (ASCII, Excel, Word, XML, SKOS…); thus heuristics have been developed and implemented to encode them into a common legivoc-specific SKOS format. Introducing new legislative corpora, e.g., from countries wishing to join legivoc, requires the design and implementation of new approximate algorithms, unless the data is already encoded into the legivoc SKOS format, which is strongly advised.

Even though the presence of such diverse formats and possibly incompatible semantics is a clear challenge and the existence of a general, widely adopted vocabulary format would be a desirable feature, we take, with legivoc, a "can-do" approach, and try to leverage existing corpora instead of waiting for an eventual standard. In fact, our own legivoc SKOS format can be seen as a first proposal in this direction. Figure 3 shows how IT specialists can write and execute (possibly from a remote site, see Section 4) legivoc SPARQL commands to answer specific requests emanating from law or judicial experts. In this particular example, one asks for the list of all concepts, given by their URI, and their preferred labels, as strings, present in the Greek vocabulary. An excerpt of the output is given in Figure 4.

Alignment Management

Alignment is a feature supported by SKOS, via the predefined closeMatch (see an example in Figure 2), exactMatch, broadMatch, narrowMatch and re-latedMatch mapping properties that can relate two concepts in a somewhat hierarchical manner. Introducing such information between vocabularies greatly enriches the semantic knowledge already embedded in legivoc. Yet, the size of the legivoc database, with its (up-to-now) 13 vocabularies sporting each an average number of concepts in excess of 7,000, would make this an expensive undertaking if one were to only use the text-based concept (and alignment) editor provided by legivoc.

One possible approach to handle data in such high volumes is to rely on automatic semantic analysis tools and techniques, e.g., machine learning, to suggest possible alignments to the user, an approach akin to the one taken, for instance, in the EU-Cases project4. Given the more homogeneous nature of our data (only vocabularies), we decided to try another route. We designed an extension to legivoc so that any benevolent user can help improve, in an intuitive, friendly and even "fun" way, the budding ontology induced by alignments, thus following approaches such as crowdsourcing (Wikipedia), human computation [START_REF] Von | Human Computation[END_REF] or "gamification" [START_REF] Deterding | Gamification using game-design elements in non-gaming contexts[END_REF]. Indeed, all alignments are reported on Twitter, enabling following users to discover in real time when new alignments are being added and by whom, thus creating a sense of community and challenge. New alignments are currently checked a posteriori by experts, to prevent as much as possible the input of possibly incorrect or conflicting information in the legivoc database; if need be, malevolent users could be blocked in short order and their actions reverted by a SPARQL command.

There are currently three new modalities for introducing in an intuitive manner new concept alignments involving two different vocabularies, based on how the relevant concepts are found:

• list, where concepts are displayed in alphabetic order; • search, where the user inputs keywords to legivoc, which returns a list of concepts matching those words; • pick, where the system chooses at random a given concept, and challenges the user to find a related concept in the other vocabulary.

The user then only has to mouse-select one concept in a given vocabulary and drag it on top of the other concept, in the second vocabulary. This process is made even easier and more informed via the use of dendograms, which display in an intuitive manner the hierarchical structure of law concepts (see Figure 5

for a particularly rich example).

A significant illustration of the alignment environment is provided in Figure 5. The top half of the screen is dedicated to the UK vocabulary, in list mode (by clicking twice on a concept name, here "communication", its partly elided dendogram has appeared), while the second half is in search mode on the Spanish vocabulary. Note that we use the English version of the Spanish law, obtained via MT@EC. The user has already dragged the blue bullet along the word "Media and the press" on top of "Public communication", thus creating an alignment, reported in the left window.

We are currently experimenting on the motivational aspects of our approach. As already mentioned and as graphically indicated by the ticked box dedicated to alignment tweeting, all alignments are tweeted on the @legivoc account, in the hope of motivating users. We also intend to use in the future this medium to keep users informed of legivoc developments and upgrades. Ultimately, users could also contribute their own tweets on this account, on a limited basis.

legivoc as a Web Service

We already alluded to the possibility of accessing legivoc remotely. This can currently be done in two ways: structured or not. The first one is via SPARQL commands (see Section 2) sent to a dedicated legivoc URL: legivoc.org/sparql_form. The first argument, query, is a string corresponding to the command to run, while the second one, db, is the ISO country code of the vocabulary on which the command is to be run. The output uses the XML format required by the SPARQL specifications. This service allows arbitrary, non-modifying requests to be run on the legivoc database, thus providing a powerful and generic API for remote users and servers.

The second access method is via the legivoc.org/search_concepts URL. It can be used to perform non-structured, textual searches on the legivoc database. The output, which includes the matching concepts URIs, with some additional data, is formatted according to the JavaScript Object Notation (JSON) standard.

Alignments, being encoded within legivoc as full-fledged triples, can be retrieved remotely as well as all other data elements.

Obvious security concerns can naturally be raised by such powerful remote access mechanisms. legivoc relies on dedicated cookies to ensure proper, fine-grained user rights management; these small pieces of data are transferred and locally stored after performing POST requests at the legivoc.org/logged_in URL, with proper name and password parameters. These transferred cookies will have to be passed along subsequent data access requests, ensuring that only registered users are granted access to the system.

In order to validate legivoc's remote access approach, it is currently being tested within the legicoop5 network for legislative cooperation between the Ministries of Justice of the European Union.

Conclusion

We presented a new approach to the alignment input process for the international legal vocabularies stored within the legivoc infrastructure. Heavily based on existing W3C standards, it offers both an intuitive and "fun" interactive interface and a remote API. We rely on motivational techniques based on social networks tools such as Twitter to (hopefully) increase the amount of alignment information required to make legivoc a success.

Future work will address reasoning over alignment information, e.g., transitive properties or alignment semantics. On the motivational front, it will be mostly driven by the measured effectiveness of the tools used in legivoc to fuel the alignment process. In addition to relying on community effects, one could, if need be, envision looking at a higher degree of gamification.

Fig. 1 .

 1 Fig. 1. legivoc home page

Fig. 2 .

 2 Fig. 2. Concept for "droit civil" (excerpt)

Fig. 3 .

 3 Fig. 3. Querying the Greek vocabulary

Fig. 4 .

 4 Fig. 4. Greek concepts and labels (excerpt)

Fig. 5 .

 5 Fig. 5. Aligning the UK and English-translated Spanish vocabularies

http://legivoc.org (the site is open, although in an "alpha" version).

http://eurovoc.europa.eu

http://www.plinn.org

http://eucases.eu

http://legicoop.eu

Acknowledgments. We thank Claire Medrala for her help with the implementation of the Twitter interface. We also thank the reviewers for their helping us improve our paper.


Gérald Tenenbaum

Integers with a large friable component

Introduction and statement

It is well-known (see, e.g., ['Te95'], chap. III.3) that the logarithms of the prime factors of an integer normally have exponential growth. Therefore, it is expected that the product of the small prime factors of a typical integer remains small-a device which has been employed by Erdős in many different contexts and for which various effective versions appear in the literature. We return here to the problem of finding a quantitative estimate for the number of exceptional integers. Some similar results have been obtained concomitantly, through a more elementary approach, by Banks and Shparlinski ['BS06'].

Given an integer n and a real parameter y 1, we define

n y := p ν n, p y p ν
as the y-friable component of n and we put

Θ(x, y, z) := n x ny>z 1 (x 1, y 1, z 1).
We also write, for complex s with positive real part,

ζ(s, y) := P (n) y 1/n s = p y 1 -p -s -1 ,
where P (n) denotes the largest prime factor of n with the convention that P (1) := 1, we let designate Dickman's function and we set S(y, z) :=

P (m) y m>z 1 m .
It has been shown in ['Te99'], Corollary 2, that, writing u := (log x)/ log y, we have

(1•1) Θ(x, y, z) = xS(y, z) ζ(1, y) + O x (u)2 (1+ε)u + x ε
uniformly for x 2, y 2, z 2, and also that, denoting Euler's constant by γ, and writing

τ (w) := ∞ w (t) dt (w 0),
we have, with v := (log z)/ log y,

(1•2) S(y, z) = 1 + O log(v + 2) log y τ (v) log y
for all ε > 0 and uniformly for

(1•3) y 2, 1 z exp exp (log y) 3/5-ε .
Thus, for all x 2 and y, z satisfying (1•3), we have

(1•4) Θ(x, y, z) = e -γ + O log(v + 2) log y xτ (v) + O x (u)2 (1+ε)u + x ε .
Note that Θ(x, y, z) = 0 unless z x and that, when the latter holds, (1•3) is implied by Hildebrand's condition (H η )

x 2, exp (log 2 x) 5/3+η y x with η = 3ε.

In particular, if condition (1•3) holds, u → ∞, y → ∞, and, say, z x 1-ε , then

(1•5) Θ(x, y, z) ∼ e -γ τ (v)x.
Formula (1•1) has been derived in ['Te99'] as a by-product of a general result on the Kubilius model of probabilistic number theory. However, the estimates established in ['Te99'] easily yield an asymptotic formula that is valid also when u is bounded. Let ω denote Buchstab's function. We obtain the following result in which we put

σ(u, v) := ∞ v (t)ω(u -t) dt ϑ(u, v) := (u) + σ(u, v) κ(u, v) := (1 -γ) (u -1) + γ (v)ω(u -v) (u 1, v 0).
Theorem 1.1. Let ε > 0. Under conditions (1•3) and 1 z x/y, we have uniformly

(1•6) Θ(x, y, z) = x ϑ(u, v) - κ(u, v) log y + O τ (v) log y + (v) log(v + 2) (log y) 2 + 1 z .
In particular, if (log y) 2 z min x/y 1+ε/ log(u+1) , e √ y , we have

(1•7) Θ(x, y, z) = 1 + O log(v + 2) log y ϑ(u, v)x.
Remarks. (i) The condition z x/y is not restrictive since Θ(x, y, z) = Ψ(x, y) -Ψ(z, y) otherwise.

(ii) It will be clear from the proof that, under suitable assumptions, more precise estimates may be derived by the same method.

(iii) It follows from classical estimates on Dickman's function (see e.g. ['Te95'], chap. III.5) that ['Te95'], chaps. III.5 and III.6), this implies, for instance, that ϑ (u, v) τ (v) whenever u -1v 1/ log(v + 1).

(1•8) τ (w) = (w) log(w + 1) 1 + O 1 log(w + 1) (w 1). Since 1 2 ω(t) 1 (t 1) and (v + h) (v){v log(v + 1)} -h (0 h 1 v)(see e.g.

Proof of 'evalT'

We start with an improvement of (1•2) established by the same method. As usual, we define the derivatives of the Dickman function by right continuity at integer points. It is known (see e.g. ['Te95'], cor. III.5.8.3) that (k) (w) ∼ (-1) k (log w) k (w) as w → ∞. We also denote by {a j } ∞ j=0 the Taylor coefficients of sζ(s + 1)/(s + 1) at s = 0.

Lemma 2.1. Let ε > 0 and k ∈ N be given. Then, uniformly under condition (1•3), we have

(2•1) S(y, z) = τ (v) log y - 0 j k a j+1 (j) (v) (log y) j - Ψ(z, y) z + O (v){log(v + 2)} k+1 (log y) k+1 .
In particular, we have

(2•2) S(y, z) = τ (v) log y -γ (v) + O (v) log(v + 2) log y + 1 z .
Proof. We have

S(y, z) = (log y) ∞ v Ψ(y w , y) y w dw - Ψ(z, y) z .
Inserting Saias' estimate for Ψ(y w , y) (see ['Sa89'] or ['Te95'], th. III.5.9) in its range of validity and estimating the contribution of large w as in ['Te99'], we obtain

∞ v Ψ(y w , y) y w dw = 1 + O e -(log y) 3/5-ε ∞ 0- τ (v -t) d [y t ]
y t . Formula (2•1) follows by integrating by parts and inserting the generalized Taylor expansion for the Dickman function established in ['FT91'], lemma 4.2. We omit the details, which are very similar to those in ['FT91']. Then, we derive (2•2) by appealing to Hildebrand's formula ['Hi86a'] (2•3)

Ψ(z, y) = z (v) 1 + O log(v + 1) log y + O(1) z 2, y e (log 2 z) 5/3+ε .
For y 2, t 1, we write u t := (log t)/ log y.

Lemma 2.2. Under conditions (1•3) and 1 z x/y, we have uniformly

(2•4) P (m) y m>z ω(u -u m ) m = σ(u, v) log y -κ(u, v) + (u -1) + O τ (v) + (v) log(v + 2) log y + 1 z .
Proof. Since ω(s) is continuous for s 1 and differentiable for s > 1, we have

P (m) y m>z ω(u -u m ) m = P (m) y z<m x/y 1 m 1 + u-1 um ω (u -t) dt = S(y, z) -S(y, x/y) + u-1 v ω (u -t){S(y, z) -S(y, y t )} dt = ω(u -v)S(y, z) -S(y, x/y) - u-1 v ω (u -t)S(y, y t ) dt.
The required formula then follows by inserting (2•2), using the estimate (1•8). We omit the details which only involve standard partial integration and the fact that ω ∈ L 1 (R).

We are now in a position to complete the proof of 'evalT'.

We first consider the case when (x, y) lies outside the region (H ε ). Appealing to the bound ω(t)e -γ (t) (t 0) established, in a more precise form, in lemma 4 of ['Te99'] and noting that, say, u > 3v provided y is large enough, we see that

σ(u, v) = e -γ τ (v) 1 + O 1/(log y) 2 , κ(u, v) = γe -γ (v) 1 + O 1/(log y) 2 .
Thus (1•6) is in this case an immediate consequence of (1•1) and (2•2).

When (x, y) ∈ H ε , z x/y, we apply the formula Θ(x, y, z) = P (m) y z<m x/y Φ x m , y + Ψ(x, y) -Ψ(x/y, y),

where Φ(t, y) denotes the number of positive integers not exceeding t and all of whose prime factors exceed y. The last two terms may be evaluated by (2•3). Note that Ψ(x/y, y) may be regarded as an error term since this is x (v)/y. Thus, we may restrict our attention to evaluating the m-sum. To this end, we apply Corollary 3 of ['Te99'] By (1•2), the contribution of remainder term of the left-hand side is dominated by that of (1•6) and that of the second term equals -x (u -1)/ log y to within an acceptable error. Since the remaining sum depends on (2•4), this completes the proof of (1•6). Formula (1•7) then follows from the bound τ (v) v -2v .

  u m ) m(log y) 2 (z < m x/y).


Emilio Jesús

Gallego Arias

Pierre Jouvelot

Adventures in the (not so) Complex Space *

We report on the progress of a constructive mechanization for a small subset of signal processing theory, built upon the SSREFLECT and MATHCOMP libraries.

The development was started to provide mechanized semantics for audio programming languages. Currently, we have formalized several standard properties of the Discrete Fourier Transform, such as its unitary matrix form and its power and convolution theorems. Future goals include transfer functions and constant overlap-add processing.

At the workshop, we aim to discuss the needs and limits of our current approach, surveying some mathematical concepts not covered by existing libraries, and similar efforts in other frameworks and theorem provers.

Introduction and Motivation

A key component in audio programming and analysis is the Discrete Fourier Transform (DFT). Its efficient implementation -the Fast Fourier Transform -has made practical a myriad of soundprocessing algorithms, from convolution-based filtering to envelope extraction.

The need for a mechanized treatment of the DFT and its properties arose in our quest to develop a mechanized semantics for Faust [START_REF] Grame | The Faust Project[END_REF], a functional stream-based audio programming language.

Faust's time-domain semantics largely correspond to wellunderstood notions in the synchronous programming paradigm [START_REF] Berry | The foundations of Esterel[END_REF][START_REF] Auger | Compilation Certifiée de SCADE/LUSTRE[END_REF]. However, frequency-domain aspects -central in audio -seem less explored in the literature. Thus, a natural preliminary step was to attempt the mechanization of basic DFT and DSP (Digital Signal Processing) theory.

We have chosen as a reference text the excellent book series by J.O. Smith [START_REF] Smith | Mathematics of the Discrete Fourier Transform (DFT): with Audio Applications[END_REF][START_REF] Smith | Introduction to Digital Filters: with Audio Applications[END_REF][START_REF] Smith | Spectral Audio Signal Processing[END_REF]. Among other nice qualities -like detailed paper proofs -the series is specific to audio applications, reflecting very well the particular, domain-specific considerations of audio DSP. Additionally, the author has ample experience with Faust and stream-based functional audio programming [START_REF] Smith | Audio Signal Processing in Faust[END_REF].

The first book in the series, "The Mathematics of the Discrete Fourier Transform (DFT): with Audio Applications", presents the basic theory about the DFT: linearity, basis, convolution, and power conservation.

Such theorems are far from mathematically challenging, notwithstanding that they pose a few difficulties in the mechanized constructive setting. In particular, the basic theory of the DFT relies on finite and infinite series, linear algebra, trigonometry, and complex analysis.

The first proof in the book is Euler's formula: e ix = cos x + i sin x. Indeed, in DSP trigonometry and complex analysis are pervasive, and most definitions crucially depend on complex exponen- * Research funded by the ANR FEEVER project. tiation. Thus, the logical path to mechanization seems to require a library supporting complex analysis, such as [START_REF] Cruz-Filipe | C-CoRN, the Constructive Coq Repository at Nijmegen[END_REF][START_REF] Boldo | Coquelicot: A User-Friendly Library of Real Analysis for Coq[END_REF][START_REF] Lelay | More than real analysis in Coq[END_REF].

However, we soon realized that good support for advanced linear algebra was maybe even more crucial. For that domain, our preferred choice is the linear algebra library of MATHCOMP [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF].

Unfortunately, integration of MATHCOMP and constructive complex analysis doesn't seem immediate, due to different definitions of key algebraic structures. A combination of MATHCOMP with classical analysis works, and seemed the most viable choice, even if at the cost of abandoning hopes for a constructive, axiom-free development.

But once we were more familiar with standard DSP practice, it became apparent to us that "true" complex numbers were not a hard requirement for the key parts of the discrete transform theory. Indeed, the SSREFLECT constructive algebraic numbers could pack enough power for our needs. 1 This amounts to work in pre-Hilbert spaces, which seems enough for our case.

Indeed, libraries for algebraic numbers, big operators, and matrix libraries [START_REF] Bertot | Canonical Big Operators[END_REF][START_REF] Gonthier | Point-Free, Set-Free Concrete Linear Algebra[END_REF] have made our job straightforward, to the point that it has felt like an exercise. It is also remarkable how close our proofs are to the pen and paper versions.

Most of our time was spent in proving some technical lemmas about primitive roots of the unity, and by finding a convenient definition of inner product of (algebraic) vectors. Another remarkable fact of the library is that we didn't use induction in the whole development, "all the required induction was already contained in the provided lemmas".

In the rest of the abstract, we give a quick overview of the development, to briefly conclude with some thoughts on related and planned work. An version of the code is available at https://www.cri. ensmp.fr/people/gallego/coq-2015/dft.v; we warn the reader that it is quite in-flux, we expect it to significantly change in the next weeks. We also hope that the expert reader will excuse our lack of knowledge about the vast MATHCOMP libraries; given its sheer size it could be well the case that we are redefining already present notions nor using it in an optimal way.

The Basic Ingredients

Inner Products, Normed Vector Spaces We work over the algebraic numbers C. For any x ∈ C, x = x + i x, where i 2 = -1. The conjugation of a number is given by x + iy = x -iy.

Assume x, y ∈ C n , elements of the vector space obtained by n copies of C. We will identify C n with time-sampled signals of n samples. Then the inner product of x and y is x, y = n-1 m=0 x(m)y(m), and a norm is then defined as x =

x, x .

We write x ⊥ y for x, y = 0, and we say that x and y are orthogonal.

We assume our vector spaces to be cyclic, that is, for x ∈ C n we perform indexing modulo n. We also have a shift operator, SHIFT k x(n) = x(n -k mod n).

Roots of the Unity

A n-root of the unity is any z such that it is a solution of the polynomial z n = 1. Informally, a primitive root of the unity is a generator of all the other roots. Given ω a primitive root, some properties of interest are n-1 m=0 ω m = 0, |ω| = 1, etc. . . Given s k ∈ C n such that s k (n) = ω kn , we have

s k ⊥ s l ⇐⇒ k = l.
The Discrete Fourier Transform We define the DFT as:

DFT k x = n-1 m=0 x(m)ω mk .
The definition in matrix form is also concise and convenient:

Definition W := \matrix_(i < n, j < n) ' ω ˆ+ (i * j).
Linearity follows directly, while the shifting lemma:

DFT k (SHIFTm x) = ω m k DFT k x can be proved in 3 lines.
Convolution The relation of DFT with convolution is a key property; using the efficient form of the DFT (FFT), we can perform convolution -and thus FIR filtering -in O(n log n) vs O(n 2 ).

Definition 1 (Circular Convolution).

(x y)(k) = n -1 m=0 x(m)y(k -m) Theorem 1 (Circular Convolution). DFT k (x y) = DFT k x • DFT k y
Commutativity of convolution needs 3 lines of proof; the convolution theorem, 5.

Unitary Property Define the Hermitian transpose of a matrix A * ≡ A T . A matrix is unitary if A * A = AA * = I. This states that the columns of A are orthogonal. For the DFT matrix W, we have W * W = WW * = nI, and thus its normalized form W = 1 √ n W is unitary. The Power Theorem In particular, this implies the power theorem:

x , y = 1 N DFT x , DFT y
of which an easy corollary is Parseval's:

x 2 = 1 N DFT x 2 .

What's next?

We are still working on completing and cleaning up the development: improving naming, trying to find the best interfaces for some of our tasks -namely exponentiation modulo, inner products, Vandermonde or unitary matrices -and exploring other related finite transforms like [START_REF] Brown | Calculation of a constant Q spectral transform[END_REF]. Studying the relation of our approach to rational trigonometry could be interesting too.

Algebraic Signal Processing

The next candidate for mechanization is the Z-transform, a generalization of the Fourier transform that replaces the roots of unity by an arbitrary complex number z.

The Z-transform reduces analysis of linear systems to their "transfer functions" and "region of convergence", that is to say, values of z for which the transform converges.

The Z-transform has been recently mechanized in a classical setting [START_REF] Siddique | On the Formalization of Z-Transform in HOL[END_REF], allowing the verification of linear systems, although no convolution is included.

Unfortunately for us, the Z-transform is essentially defined as an infinite time summation, which doesn't translate well to the approach we have followed here. Notwithstanding, there exists work in algebraic signal processing [START_REF]Algebraic Theory of Signal Processing[END_REF][START_REF] Püschel | Algebraic Signal Processing Theory[END_REF] that allows the definition of a finitary version of the Z-transform based on polynomial algebras. The concrete details are outside of the scope of this abstract, but the basic idea is to view linear filters as an algebra A, with filtering defining an A-module over the vector space V of signals. In this setting, the values z ∈ ROC act as generators for the polynomial algebras, with elements in the sequence space 1 for the infinite time case, etc... Going to the Infinite It would be very interesting to extend our formalization to the infinite-dimensional case. However, we would lose the great convenience that the big operators and linear algebra libraries offer.

Extending big operators to handle infinite sums is far from trivial, we believe that mainly due to convergence issues. Indeed, in [START_REF] Siddique | On the Formalization of Z-Transform in HOL[END_REF] linearity theorems for the Z-transform only hold if z ∈ ROC . A possibility would be to pack convergence proofs in the operator itself, or to extend the base type to include elements capturing divergence, as done in other approaches.

Efficient, Certified Computation It could be worth to try to use existing tools for effective linear algebra [START_REF] Dénès | A refinement-based approach to computational algebra in COQ[END_REF] to achieve verified computation of the DFT. It would mainly require computation over the algebraic numbers; the rest would be captured by the existing matrix multiplication. Going beyond that and refining the algorithm to the FFT [START_REF] Capretta | Certifying the Fast Fourier Transform with Coq[END_REF] is possible, but likely to be quite challenging.

Indeed, in a presentation preceding this work, the first author was asked whether the algebraic numbers would suffice. We wrongly responded no; however there are still corners of the theory that may be difficult to capture without working in a complete metric space.