Add actual state.

Besides the CCC, the source bundle includes a light-weight virtual machine

for the Cthulhu programs implemented in Python with complete support for the code

emitted by the CCC. However, its mainly used for testing purposes

emitted by the CCC.

\section{Front-end}

The front end part the of the CCC consist of \textit{tokenizer}, \textit{parser}

\label{def:const}

\end{theorem}

\noindent The motivation behind quote instructions is the ability to create new instructions directly during

program execution. For instance, this capability proves very useful when modelling control flow statements.

For this purpose, a structure \textit{quote} is defined as one that implements constructors for a given instruction set.

\begin{theorem}

    Given the set of instructions $\mathcal{I}$, where $\forall i \in \mathcal{I}: i.m \neq quote$.

    Given a set of instructions $\mathcal{I}$, where $\forall i \in \mathcal{I}: i.m \neq quote$.

    Structure quote is a quadruple \texttt{(T, Sym, $\varphi$, $\tau$)}, where:

    \begin{itemize}

        \item $T = \{t\}$,

        \item $Sym = \{(instr)~|~instr~is~an~instruction~from~\mathcal{I}\}$,

        \item $(instr)~::~(\vartextvisiblespace \rightarrow t)$.

        \item $(instr)~::~(\vartextvisiblespace \rightarrow t)$,

        \item implementation assigned by $\tau$ is dependent on a Cthulhu machine.

    \end{itemize}

    The notation $(instr)$ represents a constructor as defined in \myref{def.}{def:const} for

    the instruction $insrt \in \mathcal{I}$.

\label{quote}

\end{theorem}

\noindent Based on the above definition, it is now possible to define a quote instruction:

\noindent Based on the \myref{definition}{quote}, it is now possible to define a quote instruction:

\begin{theorem}

    A quote instruction is a triple \texttt{(m, op, id)}, where:

    \begin{itemize}

\end{exmp}

\subsection{Program definition}

A Cthulhu machine state from which a program starts its computation is determined by a program parameter.

This state is constrained to values exclusively from a predefined set, also specified as a program parameter.

This set contains arbitrary values, including instructions.

Additionally, the program needs a set of signatures on its input to determine what operation is involved during computation.

Of course, this determination must be unambiguous; thus, the sets of operations in the signatures must be mutually exclusive.

Moreover, the program must know the structures implementing the operations to assign them semantics. Based on the above,

a Cthulhu program has the following definition:

The program's definition is primarily motivated by providing a precise description of the computations

executed on a Cthulhu machine. As discussed in Section 1, the computation in Cthulhu takes place on stacks

whose contents are defined on a given set of values. Therefore, to perform any computation, it is necessary

to supply a set of values on which a state of a Cthulhu machine is defined. Among the values of this

set are instructions that carry information about operations. Knowing the set of signatures from which the

operations used in the computation originate is necessary to identify these operations. Furthermore, to perform

a given operation, it is necessary to know its semantics. Therefore, it is also essential to know the structures

that implement the operations used during computation.

The above observations imply that in order to perform a computation, it is necessary to know the set of

signatures that define the operations used in the computation, the set of structures that provide the

semantics of the operations, the set of values on which the computation is performed, and finally the

state of the Cthulhu machine. The Cthulhu program is created by combining these four elements.

\begin{theorem}

    A program is defined as a quadruple \texttt{($\Sigma$, M, V, $\psi$)}, where:

This section defines an \textit{evaluation step} in a Cthulhu machine. Each evaluation step consists of the following:

\begin{enumerate}

    \item Popping an instruction from the first stack.

    \item Execution of the popped instruction according to provided implementation.

    \item Execution of the operation from the popped instruction according to the provided implementation.

          It can result in two situations:

          \begin{itemize}

              \item Instruction is executed without failure, and the program transits to another program.

              \item Operation is executed without failure, and the program transits to another program.

               Due to non-determinism, several programs might be reachable from a particular program.

              \item Instruction execution fails and the program ends in the undefined state $\bot$.

          \end{itemize}

\end{enumerate}

\noindent To define an evaluation step, firstly, the mapping $\kappa$ is defined. This mapping describes a

\textit{transition} among programs. The definition of the mapping $\kappa$ is as follows:

\noindent When an operation from the instruction from the first stack is executed in a program

$\mathcal{P}$, the only thing that changes is the program's state $\mathcal{P}.\psi$.

$\mathcal{P}.\Sigma$, $\mathcal{P}.M$, and $\mathcal{P}.V$ remain unchanged. The way in which

$\mathcal{P}$ transits its state $\mathcal{P}.\psi$ is called \textit{an effect of an instruction}.

Based on this transition is defined the relation $\vdash$ between two programs. This relation

represents an \textit{evaluation step} of a Cthulhu program.

\begin{theorem}

    Assume a program $\mathcal{P}$. Let $\Theta$ be a finite set of states defined as $\Theta = \mathcal{P}.V^n$,

    where $n$ is the number of stacks in a Cthulhu machine. Let $\Omega$ be a finite set of programs defined

    as $\Omega = \{(\mathcal{P}.\Sigma,~\mathcal{P}.M,~\mathcal{P}.V,~\theta)~|~\theta \in \Theta\}$.

    Let $\mathcal{J} \subseteq \mathcal{P}.V$ be a set of all instructions (including quoted instructions)

    in program $\mathcal{P}$. Mapping $\kappa$ is defined as:

    \[\kappa :: \Omega \times \mathcal{J} \rightarrow 2^\Omega.\]

    $\kappa$ assigns a set of programs to the program $\mathcal{P}$, into which the program $\mathcal{P}$

    is transformed when an instruction from the set $\mathcal{J}$ is executed.

\label{def-kappa}

    Assume a program $\mathcal{P}$ and a program $\mathcal{P'}$, where $\mathcal{P}.\Sigma = \mathcal{P'}.\Sigma$,

    $\mathcal{P}.M = \mathcal{P'}.M$, and $\mathcal{P}.V = \mathcal{P'}.V$. Programs $\mathcal{P}$ and $\mathcal{P'}$

    are in relation $\vdash$ if the effect of an instruction transits state $\mathcal{P}.\psi$ to

    the state $\mathcal{P'}.\psi$.

\end{theorem}

\begin{theorem}

    Assume a program $\mathcal{P}$ and a set of programs as defined in \myref{def.}{def-kappa}. An evaluation step in

    a Cthulhu machine is a binary relation $\vdash$ on the set $\Omega \times \Omega$. Let \texttt{i} be an

    instruction popped from the top of the first stack. Two programs from the set $\Omega$ are in the relation $\vdash$

    if the following holds:

    \[ \forall \mu,~\pi \in \Omega: (\mu,~\pi)_{\vdash} \Leftrightarrow \pi \in \kappa(\mu,~i).\]

\end{theorem}

\noindent Finally, an evaluation of a Cthulhu program is defined as repeated application

of an evaluation step.

\begin{theorem}

    An evaluation $\vdash^*$ of a Cthulhu program $\mathcal{P}$ is defined as a sequence of evaluation steps, where:

\chapter{Structures for the C compiler}

This chapter introduces structures used by the C compiler for the Cthulhu language.

These structures are directly executable in the provided Cthulhu machine. Each description

begins with the definition of a signature that a particular structure implements.

These structures are directly executable in the provided Cthulhu machine. 

\section{Sequences}\label{code}

The first two signatures are CODE[U, P] and SEQ[U, P]. These signatures differ in the conditions

\\\\

\noindent \textbf{CODE[U, P]} is signature \texttt{(T, Sym, $\varphi$)}, where:

\begin{itemize}

    \item $T~=~\{U, P\}$,

    \item $T~=~\{U,~P\}$,

    \item $Sym~=~\{pack,~unpack,~flip,~dup,~move,~pivot,~drop,~amb\}$,

    \item $pack~::~(U \rightarrow \vartextvisiblespace)

                  ~(\vartextvisiblespace \rightarrow P)$,