tomoyanonymous/ifc-2024-lambdammm
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

writiiiinig

Browse Source
This commit is contained in:
松浦 知也 Matsuura Tomoya
2024-07-08 09:58:32 +00:00
parent b27330d89d
commit 065400e675
1 changed files with 140 additions and 30 deletions
Download Patch File Download Diff File Expand all files Collapse all files

146
src/main.tex
View File

@@ -34,7 +34,7 @@
%------------------------------------------------------------------------------------------
% ! ! ! ! ! ! ! ! ! ! ! ! user defined variables ! ! ! ! ! ! ! ! ! ! ! ! ! !
% Please use these commands to define title and author(s) of the paper:
\def\papertitle{Design of VM Instruction Set for Lambda-Calculus Based Synchronous Signal Processing Language}
\def\papertitle{$\lambda_{mmm}$: the Intermediate Representation for Synchronous Signal Processing Language Based on Lambda Calculus}
\def\paperauthorA{Tomoya Matsuura}
@@ -171,6 +171,7 @@
%-------------------------------------FOUR-AUTHOR HEADER ENDS------------------------------------------------------
\def\lambdammm{$\lambda_{mmm}$}
\begin{document}
% more pdf-tex settings:
@@ -195,44 +196,69 @@ submission.
\section{Introduction}
\label{sec:intro}
A number of programming languages for sound and music have been developed to date, but not many have strongly formalised semantics. One language that is both rigorously formalised and practical is Faust\cite{Orlarey2004}, which combines blocks with inputs and outputs in five operations - parallel, series, branch, join and recursion - and uses them as primitive The BDA is a primitive block with a delay, which allows the description of any synchronous signal processing. In a later extension, the introduction of macros based on a term rewriting system has also allowed systems with an arbitrary number of inputs and outputs to be highly abstracted\cite{graf2010}.
A number of programming languages for sound and music have been developed to date, but not many have strongly formalised semantics. One language that is both rigorously formalised 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 and delay as a primitive block, any type of signal processing can be written in Faust. In a later extension, macros based on a term rewriting system has introduced that allows the higher abstraction of systems with an arbitrary number of inputs and outputs\cite{graf2010}.
This strong abstraction capability through formalisation enables Faust to be translated to various code bases, such as C++ and Rust. 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, the assumption is basically pure function calls without 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.
This strong abstraction capability through formalisation enables Faust to be translated to various backends, such as C++ and Rust. 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, the assumption is basically pure function calls without 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.
Proposing a computational model for signal processing that underlies the computational models used in more generic programming, such as the lambda calculation, has the potential to facilitate the appropriation of existing optimisation methods and the implementation of compilers and run-time.
In addition, macros in Faust are independent as a term rewriting system that generates BDA based on pattern matching. Therefore, even though the distinction between real and integer types does not exist in BDA, the arguments for pattern matching implicitly required to be an integer, which causes compile errors. This implicit typing rules are not intuitice for novice users.
Currently, it has been proved that BDA can be converted to a general-purpose functional language in the form of using Arrows, a higher-level abstraction of monads\cite{gaster2018}. But 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 speech signal processing, where real-time performance is important.
Proposing a computational model for signal processing that is based on the more generic computational models, such as the lambda calculus has the potential to interoperate between many different general-purpose languages, and also facilitate the appropriation of existing optimisation methods and the implementation of compilers and run-time.
Currently, it has been proved that BDA can be converted to a general-purpose functional language in the form of using Arrows, a higher-level abstraction of monads\cite{gaster2018}. But 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 the real-time signal processing.
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 lambda computation in which the type itself is the object of the lambda abstraction (a function can be defined that computes the type and returns a new type). The W-calculus limits the systems it represents to linear time-invariant ones and defines a more formal semantics, aiming at automatic proofs of the identity of graphs with seemingly different topologies, etc. It aims, for example, at automatic proofs of identity between graphs of seemingly different topologies.
Previously, the author proposed programming language \textit{mimium} that by adding the basic operators of delay and feedback to lambda-calculus, signal processing can be expressed concisely while having a syntax close to that of general-purpose programming languages\cite{Matsuura2021}.
In this paper, we present the syntax and semantics of a computational model: lambda-mmm, which is an intermediate representation of mimium based on W-calculus. We also propose a virtual machine and its instruction set for efficient execution of this computational model.
In this paper, we present the syntax and semantics of a computational model: \lambdammm, which is an intermediate representation of mimium based on W-calculus. We also propose a virtual machine and its instruction set for efficient execution of this computational model.
\section{Syntax}
\label{sec:syntax}
\begin{figure}[ht]
\begin{tabular}{cc}
\begin{tabular}{cc}
\begin{minipage}[t]{0.4\hsize}
\centering
\it{Types}
\begin{equation*}
\begin{aligned}
\tau_p& ::= &\; R\ &[real] \\
& \ | &\; N\ &[nat] \\
\tau & ::= &\; \tau_p\ & \\
& \ | &\; \tau \rightarrow \tau \ &[function] \\
& \ | &\; \tau \to \tau \ &[function] \\
% |&\quad \langle \tau \rangle
\end{aligned}
\end{equation*}
\textrm{Types}
\end{minipage}&
\begin{minipage}[t]{0.4\hsize}
\centering
\it{Terms}
\begin{equation*}
\centering
\begin{equation*}
\begin{aligned}
e \; ::=& \ x \; & x \in \mathbb{V} \\
v_p \; ::=& \ r & r \in \mathbb{R} \\
|& \ n & n \in \mathbb{N}\\
v \; ::=&\ v_p & \\
|& \ cls(\lambda\ x.e, E) & \\
%%|& \quad (e_1,e_2) \quad & [product]\\
%%|& \quad \pi_n e \quad n\in \mathbb{N},\; n>0 \quad & [project]\\
%%|& \quad \langle e \rangle \quad & [code] \\
%%|& \quad \textasciitilde e \quad & [escape]
\
\end{aligned}
\end{equation*}
\textrm{Values}
\end{minipage}\\
\multicolumn{2}{c}{
\begin{minipage}[t]{0.4\hsize}
\centering
\begin{equation*}
\begin{aligned}
e \; ::=& \ x \quad x \in {v_p}\\
|& \ \lambda x.e & \\
|& \ let\; x = e_1\; in\; e_2 & \\
|& \ fix \; x.e & \\
@@ -244,11 +270,13 @@ In this paper, we present the syntax and semantics of a computational model: lam
%%|& \quad \langle e \rangle \quad & [code] \\
%%|& \quad \textasciitilde e \quad & [escape]
\end{aligned}
\end{equation*}
\end{equation*}
\textrm{Terms}
\end{minipage}
}
\end{minipage}
\end{tabular}
\caption{\label{fig:syntax_v}{\it Definition of Type and Terms of the $\lambda_{mmm}$.}}
\caption{\label{fig:syntax_v}{\it Definition of Types, Values and Terms of the $\lambda_{mmm}$.}}
\end{figure}
Definition of types and terms of the $\lambda_{mmm}$ are shown in Figure.\ref{fig:syntax_v}.
@@ -267,7 +295,7 @@ Two terms are added in addition to the usual simply-typed lambda calculus, $dela
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 is shown in Listing.\ref{lst:onepole}. This code can be expressed in $\lambda_{mmm}$ as Figure.\ref{fig:onepole}.
\begin{figure}
\begin{figure}[ht]
\begin{equation*}
\centering
\begin{aligned}
@@ -275,9 +303,91 @@ mimium by the author has a keyword $self$ that can be used in function definitio
& \ \lambda x. \lambda g.\ feed\ y.\ x *(1.0 - g) + y * g \ in\ ...
\end{aligned}
\end{equation*}
\caption{\label{fig:onepole}{\it Equivalent expression to Listing.\ref{lst:onepole} in $\lambda_{mmm}$}}
\caption{\label{fig:onepole}{\it Equivalent expression to Listing.\ref{lst:onepole} in $\lambda_{mmm}$.}}
\end{figure}
\subsection{Typing Rule}
\label{sec:typing}
Additional typing rules to usual simply-typed lambda calculus are shown in Fig.\ref{fig:typing}.
In the W-calculus, a starting point of designing \lambdammm, function types can takes 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 \lambdammm, the problem of memory allocation for closures is left to the implementation of the runtime, 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 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.
\begin{figure}[ht]
\begin{tabular}{cc}
\begin{minipage}[t]{0.45\hsize}
\centering
\begin{equation*}
\frac{\Gamma, x:\tau_a \vdash e:\tau_b}{\Gamma \vdash \lambda x.e:\tau_a \to \tau_b }
\end{equation*}\textrm{T-LAM}
\end{minipage} &
\begin{minipage}[t]{0.45\hsize}
\centering
\begin{equation*}
\frac{ \Gamma \vdash e_1:N \quad \Gamma \vdash e_2:\tau }{\Gamma \vdash delay\ e_1\ e_2 : \tau}
\end{equation*}\textrm{T-DELAY}
\end{minipage}\\
\begin{minipage}[t]{0.45\hsize}
\centering
\begin{equation*}
\frac{\Gamma, x : \tau_p \vdash e: \tau_p }{\Gamma \vdash feed\ x.e:\tau_p}
\end{equation*}\textrm{T-FEED}
\end{minipage}&
\end{tabular}
\caption{\label{fig:typing}{\it Typing rules for lambda abstraction and feed abstraction in $\lambda_{mmm}$.}}
\end{figure}
\section{Semantics}
\label{sec:semantics}
\begin{figure*}[ht]
\centering
\begin{tabular}{|c|c|c|}
\begin{minipage}[b]{4.5cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_1 \Downarrow v_1\ E^{n-v_1} \vdash e_2 \Downarrow v_2}{E^n \vdash\ delay\ e_1\ e_2 \Downarrow v_2}
\end{equation*}\textrm{E-DELAY}
\end{minipage} &
\begin{minipage}[b]{4.5cm}
\centering
\begin{equation*}
\frac{}{E^n \vdash\ \lambda x.e \Downarrow cls(\lambda x.e , E^n) }
\end{equation*}\textrm{E-LAM}
\end{minipage}&
\begin{minipage}[b]{6cm}
\centering
\begin{equation*}
\frac{ E^{n-1} \vdash e \Downarrow v_1\ E^n, x \mapsto v_1 \vdash e \Downarrow v_2 }{E^n \vdash\ feed\ x\ e \Downarrow v_2}
\end{equation*}\textrm{E-FEED}
\end{minipage}
\\
\multicolumn{3}{c}{
\begin{minipage}[b]{8cm}
\centering
\begin{equation*}
\frac{E^n \vdash e_1 \Downarrow cls(\lambda x_c.e_c, E^n_c) E^n \vdash e_2 \Downarrow v_2\ E^n_c, x_c \mapsto v_2 \vdash e_c \Downarrow v }{E^n \vdash\ e_1\ e_2 \Downarrow v }
\end{equation*}\textrm{E-APP}
\end{minipage}
}
\end{tabular}
\caption{\label{fig:semantics}{\it Big-step Semantics of $\lambda_{mmm}$.}}
\end{figure*}
The operational semantics of the \lambdammm is shown in Fig.\ref{fig:semantics}. This big-step semantics is a conceptual explanation of the evaluation that, when the current time is $n$, the previous evaluation environment $t$ samples before can be referred to as $E^{n-t}$ , and that when the time < 0, the evaluation of any term is evaluated to the default value of its type (0 for the numeric types).