Revisiting Sebastian's thesis with Freeness

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 Chapter 7.