Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families
Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families
复制标题
根据递归构造图族问题的谓词演算描述自动生成线性时间算法
作者：
R. Borie
本文描述了一个谓词演算，在图的问题可以表示。任何具有这样一个表达式的问题都可以在任何递归构造的图上以线性时间求解，只要知道它的分解树。此外，线性时间算法可以从表达式自动生成，因为我们的所有定理都是构造性证明的。演算是建立在一个简短的基本谓词列表上的，这些谓词又由基本逻辑运算组合而成。这个框架是丰富的，足以包括绝大多数已知的线性时间可解问题。我们通过利用Bernet等人的框架，独立于Courcelle [11]，[12]的类似结果，得到了这些结果。我们相信我们的形式主义是更实用的程序员谁将实现自动生成机制，更容易理解的许多理论家。
This paper describes a predicate calculus in which graph problems can be expressed. Any problem possessing such an expression can be solved in linear time on any recursively constructed graph, once its decomposition tree is known. Moreover, the linear-time algorithm can be generatedautomatically from the expression, because all our theorems are proved constructively. The calculus is founded upon a short list of particularly primitive predicates, which in turn are combined by fundamental logical operations. This framework is rich enough to include the vast majority of known linear-time solvable problems.We have obtained these results independently of similar results by Courcelle [11], [12], through utilization of the framework of Bernet al. [6]. We believe our formalism is more practical for programmers who would implement the automatic generation machinery, and more readily understood by many theorists.