压缩路径序与重写系统的结构测度

结构测度对于判别重写系统的合流性是极为重要的,本文着重研究结构测度的有效定义方法。本文引入了压缩路径序概念,只要给出符号集上了拟序关系和相对该拟序关系协调的压缩结构,即可方便地生成良拟序的压缩路径序,同时可以有效地检查这一路径压缩序是否为给定重写系统的结构测度,本文提出的方法有力地支持了在非终止条件下对重写系统合流性的判别。

重写系统中的显式归纳方法

提出了重写系统中的显式归纳方法，设计了一个新的归纳定理证明系统。实例表明，显式归纳方法要比无归纳的归纳方法来得简单直观。

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

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

项重写系统弱基终止性的归纳证明

This paper proposes a novel method for proving weakly ground termination in a restricted domain of a term rewriting system based on structural and cover set induction. For this prupose,we introduce the concepts of base set and set of ground terms defined recursively over base sets,which plays a crucial role in the inductive method. The method can be used for non-terminating,non-confluent and/or non-linear term rewriting systems,and have application in inductive equivalence testing and program verification.

重写系统中解决发散现象的扩充技术

本文介绍和提出用于解决发散问题的各种基于保守扩充技术的方法。我们特别地用实例证明了这几种新方法可以对带AC算子的重写系统进行归纳完备化。

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

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

基于改进的网重写系统的Petri网逻辑控制器的自重构方法

提出一种基于改进的网重写系统的可重构制造系统的Petri网模型的自重构方法。通过改进,克服了网重写系统的若干固有缺陷,提出了Petri网逻辑控制器的自重构方法,这种方法能保证重构中逻辑控制器的正确性,避免复杂的数学分析验证。通过可重构制造单元的实例演示了该方法,并验证了其有效性。

左线性重写系统的合流性

讨论左线性的项重写系统的合流性,通过引入重写系统的局部归约序,可证明对于具有局部归约序的左线性重写系统R,R具有合流性,当且仅当,对于任意M→R P和M→R Q,P和Q在M下相对局部归约序子连通。

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

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

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

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

字符串重写系统的改进算法及其在花型准备系统中的应用

介绍了字符串重写系统的基本原理及其改进算法——模板重写算法.给出了模板重写算法的操作步骤,并详细讨论此算法在花型准备系统中的具体应用.

重写系统的模块分解

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

利用重写系统研究缺省逻辑

本文在布尔环重写系统中研究了缺省逻辑．一个缺省理论等价于一个布尔环方程组．本文还分析了命题缺省理论外延的结构，证明了一个缺省理论的外延的模型集合就是对应的布尔环方程组的极大缺省解，从而为确定缺省理论的外延提供了一种简便实用的方法．

有趣的重写系统

本文通过字符串的重写过程，模拟冯·诺依曼架构计算机的工作流程。需要的工具，可以从一支笔、一张纸开始。

“活”过来的经典计算机——马尔科夫重写系统

如果有一台机器，它所做的事情十分单一，就是把一个符号串中的一些字符替换成另外一些，反复替换后，这台机器就能实现通用计算。换句话说，人们给通用计算机编写的程序，都可以移植到这台简单的字符替换机器上。这听上去让人惊讶，但基于马尔科夫算法(Markovalgorithm)的字符串重写系统（StringRewritingSystem）证明，这不仅在理论上可行，而且若真的想用这个系统来编写程序实现特定任务，也不是特别难的事情。这个系统在理论计算科学的发展历史中具有很重要的意义。

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

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

基于项重写系统的联锁系统模型检测方法研究

模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。

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

项重写系统是一种简洁通用的计算模型，在许多领域中有着重要的应用．但是，在一些应用中，它不能很好地解决问题，为此，文中提出了一种新的项重写计算模型——依赖项重写系统，并给出了它在程序设计语言中的应用．直观上说，依赖项重写系统是重写规则之间存在着关于函数符号的依赖关系的项重写系统．这一模型具有较好的性质（例如，合流性、终止性等）和很强的表达能力．应用它，能够解决某些计算不终止问题，并有利于并行性的开发．

项重写系统和自由幺半群

项重写系统起源于数理逻辑,是理论计算机科学的重要组成部分.关于项重写系统的一个主要问题是描述一个重写系统是否具有汇合或终止等基本性质.本文首先将一个项重写系统与自由幺半群上的二元关系联系起来.然后,基于自由幺半群上的项重写系统,刻画了收敛项重写系统与自由幺半群的商截面之间的关系.作为应用,分别给出了由三个元素生成的Platic幺半群和中国幺半群的截面.