It is the approach and practice of Formal Methods to describe any part of Cyberspace mathematically (popular model-based formalisms consistent with our treatment here are given by Z [16] and VDM [10]). Here we adopt that approach to conceptualise the part of Cyberspace in which we are interested, at a particular time, as an object (or module, or abstract data type) having a set of precisely-defined states operated on by a family of mathematically specified actions (or methods or operations). Examples are provided in section 5.
Let denote the set of
states -- the state space -- of the system under consideration. It could be one small
component, like an editor, on a specific machine with the actions it offers the user, or a
network with many terminals and filestores connected to the internet and all its attendant
actions. In the extreme case, it is the whole of Cyberspace. We now introduce the notion
of entropy structure on
. The elements in the definition are routine (see, for example, [3]).
We use the following notation. The symbol means 'equals by
definition'. All variables of each predicate are assigned a type and quantification is
over the appropriate type. The predicate
is read for all x in X, P holds. Thus the symbol is used to separate the typed quantifiers from
the body of the predicate. We write
for the predicate P implies Q and
for the space of all functions from to
. Otherwise our notation is standard.
A relation on
is a subset of the Cartesian
product of
with itself
Membership of an ordered pair to relation
is read A relates x to x' and written in infix:
The converse of a relation
on
is its
'mirror image'
A pre-order on
consists of a relation
on
which is reflexive (i.e. includes the identity relation) and transitive
(i.e. closed under sequential composition):
A pre-order is total iff any two elements of
are related by either
or its converse
The equivalence relation of a pre-order
is the relation on
equal to the intersection of
and its converse
To be an equivalence relation means that it is not only a pre-order on , but also symmetric
(i.e. contained in its converse):
The -equivalence class of
consists of all elements of
equivalent to
The definition of pre-order is sufficient to ensure that the equivalence classes of
elements of partition
:
Furthermore the pre-order is well-defined on equivalence classes: the relation, again
called
, which is defined on equivalence classes if the original pre-order holds
between representative elements of those classes
is well-defined (i.e. does not depend on the representatives), is again a pre-order, and in addition is antisymmetric:
In other words becomes a partial order on
-equivalence
classes.
An important way to define a pre-order on
is to define a level function
from
to the real numbers,
, and then to define the derived pre-order
by setting
(1) |
where the order denotes the standard (total) ordering between
real numbers. Pre-orders so defined are automatically total partial orders, by properties
of
. In fact, because Cyberspace is discrete by choice of an
appropriate encoding, we can always ensure that
there is replaced by the natural numbers
whose ordering
is a restriction of
. But use of
permits us the
flexibility of considering also 'continuous' examples from the 'real' world.
By an entropy structure we mean a triple consisting of a set
, a pre-order
on
and the equivalence relation
of
.
It is worth emphasising that the definitions of the ingredients of an entropy structure can be couched in whatever mathematical notions are convenient. Typically, level functions and pre-orders are expressed using concepts perceived only from 'outside' the system under consideration. That ought not to be surprising: whilst the subsystem of Cyberspace must be self-contained its description is a meta-activity.