From a14d77f0757a7adeae1df323f4956c201e8e0373 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:10:16 +0000 Subject: [PATCH] fixed broken ref --- src/main.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main.tex b/src/main.tex index 8de8b41..f159d9e 100644 --- a/src/main.tex +++ b/src/main.tex @@ -217,14 +217,14 @@ In this paper, I propose the syntax and semantics of \lambdammm, an extended cal \input{syntax.tex} -The types and terms of \lambdammm\ are defined in Figure \ref{fig}. +The types and terms of \lambdammm\ are defined in Figure \ref{fig:syntax_v}. 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} -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}. +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:onepole}. This code can be expressed in \lambdammm\ as shown in Figure \ref{fig:onepole}. \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){ @@ -248,13 +248,13 @@ The programming language \textit{mimium}, developed by the author, includes a ke \input{typing.tex} -Additional typing rules for the usual simply-typed lambda calculus are shown in Figure \ref{fig}. +Additional typing rules for the usual simply-typed lambda calculus are shown in Figure \ref{fig:typing}. 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 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 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. +In \lambdammm, the problem of memory allocation for closures is delegated to the runtime implementation (see Section \ref{sec:vm}), 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}