Jonathan Aigrain

Séverine Dubuisson

Marcin Detyniecki

Mohamed Chetouani

Person-specific behavioural features for automatic stress detection

This paper introduces behavioural features for automatic stress detection, and a person-specific normalization to enhance the performance of our system. The presented features are all visual cues automatically extracted using video processing and depth data. In order to collect the necessary data, we conducted a lab study for stress elicitation using a time constrained arithmetic mental test. Then, we propose a set of body language features for stress detection. Experimental results using a SVM show that our model can detect stress with high accuracy (77%). Moreover, person specific normalization significantly improves classification results (from 67% to 77%). Also, the performance of each of the presented features is discussed.

I. INTRODUCTION

One of the key elements in human-human interaction is to understand the nonverbal cues and the social signals of the person we are communicating with. It has been shown that nonverbal communication conveys an important part of the meaning of a message [START_REF] Ekman | Hand Movements[END_REF], [START_REF] Ekman | Detecting Deception From The Body Or Face[END_REF], [START_REF] Wallbott | Bodily expression of emotion[END_REF]. Designing machine sensing and understanding social signals is a difficult task, since the meaning of these signals is person and context dependent. In this paper, we focus on the specific context of stressful situations, and we aim at automatically detect the presence of stress by studying the body language.

Automatic detection of stress is an emerging domain. It faces issues related to the difficulty to obtain a natural database and to ethical problems. Current detection techniques are based mainly on speech signals [START_REF] Fernandez | Modeling drivers' speech under stress[END_REF], [START_REF] Lefter | automatic stress dectection in emergency calls[END_REF] and/or from physiological signals, using either traditional sensors (ECG, skin conductance, . . . ) [START_REF] Barreto | Non-intrusive Physiological Monitoring for Automated Stress Detection in Human-Computer Interaction[END_REF], [START_REF] Gaggioli | A system for automatic detection of momentary stress in naturalistic settings[END_REF], [START_REF] Healey | Detecting Stress During Real-World Driving Tasks Using Physiological Sensors[END_REF], [START_REF] Shi | Personalized Stress Detection from Physiological Measurements[END_REF] or hyperspectral images [START_REF] Chen | Detection of Psychological Stress Using a Hyperspectral Imaging Technique[END_REF].

In [START_REF] Fernandez | Modeling drivers' speech under stress[END_REF] and [START_REF] Healey | Detecting Stress During Real-World Driving Tasks Using Physiological Sensors[END_REF], stress is detected though voice and physiological signals during a real-world driving-task. However, in this context, voice and physiological signals are not necessarily the most suited sources in order to detect stress. Someone who is driving does not always talk enough, and physiological sensors are obstructive. In this case, cues extracted from the body language are likely to be the most convenient sources of information to assess stress since they can be captured by camera sensors. To our knowledge, there are few papers adressing stress detection using body language. Giakoumis et al. [START_REF] Giakoumis | Using activity-related behavioural features towards more effective automatic stress detection[END_REF] showed that behavioural features enhanced the performance of automatic stress detection systems using physiological features. Soury [START_REF] Soury | Détection multimodale du stress pour la conception de logiciels de remédiation[END_REF] used This work was partially supported by the Labex SMART (ANR-11-LABX-65) under French state funds managed by the ANR within the Investissements d'Avenir programme under reference ANR-11-IDEX-0004-02.

postural features in a multimodal fusion model, but in this work, this modality turned out to be the least efficient.

However, the correlation between behavioural cues and affective states has been extensively studied, mainly for automatic emotion recognition [START_REF] Glowinski | Toward a Minimal Representation of Affective Gestures[END_REF], [START_REF] Hoey | Body Movements for Affective Expression : A Survey of Automatic Recognition and Generation[END_REF], [START_REF] Kleinsmith | Affective Body Expression Perception and Recognition: A Survey[END_REF] and expression synthesis [START_REF] Caridakis | Synthesizing Gesture Expressivity Based on Real Sequences[END_REF], [START_REF] Hoey | Body Movements for Affective Expression : A Survey of Automatic Recognition and Generation[END_REF], [START_REF] Kleinsmith | Affective Body Expression Perception and Recognition: A Survey[END_REF], as well as in the psychology [START_REF] Ekman | Hand Movements[END_REF], [START_REF] Ekman | Detecting Deception From The Body Or Face[END_REF], [START_REF] Wallbott | Bodily expression of emotion[END_REF]. However, though most of the affective information studied can be used to effectively detect a large number of emotions, there likely are some visual cues that are specific to the expression of stress.

In this paper, we present the first results of a preliminary study on stress detection by extracting and analyzing human body features. This paper is organized as follows: Section 2 reports the stress concept by reviewing the different approaches in the psychology literature. Section 3 presents our lab study for stress elicitation, in particular the protocol, the setup and the annotation of the subjects' stress level. Section 4 describes our feature extraction framework. Section 5 presents the person-specific normalization and its motivation. Section 6 outlines and discusses the results obtained by our learning approach based on SVM. We present the impact of kernel functions, person-specific normalization and features used. Finally, Section 7 concludes by discussing future research directions.

II. THE STRESS CONCEPT

The term stress appeared in the medical literature in 1950s [START_REF] Lyon | Stress, Coping, and Health[END_REF]. Since then, it has been widely used [START_REF] Koolhaas | Stress revisited: a critical evaluation of the stress concept[END_REF], [START_REF] Lyon | Stress, Coping, and Health[END_REF]. Holmes and Rahe [START_REF] Holmes | The social readjustement rating scale[END_REF], when developping a tool called the Social Readjustment Rating Scale (SRRS), described stress as a set of events that require a fixed amount of adjustement. In this case, stress is used as the stimulus that triggers the adaptation, but it can also be used to describe the response to a stimulus. Hans Selye viewed stress as the "nonspecific response of the body to noxious stimuli" [START_REF] Selye | The stress of life[END_REF]. In his work, he described a noxious stimulus as a stimulus that threatens homeostasis, the body "preferred" set-point for physiological variables.

One of the main problems in both Holmes' and Selye's conceptions of stress is the absence of impact from individual perception of the stimulus. Ursin et al. [START_REF] Ursin | Psychobiology of stress -a study of coping men[END_REF] later demonstrated that coping behaviour reduced physiological activity. Thus, we think that transactional models of stress such as those presented in [START_REF] Lazarus | From psychological stress to the emotions: a history of changing outlooks[END_REF], [START_REF] Levine | Developmental determinants of sensitivity and resistance to stress[END_REF] fits better our intuitive vision of stress. These models present stress as a process that includes the stimulus, the appraisal of the situation and the physiological, behavioural and psychological reactions.

In addition, Koolhaas et al. [START_REF] Koolhaas | Stress revisited: a critical evaluation of the stress concept[END_REF] stated that the stimulus had to be uncontrollable and/or unpredictable in order to define this process as stress.

The protocol of our stress-induction experiment is mainly based on the transactional definition of stress.

III. DATA COLLECTION

In this section, we present how we collected the data through a stress-induction experiment.

A. Stress induction procedure

According to Dickerson and Kemeny [START_REF] Dickerson | Acute stressors and cortisol responses: a theoretical integration and synthesis of laboratory research[END_REF], the best way to increase a subject's cortisol level, which is largely considered as being correlated to psychological stress [START_REF] Cohen | Psychological Stress and Disease[END_REF], [START_REF] Dickerson | Acute stressors and cortisol responses: a theoretical integration and synthesis of laboratory research[END_REF], [START_REF] Lyon | Stress, Coping, and Health[END_REF], [START_REF] Soury | Détection multimodale du stress pour la conception de logiciels de remédiation[END_REF] is to make her perform a task that combines public speaking and cognitive challenges. Indeed, tasks that contain uncontrollable traits and/or social evaluation are the most stressful ones. Thus, we designed an evaluated timeconstrained mental arithmetic test. Figure 1 shows a screenshot of the test. The question asked is shown in the middle of the screen. There are two possible answers below it. At the bottom, the progress bar represents the time limit for the current question. On the right is the score bar, which gives the subject a feedback of her performance. The color of the score bar has a meaning: green means "above average", yellow "average" and red means "below average".

The test is composed of 6 steps of increasing difficulty. The three first steps contain 20 questions, the others contain 30 questions. The timing of each step is about 1 minute and there is a break period of 5 seconds between them. The subjects are told that both quickness and correctness of their answers are taken into account for their score. It gives the subject the impression of being evaluated, but in reality the values the score bar shows are set in advance. It displays an "above average" score at the beginning. Thus, the participant finds the test easy enough and feels like she should suceed. Then, the score drops to "average" and "below average" levels, giving the participant the impression she is failing the test.

B. Stress level annotation

At the end of the test, a questionnaire including stress self-assessment is conducted for each step of the test, using a Likert-scale [START_REF] Barreto | Non-intrusive Physiological Monitoring for Automated Stress Detection in Human-Computer Interaction[END_REF][START_REF] Bernhardt | Detecting affect from non-stylised body motions[END_REF][START_REF] Bianchi-Berthouze | On Posture as a Modality for Expressing and Recognizing Emotions[END_REF][START_REF] Caridakis | Synthesizing Gesture Expressivity Based on Real Sequences[END_REF][START_REF] Chen | Detection of Psychological Stress Using a Hyperspectral Imaging Technique[END_REF]. Since the quality of the annotation is greatly dependent of subjects' memory, they watch their own videos of the different steps before giving a stress level.

Self-assessment has been chosen because it is the most faithful annotation to the used definition of stress, which gives great importance to the personal perception. In addition, annotation based on judgement of human experts can induce a bias in the performance of some features, and there were some cases where annotators did not achieve a good agreement score [START_REF] Soury | Détection multimodale du stress pour la conception de logiciels de remédiation[END_REF]. Regarding the use of hormone levels for annotation, [START_REF] Weisman | Oxytocin shapes parental motion during father-infant interaction[END_REF] has shown that the difference in dynamics between behaviour and hormone levels makes it complex, but it will be investigated in future works.

C. Experimental setup

Participants are standing at a distance of around 3 meters from the screen where the test is displayed. For each question, they have to clearly express to a staff member which answer they choose among the two propositions. Video and skeleton data were collected with a Microsoft Kinect placed under the screen. A high definition camera located above the screen provides an optic zoom of the particpant's face.

D. Participants

Fourteen subjects participated in the experiment (3 women, 11 men, mean age = 24.8 ± 2.8 years old). Each subject is aware of the purpose of the experiment, but do not know about the biased behaviour of the score bar, and gives written consent.

E. Acquired data

For each of the 14 partipants, for each of the 6 steps, the acquired data are:

• video of the whole body in 640 × 480 from the Kinect • skeleton from the Kinect • video of the face in 1440 × 1080 from the HD camera • self-assessed stress level The average duration of a video is 57.8 seconds ± 12.6.

IV. FEATURE EXTRACTION

In this section, extracted features and procedures to extract them are described. First, the features extracted from the Kinect video are presented, followed by those extracted from the video of the face. All features are computed over the whole video for each step of the protocol. They are summarized in Table II.

A. Body activity features

There is few research of how stress can affect our body language. However, in order to recognize or to regenerate someone's affective state, there are several sets of features extracted from the body that are usually used: the body activity [START_REF] Caridakis | Synthesizing Gesture Expressivity Based on Real Sequences[END_REF], [START_REF] Giakoumis | Using activity-related behavioural features towards more effective automatic stress detection[END_REF], [START_REF] Glowinski | Toward a Minimal Representation of Affective Gestures[END_REF], [START_REF] Kleinsmith | Affective Body Expression Perception and Recognition: A Survey[END_REF], posture information such as symmetry [START_REF] Giakoumis | Using activity-related behavioural features towards more effective automatic stress detection[END_REF], [START_REF] Glowinski | Toward a Minimal Representation of Affective Gestures[END_REF], center of gravity displacements [START_REF] Giraud | Assessing postural control for affect recognition using video and force plates[END_REF], or the spatial extent [START_REF] Caridakis | Synthesizing Gesture Expressivity Based on Real Sequences[END_REF], [START_REF] Glowinski | Toward a Minimal Representation of Affective Gestures[END_REF], kinematics information such as smoothness [START_REF] Caridakis | Synthesizing Gesture Expressivity Based on Real Sequences[END_REF], [START_REF] Glowinski | Toward a Minimal Representation of Affective Gestures[END_REF] and detection of specific gestures [START_REF] Giakoumis | Using activity-related behavioural features towards more effective automatic stress detection[END_REF], [START_REF] Glowinski | Toward a Minimal Representation of Affective Gestures[END_REF].

Using the skeleton and the video captured by the Kinect, 3 categories of features are extracted: the Quantity of Movement (QoM) and its derivatives, the detection of periods of high activity and posture changes and the detection of selftouching in the region of the head.

1) Quantity of Movement: The QoM is the activity of the body or of some parts of it. For a given frame, we compute the QoM in two different ways. The first one (SQoM) uses the skeleton extracted by the Kinect and is the sum of the displacements of each joint between two frames.

QoM skel (i) = ∑ j∈ joints (v j i -v j i-1 ) 2
with i the frame index and v j i the 3D position vector of the joint j in the i th frame. We also compute the QoM using RGB videos, and call it IQoM. This corresponds to the number of pixels that have changed between successive frames.

QoM video (i) = Card({p i |abs(p i -p i-1 ) > t})
with p i the RGB vector of pixel p for the i th frame and t a threshold. Once the QoM has been computed on all frames, the mean value is used as the feature. In order not to be biaised by the size of a person, it is also divided by the surface of the bounding box containing the skeleton.

The SQoM is computed separately for the whole body and the head (HeM). For the head only, we also compute the SQoM following Z-axis only (HeMZ). For the body only, the Fourier transform of the signal is calculated, divided into 10 bins (FFT1 -FFT10), which gives frequency information about the subject's activity.

2) Detection of high activity periods and posture changes: Using the peaks of the QoM computed for each frame, the periods of high activity are extracted (see Fig. 2) . The number of periods (HAPC), their mean duration (HAPMD) and their mean intensity (HAPMV) are used as features. For each peak, the frame at the beginning and the one at the end are compared to determine whether the person has changed her posture. The number of posture changes (PCC) is used as a feature. We make the hypothesis that posture changes may reflect an increasing uncomfortability.

3) Detection of self-touching: It has been shown that selftouching can be an indicator of negative affect [START_REF] Harrigan | Self-touching as an indicator of underlying affect and language processes[END_REF]. We detect self-touching in two parts of the body: the head and the hands. To detect whether a person is self-touching in the region of the head, we compute the distance between hand, head and neck joints. If one of the distances is below a Fig. 2. Example of detection of a posture change. The left image is the frame at the start of the peak, the middle image is the frame at the end, and the right one is the difference between the two others threshold, the person is considered as self-touching the head (see Fig. 3). The number of times we detect a single hand as self-touching the head (STHC) and the mean duration (STHMD) of it are used as features. We extract the sames features in cases of two hands face-touching (ST2HC and ST2HMD). The detection of hand self-touching is more complex. Indeed, the skeleton given by the kinect cannot be used alone in order to detect movements such as fingers rubbing. Thus, we compute the extraction of this feature as follows:

• Detection of the hands: because the skeleton provided by the Kinect can be imprecise in terms of joint location, we also use skin detection to find a more reliable position of the hands. Thus, starting from the original hand joint position, we look for the closest pixel where skin has been detected. This becomes the new hand position. • Computation of the QoM: using the position we detected, we extract the sub-image of the hands. Then, we compute the video QoM between following hands frames. The QoM for each hand separately (LHM for the left hand and RHM for the right one) and the QoM of both hands (HM) are used as features.

B. Facial features

Using the method described in [START_REF] Nicolle | Facial Action Unit Intensity Predicition via Hard Multi-task Metric Learning for Kernel Regression[END_REF], we extract the activation level of 12 Action Units (AU). Action Units are presented by Ekman in the Facial Action Coding System (FACS) [START_REF] Ekman | Facial action coding system[END_REF], which is a common standard to systematically categorize the physical expression of emotions. The 12 AU extracted are described in Table II. Since the activation level is given by frame, we compute the mean over all frames and the standard deviation for each AU as features.

V. PERSON-SPECIFIC NORMALIZATION

In addition to testing the features, the impact of a personspecific normalization is evaluated. As said in [START_REF] Shi | Personalized Stress Detection from Physiological Measurements[END_REF] regarding physiological signals or in [START_REF] Bernhardt | Detecting affect from non-stylised body motions[END_REF] regarding body motions, the evolution of the signal compared to a personal baseline is likely to be more meaningful than its absolute value. Thus, for each person, we compare the value of each feature to its value during the first step of the experiment, considered as non-stressful.

f p j = f p j -f p1 f p1
where p a person, j the step the video has been extracted from, f p j the vector of features for the person p on step j and f p j the normalized vector. Thus, the features are expressed as an evolution percentage rather than a raw value.

VI. STRESS DETECTION

This section presents the results obtained by our model. First, the evaluation process is described. Then, the impact of several parameters -the SVM kernel function, the personspecific normalization and the different features -are discussed.

A. Evaluation process

In order to test whether our features are predictive or not, we use Support Vector Machines (SVMs) to build a classification model. Each video is associated with a label: stress (S) for video associated with a stress level above or equal to 4, non-stress (NS) for the remaining ones. For each evaluation, we use a leave-one-subject-out cross validation: videos from all people but one person are used as the training set, and the videos of the remaining person is used as the testing set. This cross validation is repeated 10 times in order to reduce the impact of randomness in the SVM margin initialization. The mean accuracy and its standard deviation are presented.

We discard videos that are labelled as non-stress if they followed a stress labelled video. These videos represent people acknowledging that they psychologically gave up because of the difficulty. Thus, the accuracy is computed on 76 out of the 84 videos for raw features, 49 labelled as non-stress and 27 labelled as stress. Since the person-specific normalization uses the features extracted from the first step, the accuracy is computed on 62 videos for normalized features, 35 labelled as non-stress and 27 labelled as stress. III shows the results obtained by 3 different kernel functions: the Radial Basis Function (RBF), the polynomial of degree 5 (Poly 5) and the linear kernel. There is no significant difference between the 3 kernels concerning the mean accuracy. Since the linear kernel is known to be faster to train, we have chosen to keep it for the following experiments.

B. Results

2) Impact of the person-specific normalization: It clearly appears that using the person-specific normalization significantly improves classification results, by 13%, 11% and 10% for the polynomial, RBF and linear kernels, respectively as shown in Table III. However, as we can see with Table IV, the normalization is not effective on facial features. This might be explained by the much smaller range of values the facial features can take compared to body features. Indeed, facial features values vary from 0 to 5, and there is little difference in scale among the participants. In comparaison, the IQoM can be 30 times bigger from a subject to another. 3) Performances of facial versus body features: Table IV shows the impact of the choice of features on the classification accuracy. When using raw features, facial features give better results than body features. This is probably due to smaller inter-individual differences with facial features. However, information on the evolution of body features are much more discriminative than information on the evolution of facial expressions. This confirms the idea that body language can bring valuable information to determine someone's emotion state.

4) Performances of individual features:

In order to better understand the relevance of each feature, we calculated their classification accuracy if used alone. We use the RBF kernel to compute these results, since a linear kernel would allow only a single "split value" along the feature axis. The results for raw features are presented in features. Thus, we can see that a single feature can be enough to detect stress with good accuracy. Among these features, it appears that brows activity as raw features is a valuable information for our study. Indeed, AU4 and AU9 are correlated since AU4 is often activated when AU9 is. The number of times a subject changes its posture also achieve good classification results, both for raw and person-specific features. Features on body activity level such as FFT1 or information on periods of high ativity also achieve good accuracy as person-specific features. It is however difficult to interpret what FFT7 really means in an intuitive way. Finally, we can see that person-specific normalization works well for body features, but not for facial ones. Figure 4 shows how normalization on FFT 1 improved the seperation between the two classes. The 5 best person-specific features are body features, and the 5 worst are all facial features. This observation can not be made for raw features, where body and facial information are both represented in the best and worst features.

VII. CONCLUSIONS AND FUTURE WORKS

In this paper, we have presented behavioural features for automatic stress detection, and a person-specific normalization to enhance the performance of our system. We have discussed the stress concept and presented a set of 49 automatically extracted behavioural features. We also observed that a person-specific normalization significantly improved the performance of our model, and that, for our study, the body language of the subjects provided more valuable information than their facial expressions. Finally, we saw that it is possible to have an unobtrusive stress detection system using only video and depth data.

However, the results obtained can still be improved. The results presented in Table VII and VIII clearly show that some features do not bring valuable information and thus should not be included training the SVM. Preliminary tests on feature selection showed promising results for classification accuracy. Moreover, we saw that person-specific normalization is effective only for body features. Trying to include both raw facial and person-specific body features in our model may give interesting results.

Finally, more subjects will participate in our experiment. However, they will not be aware of the purpose of the study. Thus, we will be able to observe the impact of individual perception of a situation on stress level.

Fig. 1 .

 1 Fig. 1. Screenshot of the test software used for the study

Fig. 3 .

 3 Fig. 3. Examples of detection of self-touching in the region of the head. On the left is an example of self-touching with one hand. On the right is an example with two hands

Fig. 4 .

 4 Fig. 4. Distribution of FFT 1 raw and normalized values

TABLE VII FIVE

 VII BEST AND FIVE WORST RAW FEATURES ACCORDING TO THEIR CLASSIFICATION ACCURACY IF USED ALONE USING THE RBF KERNEL.

	feature	accuracy
	PCC	0.73 ± 0.02
	AU9 -std	0.72 ± 0.01
	FFT2	0.72 ± 0.01
	AU4 -std	0.72 ± 0.01
	AU4 -mean	0.72 ± 0.01
	AU25 -mean 0.60 ± 0.03
	RHM	0.58 ± 0.01
	AU5 -std	0.58 ± 0.02
	AU9 -mean	0.56 ± 0.01
	HAPMD	0.55 ± 0.04

  Table VII, those for personspecific features in Table VIII. Concerning raw features, we can see that several features achieve better average classification accuracy when used alone than when combined with others. FFT1 for person-specific features also achieve alone a similar score to what we obtain with all normalized

TABLE VIII FIVE

 VIII BEST AND FIVE WORST PERSON-SPECIFIC FEATURES ACCORDING TO THEIR CLASSIFICATION ACCURACY IF USED ALONE USING THE RBF

	KERNEL.
	feature	accuracy
	FFT1	0.76 ± 0.02
	HAPC	0.74 ± 0.01
	FFT7	0.73 ± 0.02
	HAPMV	0.73 ± 0.02
	PCC	0.73 ± 0.02
	AU1 -std	0.49 ± 0.03
	AU25 -mean 0.46 ± 0.02
	AU26 -mean 0.45 ± 0.02
	AU15 -mean 0.45 ± 0.03
	AU17 -std	0.43 ± 0.04


Orlarey Yann
email: orlarey@grame.fr

Grame

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

Signal Rate Inference for Multi-Dimensional Faust

Keywords: Faust, audio signal processing, type systems

We introduce a new signal-level, type-and rate-based semantic framework for describing a multi-rate version of the functional, domain-specific Faust language, dedicated to audio signal processing, and here extended to support array-valued samples. If Faust is usually viewed as a formalism for combining signal processors, which are expressions mapping input signals to output signals, we provide here the first formal, lower-level semantics for Faust based on signals instead. In addition to its interest in understanding the inner workings of the Faust compiler, which uses symbolic evaluation of signal expressions, this approach turns out to be useful when introducing a language extension targeting multi-rate and multi-dimensional (array-valued) processing.

More precisely, we provide (1) new syntax and dynamic semantics for (recursive) Faust-based signals, (2) a type and, more interestingly, rational rate static semantics and (3) a new rate inference algorithm, together with its soundness and (relative) completeness theorems. Preliminary experiments in a prototype implementation of this extension in the Faust compiler are underway.

INTRODUCTION

The specifics of computer music call for the design and implementation of domain-specific programming languages (DSL) [START_REF] Barkati | Synchronous programming in audio processing: A lookup table oscillator case study[END_REF]. Faust [START_REF] Orlarey | Syntactical and semantical aspects of Faust[END_REF] is one of these languages for real-time signal processing applications, in particular real-time audio processing; it boasts a thriving community of users, both in academia (e.g., [START_REF] Smith | Introduction to Digital Filters: With Audio Applications[END_REF]) and industry 1 . Faust is based on a few core foundational principles.

Real-time signal processing. Because of its real-time target, Faust is focused on the specification and efficient implementation of programs based on causal 1 See, for instance, http://faustone.com.

ACM ISBN 978-1-4503-2138-9. DOI: 10.1145/1235 computations, with bounded memory and CPU footprints, and minimal latency.

Simple well-defined formal semantics. Faust is not intended to model the internal behavior of systems or circuits. The only "interesting" semantics in is the one that can be observed from the outside, that is of a function that maps a tuple of time-dependent input signals to a tuple of output signals.

High-level specification. Faust is designed to be a highlevel specification language rather than an implementation language. A key design choice is to make a clear separation between the users' role, in charge of specifications, and the role of the compiler, in charge of implementing them. The way the user writes a Faust program should not matter; only its meaning should count. Ideally two different Faust programs with the same meaning should have the same implementation2 .

Functional approach. Functional programming provides Faust with a high level of modularity, both to compose and understand Faust programs. Moreover it offers a very natural framework for signal processing.

Periodically-sampled digital signals can be modeled as functions of time. Signal processors, which are Faust primary constituants, are second-order functions operating on signals. Faust block-diagram algebra is a set of third-order composition operations on signal processors. Finally, user-defined functions are higher-order functions on block-diagram expressions.

The current version of Faust is monorate: all signals are isomorphic to functions mappings integers (clock ticks) to (scalar) sample values. In [START_REF] Jouvelot | Dependent vector types for data structuring in multirate Faust[END_REF], an innovative extension to Faust for handling both different clocks and multi-dimensional samples has been proposed: these features are of key import when targeting efficient spectral processing applications. These clocks are introduced here as rational rates that interact with the size of the array-valued samples. When building a signal of vectors of size n from a signal of rate r carrying scalar, integer say, samples, one gets a signal operating at rate r/n; conversely, serializing a signal of rate r carrying samples that are vectors of size n, the resulting signal has a rate rn. The overall purpose of this paper is to describe how this approach can be handled within the Faust compiling infrastructure, while maintaining the general design principles sketched above.

To fulfill its goals, the Faust compiler uses optimization techniques based on a blend of symbolic evaluation and abstract interpretation approaches. Instead of using Faust signal processors directly as its core data structure to compile user code, it uses an intermediate representation (Faust IR) based on signal expressions 3 . Basically, a Faust signal processor is first converted to a tuple of signal expressions during a phase of symbolic propagation performed in the compiler front-end. For example, the signal processor + abs process process = + : abs ;

expects two (the arity of +) inputs, sums them and feeds the result (via the combinator :) to the absolute value signal processor. This Faust signal processor expression is converted into the Faust IR signal expression abs(I0 + I1) after propagating the tuple of input signals I0, I1 ; as explained below, input signals are members of the dedicated domain I of symbolic identifiers. New tuples X = X0, ..., Xn of signal identifiers Xi are introduced, together with their definitions D(X) as tuples of signal expressions, when ~-recursive expressions occur in Faust. For instance, the signal processor + process process = + ~_ ; both outputs a signal S and feeds back (via the _ identity signal processor) this same S, after a one-sample delay, as the first argument of the + signal processor. This signal processor expression is converted to the signal expression X0, together with a binding D(X) = X0@1 + I0 where 4 X = X0 , after propagating the tuple of input signals I0 ; there, the @n expression denotes a n-sample delay operation. A more complex example, introducing vector features, is given, in a graphical representation actually generated by the Faust compiler, in Figure 2.

In this paper, we provide the following contributions: 3 In fact, the Faust compiler uses various IRs; we concentrate here on the signal-level Faust IR. 4 Here, X is a tuple, since there may be multiple recursive signals in a single recursive signal processor expression.

• the first formal definition of Faust IR, including its extension to handle the new multi-rate framework of [START_REF] Jouvelot | Dependent vector types for data structuring in multirate Faust[END_REF];

• a new definition of multi-rate signals, based on a rational model for its clocking mechanism;

• a new rate inference algorithm, for which both soundness and (relative) completeness theorems are specified and proven;

• a prototype implementation of this algorithm in an experimental multi-rate version of Faust.

In Section 2, we describe a proposal for multi-rate signals that use rational clocks. A multi-rate Faust IR based on typed and rated signals is introduced in Section 3, together with a clocked semantics and a Rate Subject Reduction property. We provide a set of type and rating rules adapted to multi-rate signals in Section 4 for which we state a (value) Subject Reduction property. The core of the paper is Section 5 where we describe our new rate inference algorithm, together with its soundness and (relative) completeness theorems. We briefly report on the related work in Section 6 and discuss possible future work in Section 7 before concluding.

MULTI-RATE AND -DIMENSIONAL SIG-NALS

Here we are interested in periodically-sampled and multidimensional signals. We consider sampled signals as approximations of continuous signals, and we want to express signals sampled at various rates, but also signals with multidimensional sample values (that is not only signals of numbers, but also signals of fixed-size vectors of numbers, fixedsize vectors of fixed-size vectors of numbers, etc.).

We define below more precisely the notions of time, sample value and signal we are interested in.

Periodic time domain

In order to capture the idea of a sampled signal with a specific sampling rate, we introduce the concept of periodic time domain, notated Tr. The idea is to "sample" the continuous time domain R with a periodicity represented by a rational rate r.

Definition 1 (Periodic time domain). The periodic time domain Tr is the set of rational values corresponding to the periodic r-sampling of the continuous time domain R, i.e.,:

Tr = 1 r Z = { i r | i ∈ Z}, r ∈ Q * .
Here are some examples of time domains:

T1 = {. . . , - 2

Signal

We can define a multi-rate, multi-dimensional signal as a function from a periodic time domain Tr to a set of multidimensional sample values V extended with a distinguished zero value noted 0 V (see Section 2.2.1 for an explanation).

Definition 2 (Multi-rate, multi-dimensions signals). A multirate, multi-dimensional signal s is a function of time, from a periodic time domain Tr to a set of multi-dimensional sample values V or 0 V :

s : Tr → V ∪ {0 V } .
Definition 3 (Simplified notation). To simplify the notation of signal types we will use the following abbreviation:

V r = Tr → V ∪ {0 V } .
Sample values in V can be numbers (integers or floatingpoints) or fixed-size vectors of samples. These values are structurally typed, with a type in a domain T (see Section 4). Moreover numbers can be restricted to belong to an interval [l, h], where l and h are either integers or reals depending of the considered type.

Negative time

The values of signals are usually needed starting from time 0 and up. But to take into account delay operations, negative times are always mapped to zeros. In operational terms, this corresponds to assuming that all delay lines are signals initialized with 0s.

Definition 4 (Negative time). The value of a signal s : V r is always 0 V when t < 0:

∀t ∈ Tr, t < 0 =⇒ s(t) = 0 V .

Constant signal

Because of Definition 4, a constant signal is usually not constant on its whole time domain, but only on its positive half. For example, for the constant integer signal 1 and t ∈ Z ≥ 0, we have 1(t) = 1, but, if t < 0, one has 1(t) = 0 N (see Figure 1). Definition 5 (Constant signal). A signal s : T r is constant iff ∀t1, t2 ∈ Tr, t1 ≥ 0 and t2 ≥ 0 =⇒ s(t1) = s(t2) .

SIGNAL EXPRESSIONS

This section introduces the language of signal expressions that form the basis of Faust IR. We describe its syntax, semantics, including its new multi-rate and multi-dimensional features.

Syntax

Definition 6 (Signal expression). A signal expression (E, D) in S, resulting from the phase of symbolic propagation, is defined by the following abstract syntax:

E ∈ S ::= k | f | In | Xi | E1 E2 | E1@E2 | E ↑ n | E ↓n | v(E, n) | s(E) | E1#E2 | E1[E2] (1)
where all recursively-defined tuple lists of identifiers X = X0 . . . Xn-1 are bound in D, such that:

D(X) = E0E1 . . . En-1 (2)
for a number n ∈ N + of recursively-defining expressions Ei.

In the previous definition, we assume that:

-k is a constant integer signal;

-f is a constant float signal;

-In represents an external input signal;

-Xi, with D(X) = E0E1 . . . En-1 , represents the signal Ei of a group of mutually recursive signals;

-E1 E2 is a generic numerical operation on two signals;

-E1@E2 is a variable delay operation;

-E ↑ n is an up-sampling by a (strictly) positive factor n ∈ N + ; -E ↓n is a down-sampling by a factor n ∈ N + ; -v(E, n) is a vectorization operation of size n ∈ N + ; -s(E) is a serialization of a vector signal; -E1#E2 is a concatenation of two vectors;

-E1[E2] is an access to the element of index E2 of the vector-valued signal E1.

As can be noticed, even though signal expressions can be recursive, the language S is in fact closer to Kleene's primitive recursive functions [START_REF] Kleene | General recursive functions of natural numbers[END_REF] or recurrence equations than to a standard functional programming language. In fact, Faust functional status is mostly embedded in its higher-level, macro subsystem; all higher-order expressions expressed there are evaluated, at compile time, to generate signal expressions in S, which are studied in this paper.

Semantics

We assume that all expressions are decorated with a rate information E (r) ; how to get this information is the main purpose of this paper and is explained below.

We define the semantics Sa(E (r) , D) of a signal expression E of rate r with recursive definitions D (we omit D when not needed in the equations below) in an input environment a, mapping input identifiers to signals, as a function from positive times, in Tr, to values 5 in some V ⊥ V , with V = V ∪ {0 V }. As mentioned above, all signal samples for negative times in Tr have the appropriate 0 V value.

The denotational semantics of a signal expression E (r) based on rational clocks is defined as λt.(Sa(E (r) )t, if t ∈ Tr, and ⊥ V , otherwise) , where S is defined as the least fixed point of the equations

Sa(k)t = k , Sa(f )t = f , Sa(In)t = a(In)t , Sa(Xi, D)t = Sa(πi(D(X)))t , Sa(E1 E2)t = s1(t) s2(t) , Sa(E1@E2)t = s1(t -s2(t)/r) ,
where we note si(t) = Sa(E

(r i ) i
)t the value of Signal si, corresponding to Ei, at Time t, while πi is the i-th projection operator on lists. The multi-dimensional-specific features are (partially) defined as

Sa(E1 ↑ n )t = s1( tr1 /r1) , Sa(s(E1))t = s1( tr1 /r1)[mod(rt, n)], if |s1(t)| = n , Sa(E1 ↓n)t = s1(t) , Sa(v(E1, n))t = [s1(t -(n -1)/r1), ..., s1(t -1/r1), s1(t)] , Sa(E1#E2)t = s1(t)#s2(t) , Sa(E1[E2])t = s1(t)[s2(t)] .
where |v| denotes the length of Vector v.

Discussion

There are a couple of unusual features in the semantics we just introduced. First, note that the recursive signals as defined here are non-causal: nothing prevents meaningless expressions (E, D) such as ( X0 , ⊥[X → X0 + 1 ]), where ⊥ denotes here a mapping for recursive definitions with an empty domain. In practice, the Faust compiler always adds an explicit 1-sample delay in recursive definitions, yielding expressions such as X0 , ⊥[X → (X0@1) + 1 ]). Figure 2 provides an example of the introduction of these explicit delays on feedbacks, on a different example. In the sequel, we will always assume that signal expressions are syntactically causal, along the scheme just presented.

Second, the creation of vectors via the vectorize v construct is designed to minimize latency, a key issue in audio processing. In Faust multi rate, compiled to the signal language presented here, as soon as a single input sample is available, it is padded with 0s and an almost empty vector is output. The vectorize construct semantics is illustrated in Figure 3 (some information regarding a possible implementation of vector operations is provided in Figure 4). This unusual initialization process is designed to ensure the following properties.

Proposition 7 (Vector Commutation Properties). The signal semantics S ensures that:

• vectorize(n):serialize = @(n-1); 5 As usual, a partially-ordered domain X ⊥ X is defined for every set X, such that ⊥X < x for all x ∈ X. A partial function f defined over X and with values in Y can thus be seen as a total function from X to Y ⊥ Y ; its domain of definition Dom(X) is defined as {x ∈ X | f (x) = ⊥Y }. Finally, the upsampling operation does not introduce 0padding as is often done in the literature. As described above, our model keeps the sample value constant between each time tick. Informally, we view the up-and down-sampling operations as performing "focus-varying" approximations over an (ideal) continuous function representing the "actual" signal, viewed as the limit of a family of step functions, i.e., constant over intervals. Performing upsampling this way has the advantage, as we will see, of keeping the upsampled types tight, without having to perform a least upper bound operation with a zero type to accommodate for 0-padding.

TYPING RULES

Types and rates of signal expressions are defined by a set of rules Γ (E, D) : T r indicating how to compute the type T r of a signal expression E with recursive definitions D according to a signal type environment Γ storing type hypothesis for each input and recursive signal. x

Types

0 0 x(0) x(1) x(2) x(3) x(4) x(5) x(6) V[0]:=0 V'[0]:=x(1) V[0]:=x(4) fill V[1]:=0 V'[1]:=x(2) V[1]:=x(5) V[2]:=x(0) V'[2]:=x(3) V[2]:=x(6) V[0] V'[0] V[0] V[1] V'[1] V[1] V[2] V'[2] V[2] V[0] V[1] V[2] V'[0] V'[1] V'[2] V[0] 0 0 x(0) x(1) x(2) x(3) x (4
T ::= int[l, h] | float[l, h] | [n]T ,
where types denote the set of values they abstract. Signals are associated to types derived from the type of their sample values. We note T r the type of a signal that maps the time domain Tr to sample values of type T. This way, a signal in V r has type T r .

Definition 9 (Type model). A sample type T is associated to the set of values M(T) it denotes, defined inductively as:

• {n ∈ Z | l ≤ n ≤ h}, if T = int[l, h]; • {r ∈ R | l ≤ r ≤ h}, if T = float[l, h]; • {(v0, ..., vn) | vi ∈ M(T1)}, if T = [n]T1, i.e.
, the set of fixed-size vectors of n > 0 elements in M(T1).

Note that our interval calculus does not allow for undefined values to occur. It is customary in other languages to assume that a type does not preclude the appearance of undefined values (denoted by the ⊥ V symbol in the language semantics above). Our type system is designed to ensure, at compile time, that such "values" cannot occur in an actual well-typed signal expression; the function it denotes is always total. For instance, a signal expression trying to perform a division operation with a signal of divisors of sample type int[-2, 2] will be rejected by the type checker 6 . Our interval calculus is also used to ensure that audio delay lines have a bounded size (to guarantee a fixed memory footprint for signal processors) and that array sizes are compile-time constants.

Definition 10 (Zero type). Each sample type T has an associated zero type, notated 0 T , defined by the rules below:

0 int[l,h] = int[0, 0] ; 0 float[l,h] = float[0.0, 0.0] ; 0 [n]T = [n]0 T .
When V represents the set of sample values denoted by a type T, we know 0 V has7 also type 0 T . Definition 11 (Type operations). The type domain supports type operations that are either (1) extensions of usual arithmetic operations or (2) a least-upper bound operation . For a generic type operator (including ) and N, N ∈ {int, float}, they are partially defined by the following rules:

int float = float ; [l, h] [l , h ] = [min(l, l ), max(h, h )] ; N [l, h] N [l , h ] = (N N )([l, h] [l , h ]) ; [n]T [n]T = [n](T T ) .
Γ(Xi) = N [l, h] r , N ∈ {int, float} ; Γ(In) = float[-∞, +∞] r , (3)
and, in each binding, for some appropriate N, l, h and r. Note how scalar types are annotated with a value interval. This information is crucial to ensure that Faust expressions can be compiled with a statically-known memory footprint, in particular when handling delay lines. This information is also used to ensure that vector operations are safe: the size information used to create them is know at compile time, while array accesses are known to be within array bounds. As we can see, since Faust is a mostly audio-oriented DSL, it has been decided that only scalar signal types can be assigned to input signals. This means that communications with the outside world are limited to scalar signals (this scalar property is also checked for the resulting output signals), and that vectors can only be communicate in serialized form. While the full audio range is often represented by the interval [-1.0, +1.0] in practice, this restriction is not enforced in Faust and signals can make use of the full floating-point range.

Mutually recursive signals can be seen as additional scalar inputs and outputs, where each output is connected to the corresponding input via a 1-sample delay. The type and rate of the corresponding input and output must be the same. Even though our algorithm could probably handle arbitrary types on recursive signals, we indeed believe that taking a simpler approach is granted in the type of audio applications we envision.

Typing rules

Definition 16 (Delay operation).

Γ E1 : T r 1 Γ E2 : int[k1, k2] r 0 ≤ k1 ≤ k2 Γ E1@E2 : (T1 0 T 1 ) r (Delay)
Definition 17 (Up and Down sampling).

Γ E : T r Γ E ↑ n : T nr (Up) Γ E : T nr Γ E ↓ n : T r (Down)
Definition 18 (Vectorize and Serialize).

Γ E : T nr Γ v(E, n) : [n]T r (Vectorize) Γ E : [n]T r Γ s(E) : T nr (Serialize) Γ Ei : [ni]T r i T = T1 T2 Γ E1#E2 : [n1 + n2]T r (Concat) Γ E1 : [n1]T r 1 Γ E2 : int[k1, k2] r 0 ≤ k1 k2 < n1 Γ E1[E2] : T r 1 (Access)
Definition 19 (Type/rate-correct signal expression). A signal expression (E, D) is said type/rate-correct iff there exist Γ, T and r such that Γ (E, D) : T r .

Definition 20 (Signal type). A signal s is said to have type T r , noted s : T r , iff, for all t ∈ Tr, one has s(t) : T.

Proposition 21 (Subject Reduction). Assume a causal and type/rate-correct signal expression (E, D) such that Γ (E, D) : T r . Then:

• Tr = Dom(Sa(E (r) ));

• and, if a(In) : Γ(In) for all input signals In, then

Sa(E (r) ) : T r .

Note that the first consequence of this Proposition is not as obvious as might be thought at first: if the fact that Dom(Sa(E (r) )) ⊆ Tr is indeed obvious (see Section 3), the equality is a consequence of the typing constraints.

Sample-type inference

In all signal typing rules above but one, sample types and rates are independent. The only one that creates a dependence is (Serialize); the size of the vector of the incoming signal is needed to compute the rate of the output signal. Therefore, we can infer first the sample-types independently, and then the rates, once the type information is available. In this section, we will rewrite the typing rules by separating the sample-types and the rates, in a two-step process.

First, a new, simpler type environment, noted Ω = Ω(Γ), is derived from Γ; it is just a mapping that associates to each x in the domain of Γ the value type T, discarding the rate information r present in Γ(x) = T r .

Second, the sample-type rules are defined as just the signal typing rules of Section 4 where rate information is erased. In each rule, all typing judgments Γ (E, D) : T r are replaced by Ω (E, D) : T.

Lemma 22 (Sample Type Consistency). If Γ (E, D) : T r , then Ω(Γ) (E, D) : T.

Proof. Trivial. Since the datatypes of signal values do not depend on rates, removing rate information does not prevent data-only type checking to proceed.

With this two-step approach, the role of the straightforward sample-type inference algorithm (not presented here) will just be to compute a sample type environment Ω for any given signal (E, D).

RATE INFERENCE

Starting with a tuple of expressions L = E0, E1, . . . that share a common recursive environment D and which, typically, represent the output signals of a Faust program, the rate inference algorithm is a three-stage process that

• extends L with all the recursive subexpressions that can be reached,

• infers a rate environment ∆i for each expression Ei of the extended L,

• and forms ∆ by combining the ∆i together.

Rate environments

Definition 23 (Rate environment). A rate environment ∆ is a mapping that associates to some input signal In and mutually recursive signal Xi a rate r.

Definition 24 (Joinable environments). Two environments ∆1 and ∆2 can be joined, written ∆1 ∆2, iff

∀x ∈ Dom(∆1) ∩ Dom(∆2), ∆1(x) = ∆2(x) . (4)
Definition 25 (Union of joinable environments). The union of two joinable environments ∆1 and ∆2 is written ∆1 ∪ ∆2. The resulting environment is such that:

Dom(∆1 ∪ ∆2) = Dom(∆1) ∪ Dom(∆2) ; (∆1 ∪ ∆2)(x) = ∆1(x), if x ∈ Dom(∆1) ∆2(x), if x ∈ Dom(∆2) . (5)
Definition 26 (Scaled environment). We define n∆ as the environment ∆ scaled by an integer factor n, i.e., such that:

Dom(∆) = Dom(n∆) ; ∀x ∈ Dom(∆), (n∆)(x) = n∆(x) . (6)
Definition 27 (Rate-scalable expressions). A typable expression E is rate-scalable, written Adj(E), if one can scale, or "adjust", its rate r by scaling its environment, i.e., for any signal type environment Γ and type T:

Γ E : T r ⇒ nΓ E : T nr , (7)
where the notion of rate environment scaling is straightforwardly extended to signal type environments Γ. The idea behind rate-scalable expressions is that some signals can have their rate adjusted, i.e., properly scaled, when the context in which they are used requires it, and others don't. For instance, X1 ↓ 3 +2 cannot see its rate, here 1 (constants have a fixed rate of 1), modified, while X1 ↑ 2 +I0, whose rate only depends on the ones of X1 and I0, can indeed be adapted if these do have to change. Our algorithm will take advantage of such flexibility whenever possible. Environments of identifiers that are all rate-scalable are decorated with a rate scalability of 1: ∆ 1 . For other expressions, the environment will be decorated with a 0 value: ∆ 0 . In the sequel, all rate-scalable rate environments are uniform.

Combining rate environments

Definition 30 (Independent rate environments). Two rate environments ∆1 and ∆2 are independent iff

Dom(∆1) ∩ Dom(∆2) = ∅ . ( 8
)
Definition 31 (Dependent rate environments). Two rate environments ∆1 and ∆2 that are not independent are called dependent and thus satisfy the following equation:

Dom(∆1) ∩ Dom(∆2) = ∅ . ( 9
)
Definition 32 (Rate environment addition). The addition

∆ v 1 1 + ∆ v 2 2 of two dependent environments ∆ v 1 1 and ∆ v 2 2
is (partially) defined as follows, for some x ∈ Dom(∆1) ∩ Dom(∆2):

ri = ∆i(x) m = lcm(r1, r2) ( m r1 ) v 1 ∆1 ( m r2 ) v 2 ∆2 ∆ v 1 1 + ∆ v 2 2 → (( m r1 ) v 1 ∆1 ∪ ( m r2 ) v 2 ∆2) v 1 v 2 (10)
Basically, if there is an identifier x in the intersection of the ∆i, we need to be sure they provide the same rate to x, to allow the ∆i to be combined together. If one of these environments is fixed (vi = 0), we just have to recover the rate associated to x there, namely ∆i(x). However, if one environment (or both) is rate-scalable, we have more leeway, and can scale them to ensure they provide the same rate; we pick here the lcm(r1, r2) to be this common rate. Two comments are warranted about this important rule. First, note that the above definition is well-formed; the exact choice of x in the rules above has no impact on the end result, since all rate environments are uniform, and so rates will be modified always in the same way. Second, even though the least common multiplier operation is usually applied to natural numbers, we use here its extension to rationals (see, e.g., [START_REF] Zazkis | From trigonometry to number theory... and back: Extending lcm to rational numbers[END_REF]), where lcm(n1/p1, n2/p2) = lcm(n1, n2)/gcd(p1, p2). The important aspect here is that the ratio of such a least common multiplier with its ni/pi arguments is always a natural number.

Lemma 33. The addition of two rate environments

∆ v 1 1 + ∆ v 2
2 defined by the rule above is a (1) commutative and (2) associative operation.

Proof.

1. Commutativity is obvious, since is an equivalence relation 2. Associativity is a direct consequence of the associativity of the operators used to define rate environment addition: multiplication on rates, product of rate-scalabilities, set intersection and union, and lcm operation on rationals. .

The domain of dependent rate environments is thus a commutative semigroup for addition.

Local rate inference rules

The rate inference algorithm described here uses a set of rules

E, Ω → ∆ v , r
that express how to compute, for an expression E and sampletype environment Ω, a compatible rate environment ∆, with its rate-scalability v, and a so-called local rate r. They are called local since they don't handle recursive signals, which is addressed in a subsequent phase. As usual, Ω is omitted when not needed locally.

Note that our algorithm infers, from rates for constants, inputs and recursive signals that are assumed to be integers, rates that are also integer, and not rational, as introduced above. Also, to show the flexibility of our approach, we fixed the rate scalability of constants to 0 and the ones of identifiers to 1; this could easily be parameterized by introducing a rate scalability environment, for instance to include fixed-rate input signals.

Definition 34 (Rules for numbers). All numbers are of fixed rate 1. We note ⊥ the rate environment with an empty domain.

k → ⊥ 0 , 1 (Int)
f → ⊥ 0 , 1 (Float)
Definition 35 (Rules for inputs). All inputs, actual inputs but also inputs of recursive signals, are of rate-scalable rate, initially 1.

In → ⊥[In → 1] 1 , 1 (Input) Xi → ⊥[Xi → 1] 1 , 1 (Recursive)
Definition 36 (Rules for up-sampling and serialize).

E → ∆ v , r E ↑ n → ∆ v , nr (Upsampling)
Ω E : [n]T E → ∆ v , r s(E) → ∆ v , nr (Serialize)
Definition 37 (Rules for down-sampling and vectorize). Note the "-var" rule variants below are compatible with their non-"-var" versions; consistency is thus ensured.

E → ∆ v , nr E ↓ n → ∆ v , r (Down)
E → ∆ 1 , r m = lcm(n, r) E ↓ n → ( m r ∆) 1 , m/n (Down-var) E → ∆ v , nr v(E, n) → ∆ v , r (Vectorize)
E → ∆ 1 , r m = lcm(n, r) v(E, n) → ( m r ∆) 1 , m/n (Vect-var)
Definition 38 (Rules for monorate binary signal expressions). To handle in a general way binary expressions that force their subexpressions to have the same rate, we introduce, for the sake of simplicity, a generic monorate pairing operator between signal expressions, typed with a pair of types.

(E1, E2) → ∆ v , r E1 E2 → ∆ v , r (Op)
(E1, E2) → ∆ v , r E1@E2 → ∆ v , r (Delay)
(E1, E2) → ∆ v , r E1#E2 → ∆ v , r (Concat)
(E1, E2) → ∆ v , r E1[E2] → ∆ v , r (Access)
Definition 39 (Rules for pairs of expressions). General rule for a monorate pair of expressions (E1, E2).

Ei → ∆ v i i , ri ∆ i = ∆i[o → ri] ∆ v 1 1 + ∆ v 2 2 → ∆ v (E1, E2) → ∆ v /o , ∆(o) (Pair
) where ∆ i introduces o as a free identifier not in the domain of any of the ∆i; here, one can think of o as a proxy for the result. Since it is used in the correctness proof, but serves no other purpose, it is removed in the end result environment (∆ /x is identical to ∆, except it is undefined for x).

Proposition 40. If E, Ω → ∆ 1 , r , then E is rate-scalable.

Soundness

Definition 41 (Well-typed Mapping). A recursive mapping D is well-typed in Γ, written Γ D, iff, for all X ∈ Dom(D) and i ∈ [0, length(D(X)) -1], one has Γ (Ei, D) : Γ(Xi).

Definition 42. A pair (Ω, ∆) is included into Γ, written (Ω, ∆) < Γ, iff, for all x in Dom(∆), one has Γ(x) = Ω(x) ∆(x) . Lemma 43. If (Ω, ∆1 ∪ ∆2) < Γ, then (Ω, ∆i) < Γ.
Proof. By definition.

Theorem 44 (Local Rate Inference Soundness). Assume that Ω (E, D) : T and (E, Ω) → ∆ v , r , for some ∆, v and r. Then, for any integer p and signal environment Γ, if one has

• (Ω, p v ∆) < Γ • and Γ D , then Γ (E, D) : T p v r .
This is the first of the main theorems of this paper. Assume that we have a signal expression E that includes recursive signals kept into the mapping D. Moreover, we assume that E, together with D, is properly sample-typed, i.e., it has a "standard" type T in some "standard" sample type environment Ω. Assume also that, when performing rate inference on (E, Ω) via the → relation, we derive some rate environment ∆ and related rate scalability v, together with a rate r for Signal E. Then, two cases can occur.

• Either v = 0, in which case p v = 1 for all p, and thus we also assume that (Ω, ∆) is compatible with, i.e., is included into, some signal environment Γ (which includes rate information for identifiers), with which moreover D can be also properly typed.

• Or v = 1, in which case ∆ is rate-scalable, and thus we can pick any p and Γ such that (Ω, p∆) is compatible with Γ, as long as D is properly typed.

Then, under all these assumptions, the theorem states that E with D has Type T and Rate r (or pr, if v = 1) in the type and rate environment Γ. The rate inference algorithm is thus sound.

Proof. By induction on E and case analysis.

Numbers. Trivial, with the (Int) and (Float) typing rules, since v = 0, ∆ = ⊥ and r = 1.

Input. We have ∆ v , r = ⊥[In → 1] 1 , 1 .
By definition of < with v = 1, we know Γ = Γ0[In → float[-∞, +∞] p ] for some Γ0. Since v = 1 and r = 1, we have T p v r = Ω(In) p = float[-∞, +∞] p . We thus get the conclusion by the (Input) typing rule.

Recursive. We have

∆ v , r = ⊥[Xi → 1] 1 , 1 .
By definition of < with v = 1, we know Γ = Γ0[Xi → Ω(Xi) p ] for some Γ0. Since, moreover, r = 1, we have T p v r = Ω(Xi) p . Also, since Γ D, we know that for all X ∈ Dom(D) and Xi ∈ Dom(X), one has Γ Ei : Γ(Xi). Thus, by application of the (Recursive) typing rule, we deduce that Γ Xi : Γ(Xi), yielding the conclusion.

Upsampling. We have E = E ↑ n and ∆ v , r = ∆ v , nr , with E → ∆ v , r . By the (Up) sample typing rule, Ω E : T implies that Ω E : T. Thus, by induction, we get Γ E : T p v r .

By the (Up) typing rule, we then get Γ E : T np v r . Since r = nr , then, we obtain the conclusion.

Serialize.

We have E = s(E ) and ∆ v , r = ∆ v , nr , with

E → ∆ v , r with Ω E : [n]T .
By induction, we get Γ E : [n]T p v r .

By the (Serialize) typing rule, we then get Γ E : T np v r . Since r = nr , then, we conclude Γ E : T p v r .

Down.

We have E = E ↓ n and ∆ v , r such that E → ∆ v , r and r = nr. By the (Down) sample typing rule, Ω E : T implies that Ω E : T. Thus, by induction, Γ E : T p v r .

By the (Down) typing rule, since T p v r = T p v nr , we then get Γ E : T p v r , yielding the conclusion.

Down-var.

We have E = E ↓ n and ∆ v , r = ( m r ∆ ) 1 , m/n such that E → ∆ 1 , r and m = lcm(n, r ). We also assume that (Ω, p∆) < Γ, since v = 1. By the (Down) sample typing rule, Ω E : T implies that Ω E : T. Thus, by induction on E , with p m r as p and v = 1 in this inductive step, we get Γ E : T p m r r , i.e., Γ E : T pm . By the (Down) typing rule, we then get Γ E : T pm/n , yielding the conclusion.

Vectorize and Vect-var. Use the same reasoning as for (Down) and (Down-var).

Binary expressions. Direct consequence of the proof for pairs of expressions.

Pair of expressions.

We have E = (E1, E2) and

E → ∆ v /o , r such that Ei → ∆ v i i , ri , ∆ v 1 1 + ∆ v 2
2 → ∆ v and r = ∆(o). We proceed by case on the pair (v1, v2). Note that the removal of Identifier o from ∆ has no influence on the induction steps taken in the proof below, since they are irrelevant in the typing of Ei.

RELATED WORK

As a specifically audio-oriented DSL, Faust takes its roots into at least three domains: functional languages, music languages and synchronous languages. The last two families are strongly related to clocking issues.

Music languages such as Faust or Csound [START_REF] Boulanger | The Csound Book: Perspectives in Software Synthesis, Sound Design, Signal Processing, and Programming[END_REF] make a clear distinction between audio rates, the pervasive digital audio sample rate information (44 kHz or 48 kHz), and control rates (kr in Csound parlance), related to the frequency at which, for instance, user interface components are sampled. The distinction is, in fact, mostly motivated by performance issues. Our rate information provides a finer-grained and more flexible way to handle a wide variety of rate requirements.

Regarding synchronous languages, the most relevant references are the ones related to the Synchronous Dataflow Model (see Lee et al's seminal work [START_REF] Lee | Synchronous data flow[END_REF], or [START_REF] Bebelis | Bpdf: A statically analyzable dataflow model with integer and boolean parameters[END_REF] for a more recent, parameterized variant). In fact, our work can be seen as both (1) a reframing of the solving of "balance equations" in SDF [START_REF] Lee | Static scheduling of synchronous data flow programs for digital signal processing[END_REF] in the framework of annotated type systems [START_REF] Nielson | Annotated type and effect systems[END_REF] and (2) an extension of this scheme to rational rates. Contrarily to Lee et al's global, integer matrix-based version, our rate algorithm is defined by induction on the syntax of expressions, allowing for the early and precise detection of rate inconsistencies and type theoretic-like correctness proofs. Our technique can also handle explicit rate and type constraints on input-output signals; in particular, typical audio environments expect them to carry scalar values, with no buffering required and fixed rates. More generally, our type and rate scheme is intended to include more involved typing and rational rating conditions (see Section 7). We believe that our static semantics approach, complimentary to the one usually adopted in the literature, is thus flexible.

Moving to other synchronous languages such as Lustre [START_REF] Caspi | Lustre: A declarative language for real-time programming[END_REF], Signal [START_REF] Benveniste | Synchronous programming with events and relations: the Signal language and its semantics[END_REF] or Lucid Synchrone [START_REF] Caspi | Lucid synchrone: un langage pour la programmation des systèmes réactifs[END_REF], to mention a few, Faust does not attempt to provide the wide spectrum of clocking and data manipulation specifications present in these general-purpose synchronous languages. The emphasis is, as presented in the introduction, to match audio DSP features and their associated hard real-time, efficiency requirements. If our rational model for rates can be seen, in some sense, as a special case of the more abstract clocking mechanisms provided in these frameworks, i.e., "clocks as abstract types" [START_REF] Colaço | Embedded Software: Third International Conference, EMSOFT 2003[END_REF] or integer clocks [START_REF] Guatto | A Synchronous Functional Language with Integer Clocks[END_REF], we believe that the tight intertwining of our rate model and efficient inference algorithm will provide value to Faust users.

Even though some papers on type-based clock mechanisms mention explicit rate inference algorithms, most authors limit their covering of this topic to a few comments about Hindley-Milner-based schemes. Yet, interestingly, in [START_REF] Talpin | Automated clock inference for stream function-based system level specifications[END_REF], a more precise description of a clock inference system is provided. In some sense, our usage of scalability parameters can be seen as a way of handling the equivalent of "rate schemes" within the rate inference algorithm itself. But, in addition to the structural type information found in Hindley-Milner systems, our problem also addresses the algebra of rate annotations.

FUTURE WORK

The typing rules and inference of Sections 4 and 5 are probably too strict to be of real practical interest. In particular, constant signals, for instance numbers, have to be up-sampled to be used in any expression of rate r > 1, which is very inconvenient. In this section we propose possible future work related to relaxing the typing and rate rules, and mention the probable impact on the rate inference process.

One possible evolution of the typing rules is to accept to combine signals of different rates provided one rate is a multiple of the other. This can done with the introduction of a single Rate coercion rule, as follows, assuming n ∈ N * . Γ E : T r Γ E : T nr (Rate coercion)

All equations r1 = r2 that appeared in the strict rate inference algorithm, and had to be enforced via unification, have, in the relaxed rate inference algorithm, to be replaced by appropriate parametrized equalities of the form n1r1 = n2r2. Note that the introduction of the (Rate coercion) rule is equivalent to adding implicit up sampling operations in the language, thus allowing, in theory, to get rid of the explicit (Upsampling) rule. We suggest to keep it nonetheless, if only for documentation purposes.

Another possibility would be to add an explicit subrating rule such as

Γ Ei : T r i i T r = T r 1 1 T r 2 2 Γ E1 E2 : T r (Subrating)
which would allow subrated expressions to be passed to primitive operations. We introduce here a natural extension of the relation over sample types with T r 1 1 T r 2 2 = (T1 T2) max(r 1 ,r 2 ) , if min(r1, r2)|max(r1, r2) . The difference between the two approaches is that, for instance, the constant signal 10 becomes a signal with multiple rates in the first case, while, with the second approach, it is the flexibility of the subrating rule that allows to pass 10 (with its rate of 1) to an operator where a signal of a different rate, 2 say, is expected, as would be the case in an expression such as 10 + 7 ↑ 2 . Referential transparency issues, and more experiments, can help decide which approach is best.

More unusual, and intriguing, would be to allow some sort of "contravariant" subrating on constant expressions. For instance, when connecting a constant signal K of value 10 at Rate 1 to a slow-going signal expression S (for instance a slider enabling some sort of user interfacing at Rate 1/100), it would interesting to allow K to be deemed equivalent rate-wise to this slower signal (note this is going the opposite way of the previous proposals, which would have forced S to go as fast as K, i.e., adopt a rate of 1). This makes sense since our knowledge of the constancy of K makes it amenable to a slower rate without loss of information. Moreover, this information is explicitly present with our type system, K having the type int[10, 10] 1 (and this behavior would be generalized automatically to all expressions proven constant by the typechecker).

Finally, we are envisioning the possibility of adding rate constraints explicitly, either at the language level or within the embedding sound architecture, for instance to enforce a particular I/O rate, required by the outside world (e.g., the fact that a particular rate must be an integer, say 44kHz). The best way of doing so is also a matter of more experimenting, at the language-design and usage levels.

CONCLUSION

We show in this paper how the Faust digital audio processing language, traditionally based on scalar monorate signals, can be extended to handle multi-dimensional multi-rate signals. Specifically, we provide a formal definition of a new Intermediate Representation for Faust extended to enable the handlingof the multi-rate framework proposed in [START_REF] Jouvelot | Dependent vector types for data structuring in multirate Faust[END_REF]. We show how such signals can be formally defined on a rational model of its clocking mechanism.

On the practical side, we designed a new (type and) multirate inference algorithm, for which both soundness and (relative) completeness theorems are specified and proven. A prototype implementation of this algorithm in the Faust compiler static semantics phase, in a experimental multi-rate version of Faust, is underway.

, - 1 ,

 1 0, 1, 2, . . . } ; T2 = {. . . , -1, -0.5, 0, 0.5, 1, . . . } ; T 1/3 = {. . . , -6, -3, 0, 3, 6, . . . } . Time domains have the following properties, for all r ∈ Q * and n ∈ N * : Tr = T-r ; Tr ⊆ Tnr ; 0 ∈ Tr .

Figure 1 :

 1 Figure 1: Constant signal 1: int[1, 1] 1

Figure 2 :

 2 Figure 2: process = vectorize(10,_) : +~_ : serialize;

Figure 3 :

 3 Figure 3: Vectorization by 3

) Vectorize(x, 3 )Figure 4 :

 34 Figure 4: How vectorize is implemented

  under the sole conservative constraint that, for any arithmetic operator , [l, h] [l , h ] = [L, H] such that, for all x ∈ [l, h] and x ∈ [l , h ], the value of x x is in [L, H]. Note that total arithmetic type operations are thus always definable, using the worst-case definition [l, h] [l , h ] = [-∞, +∞].

4. 2

 2 Signal type environment Γ Definition 12 (Signal-type environment). A signal type environment Γ is used to store type hypotheses for incoming signals. It maps each mutually recursive signal Xi and each input signal In to an appropriate signal type T r :

  Proposition 28. Expressions E ↓ n , E ↑ n , v(E, n) and s(E) are also rate-scalable, as are binary expressions, when, recursively, E is rate-scalable. Definition 29 (Uniform rate environment). A rate environment ∆ is said uniform iff all x in Dom(∆) have the same rate scalability in ∆.

Such a requirement is obviously undecidable in general, but this does not preclude the Faust compiler from making its best effort to attain it.

Faust users can always introduce explicit min and/or max operations to explicitly bound intervals to make such functions total.

[START_REF] Colaço | Embedded Software: Third International Conference, EMSOFT 2003[END_REF] We say that Value v has type T, noted v : T, when v ∈ M(T).

The signal typing rules Γ (E, D) : T r are provided below by induction on E. Since D is seldom used, we note E the pair (E, D) when D is not used locally in a given rule.Definition 13 (Constant signals typing rules). Γ k : int[k, k] 1 (Int) Γ f : float[f, f ] 1 (Float)Definition 14 (Input and recursive signals).Γ In : Γ(In) (Input) Γ (Ei, D) : Γ(Xi) D(X) = E0E1 . . . En-1 i ∈ [0, n -1] Γ (Xi, D) : Γ(Xi) (Recursive)The typing rule for recursive signals is unusual in that, in addition to specifying that the type of a recursive signal identifier is directly available in the typing environment Γ, it also checks that the corresponding recursive definition present in D is properly typed. Definition 15 (Numerical operations on signals). Γ Ei : T r i T = T1 T2 Γ E1 E2 : T r (Op)

Acknowledgments

Part of this project was funded by the ANR FEEVER project. We thank Emilio Gallego Arias and Olivier Hermant for their thorough proofreading of this paper.

(0, 0). By definition of the rate environment addition, we have ∆ v = (∆ 1 ∪ ∆ 2) 0 with ∆ 1 ∆ 2. Thus, for all x in Dom(∆ 1) ∩ Dom(∆ 2) and thus o, one has ∆(x) = ∆ 1(x) = ∆ 2(x). This entails r1 = ∆ 1(o) = ∆ 2(o) = r2. By induction, since (Ω, ∆ 1 ∪ ∆ 2) < Γ implies (Ω, ∆ i) < Γ and thus (Ω, ∆i) < Γ, we have Γ Ei : T r i i . Thus, with r1 = r2 = ∆(o) and T = (T1, T2), we get the conclusion Γ E : T r . (0, 1). We have ∆ v = (∆ 1 ∪ n∆ 2) 0 , for n = m/r2.

Here, one can show, similarly as above with ∆ 1 n∆ 2, that r1 = nr2. By induction, since (Ω, (∆ 1 ∪ n∆ 2)) < Γ implies (Ω, n v i ∆ i) < Γ and thus (Ω, n v i ∆i) < Γ, we have (using p2 = n) that Γ Ei : T n i r i i with ni = n v i . Thus, with n 0 r1 = n 1 r2 = ∆(o) and T = (T1, T2), we get the conclusion Γ E : T r . [START_REF] Barkati | Synchronous programming in audio processing: A lookup table oscillator case study[END_REF]0). This is the symmetrical case of the previous one. [START_REF] Barkati | Synchronous programming in audio processing: A lookup table oscillator case study[END_REF][START_REF] Barkati | Synchronous programming in audio processing: A lookup table oscillator case study[END_REF]. Here, r = ∆(o) = lcm(r1, r2). The rate addition rule ensures that

Since (Ω, p∆) < Γ implies (Ω, p r r i ∆ i) < Γ and thus (Ω, p r r i ∆i) < Γ, we have, by induction with pi = p r r i , that Γ Ei :

. Thus, with p r r i ri = pr = p∆(o) and T = (T1, T2), we get the conclusion Γ E : T pr .

Integer Completeness

We define an integer-only version Γ N E : T R of the Γ E : T R typing relation. In N , it is assumed that all derivation trees use only integer rates.

Theorem 45 (Local Rate Inference Integer Completeness).

This is the second important theorem of this paper. Assume that there exists a derivation, involving only integer rates, of the type and integer rate T R of a signal expression E in a signal environment Γ. Then, this theorem states that the rate inference algorithm (E, Ω(Γ)) → ∆ v , r will succeed in finding a rate environment ∆ with a rate-scalability v and (integer) rate r. Moreover, the inferred rate r will be minimal in the sense that, if the expression is found rate-scalable (v = 1), then the derived rate R will be an integer multiple of r and the multiplication factor (k = R/r) is fine-tuned to make all signals in ∆ compatible, after multiplication with k, with the signal environment Γ. Proof. By induction on E and case analysis, assuming Γ N E : T R . As usual, Ω(Γ) is omitted when not needed.

Numbers. Trivial, with the (Int) and (Float) typing rules, with ∆ = ⊥, v = 0, r = 1 and any k.

Input. We just have to choose ∆, v and r such that ∆ v , r = ⊥[In → 1] 1 , 1 . Since we know that Γ N In : T R , finally just choose k = R to ensure the conclusion.

Recursive. This case is the same as for inputs (note that the usually tricky handling of recursive types does not translate when only looking at rates).

Upsampling.

We have E = E ↑ n and, using the (Up) typing rule, we have Γ N E : T R with R = nR .

By induction, there exist a tuple ∆ v , r and k such that (E ,

Applying the (Up) sampling step of the rate inference algorithm, we just choose ∆ v , r = ∆ v , nr . We are left with finding k such that R = rk v , i.e., such that nR = nr k v or R = r k v . We just choose k = k .

Serialize.

We have E = v(E , n). This case is similar to the upsampling case, except that, in addition, one needs to use the Sample Type Consistency property to establish Ω(Γ) E : [n]T , which is needed to execute the (Serialize) algorithm step.

Down.

We have E = E ↓ n and, using the (Down) typing rule, we have Γ N E : T R with nR = R .

By induction, there exist a tuple ∆ v , r and k such that (E , Ω(Γ)) → ∆ v , r and R = r k v .

There are three cases.

• First, assume there is r such that r = nr . Using the (Down) algorithm step, choose ∆ v , r = ∆ v , r .

Then, we only have to find k such R = r k v , i.e., nR = nr k v = r k v , i.e., such that R = r k v . Thus, just choose k = k to complete the step.

• Then, assume that there is no such r and v = 0. This would make the rate inference algorithm fail. Yet, such a case is impossible, since, having both R = r k 0 by induction and R = nR by typing, the rate r must be a multiple of n, a contradiction.

• Finally, we have v = 1, which enables the (Downvar) algorithm step.

Here, we choose ∆ v , r = m r ∆ 1 , m/n , where m = lcm(n, r ). We need to find k such R = (m/n)k v , i.e., such that nR = mk 1 . We choose k = r k /m, First, k is indeed an integer. We have r |r k and n|r k , since r k = R = nR. Thus m = lcm(n, r )|r k . Moreover, k∆ = r k /m( m r ∆ ) = k ∆ , and thus (Ω(Γ), k v ∆) Γ, completing the step.

Vectorize. Use the same reasoning as for (Down).

Pair of expressions.

We have E = (E1, E2). Using the (Op) typing rule, we also have Γ N Ei :

By induction, there exist tuples ∆ v i i , ri and ki such that (Ei, Ω(Γ)) → ∆ v i i , ri , with the conditions R = rik v i i and (Ω(Γ),

Using the (Pair) algorithm step, choose

2 ) v 1 v 2 and r = ∆ (o). This environment addition is well-defined, since (1) one can take x = o in the antecedent of the definition of addition and (2) ( m r 1 ) v 1 ∆ 1 ( m r 2 ) v 2 ∆ 2 , with m = lcm(r1, r2). Property ( 2) is true by the Joinable Environment Scaling Equivalence lemma (see below) for ∆1 and ∆2, since, by induction, we have (Ω(Γ), k v i i ∆i) Γ. It is, also, true for o, present in both ∆ i . Indeed,

, one has R = m m for some m . Thus, we get ∆ i (o)= m v i (m m) 1-v i = mm 1-v i , and two cases occur.

• When the values of vi are equal, we obtain the sought equality.

• Assume then, wlog, that v1 = 0 and v2 = 1. We need to show that m (for v2 = 1) is equal to R (for v1 = 0). Indeed, in this particular case, m = lcm(r1, r2) = lcm(R, R/k2) = R.

We can now proceed to proving the two conclusion conditions of the theorem.

• We have to find

1 , which is true. In the second case, the vi are different. Then, wlog, we take v1 = 0. After simplifying the formula for R, we need to show that R = m. This is indeed true, since R = r1 = r2k2 and k2 is an integer, leading to m r1 = R.

• We need to show that (Ω(Γ),

1 ∆1, giving the conclusion. In the second case, with different vi and v1 = 0, we need to show (Ω(Γ), ∆) Γ. It is a direct consequence of the induction for ∆1. For the ∆2 part of ∆, we need to show that (Ω(Γ), ( m r 2 ) 1 ∆2) Γ. Yet, we have R = r1 = r2k2, yielding m = r1; we need (Ω(Γ), ( r 1 r 2 )∆2) Γ, i.e., (Ω(Γ), k2∆2) Γ, which is true, by induction.

Lemma 46 (Joinable Environment Scaling Equivalence).

Proof. For all elements in ∆1 ∩ ∆2, by case on vi [START_REF] Orlarey | Signal rate inference for multi-dimensional faust[END_REF].

Rate inference

Rate inference is performed by first computing the local rates of the expressions Ei in the list L of signal outputs; all recursively defined signals used in Ei are gathered in a mapping D. If a rate can be successfully inferred for every expression Ei, the next step is to compute a global ∆ by combining all these ∆ v i i environments. At the end of this process, one compute a reduced rate environment ∆. The last point is then to check that all recursive signals have the same input and output rate. The rate inference algorithm is provided in Figure 5 Proof. By definition of type/rate correctness, picking rates(L, D) for Γ, one needs to show that, for all Ei, there exist a type and rate. For this, for each expression Ei, we use the Local Rate Inference Soundness theorem, after checking that each of its conditions is valid.

1. The first condition, Ωi (Ei, D) : Ti, is satisfied, since sample type inference is performed on each Ei with the sample_type algorithm (not described here). Use then the weakening typing rule, from Ωi to Ω.

2. The second condition, (Ei, Ωi) → ∆ v i i , ri , is ensured by the calls to local_rate.

3. For the third condition, using p = ∆(oi)/ri, we see that Γ is built so that (Ω, p v i ∆i) < Γ.

4. The fourth and final condition, Γ D, is satisfied by the final checks on Γ.

Thus, by Local Rate Inference Soundness, proper sample type Ω(oi) and rate ∆(oi) exist for each expression Ei.

Theorem 49 (Minimum Rate). The rates provided by rates are minimal.

Proof. Consequence of the Local Rate Inference Integer Completeness theorem, since all k there are integers.