diff --git a/src/main.tex b/src/main.tex index 20339d6..3aeaddb 100644 --- a/src/main.tex +++ b/src/main.tex @@ -215,69 +215,7 @@ In this paper, we present the syntax and semantics of a computational model: \la \section{Syntax} \label{sec:syntax} -\begin{figure}[ht] - - \begin{tabular}{cc} -\begin{minipage}[t]{0.4\hsize} -\centering - -\begin{equation*} - \begin{aligned} - \tau_p& ::= &\; R\ &[real] \\ - & \ | &\; N\ &[nat] \\ - \tau & ::= &\; \tau_p\ & \\ - & \ | &\; \tau \to \tau \ &[function] \\ - % |&\quad \langle \tau \rangle - \end{aligned} -\end{equation*} -\textrm{Types} -\end{minipage}& - -\begin{minipage}[t]{0.4\hsize} - \centering - - \begin{equation*} - \begin{aligned} - 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 & \\ - |& \ 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*} - \textrm{Terms} - \end{minipage} - } - -\end{tabular} -\caption{\label{fig:syntax_v}{\it Definition of Types, Values and Terms of the $\lambda_{mmm}$.}} -\end{figure} +\input{syntax.tex} Definition of types and terms of the $\lambda_{mmm}$ are shown in Figure.\ref{fig:syntax_v}. @@ -316,76 +254,13 @@ In the W-calculus, a starting point of designing \lambdammm, function types can 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} +\input{typing.tex} \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*} +\input{semantics.tex} 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). @@ -394,6 +269,12 @@ The operational semantics of the \lambdammm is shown in Fig.\ref{fig:semantics}. \section{VM Model and Instruction Set} \label{sec:vm} +\subsection{Instruction Set} +\label{sec:instruction} + + + + \section{Discussion} \label{sec:discussion} diff --git a/src/semantics.tex b/src/semantics.tex new file mode 100644 index 0000000..a588617 --- /dev/null +++ b/src/semantics.tex @@ -0,0 +1,37 @@ +\begin{figure*}[ht] + \centering + \begin{tabular}{ccc} + + \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*} \ No newline at end of file diff --git a/src/syntax.tex b/src/syntax.tex new file mode 100644 index 0000000..1ef2c61 --- /dev/null +++ b/src/syntax.tex @@ -0,0 +1,61 @@ +\begin{figure}[ht] + + \begin{tabular}{cc} + \begin{minipage}[b]{0.45\hsize} + \centering + + \begin{equation*} + \begin{aligned} + \tau_p ::= &\; R\ &[real] \\ + \ | &\; N\ &[nat] \\ + \tau ::= &\; \tau_p\ & \\ + \ | &\; \tau \to \tau \ &[function] \\ + % |&\quad \langle \tau \rangle + \end{aligned} + \end{equation*} + \textrm{Types} + \end{minipage}& + + \begin{minipage}[b]{0.45\hsize} + \centering + \begin{equation*} + \begin{aligned} + v_p \; ::=& \ r \quad r \in \mathbb{R} \\ + |& \ n \quad 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 &x \in {v_p} \ & [value]\\ + |& \ \lambda x.e & & [abs]\\ + |& \ let\; x = e_1\; in\; e_2 & & [let]\\ + |& \ fix \; x.e & & [fixpoint]\\ + |& \ e_1 \; e_2 & & [app]\\ + |& \ delay\; n \; e_1 \; e_2 &n \in \mathbb{N}\ & [delay]\\ + |& \ feed \; x.e & & [feed]\\ + %%|& \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{Terms} + \end{minipage} + } + + \end{tabular} + \caption{\label{fig:syntax_v}{\it Definition of Types, Values and Terms of the $\lambda_{mmm}$.}} + \end{figure} \ No newline at end of file diff --git a/src/typing.tex b/src/typing.tex new file mode 100644 index 0000000..a1ea6f5 --- /dev/null +++ b/src/typing.tex @@ -0,0 +1,27 @@ +\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} \ No newline at end of file