From 71bb92f6ed6013c70ab42f0ae05ab3c5a47e8c40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?= =?UTF-8?q?a?= Date: Thu, 19 Sep 2024 05:02:03 +0000 Subject: [PATCH] english correction 1 --- src/main.tex | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/src/main.tex b/src/main.tex index 7916c6d..8de8b41 100644 --- a/src/main.tex +++ b/src/main.tex @@ -184,31 +184,32 @@ \maketitle \begin{abstract} -This paper proposes \lambdammm : a call-by-value simply-typed lambda calculus-based intermediate representation of a programming language for music that deal with synchronous signal processing, as well as a virtual machine and instruction set to run \lambdammm . Digital signal processing can be represented with a syntax that incorporates the internal states of delay and feedback into the lambda calculus. \lambdammm\ is a superset of the lambda calculus, which allows users to construct a generative signal processing graph and its execution in identical semantics. On the other hand, due to its specification, a problem was found that when dealing with higher-order functions, the users have to determine whether the execution is in the global environment evaluation or the DSP execution, and it is implied that the multi-stage computation can solve the issue. +This paper proposes \lambdammm , a call-by-value, simply-typed lambda calculus-based intermediate representation for a music programming language, which handles synchronous signal processing, Additionally, it introduces a virtual machine and instruction set to execute \lambdammm . Digital signal processing is represented through a syntax that incorporates the internal states of delay and feedback into the lambda calculus. \lambdammm\ extends the lambda calculus, allowing users to construct generative signal processing graphs and execute them with consistent semantics. However, a challenge arises when handling higher-order functions, as users must determine whether execution occurs within the global environment or during DSP execution. This issue can potentially be resolved through multi-stage computation. \end{abstract} \section{Introduction} \label{sec:intro} -Many programming languages for sound and music have been developed, but only a few have strongly formalized semantics. One language that is both rigorously formalized and practical is Faust\cite{Orlarey2004}, which combines blocks with inputs and outputs with five primitive operations - parallel, sequential, split, merge, and recursive connection. By having basic arithmetics, conditional and delay as primitive blocks, any type of signal processing can be written in Faust. In a later extension, a macro based on a term rewriting system has been introduced, allowing users to parameterize blocks with an arbitrary number of inputs and outputs\cite{graf2010}. -This strong abstraction capability through formalization enables Faust to be translated to various backends, such as C, C++, Rust and LLVM IR. On the other hand, BDA lacks theoretical and practical compatibility with common programming languages. Although it is possible to call external C functions in Faust, those functions are assumed to be pure functions without a heap memory allocation and deallocation. Therefore, while it is easy to embed Faust in another language, it is not easy to call another language from Faust. +Many programming languages for sound and music have been developed, but only a few possess strongly formalized semantics. One language that is both rigorously formalized and practical is Faust \cite{Orlarey2004}, which combines blocks with inputs and outputs with five primitive operations: parallel, sequential, split, merge, and recursive connection. By providing basic arithmetic, conditionals, and delays as primitive blocks, almost any type of signal processing can be written in Faust. In a later extension, a macro based on a term rewriting system was introduced, allowing users to parameterize blocks with an arbitrary number of inputs and outputs \cite{graf2010}. -In addition, a macro for Faust is an independent term rewriting system that generates BDA based on a pattern matching. Therefore, the arguments for pattern matching are implicitly required to be an integer, which sometimes causes compile errors despite the distinction between real and integer types does not exist in BDA. These implicit typing rules are not intuitive for novice users. +This strong abstraction capability through formalization enables Faust to be translated to various backends, such as C, C++, Rust, and LLVM IR. On the other hand, Faust's Block Diagram Algebra (BDA) lacks theoretical and practical compatibility with common programming languages. Although it is possible to call external C functions in Faust, those functions are assumed to be pure functions that do not require heap memory allocation or deallocation. Therefore, while it is easy to embed Faust in another language, it is not easy to call another language from Faust. -Proposing a computational model for signal processing based on the more generic computational models, such as a lambda calculus has the potential to interoperate between many different general purpose languages on run-time, and also facilitate the appropriation of existing optimization methods and the implementation of compilers and run-time. +In addition, a macro for Faust is an independent term rewriting system that generates BDA based on pattern matching. As a result, the arguments for pattern matching are implicitly required to be integers, which can sometimes lead to compile-time errors, despite the fact that BDA does not distinguish between real and integer types. These implicit typing rules are not intuitive for novice users. -Currently, it has been proved that BDA can be converted to a general-purpose functional language in the form of using arrow, a higher-level abstraction of monads\cite{gaster2018}. However, higher-order functions on general-purpose functional languages are often implemented on the basis of dynamic memory allocation and release, which makes it difficult to use them in host languages for real-time signal processing. +Proposing a computational model for signal processing based on more generic computational models, such as lambda calculus, has the potential to enable interoperability between many different general-purpose languages, and also facilitate the appropriation of existing optimization methods and the implementation of compilers and run-time. -Also, Kronos\cite{norilo2015} and W-calculus\cite{arias2021} are examples of attempts at lambda calculus-based abstraction while being influenced by Faust. Kronos is based on the theoretical foundation of System-$F\omega$, a variation of lambda calculus in which the type itself can be abstractized (a function that takes the type as an input and returns a new type can be defined). In Kronos, a calculation of type corresponds to the signal graph generation and a calculation of value corresponds to the actual processing. A special primitive operation is only delay in Kronos, and the feedback routing can be represented as a recursive function application in a calculation of types. +Currently, it has been demonstrated that BDA can be converted to a general-purpose functional language using an arrow, a higher-level abstraction of monads \cite{gaster2018}. However, higher-order functions in general-purpose functional languages are often implemented based on dynamic memory allocation and deallocation, making them difficult to use in host languages designed for real-time signal processing. -The W-calculus has feedback operation as a primitive, along with the access to the value of the variable in the past(= delay). W-calculus limits the systems so that can represents to linear-time-invariant such as filters and reverbrators and defines a more formal semantics, aiming at automatic proofs of the linearity and identity of graph topologies. +Additionally, Kronos \cite{norilo2015} and W-calculus \cite{arias2021} are examples of lambda calculus-based abstractions influenced by Faust. Kronos is based on the theoretical foundation of System-$F\omega$, a variation of lambda calculus in which types themselves can be abstracted (i.e., a function that takes a type as input and returns a new type can be defined). In Kronos, type calculations correspond to signal graph generation, while value calculations correspond to the actual processing. Delay is the only special primitive operation in Kronos, and feedback routing can be represented as a recursive function application in type calculations. -Previously, the author designed a programming language for music \textit{mimium} \cite{matsuura2021a}. By adding basic operations of delay and feedback to lambda calculus, signal processing can be concisely expressed while having a syntax close to that of general-purpose programming languages (especially, the syntax of mimium is designed to be looks like Rust language). +W-calculus includes feedback as a primitive operation, along with the ability to access the value of a variable from the past (i.e., delay). W-calculus restricts systems to those that can represent linear-time-invariant processes, such as filters and reverberators, and it defines more formal semantics, aiming for automatic proofs of linearity and the identity of graph topologies. -One of the previous issues with mimium was the inability to compile the codes, which contain a combination of recursive or higher-order functions with stateful functions that contains delay or feedback because the compiler could not determine the data size of the internal state of the signal processing. +Previously, the author designed the music programming language \textit{mimium} \cite{matsuura2021a}. By incorporating basic operations such as delay and feedback into lambda calculus, signal processing can be concisely expressed while maintaining a syntax similar to that of general-purpose programming languages. Notably, \textit{mimium}'s syntax is designed to resemble the Rust programming language. -In this paper, I propose a syntax and semantics of \lambdammm, an extended call-by-value simply-typed lambda calculus, as a computation model that is supposed to be an intermediate representation for mimium. Also, I propose a virtual machine and its instruction set based on Lua's VM, to execute this computation model practically. Lastly, I discuss the problem and the potential, one that the current \lambdammm\ that users have to care whether the calculation happens in a global context or an acutal signal processing, another that the run-time interoperation between the other programming languages can be easier than the existing DSP languages. +One of the earlier issues with \textit{mimium} was its inability to compile code that contained combinations of recursive or higher-order functions with stateful functions involving delay or feedback, as the compiler could not determine the data size of the internal state used in signal processing. + +In this paper, I propose the syntax and semantics of \lambdammm, an extended call-by-value simply-typed lambda calculus, as a computational model intended to serve as an intermediate representation for \textit{mimium}. Additionally, I propose a virtual machine and its instruction set, based on Lua's VM, to execute this computational model in practice. Finally, I discuss both the challenges and potential of the current \lambdammm\ model: one challenge is that users must differentiate whether a calculation occurs in a global context or during actual signal processing; another is that run-time interoperability with other programming languages could be easier than in existing DSP languages. \section{Syntax} @@ -216,14 +217,14 @@ In this paper, I propose a syntax and semantics of \lambdammm, an extended call- \input{syntax.tex} -Definition of types and terms of the \lambdammm\ are shown in Figure \ref{fig:syntax_v}. +The types and terms of \lambdammm\ are defined in Figure \ref{fig}. -Two terms are added in addition to the usual simply-typed lambda calculus, $delay\ n\ e_1\ e_2 $ that refers a previous value of $e_1$ to $e_2$ sample before (with maximum delay value $n$ to limit memory size to finite), and $feed\ x.e$ abstraction that the user can refer the result of the evaluation of the $e$ one unit time before as $x$ during the evaluation of $e$ itself. +Two terms are introduced in addition to the standard simply-typed lambda calculus: $delay\ n\ e_1\ e_2$, which refers to the previous value of $e_1$ by $e_2$ samples (with a maximum delay of $n$ to limit memory usage to a finite size), and $feed\ x.e$, an abstraction that allows the user to refer to the result of evaluating $e$ from one time unit earlier as $x$ during the evaluation of $e$ itself. \subsection{Syntactic sugar of the feedback expression in mimium} \label{sec:mimium} -mimium by the author has a keyword $self$ that can be used in function definition, that refers to the previous return value of the function. The example code of the simple one-pole filter function that mixes input and last output signal so as to a sum of gains of input and feedback should be 1, is shown in Listing \ref{lst:onepole}. This code can be expressed in \lambdammm\ as Figure \ref{fig:onepole}. +The programming language \textit{mimium}, developed by the author, includes a keyword $self$ that can be used in function definitions to refer to the previous return value of the function. An example of a simple one-pole filter function, which mixes the input and the last output signal such that the sum of the input and feedback gains is 1, is shown in Listing \ref{lst}. This code can be expressed in \lambdammm\ as shown in Figure \ref{fig}. \begin{lstlisting}[float,floatplacement=H,label=lst:onepole,language=Rust,caption=\it Example of the code of one-pole filter in mimium.] fn onepole(x,g){ @@ -247,13 +248,13 @@ mimium by the author has a keyword $self$ that can be used in function definitio \input{typing.tex} -Additional typing rules to usual simply-typed lambda calculus are shown in Figure \ref{fig:typing}. +Additional typing rules for the usual simply-typed lambda calculus are shown in Figure \ref{fig}. -As primitive types, there are a real number type to used in most of signal processing and a natural number type that is used for the indice of delay. +The primitive types include a real number type, used in most signal processing, and a natural number type, which is used for the indices of delay. -In the W-calculus, which is a direct inspiration to designing \lambdammm, function types can takes only tuples of real numbers and return tuples of real numbers. This means that higher-order functions cannot be written. While this restriction is reasonable as a design choice for a language for signal processing since higher-order functions require data structures that require dynamic memory allocation, such as closures, for their implementation, it also lacks the generality of the lambda calculus. +In W-calculus, which directly inspired the design of \lambdammm, function types can only take tuples of real numbers and return tuples of real numbers. This restriction prevents the definition of higher-order functions. While this limitation is reasonable for a signal processing language—since higher-order functions require data structures like closures that depend on dynamic memory allocation—it also reduces the generality of the lambda calculus. -In \lambdammm, the problem of memory allocation for closures is left to the implementation of the runtime in the Section\ref{sec:vm}, and higher-order functions are allowed. However, the $feed$ abstraction does not allow function types as its input and output. Allowing the return of function types in the $feed$ abstraction means that it is possible to define functions whose processing contents may change time-to-time. While this may be interesting theoritically, there are currently no practical cases in real-world signal processing, and it is expected to further complicate implementations. +In \lambdammm, the problem of memory allocation for closures is delegated to the runtime implementation (see Section \ref{sec}), allowing the use of higher-order functions. However, the $feed$ abstraction does not permit function types as either input or output. Allowing function types in the $feed$ abstraction would enable the definition of functions whose behavior could change over time. While this is theoretically interesting, there are no practical examples in real-world signal processing, and such a feature would likely complicate implementations further. \section{Semantics} \label{sec:semantics}