X-MACHINE

The 'X-machine' is a theoretical model of computation introduced by Samuel Eilenberg in 1974. In its original form, the X-machine is rarely encountered, though Mike Stannett introduced a continuous-time variant in 1990 (the Analog X-Machine) that is relevant to early work in hypercomputation theory. More recently, NASA have discussed using a combination of X-machines and process calculus in the development of ''swarm satellite'' systems (Hinchey ''et al'', 2005).
The most commonly encountered X-machine variant is Gilbert Laycock's Stream X-Machine (SXM) model, which has acquired some significance as the basis for much work in the development of software that can be guaranteed to be testable.

Contents

Formal definitions

Example

References

Formal definitions

An X-machine is essentially a "machine for manipulating objects of type X". Suppose that X is some datatype, called the ''fundamental datatype'', and that Φ is a set of relations φ: X → X. An X-machine is a finite-state machine whose arrows are labelled by relations in Φ. Each recognised path through the machine generates a list φ₁ ... φ_''n'' of relations. We call the composition φ₁ o ... o φ_''n'' of these relations the ''path relation'' corresponding to that path. The ''behaviour'' of the X-machine is defined to be the union of all its path-behaviours. In other words, an X-machine can perform a manipulation just so long as one of its recognised paths can perform that computation.

Example

A word-processor can be thought of as a 'Document'-machine, where 'Document' is some data type representing documents. Typical processing relations might include 'A', a function that inserts the letter 'A' at the current cursor position.
Suppose the machine contains a state called 'Editing', representing the state in which editing of the document is allowed (as opposed to printing, saving, etc). For each of the letters A - Z, the machine will be equipped with an arrow from 'Editing' to itself. That is, we'll have arrows
Editing →^A Editing
Editing →^B Editing
Editing →^C Editing
and so on.
Suppose also that the keyboard has a special key marked ''Save'', and that pressing ''Save'' takes the machine from the 'Editing' state to the terminal state 'Saved'. Hitting the ''Save'' button has no effect on the document itself - it simply changes machine state. We'd model it as the ''identity'' function ('id') on documents. Likwise, we can imagine that the machine always starts up in edit-mode, so that 'Editing' is the machine's initial state.
Now imagine that you're using the word processor to edit a document. One particular path from 'Editing' to 'Saved' would be

Editing →^H
Editing →^E
Editing →^L
Editing →^L
Editing →^O
Editing →^id
Saved

This path goes from the initial state 'Editing' to the terminal state Saved, so it is recognised by the finite state machine, and contributes to the behaviour of the X-machine. The path relation computed by this path has the effect of inserting the word "HELLO" into the document.

References

# Samuel Eilenberg (1974) ''Automata, Languages and Machines, Vol. A''. Academic Press, London.
# M. G. Hinchey, C. A. Rouff, J. L. Rash and W. F. Truszkowski (2005) "Requirements of an Integrated Formal Method for Intelligent Swarms", in ''Proceedings of FMICS'05, September 5–6, 2005, Lisbon, Portugal''. Association for Computing Machinery, pp. 125-133.
# Gilbert Laycock (1993) ''The Theory and Practice of Specification Based Software Testing''. PhD Thesis, University of Sheffield, Dept of Computer Science. Abstract
# Mike Stannett (1990) 'X-machines and the Halting Problem: Building a super-Turing machine'. ''Formal Aspects of Computing'' '2', pp. 331-41.