Decidability of Strong Equivalence for Subschemas of a Class of Linear, Free, near-Liberal Program Schemas

In this paper we introduce
near-liberal schemas, in which this non-repeating condition applies only to terms
not having the form g() for a constant function symbol g. Given a schema S that is
linear (no function or predicate symbol occurs more than once in S) and a variable v,
we compute a set of function and predicate symbols in S which is a subset of those
de�ned by Weiser's slicing algorithm and prove that if for every while predicate
q in S and every constant assignment w := g(); lying in the body of q, no other
assignment to w also lies in the body of q, our smaller symbol set de�nes a correct
subschema of S with respect to the �nal value of v after execution. We also prove
that if S is also free (every path through S is executable) and near-liberal, it is
decidable which of its subschemas are strongly equivalent to S. For the class of
pairs of schemas in which one schema is a subschema of the other, this generalises
a recent result in which S was required to be linear, free and liberal.
P