Commit 11caa092 authored by Vladimír Uhlík's avatar Vladimír Uhlík
Browse files

I dont know, zjb.

parent 4b2b7936
Loading
Loading
Loading
Loading
Loading
+15 −9
Original line number Diff line number Diff line
@@ -158,17 +158,24 @@ or the executed instruction is ill-formed. This state is denoted as $\bot$.
An \textit{instruction} is a value representing a statement that the machine can execute as an
evaluation step. Its formal definition is closely related to a program in which it is present:
\begin{theorem}
    Let $\mathcal{P}$ be a set of all programs. An instruction I in program P is a triple
    Assume an arbitrary Cthulhu program $\mathcal{P}$. An instruction I in the program $\mathcal{P}$ is a triple
    \texttt{(m, op, args)}, where:
    \begin{itemize}
        \item \texttt{m} is a structure from set $\mathcal{P}$.M. This parameter is called \textit{structure id}.
        \item \texttt{op} is an operation from set $\bigcup_{t \in T}{T.Sym}$, i.~e.~set of
        all operations defined in signatures from program $\mathcal{P}$.
        \item \texttt{args} are stack numbers.
        \item \texttt{args} is a tuple of stack numbers.
    \end{itemize}
\end{theorem}

Each instruction encoded into 32 bits.~\textit{Structure id} represents first
\begin{theorem}
    Assume an arbitrary Cthulhu program $\mathcal{P}$. A set of all instructions $\mathcal{I}$ in the program
    $\mathcal{P}$ is defined as follows:
    \[\mathcal{I} = \{(m,~op,~args)~|~m \in \mathcal{P}.M,~op \in \bigcup_{t \in T}{T.Sym},
      ~args \in \mathbb{N} \times~\ldots~\times \mathbb{N}\}\]
\end{theorem}

Each instruction is encoded into 32 bits.~\textit{Structure id} represents first
12 bits, whereas \textit{operation} and its \textit{arguments} are encoded into the remaining 20 bits.
\begin{exmp}
    As an example consider the following instruction:
@@ -594,12 +601,11 @@ In the following pseudocodes, symbols:

Finally, formal definitions of an evaluation step and an evaluation of a Cthulhu program are as follows:
\begin{theorem}
    Assume a set of all states $\Psi$ from definition five and a program $\mathcal{P}$.
    Let $\mathcal{I}$ be a set of all instructions used in $\mathcal{P}$.
    An evaluation step of a Cthulhu program is a binary relation $\vdash$ on the set $\Psi \times \Psi$.
    Two states $\mu$ and $\pi$ are in relation $\Psi$, if there is an instruction in set $\mathcal{I}$
    such that execution of the instruction in state $\mu$ transforms the state of the Cthulhu machine
    to state $\pi$.
    Assume a program $\mathcal{P}$, a set of all states of this program $\Theta \subseteq \Psi$ and a set $\mathcal{I}$, which
    is a set of all instructions used in $\mathcal{P}$. An evaluation step of a Cthulhu program is a binary
    relation $\vdash$ on the set $\Theta \times \Theta$. States $\mu,~\pi \in \Theta$ are in relation $\vdash$,
    if there is an instruction in the set $\mathcal{I}$ such that execution of the instruction transforms the state of
    the Cthulhu machine from the state $\mu$ to the state $\pi$.
\end{theorem}

\begin{theorem}