mirror of
https://github.com/ProgramSnail/Lama.git
synced 2025-12-05 22:38:44 +00:00
225 lines
8.9 KiB
TeX
225 lines
8.9 KiB
TeX
|
\section{Operational Semantics}
|
||
|
|
|
||
|
|
The semantics for the language is given in the form of a \emph{big-step} operational semantics with the
|
||
|
|
main transition relation being
|
||
|
|
|
||
|
|
\[
|
||
|
|
\setarrow{\xRightarrow}
|
||
|
|
\trans{c}{e}{\inbr{c^\prime,\,v}}
|
||
|
|
\]
|
||
|
|
|
||
|
|
for some \emph{configurations} $c, c^\prime$, some expression $e$ and some value $v$. Besides this main relation a few supplementary are
|
||
|
|
used to handle the semantics of other syntactic categories.
|
||
|
|
|
||
|
|
\subsection{States, Worlds and Configurations}
|
||
|
|
|
||
|
|
A configuration is a triple of a \emph{state}, a \emph{memory}, and a \emph{world}. A world is an abstract entity to accomodate side-effects
|
||
|
|
potentially performed as the execution of a program proceeds, and a memory is a patrial function which maps \emph{locations} to
|
||
|
|
\emph{composite values} (arrays, S-expressions, and closures).
|
||
|
|
|
||
|
|
A state is a pair
|
||
|
|
|
||
|
|
\[
|
||
|
|
\inbr{\sigma_g,\,ss}
|
||
|
|
\]
|
||
|
|
|
||
|
|
of a \emph{global} binding and a stack (list) of local scopes, each of which is a pair
|
||
|
|
|
||
|
|
\[
|
||
|
|
\inbr{S,\,\sigma}
|
||
|
|
\]
|
||
|
|
|
||
|
|
where $S$ is a set of variable names and $\sigma$ is local bindings. For states we define two primitives to read a variable
|
||
|
|
value in a state
|
||
|
|
|
||
|
|
|
||
|
|
\[
|
||
|
|
\begin{array}{rcl}
|
||
|
|
\inbr{\sigma_g,\,\epsilon}\,x & = &\sigma_g\,x\\[2mm]
|
||
|
|
\inbr{\sigma_g,\,\inbr{S,\,\sigma}\circ ss}\,x & = & \left\{\begin{array}{rcl}
|
||
|
|
\sigma\,x &,& x\in S\\
|
||
|
|
\inbr{\sigma_g,\,ss}\,x &,&x\not\in S
|
||
|
|
\end{array}
|
||
|
|
\right.
|
||
|
|
\end{array}
|
||
|
|
\]
|
||
|
|
|
||
|
|
and to reassign a variable to another value:
|
||
|
|
|
||
|
|
\[
|
||
|
|
\begin{array}{rcl}
|
||
|
|
\inbr{\sigma_g,\,\epsilon}\,[x\gets v] & = &\inbr{\sigma_g\,[x\gets v],\,\epsilon}\\[2mm]
|
||
|
|
\inbr{\sigma_g,\,\inbr{S,\,\sigma}\circ ss}\,[x\gets v] & = & \left\{\begin{array}{rcl}
|
||
|
|
\inbr{\sigma_g,\,\inbr{S,\,\sigma\,[x\gets v]}\circ ss} &,& x\in S\\[1mm]
|
||
|
|
\inbr{\sigma^\prime_g,\,\inbr{S,\,\sigma}\circ ss^\prime}\,x &,&x\not\in S\\
|
||
|
|
& &\inbr{\sigma^\prime_g,\,ss^\prime}=\inbr{\sigma_g,\,ss}\,[x\gets v]
|
||
|
|
\end{array}
|
||
|
|
\right.
|
||
|
|
\end{array}
|
||
|
|
\]
|
||
|
|
|
||
|
|
\subsection{Expressions}
|
||
|
|
|
||
|
|
To give the semantics for the expressions we introduce a supplementary transition ``$\xRightarrow{}^*$'', which described a left-to-right computation
|
||
|
|
of the \emph{list} of expressions and results, correspondingly, in a final configuration and a \emph{list} of values:
|
||
|
|
|
||
|
|
\setarrow{\xRightarrow}
|
||
|
|
\setsubarrow{\hskip-0,3em^*\hskip0.3em}
|
||
|
|
\[
|
||
|
|
\trans{c}{\epsilon}{\inbr{c,\,\epsilon}}\ruleno{Expr$^*_\epsilon$}
|
||
|
|
\]
|
||
|
|
\[
|
||
|
|
\trule{{\setsubarrow{}\trans{c}{e}{\inbr{c^\prime,\,v}}}\qquad\trans{c^\prime}{\omega}{\inbr{c^{\prime\prime},\,\psi}}}
|
||
|
|
{\trans{c}{e\circ\omega}{\inbr{c^{\prime\prime},\,v\circ\psi}}}\ruleno{Expr$^*$}
|
||
|
|
\]
|
||
|
|
|
||
|
|
Operational semantics for core expressions is given in Fig.~\ref{semantics:core}. Note, the semantics of binary expressions is
|
||
|
|
given in terms of a primitive ``$\oplus$'', which is left undefined. The concrete semantics of binary operators is
|
||
|
|
given in Section~\ref{sec:expressions}.
|
||
|
|
|
||
|
|
\begin{figure}[t]
|
||
|
|
\setsubarrow{}
|
||
|
|
\[
|
||
|
|
\trans{c}{z}{\inbr{c,\,z}}\ruleno{Const}
|
||
|
|
\]
|
||
|
|
\[
|
||
|
|
\trans{\inbr{s,\,m,\,w}}{x}{\inbr{\inbr{s,\,m,\,w},\,s\,x}}\ruleno{Var}
|
||
|
|
\]
|
||
|
|
\[
|
||
|
|
\trans{c}{\llang{ref $\;x$}}{\inbr{c,\,\primi{ref}{x}}}\ruleno{Ref}
|
||
|
|
\]
|
||
|
|
\[
|
||
|
|
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}\trans{c}{l\circ r}{\inbr{c^\prime,\,w\circ v}}}
|
||
|
|
{\trans{c}{l\oplus r}{\inbr{c^\prime,\,w\otimes v}}}\ruleno{Binop}
|
||
|
|
\]\vskip1mm
|
||
|
|
\[
|
||
|
|
\trans{c}{\llang{skip}}{\inbr{c,\,\bot}}\ruleno{Skip}
|
||
|
|
\]
|
||
|
|
\[
|
||
|
|
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}\trans{c}{l\circ r}{\inbr{\inbr{s,\,m,\,w},\,[\primi{ref}{x}]\circ[v]}}}
|
||
|
|
{\trans{c}{\llang{$l\;$ := $\;r$}}{\inbr{\inbr{s\,[x\gets v],\,m,\,w},\,v}}}\ruleno{Assign}
|
||
|
|
\]\vskip1mm
|
||
|
|
\[
|
||
|
|
\trule{\trans{c_1}{S_1}{\inbr{c^\prime,\,v}}\qquad \trans{c^\prime}{S_2}{c_2}}
|
||
|
|
{\trans{c_1}{S_1\llang{;}\;S_2}{c_2}}\ruleno{Seq}
|
||
|
|
\]\vskip1mm
|
||
|
|
\[
|
||
|
|
\trule{\trans{c}{e}{\inbr{c^\prime,\,n}}\qquad n\ne 0\qquad \trans{c^\prime}{S_1}{c^{\prime\prime}}}
|
||
|
|
{\trans{c}{\llang{if $\ \ e\ \ $ then $\ \ S_1\ \ $ else $\ \ S_2\ \ $}}{c^{\prime\prime}}}
|
||
|
|
\ruleno{If-True}
|
||
|
|
\]\vskip1mm
|
||
|
|
\[
|
||
|
|
\trule{\trans{c}{e}{\inbr{c^\prime,\,0}}\qquad \trans{c^\prime}{S_2}{c^{\prime\prime}}}
|
||
|
|
{\trans{c}{\llang{if $\ \ e\ \ $ then $\ \ S_1\ \ $ else $\ \ S_2\ \ $}}{c^{\prime\prime}}}
|
||
|
|
\ruleno{If-False}
|
||
|
|
\]\vskip1mm
|
||
|
|
\[
|
||
|
|
\trule{\trans{c}{e}{\inbr{c^\prime,\,n}}\quad n\ne 0\quad\trans{c^\prime}{S}{\inbr{c^{\prime\prime},\,v}}\quad\trans{c^{\prime\prime}}{\llang{while $\ \ e\ \ $ do $\ \ S\ \ $}}{c^{\prime\prime\prime}}}
|
||
|
|
{\trans{c}{\llang{while $\ \ e\ \ $ do $\ \ S\ \ $}}{c^{\prime\prime\prime}}}
|
||
|
|
\ruleno{While-True}
|
||
|
|
\]\vskip1mm
|
||
|
|
\[
|
||
|
|
\trule{\trans{c}{e}{\inbr{c^\prime,\,0}}}
|
||
|
|
{\trans{c}{\llang{while $\ \ e\ \ $ do $\ \ S\ \ $}}{\inbr{c^\prime,\,\bot}}}
|
||
|
|
\ruleno{While-False}
|
||
|
|
\]
|
||
|
|
\caption{Big-step Operational Semantics for Core Expressions}
|
||
|
|
\label{semantics:core}
|
||
|
|
\end{figure}
|
||
|
|
|
||
|
|
\subsubsection{Arrays and S-expressions}
|
||
|
|
|
||
|
|
Arrays and S-expressions allow to manipulate \emph{composite valuues} which are kept in \emph{memory}. A memory is a partial function $m$
|
||
|
|
which maps \emph{locations} into composite values. Locations are abstractions of real-world memory addresses; the set of locations
|
||
|
|
is considered to be linearly ordered. We define the following primitive
|
||
|
|
|
||
|
|
\[
|
||
|
|
\primi{new}\,m\,v=\inbr{l,\,m\,[l\gets v]}\mbox{ where }l=min\{l\in\mathcal{L}\mid m\,(l)\mbox{ undefined}\}
|
||
|
|
\]
|
||
|
|
|
||
|
|
which takes a memory $m$ and a composite value $v$ and returns a \emph{new} location $l$ (previously unoccupied) and a new \emph{memory} which
|
||
|
|
associates $l$ with $v$ and preserves other associations intact.
|
||
|
|
|
||
|
|
Arrays are represented as pairs
|
||
|
|
|
||
|
|
\[
|
||
|
|
\inbr{n,\,f}
|
||
|
|
\]
|
||
|
|
|
||
|
|
where $n\in\mathbb N$ is a lengths and $f : \mathbb{N}\to\mathcal{V}$~--- element function which maps indices into values. It is assumed, that
|
||
|
|
$\primi{dom}{f}=[0\dots n-1]$.
|
||
|
|
|
||
|
|
S-expressions are represented as pairs
|
||
|
|
|
||
|
|
\[
|
||
|
|
\inbr{t,\,s}
|
||
|
|
\]
|
||
|
|
|
||
|
|
where $t$ is a \emph{tag} and $s$ is an array of subexpressions. The semantics of arrays and subexpressions is given in Fig.~\ref{semantics:arrays}.
|
||
|
|
|
||
|
|
\begin{figure}
|
||
|
|
\setsubarrow{}
|
||
|
|
\[
|
||
|
|
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
|
||
|
|
\begin{array}{c}
|
||
|
|
\trans{c}{e_1\circ\dots\circ e_k}{\inbr{\inbr{s,\,m,\,w}, v_1\circ\dots\circ v_k}}\\[2mm]
|
||
|
|
\inbr{l,\,m^\prime}=\primi{new}{m\,\inbr{k-1,\,i\mapsto v_{i+1}}}
|
||
|
|
\end{array}
|
||
|
|
}
|
||
|
|
{\trans{c}{\llang{[$e_1,\dots,e_k$]}}{\inbr{\inbr{s,\,m^\prime,\,w},\,l}}}\ruleno{Array}
|
||
|
|
\]\\[2mm]
|
||
|
|
\[
|
||
|
|
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
|
||
|
|
\begin{array}{c}
|
||
|
|
\trans{c}{e_1\circ\dots\circ e_k}{\inbr{\inbr{s,\,m,\,w}, v_1\circ\dots\circ v_k}}\\[2mm]
|
||
|
|
\inbr{l,\,m^\prime}=\primi{new}{m\,\inbr{t,\,\inbr{k-1,\,i\mapsto v_{i+1}}}}
|
||
|
|
\end{array}
|
||
|
|
}
|
||
|
|
{\trans{c}{\llang{$t\,$($e_1,\dots,e_k$)}}{\inbr{\inbr{s,\,m^\prime,\,w},\,l}}}\ruleno{Sexp}
|
||
|
|
\]\\[2mm]
|
||
|
|
\[
|
||
|
|
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
|
||
|
|
\begin{array}{c}
|
||
|
|
\trans{c}{e_1\circ e_2}{\inbr{\inbr{s,\,m,\,w},\,l\circ i}}\\[2mm]
|
||
|
|
l\in\mathcal{L}\\
|
||
|
|
m\,(l)=\inbr{k,\,f}\mbox{ or }m\,(l)=\inbr{t,\,\inbr{k, f}}\\
|
||
|
|
i\in[0\dots k-1]
|
||
|
|
\end{array}
|
||
|
|
}
|
||
|
|
{\trans{c}{\llang{$e_1\,$[$e_2$]}}{\inbr{\inbr{s,\,m,\,w},\,f\,(i)}}}\ruleno{Elem}
|
||
|
|
\]\\[2mm]
|
||
|
|
\[
|
||
|
|
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
|
||
|
|
\begin{array}{c}
|
||
|
|
\trans{c}{e_1\circ e_2}{\inbr{\inbr{s,\,m,\,w},\,l\circ i}}\\[2mm]
|
||
|
|
l\in\mathcal{L}\\
|
||
|
|
m\,(l)=\inbr{k,\,f}\mbox{ or }m\,(l)=\inbr{t,\,\inbr{k, f}}\\
|
||
|
|
i\in[0\dots k-1]
|
||
|
|
\end{array}
|
||
|
|
}
|
||
|
|
{\trans{c}{\llang{elemRef ($e_1$,$\ \ e_2$)}}{\inbr{\inbr{s,\,m,\,w},\,\primi{elemRef}{l\;i}}}}\ruleno{ElemRef}
|
||
|
|
\]\\[2mm]
|
||
|
|
\[
|
||
|
|
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
|
||
|
|
\begin{array}{c}
|
||
|
|
\trans{c}{l\circ r}{\inbr{\inbr{s,\,m,\,w},\,[\primi{elemRef}{l\;i}]\circ[v]}}\\[2mm]
|
||
|
|
m^\prime=\left\{\begin{array}{rcl}
|
||
|
|
m\,[l\gets\inbr{k,\,f\,[i\gets v]}] &,&m\,(l)=\inbr{k,\,f}\\
|
||
|
|
m\,[l\gets\inbr{t,\,\inbr{k,\,f\,[i\gets v]}}] &,&m\,(l)=\inbr{t,\,\inbr{k,\,f}}
|
||
|
|
\end{array}
|
||
|
|
\right.
|
||
|
|
\end{array}
|
||
|
|
}
|
||
|
|
{\trans{c}{\llang{$l\;$ := $\;r$}}{\inbr{\inbr{s,\,m,\,w},\,v}}}\ruleno{AssignElem}
|
||
|
|
\]
|
||
|
|
\caption{Big-step Operational Semantics for Arrays and S-expressions}
|
||
|
|
\label{semantics:arrays}
|
||
|
|
\end{figure}
|
||
|
|
|
||
|
|
\subsubsection{Pattern Matching}
|
||
|
|
|
||
|
|
\subsubsection{Declarations}
|
||
|
|
|
||
|
|
\subsubsection{Functions and Closures}
|
||
|
|
|