Linear Schemas for Program Dependence (EPSRC)

I am the principal investigator on Linear Schemas for Program Dependence (EPSRC: EP/E002919/1) (Collaboration with Kings College London, Brunel University, @UK PLC and AT & T, Bell Research Labs, USA.) Program schemas, (also called schemas, or schemata) define a class of programs, all of which have identical statement structure, but whose expressions may differ. Program Schemas have a well developed theory.

As a result of our work in program slicing, we found that program schema theory enabled us to precisely express the problems that we were tackling; namely the existence of statement minimal slicing algorithms at the `dataflow' level of abstraction. For such problems a class of schema which we called a `linear schema' was introduced. A linear schema is one in which no predicate or function symbol occurs more than once. Serendipitously, the proposers later discovered that the linearity condition helped in proving decidability of equivalence of schemas. Decidability of equivalence is the ability to automatically check whether two different schemas represent the same class of programs. We proved that equivalence of conservative, free, linear schemas is decidable and later strengthened this by proving that equivalence of liberal, free linear schemas is decidable in polynomial time. This work represented significant progress in the field of schema theory.