Linear Schemas for Program Dependence

程序模式是一种表示具有相同语法结构的无限计算机程序集的符号。如果程序模式的一个性质可以被证明，则该性质对由该模式表示的无限程序集中的每个程序都成立。因此，使用模式进行推理是一种非常强大的机制。由于他们在程序切片方面的工作，提议者发现程序图式理论使他们能够精确地表达他们正在处理的问题；即在“数据流”抽象层次上存在语句最小切片算法。对于这类问题，他们引入了一类被称为“线性模式”的模式。线性模式是谓词或函数符号不重复出现的模式。后来，作者偶然发现线性条件有助于证明图式等价的可决性。等价的可判定性是指自动检查两个不同的模式是否表示同一类模式的能力。他们证明了保守的，自由的，线性图式的等价性是可决定的后来又通过证明自由的，自由的线性图式的等价性在多项式时间内是可决定的来加强这一点。这项工作代表了图式理论领域在中断约三十年后的重大进展。有强有力的证据表明，强加这种额外但自然的线性条件（或部分线性形式）将导致图式理论中进一步的可决性结果。作者希望他们的新结果将导致对程序图式理论中大量工作的重新评估，并进一步研究其在现代框架中的应用。这是本研究计划的主要动机之一。许多静态程序转换和分析，实际上所有使用数据和控制流的分析，都发生在抽象的模式级别上。这意味着对程序的分析将对其模式等价类中的所有程序产生相同的结果。这项研究的一个重要部分将是进一步调查模式理论的大量工作在多大程度上与切片相关，特别是与其他形式的静态程序分析和转换相关。

Program schemas are a notation for representing an infinite set of computer programs all with the same syntactic structure. If a property of a program schema can be proved, this property will hold for every program in the infinite set of programs represented by the schema. Reasoning with schemas is, thus, a very powerful mechanism.As a result of their work in program slicing, the proposers found that program schema theory enabled them to precisely express the problems that they were tackling; namely the existence of statement minimal slicing algorithms at the `dataflow' level of abstraction. For such problems a class of schema which they 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 schemas. They 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 after a hiatus of about thirty years. 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.The proposers hope that their 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. This is one of the main motivations of this research proposal.Much static program transformation and analysis, in fact all analysis which uses data and control flow, takes place at the schema level of abstraction. This means the analysis of a program will produce the same results for all programs in its schema equivalence class. An important part of this research will be to investigate further the extent to which the large body of work on the theory of schemas is relevant to slicing in particular and to other forms of static program analysis and transformation in general.