A faulty editor

In this section we demonstrate how a more complex entropy structure may be produced from simpler ones using the techniques of section 4.3. The example is that of a line editor, which inputs words and checks them for spelling against a dictionary.

Words are input from a keyboard and represented on screen by the editor. A binding associates each sequence of characters with its representation on screen (in practice that is done character-by-character, but for this example we suppose it to be done by word). The correct binding is a function

$$c : W \fun \textit{Reps}$$

where $W$ denotes the set of all words (i.e. sequences of characters) and Reps denotes their representations on screen. The state of a line editor is a sequence of words input so far, with the representation of each

$$X_A \ =_{\textit{\tiny def}}\ \ \textit{seq}\, (W \times \textit{Reps}) .$$

Initially the state is empty. The action $E_A$ of editing the next word extends the state by a pair consisting of the input word $\omega : W$ and its representation $\rho : \textit{Reps}$

$$\sigma~E_A~\sigma .\, (\omega, \rho) .$$

That action is deemed to be good or benign if all words are represented correctly and otherwise it is deemed to be evil. Such intuition is captured by taking the entropy structure defined by the level function $\lambda_A : X_A \fun {\mathbb{N}}$ which captures the number of words incorrectly represented

$$\lambda_A ( \sigma ) \ =_{\textit{\tiny def}}\ \ \char93 \{ i \mid c(p_1 (\sigma (i))) \neq p_2(\sigma (i)) \}$$

where projection functions $p_1$ and $p_2$ are defined by $p_1 (\omega, \rho) = \omega$ and $p_2 (\omega, \rho) = \rho$. The resulting entropy structure ${\cal A} =_{\textit{\tiny def}}\ (X_A,\leq_A,\sim_A)$ provides a simple generic example.

Now suppose that it is deemed important to represent certain words correctly but that other words are of less concern. Perhaps, for example, correct representation of text is more important than that of strings of mathematical symbols; or vice versa. Such decisions are codified by a pre-order $\leq_W$ on words. For example to ensure that words in some set $S$ are more important than others, take the pre-order given by the level function $\lambda_W : W \fun {\mathbb{B}}$, defined

$$\lambda_W (w) \ =_{\textit{\tiny def}}\ \ (w \in S) .$$

But of course in general pre-order $\leq_W$ may be total. To modify the entropy structure $\cal A$ to reflect that extra information, it suffices to use the lexical pre-order in which $\leq_A$ is refined by $\leq_W$. For then the resulting pre-order $\leq_B$ orders first states with no errors, then all states with one error, ordered where possible by $\leq_W$, then states with two errors and so on. The resulting entropy structure has the same state as $\cal A$, but the more complex lexical pre-order and equivalence defined in terms of simpler ones; we write it ${\cal B} =_{\textit{\tiny def}}\ (X_A,\leq_B,\sim_B)$. So much for input of words.

A line editor uses a dictionary to check the spelling of the words it inputs. But the dictionary may have some errors, or we may use an American dictionary to check a British English text, or vice versa. Let $RH \subseteq W$ denote the actual dictionary used by the editor and $OED \subseteq W$ the correct one. (We overlook order in our dictionaries since we are here not interested in implementing the lookup function). A word is correctly classified by dictionary $RH$ iff both $RH$ and $OED$ would give the same answer, i.e. the word lies in the set

$$V \ =_{\textit{\tiny def}}\ \ (RH \cap OED) \cup \overline{(RH \cup OED)} ,$$

where $\overline{S}$ denotes the complement of subset $S$ of $W$. The edit action $E_C$ appends to state a word and a bit saying whether or not that word is correctly classified by $RH$. Thus state is given by

$$X_C \ =_{\textit{\tiny def}}\ \ \textit{seq}\, (W \times {\mathbb{B}})$$

and the edit action given by

$$\sigma~E_C~(\sigma .\, \omega, (\omega \in V)) .$$

A good or benign action appends only correct words; an evil one commits at least one error. That is captured by the entropy structure whose level function $\lambda_C : X_C \fun {\mathbb{N}}$ captures the number of words incorrectly spelt according to $RH$

$$\lambda_C (\sigma ) = \char93 \{ j \mid \neg p_2 (\sigma (j)) \} .$$

The result is another simple entropy structure ${\cal C} =_{\textit{\tiny def}}\ (X_C,\leq_C,\sim_C)$.

Finally an editor uses a keyboard for entry of words and a dictionary to check the correctness of their spelling. Let us see how to define this simply in terms of $\cal A$ and $\cal C$. Firstly, the state combines both $X_A$ and $X_C$: it consists of a single sequence of input words

$$X_D \ =_{\textit{\tiny def}}\ \ \{ \sigma : X_A \times X_C \mid p_1(p_1(\sigma )) = p_1(p_2(\sigma )) \} .$$

Action $E_D$ extends state by a word together with its representation and the correctness of its spelling

$$\sigma~E_C~((\sigma .\, \omega,\rho) ,(\sigma .\, \omega, (\omega \in V) )) .$$

Such an action ought to be good iff it is good for both components; similarly for benign actions; an action ought to be evil iff it is evil for at least one component. That is achieved precisely by the conjunction entropy structure ${\cal D} =_{\textit{\tiny def}}\ (X_D,\leq_D,\sim_D)$ in which $\leq_D$ is the conjunction of pre-orders $\leq_A$ and $\leq_C$.

(As an exercise, the reader may wish to define, solely in terms of the entropy structures introduced here and the combinators of section 4.3, an entropy structure which captures the decision that errors in representing a word on screen are worse than a faulty dictionary. The ordering should be: first all states with no faulty word representations, ordered by the number of faults in $RH$, then all states with just one faulty representation, ordered by number of faults in $RH$, and so on.)