split figures

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}
 

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

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}

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}