项重写的图实现

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

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.     

半结构化查询重写的MiniCon算法

研究了基于半结构化数据查询语言TSL(tree specification language)的查询重写问题.提出了一种半结构化查询重写算法,解决了在给定一个半结构化查询和一组半结构化视图的情况下,找到最大被包含重写的问题.算法借用了可伸缩的关系查询重写的MiniCon算法的思想,解决了半结构化数据模型之下查询重写的一些新问题(如标识符依赖、集合值变量映射等).证明了算法的正确性.     

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.     

模型转换的重写逻辑构架研究

规则式的模型转换技术在模型驱动构架的模型转换实施中占有重要地位,但目前诸实施对于转换规则的定义存在多种解释、转换的协调方面、终止性和一致性等数学属性缺乏支持。该文提出一种Maude重写逻辑基础的构架(RLBA)以实施模型转换,通过产生式规范、多方法风格的重写规则集设计、OC(对象配置)和OM(对象消息)重写规则分类等技术并结合模型检查工具,为自动产生元模型和模型的面向对象可执行代数规范、转换规则的严格形式化定义、转换协调方面的刻画、终止性和一致性等的验证提供支持。     

非一致性数据库的概率查询重写

结合概率数据库技术，以元组匹配所产生的聚类为基础，提出了一种新的基于聚类的非一致性数据的概率方法。基于可信聚类，给出了基本的查询重写技术，在有聚集的查询中，考虑了合适的元组概率、区间值、期望值。在不进行程序预处理的情况下，“重写”能被商业数据库系统有效地优化和执行，采用不一致性数据的区分度和数据库大小去理解其适应性，并使用了TPC-H基准的数据和查询。实验显示了该方法的有效性。     

一种基于模重写系统的攻击者推理方法

为了解决安全协议验证中攻击者模等式理论推理的可操作性问题,提出并设计了一种基于模重写系统的攻击者推理方法。该方法建立在一个反映两种密码原语代数特性的联合理论实例之上,由一组定向的重写规则和非定向的等式构成,前者进一步转化为项重写系统TRS(Term Rewriting System),而后者则转化为有限等价类理论,通过定义项间的模重写关系,使二者构成一个可以反映攻击者针对联合理论代数项操作能力的模重写系统。实例分析表明,该模型为攻击者模等式推理规则赋予了明确的操作语义,可以使攻击者达到对安全协议代数项规约、推理的目的。     

Hierarchical Nominal Terms and Their Theory of Rewriting

Nominal rewriting introduced a novel method of specifying rewriting on syntax-with-binding. We extend this treatment of rewriting with hierarchy of variables representing increasingly 'meta-level' variables, e.g. in hierarchical nominal term rewriting the meta-level unknowns (representing unknown terms) in a rewrite rule can be 'folded into' the syntax itself (and rewritten). To the extent that rewriting is a mathematical meta-framework for logic and computation, and nominal rewriting is a framework with native support for binders, hierarchical nominal term rewriting is a meta-to-the-omega level framework for logic and computation with binders.     

基于XPath的XML查询重写算法

XML安全视图和查询重写是实现访问控制的关键技术。研究基于XML递归安全视图的查询重写问题,提出一种基于XPath查询语言、能处理递归视图的查询重写算法,避免了视图的物化和保存。该算法具有较高通用性,实验结果验证了其有效性。     

Web安全测试中URL参数重写检测框架

Web站点中URL参数重写会对Web安全测试的准确性造成较大影响。针对该问题,设计URL参数重写检测框架,构造多个测试URL并提交请求,通过基于3种差异分析方法的随机URL取样验证策略,识别出URL中的伪路径,从而提取重写规则、并实现URL参数重写检测。应用C#语言实现的URL参数重写检测爬虫验证了该框架的有效性。     

Strategic Rewriting

This is a position paper preparing the round table organized during the 4th International Workshop on Reduction Strategies in Rewriting and Programming. I sketch what I believe to be important challenges of strategic rewriting.     

Structures for Abstract Rewriting

When rewriting is used to generate convergent and complete rewrite systems in order to answer the validity problem for some theories, all the rewriting theories rely on a same set of notions, properties, and methods. Rewriting techniques have been used mainly to answer the validity problem of equational theories, that is, to compute congruences. Recently, however, they have been extended in order to be applied to other algebraic structures such as preorders and orders. In this paper, we investigate an abstract form of rewriting, by following the paradigm of logical-system independency. To achieve this purpose, we provide a few simple conditions (or axioms) under which rewriting (and then the set of classical properties and methods) can be modeled, understood, studied, proven, and generalized. This enables us to extend rewriting techniques to other algebraic structures than congruences and preorders such as congruences closed under monotonicity and modus ponens. We introduce convergent rewrite systems that enable one to describe deduction procedures for their corresponding theory, and we propose a Knuth-Bendix–style completion procedure in this abstract framework.     

Active XML文档重写机制的研究

Active XML定义为一种动态的XML,主要思想是在XML中嵌入Web Services调用.当Active XML文档用作表示和交换时,通过调用相应的Web Services ,用返回结果取代Active XML文档中的Web Services调用或者作为子节点插入,这个过程称为重写.针对应用要求不同的场景,总结了两类重写方式无模重写,即在重写时不受Schema约束;有模重写,重写时要符合预定的Schema.在对无模方式做了简单讨论后,对有模方式的算法做了详细讨论,为拓展Active XML技术的应用领域提供了技术支持.     

基于重写技术的程序开发与验证

完整地介绍了一个基于重写技术的程序开发和验证系统,重点展示验证子系统的理论、方法 和技术.验证子系统使得系统能自动证明程序和规范中的优化规则及测试等式,从而进一步保 证程序开发过程的正确性.验证子系统所采用的主要技术是以成批证明方法和证据测试集为 特色的重写归纳方法.     

Rewriting queries using views with access patterns under integrity constraints

We study the problem of rewriting queries using views in the presence of access patterns, integrity constraints, disjunction and negation. We provide asymptotically optimal algorithms for (1) finding minimally containing and (2) maximally contained rewritings respecting the access patterns (which we call executable) and for (3) deciding whether an exact executable rewriting exists. We show that rewriting queries using views in this case reduces (a) to rewriting queries with access patterns and constraints without views and also (b) to rewriting queries using views under constraints without access patterns. We show how to solve (a) directly and how to reduce (b) to rewriting queries under constraints only (semantic optimization). These reductions provide two separate routes to a unified solution for problems 1, 2 and 3 based on an extension of the relational chase theory to queries and constraints with disjunction and negation. We also handle equality and arithmetic comparisons. We also show that in an information integration setting, maximally contained rewritings are given by the certain answers (under the usual semantics) for a set of constraints derived from the binding patterns. That is, except for defining the appropriate constraints, binding patterns do not need special treatment. Finally, we show that if there is an exact executable rewriting, there is an executable rewriting which is a union of conjunctive queries with negation.     

Rewriting systems with limited distance permitting context

By restricting the permitting context symbols in a rewriting system to be within a specified distance from the symbol to be replaced, we strictly increase the generative power above that of rewriting systems where the context symbols can appear within arbitrary distances from the symbol to be replaced.     

一种改进的基于约束关系的XML查询重写算法研究

查询重写是解决数据集成、查询优化和物理层数据独立性等问题的关键技术.以往工作主要集中在关系数据模型方面.最近Michigan大学Timber研究小组提出一种全新的基于约束的XML查询重写算法.然而,该算法未考虑存在内定谓词情况下的重写问题,应用范围受到一定限制.在原算法的重写思想基础上,提出了一种基于约束的XML查询重写的改进算法.通过引入映射规则中的约束条件,消除阻碍重写的Skolem函数,从而解决内定谓词问题,增大原算法的应用范围.证明了改进算法的正确性.性能分析和测试结果表明,改进算法并不增加实质性的性能代价.     

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.     

一种扩充语义的实视图重写查询技术

分组聚集查询已成为数据仓库领域研究的核心问题之一,实视图是提高分组聚集查询性能的有效手段。利用维属性间的层次关系,对一般意义上的实视图重写查询进行了扩展,讨论了单一视图重写查询的限制条件,并给出重写方法,在此基础上,提出了一种利用多个实视图重写查询的优化选择算法,并通过实验表明,该算法进一步提高了分组聚集查询效率。     

From Chemical Rules to Term Rewriting

In this paper, rule-based programming is explored in the field of automated generation of chemical reaction mechanisms. We explore a class of graphs and a graph rewriting relation where vertices are preserved and only edges are changed. We show how to represent cyclic labeled graphs by decorated labeled trees or forests, then how to transform trees into terms. A graph rewriting relation is defined, then simulated by a tree rewriting relation, which can be in turn simulated by a rewriting relation on equivalence classes of terms. As a consequence, this kind of graph rewriting can be implemented using term rewriting. This study is motivated by the design of the GasEl system for the generation of kinetics reactions mechanisms. In GasEl, chemical reactions correspond to graph rewrite rules and are implemented by conditional rewriting rules in ELAN. The control of their application is done through the ELAN strategy language.