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,
- a set of formulas.
- 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:
- the set of legal inference steps
which have formula a
as conclusion.
- 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:
- the set of identifiers for premises of
inference step b which has conclusion
a.
- 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
- the formula to be proved by the
c-th premise of rule b
for concluding a.
- 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.