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

writing

Browse Source
This commit is contained in:
松浦 知也 Matsuura Tomoya
2024-07-08 04:01:34 +00:00
parent 2bdad78664
commit b27330d89d
2 changed files with 135 additions and 382 deletions
Download Patch File Download Diff File Expand all files Collapse all files

95
src/main.tex
View File

@@ -51,7 +51,8 @@
\usepackage{color}
\usepackage{listings}
% \usepackage{listings}
\usepackage{listings,listings-rust}
\definecolor{mygrey}{rgb}{0.96,0.96,0.96}
\lstset{
tabsize=4,
@@ -194,40 +195,90 @@ submission.
\section{Introduction}
\label{sec:intro}
This template can be found on the conference website.
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}.
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.
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.
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.
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.
\section{Syntax}
\label{sec:syntax}
\begin{figure}[ht]
\begin{tabular}{cc}
\begin{minipage}[t]{0.4\hsize}
\centering
\it{Types}
\begin{equation*}
\begin{aligned}
\tau ::=&\quad R_a \quad & a \in \mathbb{N}\\
|&\quad I_n \quad &n \in \mathbb{N} \\\
|&\quad \tau \rightarrow \tau \quad &a,b \in \mathbb{N}\\
\tau_p& ::= &\; R\ &[real] \\
& \ | &\; N\ &[nat] \\
\tau & ::= &\; \tau_p\ & \\
& \ | &\; \tau \rightarrow \tau \ &[function] \\
% |&\quad \langle \tau \rangle
\end{aligned}
\end{equation*}
\caption{\label{fig:syntax_ty}{\it Syntax of the $\lambda_{mmm}$.}}
\end{figure}
where equation (\ref{fig:syntax_ty}) is a one pole filter with frequency response:
\begin{figure}[ht]
\end{minipage}&
\begin{minipage}[t]{0.4\hsize}
\centering
\it{Terms}
\begin{equation*}
\begin{align}
v \; ::= & \quad R \\
| & \quad \lambda x:\tau.e \quad & [lambda]\\
|& \quad fix \; x.e \quad & [fixpoint]\\
|& \quad feed \; x.e \quad & [feed] \\
\end{aligned}
\begin{aligned}
e \; ::=& \ x \; & x \in \mathbb{V} \\
|& \ \lambda x.e & \\
|& \ let\; x = e_1\; in\; e_2 & \\
|& \ fix \; x.e & \\
|& \ e_1 \; e_2 & \\
|& \ delay \; e_1 \; e_2 & \\
|& \ feed \; x.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*}
\caption{\label{fig:syntax_ty}{\it Syntax of the $\lambda_{mmm}$.}}
\end{minipage}
\end{tabular}
\caption{\label{fig:syntax_v}{\it Definition of Type and Terms of the $\lambda_{mmm}$.}}
\end{figure}
\section{Semantics}
\label{sec:semantics}
Definition of types and terms of the $\lambda_{mmm}$ are shown in Figure.\ref{fig:syntax_v}.
Two terms are added in addition to the usual simply-typed lambda calculus, $delay e_1 e_2 $ that refers a previous value of $e_1$ to $e_2$ sample before, 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.
\subsection{Syntactic sugar of the feedback expression in mimium}
\label{sec:mimium}
\begin{lstlisting}[label=lst:onepole,language=Rust,caption=Example of the code of one-pole filter in mimium.]
fn onepole(x,g){
return x*(1.0-g) + self*g
}
\end{lstlisting}
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{equation*}
\centering
\begin{aligned}
let\ & onepole = \\
& \ \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}$}}
\end{figure}
\section{VM Model and Instruction Set}
@@ -255,6 +306,6 @@ Many thanks to the great number of anonymous reviewers!
%\newpage
\nocite{*}
\bibliographystyle{IEEEbib}
\bibliography{IFC-24} % requires file IFC-24.bib
\bibliography{ref} % requires file IFC-24.bib
\end{document}