共查询到19条相似文献,搜索用时 62 毫秒
1.
Knuth-Bendix完备过程不终止的起因研究得很少,本文研究引起不终止的重写规则的结构性质,提出了相容交叉规则对的概念,推广了文献6的结论,并提出了为构造系统检验该过程是否不终止的方法。 相似文献
2.
本文介绍和提出用于解决发散问题的各种基于保守扩充技术的方法.我们特别地用实例证明了这几种新方法可以对带AC算子的重写系统进行归纳完备化. 相似文献
3.
本文考虑如何设计高效率(即重写步数较少的)重写型程序。文中以计算Fibonacci数列的程序为例.比较具有相同功能的重写型程序,展示编写高效率重写型程序的可能性。介绍利用动态项重写计算编写高效率重写型程序的直观、简洁的方法。其中.动态项重写计算是项重写系统的元计算模型,其计算同样基于项重写。 相似文献
4.
项重写系统的并行归约可以提高归约的效率,在无共享内存的Transputer网络上实现时要考虑任务的分配,项的拼装,归约任务的控制等问题,其中怎么样减少机间的机内进程的通信慢提高系统效果的关键。本文从控制方式角度讨论在不同拓扑结构的Transputer网络上实现项重写系统的方案,重点介绍基于树形结构下的控制方法,进程安排和通讯形式。 相似文献
5.
6.
7.
项重写系统等价性的归纳证明 总被引:1,自引:1,他引:0
尽管学者们在计算机软件理论及相关数学理论方面做出了不懈的努力,但伴随着计算机硬件的高速发展而来的软件危机却日益严峻,其原因复杂多样。其中,主要原因之一是缺乏程序验证的方法和工具。程序设计的主要步骤有:描述问题、设计程序、实现程序及测试程序。需要注意的是,这里是测试程序的正确性而非证明程序的正确性,这样程序的正确性就不能从根 相似文献
8.
项重写系统弱基终止性的归纳证明 总被引:3,自引:2,他引:1
1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。例如,下面的R是一个由五个重写规则组成的、定义用({0,s})表示的自然数集N上的两倍函数d(x)=2×n:N→N的项重写系统: 相似文献
9.
模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。 相似文献
10.
11.
Miki Hermann 《Formal Aspects of Computing》1990,2(1):207-225
This article introduces a generalisation of the crossed rule approach to the detection of Knuth-Bendix completion procedure divergence. It introduces closure chains, which are special rule closures constructed by means of particular substitution operations and operators, as a suitable formalism for progress in this direction. Supporting substitution algebra is developed first, followed by considerations concerning rule closures in general, concluding with an investigation of closure chain properties. Issues concerning the narrowing process are not discussed here. 相似文献
12.
Yves Metivier 《Information Processing Letters》1983,16(1):31-34
We show that in a free F-algebra endowed with a strict order we can associate with a complete rewriting system in the sense of Knuth-Bendix an equivalent proper (minimal) complete system. Furthermore, if the complete system is compatible with a strict order, then the equivalent proper complete system is unique. 相似文献
13.
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. 相似文献
14.
通用远程过程调用的设计与实现 总被引:1,自引:0,他引:1
在分布式计算系统中,远程过程调用RPC是种流行的进程间通信机制。RPC简单灵活,且功能较强。上前大多数RPC机制是同步的,严重地影响了分布式应用的并行性。我们设计和实现了一个通用的RPC。本文讨论了设计的要点和方法,并对通用RPC的实现作了介绍。 相似文献
15.
For many years, all existing completeness results for Knuth–Bendixcompletion and ordered paramodulation required the term ordering to be well-founded, monotonic and total(izable) on ground terms.Then, it was shown that well-foundedness and the subterm propertywere enough for ensuring completeness of ordered paramodulation.Here we show that the subterm property is not necessary either.By using a new restricted form of rewriting, we obtain a completenessproof of ordered paramodulation for Horn clauses with equality,where well-foundedness of the ordering suffices. Apart fromthe theoretical significance of this result, some potentialapplications motivating the interest of dropping the subtermproperty are given. The proof of the results included in thisarticle, being still technical in some parts, is pretty muchshorter and easier to read than the one we have in the preliminaryversion of this work presented at the CADE, 2002 conference(Bofill, and Rubio, 2002, CADE, Vol. 2392 of LNAI, pp. 456–470). 相似文献
16.
David A. Plaisted 《Information Processing Letters》1985,20(2):61-64
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. 相似文献
17.
Chen Yiyun 《计算机科学技术学报》1995,10(3):281-284
Further research about nonterminating rewritings is introduced.First,the previous definition of head boundedness is modified to exclude non-fair reduction sequences.A sufficient condition is then given to determine head boundedness of term rewriting systems.The condition is then developed to a method to determine head boundedness of constructor systems. 相似文献
18.
19.
有关远程过程调用的几个重要问题的讨论 总被引:1,自引:0,他引:1
远程过程调用作为构造分布式系统的一个重要工具已经得到了广泛的应用,本文详细讨论了有关RPC的七个重要问题:网络传输协议、类型一致性、错误处理、孤儿问题、效率问题、性能问题、互操作性。 相似文献