半正则重写系统及其合流性

本文着重研究重写系统的合流性,通过引入符号测度的概念,本文定义了半正则重写系统,并证明了半正则重写系统的合流性。     

模式化简序与重写系统的终止性

本文引入了模式化简序的概念,并给出了基于模式化简序的重写系统终止性判别方法。本文还着重研究了模式递归路径序,同时定义了重写规则相对模式集的上下扩张概念,以此给出了用模式递归路径序判别终止性的有效方法,原有的递归路径序是模式递归路径序的一个特例。     

基于视图的正则路径查询重写

正则路径查询的重写是实现XML查询重写优化的基础。通过比较正则路径视图和正则路径查询的结构信息,分析了两者之间进行映射应满足的条件,描述了正则路径视图到正则路径查询的映射和基于有穷自动机的映射过滤算法,并从理论上阐明了两个算法的重写等价性。借助于此两个算法,能够极大地减少需要求解的映射数目和提高正则路径查询处理的效率。     

动态项重写计算

1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。它的计算基于代入、匹配和替换,除具有方向性外,与等式推导一致。虽然项重写系统形式简单、计算单纯,但它同时又具有与λ计算及图灵机相同的计算能力。正是它的简洁性及计算能力使它受到广泛的研究和应用:项重写系统为抽象数据类型提供类型、为函数型语言提供操作语义、为定理自动证明提供推理工具。对于项重写系统本身也有大量的研究:如合流性、终止性、等价性等。     

项重写的图实现

图重写能够有效地实现项重写。文章从项重写的图实现的角度出发，研究了图重写模拟项重写的正确性和完备性：在无环出现的情况下，图重写对一切项重写下正确；在无环出现的条件下，图重写对左线性合流的项重写是完备的。     

论绘图仪用汉字库的数据特征及存贮结构

本文提出了绘图仪用汉字序的数据特征及其存贮结构, 并且进一步提出了关于这种汉字序的压缩存贮方法和笔划路径优化方法, 从而使得这种汉字库更加易于推广应用。目前, 本文所提出的汉字序已经在国内各领域得到很好的应用。     

基于重写方法的程序开发系统的设计和实现

本文介绍了一个基于重写方法的程序开发系统的设计和实现。该系统使用代数规范说明语言和扩展的函数式语言合成而形成的混合语言进行程序设计。系统将代数规范转换为合流的重写系统，并以平行最外方法辅以必要归约进行计算。该文详细介绍了系统的原理和实现技术，并以一些实例说明了系统的特点。     

XML的结构完整性约束推理

为了有效地优化XML路径表达式查询,给出了一个XML结构完整性约束体系,这个体系全面描述了XML文档中节点或路径之间的结构关系,包括必需性包含、排他性包含、路径蕴涵、路径互斥和路径同现.在此基础上研究了XML结构完整性约束的逻辑蕴涵和一致性问题.文章首先采用约束重写技术将各种约束改写为路径蕴涵约束;然后给出了一组路径蕴涵的推理规则;最后以路径蕴涵闭包为工具证明了推理规则的完备性并给出了XML结构完整性约束的一致性判断方法.     

利用模糊识别算法分析冠状动脉造影图像中的血管结构

定性与定量地描述冠状动脉血管,很大程度依赖于造影图像中的血管结构识别结果.对此,该文提出了一种多特征模糊识别算法判别血管结构.实现过程中,首先通过图像预处理获得血管初始特征,然后利用一圆周探测器沿血管路径扫描并获取多种局部测度;在定义各种局部测度的多特征模糊子集及其隶属度函数之后,通过构造模糊识别算子准确地判别血管的端、段、分支和交叉结构.该方法在仿真血管模型和多套实际冠状动脉造影图像上获得了较好的效果,对实际图像的结构识别平均正确率达到92.60%.     

序粒度标记结构及其粗糙近似

粒计算是知识表示和数据挖掘的一个重要方法.它模拟人类思考模式,以粒为基本计算单位,以处理大规模复杂数据和信息等建立有效的计算模型为目标.针对具有多粒度标记的序信息系统的知识获取问题,提出了基于序粒度标记结构的粗糙近似.首先,介绍了序标记结构的概念,并在序标记结构的对象集中定义了一个优势关系,同时给出了由优势关系导出的优势标记块,并进一步定义了基于优势关系的集合的序下近似与序上近似和序标记下近似与序标记上近似的概念,给出了近似算子的一些性质.证明了由序标记结构导出的集合的下近似质量与上近似质量是一对对偶的必然性测度与可能性测度.最后,定义了多粒度序标记结构的概念,并讨论了多粒度序标记结构中不同粒度下近似集之间的关系.     

On the recursive decomposition ordering with lexicographical status and other related orderings

This paper studies three orderings, useful in theorem proving, especially for proving termination of term rewriting systems: the recursive decomposition ordering with status, the recursive path ordering with status and the closure ordering. It proves the transitivity of the recursive path ordering, the strict inclusion of the recursive path ordering in the recursive decomposition ordering, the totality of the recursive path ordering — therefore of the recursive decomposition ordering — the strict inclusion of the recursive decomposition ordering in the closure ordering and the stability of the closure ordering by instantiation.Part of this work was done while the author was visiting the Institute for New Generation Computer Technology, Tokyo, Japan.     

Simplification orderings: Putting them to the test

Various methods for proving the termination of term rewriting systems have been suggested. Most of them are based on the notion of a simplification ordering. In this paper, a collection of well-known simplification orderings will be briefly presented including path orderings and decomposition orderings. A satisfactory application to examples often found in practice is an essential requirement concerning such orderings. We describe a detailed empirical study of their time complexities with respect to comparable pairs of terms.This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt).     

Monomial Orderings,Rewriting Systems,and Gröbner Bases for the Commutator Ideal of a Free Algebra

In this paper we consider a free associative algebra on three generators over an arbitrary fieldK. Given a term ordering on the commutative polynomial ring on three variables overK, we construct uncountably many liftings of this term ordering to a monomial ordering on the free associative algebra. These monomial orderings are total well orderings on the set of monomials, resulting in a set of normal forms. Then we show that the commutator ideal has an infinite reduced Gröbner basis with respect to these monomial orderings, and all initial ideals are distinct. Hence, the commutator ideal has at least uncountably many distinct reduced Gröbner bases. A Gröbner basis of the commutator ideal corresponds to a complete rewriting system for the free commutative monoid on three generators; our result also shows that this monoid has at least uncountably many distinct minimal complete rewriting systems.The monomial orderings we use are not compatible with multiplication, but are sufficient to solve the ideal membership problem for a specific ideal, in this case the commutator ideal. We propose that it is fruitful to consider such, more general, monomial orderings in non-commutative Gröbner basis theory.     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

Decidability for Left-Linear Growing Term Rewriting Systems

A term rewriting system is called growing if each variable occurring on both the left-hand side and the right-hand side of a rewrite rule occurs at depth zero or one in the left-hand side. Jacquemard showed that the reachability and the sequentiality of linear (i.e., left-right-linear) growing term rewriting systems are decidable. In this paper we show that Jacquemard's result can be extended to left-linear growing rewriting systems that may have right-nonlinear rewrite rules. This implies that the reachability and the joinability of some class of right-linear term rewriting systems are decidable, which improves the results for right-ground term rewriting systems by Oyamaguchi. Our result extends the class of left-linear term rewriting systems having a decidable call-by-need normalizing strategy. Moreover, we prove that the termination property is decidable for almost orthogonal growing term rewriting systems.     

The undecidability of self-embedding for term rewriting systems

The self-embedding property of term rewriting systems is closely related to the uniform termination property, since a nonself-embedding term rewriting system is uniform terminating. The self-embedding property is shown to be undecidable and partially decidable. It follows that the nonself-embedding property is not partially decidable. This is true even for globally finite term rewriting systems. The same construction gives an easy alternate proof that uniform termination is undecidable in general and also for globally finite term rewriting systems. Also, the looping property is shown to be undecidable in the same way.     

Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions

The paper presents three formal proving methods for generalized weakly ground terminating property, i.e., weakly terminating property in a restricted domain of a term rewriting system, one with structural induction, one with cover-set induction, and the third without induction, and describes their mechanization based on a meta-computation model for term rewriting systems-dynamic term rewriting calculus. The methods can be applied to non-terminating, non-confluent and/or non-left-linear term rewriting systems. They can do "forward proving" by applying propositions in the proof, as well as "backward proving" by discovering lemmas during the proof.