# State machines and rule sets

In connection with rule systems for grammars, Petersonn and Synek introduced the following class of structures (A,B,C,d) which admit a large number of applications, including one to rule sets (as in Peter Aczel's article "Inductive definitions" in the Handbook of Mathematical Logic), and one to the theory of state machines:
• A is a set. For example,
1. a set of formulas.
2. a set of protocol states.
• B is a family of sets indexed by A. For example, the set B(a) (where a is an element of A) might represent:
1. the set of legal inference steps which have formula a as conclusion.
2. the set of legal commands that may be issued by the user of a state machine when the protocol is in state a.
• C is a doubly-indexed family of sets indexed by A and B(a) (where a is an element of A). For example, C(a,b) might represent:
1. the set of identifiers for premises of inference step b which has conclusion a.
2. the set of legal responses that may be returned by the state machine to a user who has issued command b in state a.
• d is a ternary function which applied to an element a of A, and element b of B(a), and an element c of C(a,b) returns an element d(a,b,c) of A. For example d(a,b,c) might represent
1. the formula to be proved by the c-th premise of rule b for concluding a.
2. the protocol state after in state a the user issues command b and gets response c.
Essentially the same structure can be expressed as a function from A to Fam (Fam A), where Fam of a type is the type SIGMA I : Set . I -> A. This defines two monotone functions from predicates over A to predicates over A :
• User ( X ) = exists b : B a . all c : C a b . X (d a b c) There is a command which the user can issue which ensures that X holds in the next state, whatever the response. (There may be no possible response, and hence no next state.)
• Machine ( X ) = all b : B a . exists c : C a b . X (d a b c) Whatever the command, there is a way for the machine to responding which ensures that X holds in the next state.

The least fixed point of the function User is a set of states in which the user has a strategy, or interactive program which forces the machine to stop. A constructive proof that the machine can be forced to stop is essentially a well founded structure saying what commands to issue, and what to do with a possible response. It is something which can be used as a program. Note that the state of the user program is something quite different from the state of the user/machine protocol.

The least fixed point of the function Machine is a set of states in which the machine has a strategy, or interactive program which forces the user to stop. A constructive proof that the user can be forced to stop is essentially a well founded structure saying for any command what responses to give for it, and what to do next. It is something which can be used as a program for the state machine. Notice that the state of the machine is something quite different from the state of the user/machine protocol.

There are a number of other inductive constructions which arise in connection with interactive programs and state-machines. It is also interesting to consider notions of simulation, "virtual" machines, and refinement.