-
Interactive Music and Synchronous Reactive Programming
Authors:
Bertrand Petit,
Manuel Serrano
Abstract:
This paper presents Skini, a programming methodology and an execution environment for interactive structured music. With this system, the composer programs his scores in the HipHop.js synchronous reactive language. They are then executed, or played, in live concerts, in interaction with the audience. The system aims at hel** composers to find a good balance between the determinism of the composi…
▽ More
This paper presents Skini, a programming methodology and an execution environment for interactive structured music. With this system, the composer programs his scores in the HipHop.js synchronous reactive language. They are then executed, or played, in live concerts, in interaction with the audience. The system aims at hel** composers to find a good balance between the determinism of the compositions and the nondeterminism of the interactions with the public. Each execution of a Skini score yields to a different but aesthetically consistent interpretation.
This work raises many questions in the musical fields. How to combine composition and interaction? How to control the musical style when the audience influences what is to play next? What are the possible connections with generative music? These are important questions for the Skini system but they are out of the scope of this paper that focuses exclusively on the computer science aspects of the system. From that perspective, the main questions are how to program the scores and in which language? General purpose languages are inappropriate because their elementary constructs (i.e., variables, functions, loops, etc.) do not match the constructions needed to express music and musical constraints. We show that synchronous programming languages are a much better fit because they rely on temporal constructs that can be directly used to represent musical scores and because their malleability enables composers to experiment easily with artistic variations of their initial scores.
The paper mostly focuses on scores programming. It exposes the process a composer should follow from his very first musical intuitions up to the generation of a musical artifact. The paper presents some excerpts of the programming of a classical music composition that it then precisely relates to an actual recording. Examples of techno music and jazz are also presented, with audio artifact, to demonstrate the versatility of the system. Finally, brief presentations of past live concerts are presented as an evidence of viability of the system.
△ Less
Submitted 4 June, 2020;
originally announced June 2020.
-
All-Action Policy Gradient Methods: A Numerical Integration Approach
Authors:
Benjamin Petit,
Loren Amdahl-Culleton,
Yao Liu,
Jimmy Smith,
Pierre-Luc Bacon
Abstract:
While often stated as an instance of the likelihood ratio trick [Rubinstein, 1989], the original policy gradient theorem [Sutton, 1999] involves an integral over the action space. When this integral can be computed, the resulting "all-action" estimator [Sutton, 2001] provides a conditioning effect [Bratley, 1987] reducing the variance significantly compared to the REINFORCE estimator [Williams, 19…
▽ More
While often stated as an instance of the likelihood ratio trick [Rubinstein, 1989], the original policy gradient theorem [Sutton, 1999] involves an integral over the action space. When this integral can be computed, the resulting "all-action" estimator [Sutton, 2001] provides a conditioning effect [Bratley, 1987] reducing the variance significantly compared to the REINFORCE estimator [Williams, 1992]. In this paper, we adopt a numerical integration perspective to broaden the applicability of the all-action estimator to general spaces and to any function class for the policy or critic components, beyond the Gaussian case considered by [Ciosek, 2018]. In addition, we provide a new theoretical result on the effect of using a biased critic which offers more guidance than the previous "compatible features" condition of [Sutton, 1999]. We demonstrate the benefit of our approach in continuous control tasks with nonlinear function approximation. Our results show improved performance and sample efficiency.
△ Less
Submitted 20 October, 2019;
originally announced October 2019.
-
Optimal multi-asset trading with linear costs: a mean-field approach
Authors:
Matt Emschwiller,
Benjamin Petit,
Jean-Philippe Bouchaud
Abstract:
Optimal multi-asset trading with Markovian predictors is well understood in the case of quadratic transaction costs, but remains intractable when these costs are $L_1$. We present a mean-field approach that reduces the multi-asset problem to a single-asset problem, with an effective predictor that includes a risk averse component. We obtain a simple approximate solution in the case of Ornstein-Uhl…
▽ More
Optimal multi-asset trading with Markovian predictors is well understood in the case of quadratic transaction costs, but remains intractable when these costs are $L_1$. We present a mean-field approach that reduces the multi-asset problem to a single-asset problem, with an effective predictor that includes a risk averse component. We obtain a simple approximate solution in the case of Ornstein-Uhlenbeck predictors and maximum position constraints. The optimal strategy is of the "bang-bang" type similar to that obtained in [de Lataillade et al., 2012]. When the risk aversion parameter is small, we find that the trading threshold is an affine function of the instantaneous global position, with a slope coefficient that we compute exactly. We relate the risk aversion parameter to the desired target risk and provide numerical simulations that support our analytical results.
△ Less
Submitted 10 April, 2020; v1 submitted 12 May, 2019;
originally announced May 2019.
-
The Geometry of Types (Long Version)
Authors:
Ugo Dal Lago,
Barbara Petit
Abstract:
We show that time complexity analysis of higher-order functional programs can be effectively reduced to an arguably simpler (although computationally equivalent) verification problem, namely checking first-order inequalities for validity. This is done by giving an efficient inference algorithm for linear dependent types which, given a PCF term, produces in output both a linear dependent type and a…
▽ More
We show that time complexity analysis of higher-order functional programs can be effectively reduced to an arguably simpler (although computationally equivalent) verification problem, namely checking first-order inequalities for validity. This is done by giving an efficient inference algorithm for linear dependent types which, given a PCF term, produces in output both a linear dependent type and a cost expression for the term, together with a set of proof obligations. Actually, the output type judgement is derivable iff all proof obligations are valid. This, coupled with the already known relative completeness of linear dependent types, ensures that no information is lost, i.e., that there are no false positives or negatives. Moreover, the procedure reflects the difficulty of the original problem: simple PCF terms give rise to sets of proof obligations which are easy to solve. The latter can then be put in a format suitable for automatic or semi-automatic verification by external solvers. Ongoing experimental evaluation has produced encouraging results, which are briefly presented in the paper.
△ Less
Submitted 25 October, 2012;
originally announced October 2012.
-
Linear Dependent Types in a Call-by-Value Scenario (Long Version)
Authors:
Ugo Dal Lago,
Barbara Petit
Abstract:
Linear dependent types allow to precisely capture both the extensional behaviour and the time complexity of lambda terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to call-by-value evaluation. A system of linear dependent types for Plotkin's PCF is introduced, called dlPCFV, whose types reflect the complexity of evaluat…
▽ More
Linear dependent types allow to precisely capture both the extensional behaviour and the time complexity of lambda terms, when the latter are evaluated by Krivine's abstract machine. In this work, we show that the same paradigm can be applied to call-by-value evaluation. A system of linear dependent types for Plotkin's PCF is introduced, called dlPCFV, whose types reflect the complexity of evaluating terms in the so-called CEK machine. dlPCFV is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behaviour of terms can be derived, provided all true index term inequalities can be used as assumptions.
△ Less
Submitted 24 July, 2012;
originally announced July 2012.
-
A Categorical Model for the Lambda Calculus with Constructors
Authors:
Barbara Petit
Abstract:
The lambda calculus with constructors is an extension of the lambda calculus with variadic constructors. It decomposes the pattern-matching a la ML into a case analysis on constants and a commutation rule between case and application constructs. Although this commutation rule does not match with the usual computing intuitions, it makes the calculus expressive and confluent, with a rather simple sy…
▽ More
The lambda calculus with constructors is an extension of the lambda calculus with variadic constructors. It decomposes the pattern-matching a la ML into a case analysis on constants and a commutation rule between case and application constructs. Although this commutation rule does not match with the usual computing intuitions, it makes the calculus expressive and confluent, with a rather simple syntax. In this paper we define a sound notion of categorical model for the lambda calculus with constructors. We then prove that this definition is complete for the fragment of the calculus with no match-failure, using the model of partial equivalence relations.
△ Less
Submitted 5 March, 2012; v1 submitted 21 February, 2012;
originally announced February 2012.
-
Linearity in the non-deterministic call-by-value setting
Authors:
Alejandro Díaz-Caro,
Barbara Petit
Abstract:
We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F w…
▽ More
We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting.
△ Less
Submitted 15 June, 2012; v1 submitted 15 November, 2010;
originally announced November 2010.
-
Semantics of Typed Lambda-Calculus with Constructors
Authors:
Barbara Petit
Abstract:
We present a Curry-style second-order type system with union and intersection types for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an extension of lambda-calculus with a pattern matching mechanism for variadic constructors. We then prove the strong normalisation and the absence of match failure for a restriction of this system, by adapting the standard reducibility method.…
▽ More
We present a Curry-style second-order type system with union and intersection types for the lambda-calculus with constructors of Arbiser, Miquel and Rios, an extension of lambda-calculus with a pattern matching mechanism for variadic constructors. We then prove the strong normalisation and the absence of match failure for a restriction of this system, by adapting the standard reducibility method.
△ Less
Submitted 16 March, 2011; v1 submitted 17 September, 2010;
originally announced September 2010.
-
OCB: A Generic Benchmark to Evaluate the Performances of Object-Oriented Database Systems
Authors:
Jérôme Darmont,
Bertrand Petit,
Michel Schneider
Abstract:
We present in this paper a generic object-oriented benchmark (the Object Clustering Benchmark) that has been designed to evaluate the performances of clustering policies in object-oriented databases. OCB is generic because its sample database may be customized to fit the databases introduced by the main existing benchmarks (e.g., OO1). OCB's current form is clustering-oriented because of its clu…
▽ More
We present in this paper a generic object-oriented benchmark (the Object Clustering Benchmark) that has been designed to evaluate the performances of clustering policies in object-oriented databases. OCB is generic because its sample database may be customized to fit the databases introduced by the main existing benchmarks (e.g., OO1). OCB's current form is clustering-oriented because of its clustering-oriented workload, but it can be easily adapted to other purposes. Lastly, OCB's code is compact and easily portable. OCB has been implemented in a real system (Texas, running on a Sun workstation), in order to test a specific clustering policy called DSTC. A few results concerning this test are presented.
△ Less
Submitted 3 May, 2007;
originally announced May 2007.
