Definition:Algorithm/Formal Specification

From ProofWiki
Jump to navigation Jump to search


An algorithm can be implemented formally as a computational method $\left({Q, I, \Omega, f}\right)$ as follows:

Let $A$ be a finite set of symbols.

Let $A^*$ be the set of all collations on $A$:

$\left\{ {x_1 x_2 \cdots x_n: n \ge 0, \forall j: 1 \le j \le n: x_j \in A}\right\}$

The states of the computation are encoded so as to be represented by elements of $A^*$.

Let $N \in \Z_{\ge 0}$.

Let $Q$ be the set of all ordered pairs $\left({\sigma, j}\right)$ where $\sigma \in A^*, j \in \Z: 0 \le j \le N$.

Let $I \subseteq Q$ such that $j = 0$.

Let $\Omega \subseteq Q$ such that $j = N$.

Let $\theta, \sigma \in A^*$.

Then $\theta$ occurs in $\sigma$ if and only if $\sigma$ has the form:

$\alpha \theta \omega$

where $\alpha, \omega \in A^*$.

Let $f$ be a mapping of the following type:

$f \left({\left({\sigma, j}\right)}\right) = \begin{cases}\left({\sigma, a_j}\right) : & \sigma_j \text { does not occur in } \sigma \\ \left({\alpha \theta_j \omega, b_j}\right) : & \alpha \text { is the shortest element of $A^*$ such that } \sigma = \alpha \theta_j \omega\end{cases}$
$f \left({\left({\sigma, N}\right)}\right) = \left({\sigma, N}\right)$