项重写系统等价性的归纳证明

尽管学者们在计算机软件理论及相关数学理论方面做出了不懈的努力,但伴随着计算机硬件的高速发展而来的软件危机却日益严峻,其原因复杂多样。其中,主要原因之一是缺乏程序验证的方法和工具。程序设计的主要步骤有:描述问题、设计程序、实现程序及测试程序。需要注意的是,这里是测试程序的正确性而非证明程序的正确性,这样程序的正确性就不能从根     

基于重写的成批归纳证明技术

1 引言 归纳法是刻划软硬件行为和性质的一种重要方法,归纳证明的自动化始终是一个研究热点.近二十年来,涌现出了大批证明方法和实验系统.这些成果大致可分为两类:第一类方法使用项结构上的显式归纳论证,其典型工具是1979年由Boyer和Moore提出的NQTHM证明器[1].     

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

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

依赖项重写系统及其在程序设计语言中的应用

面重写系统是一种简洁通用的计算模型，在许多领域中有着重要的应用。     

项重写系统的并行实现方案

项重写系统的并行归约可以提高归约的效率，在无共享内存的Ｔｒａｎｓｐｕｔｅｒ网络上实现时要考虑任务的分配，项的拼装，归约任务的控制等问题，其中怎么样减少机间的机内进程的通信慢提高系统效果的关键。本文从控制方式角度讨论在不同拓扑结构的Ｔｒａｎｓｐｕｔｅｒ网络上实现项重写系统的方案，重点介绍基于树形结构下的控制方法，进程安排和通讯形式。     

重写系统的模块分解

Ｍｉｄｄｅｌｄｏｒｐ和Ｔｏｙａｍａ证明，强加构造原则到项重写系统可获得完备概念的模块性，并且系统分解成的各部分间可共亨函数符号和重量写规则。本文推广他们的结论，当构造性的项重写系统引用定义在其它系统中的函数符号时，完备概念的模块性仍保持。该结论对代数规范和基于项重写的编程语言等方面是很有意义的。     

项重写的图实现

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

基于重写技术的自动定理证明

重写技术是处理等式理论的一种有效方法,它已成功地应用到带等词的一阶谓词逻辑中定理的自动证明。本文介绍基于重写的定理证明方法的基本思想,以及几种具体的证明技术,最后将这类方法与经典的归结证明方法加以比较。     

基于良序集方法的程序终止性证明

在介绍程序正确性的定义和良序集的概念基础上,对良序集证明程序终止性思路和步骤进行了分析,利用实例来证明程序的终止性。     

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

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

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.     

Matrix Interpretations for Proving Termination of Term Rewriting

We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows us to prove termination and relative termination. A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.     

Proving Termination by Dependency Pairs and Inductive Theorem Proving

Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.     

Towards a Systematic Method for Proving Termination of Graph Transformation Systems

We describe a method for proving the termination of graph transformation systems. The method is based on the fact that infinite reductions must include infinite ‘creation chains’, that is chains of edges in different graphs of the reduction sequence, such that each edge is involved in creating the next edge. In our approach, the length of such creation chains is recorded by associating with each edge label a creation depth, which denotes the minimal length of a creation chain from an edge in the initial graph to that edge. We develop an algorithm which can prove the absence of such infinite chains (and therefore termination), analyse problems of the approach and propose possible solutions.     

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.     

Termination Proofs for String Rewriting Systems via Inverse Match-Bounds

Annotating a letter by a number, one can record information about its history during a rewrite derivation. In each rewrite step, numbers in the reduct are updated depending on the redex numbering. A string rewriting system is called match-bounded if there is a global upper bound to these numbers. Match-boundedness is known to be a strong sufficient criterion for both termination and preservation of regular languages. We show that the string rewriting systems whose inverse (left and right hand sides exchanged) is match-bounded, also have exceptional properties, but slightly different ones. Inverse match-bounded systems need not terminate; they effectively preserve context-free languages; their sets of normalizable strings and their sets of immortal strings are effectively regular. These languages can be used to decide the normalization, the uniform normalization, the termination and the uniform termination problem for inverse match-bounded systems. We also prove that the termination problem is decidable in linear time, and that a certain strong reachability problem is decidable, thereby solving two open problems of McNaughton’s. Like match-bounds, inverse match-bounds entail linear derivational complexity on the set of terminating strings.     

Reachability in Conditional Term Rewriting Systems

In this paper, we study the reachability problem for conditional term rewriting systems. Given two ground terms s and t, our practical aim is to prove s _R^* t for some join conditional term rewriting system R (possibly not terminating and not confluent). The proof method we propose relies on an over approximation of reachable terms for unrestricted join conditional term rewriting systems. This approximation is computed using an extension of the tree automata completion algorithm to the conditional case.     

Transformation for Refining Unraveled Conditional Term Rewriting Systems

Unravelings, transformations from conditional term rewriting systems (CTRSs, for short) into unconditional term rewriting systems, are valuable for analyzing properties of CTRSs. In order to completely simulate rewrite sequences of CTRSs, the restriction by a particular context-sensitive and membership condition that is determined by extra function symbols introduced due to the unravelings, must be imposed on the rewrite relations of the unraveled CTRSs. In this paper, in order to weaken the context-sensitive and membership condition, we propose a transformation applied to the unraveled CTRSs, that reduces the number of the extra symbols. In the transformation, updating the context-sensitive condition properly, we remove the extra symbols that satisfy a certain condition. If the transformation succeeds in removing all of the extra symbols, we obtain the TRSs that are computationally equivalent with the original CTRSs.     

Reachability Analysis over Term Rewriting Systems

This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by . An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.