Next: Equivalence Relations on
Up: Finite Automata
Previous: Equivalence Relations and
An equivalence relation 
on 
is said to be of finite
index iff 
is finite. 's index is the
cardinality of . A very important result we need is that if
is decidable and is finite, then is finite, and its
cardinaltiy is less or equal to that of . Indeed if is finite,
say of size 
, the index 
of any finite index satisfies 
. See quo_of_finite in the relation library.
Given two equivalence relations and 
on , we say that
refines iff 
We write 
. This means that the equivalences classes of 
are
possibly refined or decomposed into smaller classes. A suggestive picture is:
circle.ps
Although we will not discuss subtyping here, we note that in
general 
iff 
in 
implies in 
(so 
in 
in
which means 
is a ``subtype'' of 
). We have
for any equivalence relations, implies 
and 
. We can think of
as 
where 
iff 
in ; clearly 
for any on , so 