fixed broken ref

This commit is contained in:
2024-09-19 05:10:16 +00:00
parent 71bb92f6ed
commit a14d77f075

View File

@@ -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}