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.