X-machine
From Wikipedia, the free encyclopedia
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 model, which has acquired some significance as the basis for much work in the development of software that can be guaranteed to be testable.
[edit] 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 φ1 ... φn of relations. We call the composition φ1 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.
[edit] 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.
[edit] 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.