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.
There is strong evidence that the imposition of this extra but natural condition of linearity (or partial forms of linearity) will lead to further decidability results in the theory of schemas. We hope that our new results will lead to a re-appraisal of the substantial body of work in program schema theory and to further research its applications in a modern framework. Our paper Static Program Slicing Algorithms are Minimal for Free Liberal Program Schemas contains a good introduction to our work with all the necessary formal definitions. We have regular Schema Meetings which you are welcome to attend.
We are always looking for mathematicians and computer scientists to get involved with this work. Please contact firstname.lastname@example.org if you think you may be interested or have any questions.