In Sebastian's thesis,
he proved that if we unold a while-schema sufficiently often
we will end up with a while-free schema which has exactly the same dependencies
as the corresponding while-schema. Unfortunately he could not find an
algorithm which tells when the schema is sufficiently unfolded. In general
this may be uncomputable.
We now think that with the extra constraint that the schema must be free there
is a likelihood that the problem now becomes tractable.
An explanation of unfolding is given in
Seb's Home Page
Last updated 2007-04-30