A set-theoretic formulation of an algorithm that enforces effectiveness

This builds on the formulation of an algorithm given here. We will place restrictions on $Q$, $I$, $\Omega$ and $f$ so as to enforce effectiveness.

Let $A$ be a finite set of letters, and let $A^{\ast }$ be the set of all strings on $A$. Let $N$ be a nonnegative integer: we will then have $Q$ be the set of all $(\sigma ,j)$ where $\sigma \in A^{\ast }$ and $0\le j\le N$.

So $Q$ is the set of ordered pairs of strings in $A^{\ast }$ and integers from $0$ to $N$. We will then have $I$ be the subset where $j=0$, and $\Omega$ be the subset where $j=N$.

We will define $f$ in terms of two lists of strings and two lists of integers. The strings and integers are given by ${\theta }_j$, ${\varphi }_j$, $a_j$ and $b_j$ respectively, for $0\le j\le N$.

$$\begin{array}{rlr}f((\sigma ,j))& =(\sigma ,a_j)& \text{if }{\theta }_j\text{ does not occur in }\sigma ;\\ f((\sigma ,j))& =(\alpha {\varphi }_j\omega ,b_j)& \text{if }\alpha \text{ is the shortest possible string for which }\sigma =\alpha {\theta }_j\omega ;\\ f((\sigma ,N))& =(\sigma ,N)& \text{(thus}f\text{ leaves }\Omega \text{ pointwise fixed)}\end{array}$$

In words: $f$ takes a pair $(\sigma ,j)$, and branches the computation according to whether ${\theta }_j$ occurs in $\sigma$. If it does, then it substitutes ${\theta }_j$ by ${\varphi }_j$ in $\sigma$, and switches $j$ for $b_j$. Otherwise, $f$ does nothing to the string; it simply substitutes $j$ for $a_j$.