首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到19条相似文献,搜索用时 125 毫秒
1.
陈意云 《计算机学报》1994,17(3):161-167
Middeldorp和Toyama证明,强加构造原则到项重写系统可获得完备概念的模块性,并且系统分解成的各部分间可共亨函数符号和重量写规则。本文推广他们的结论,当构造性的项重写系统引用定义在其它系统中的函数符号时,完备概念的模块性仍保持。该结论对代数规范和基于项重写的编程语言等方面是很有意义的。  相似文献   

2.
李娜  谢冬青 《计算机科学》2006,33(8):271-274
基于项重写的安全风险分析的抽象规约模型在代数签名的基础上直接得到结果,没有提供相关攻击步骤明确描述,没有提供决策和攻击之间关系的统一视图,容易导致威胁的传播。为此,本文首先将图重写方案引入模型中,证明了引入图重写规则以后的风险分析系统仍然是终止的。然后利用图重写规则,提出了一种可以获得更优决策集合的方法,在改进的求带权二分图最小覆盖的方法的基础上,获得了一种具有相同时间复杂度和更高代价利益比的方法。整个模型高效、易于管理。  相似文献   

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

4.
归纳法推理中的项重写策略   总被引:2,自引:2,他引:0  
李卫华  张黔 《软件学报》1996,7(A00):565-571
本文介绍归纳法推理系统中的项重写策略,该策略根据不同的待重写项term,分别运用公理、重写引理、函数定义、项重写规则等重写项term,以期得到一个更接近推理目标的已重写项,这一策略已在微机上用编译LISP语言实现。  相似文献   

5.
李卫华  张黔  韩波 《软件学报》1996,7(Z1):565-571
本文介绍归纳法推理系统中的项重写策略.该策略根据不同的待重写项term,分别运用公理、重写引理、函数定义、项重写规则等重写项term,以期得到一个更接近推理目标的巳重写项.这一策略已在微机上用编译LlsP语言实现.  相似文献   

6.
嵌入一致图语法的依赖图   总被引:2,自引:0,他引:2       下载免费PDF全文
李国东  张德富 《软件学报》2004,15(7):956-968
图语法将字符串上的形式文法扩充为图上的形式文法,提供一种能够使用精确的数学方法来模拟图变换的机制.提出了几种新的基于一致图语法的方法来表示控制流图、数据流图、控制数据流图、二分图和超图,并说明如何通过图重写来自动生成依赖图并挖掘并行性,从而协助并行编译器和并行语言的设计和实现.  相似文献   

7.
本文详细讨论了重写模块的设计思想与实现技术,并讨论了利用执行引擎特点引入的一组基于等价谓调的简单语句直写规则.测试结果表明,增加重写模块的查询优化器能显著提高系统的查询效率.  相似文献   

8.
规则路径查询,其长度是任意的,这就意味着对数据库的任意多次访问,这样的代价是很昂贵的。我们采用视图重写技术,通过对某些经常使用的路径查询定义视图。从而减少了对某些高频使用的路径查询的重复搜索,最终提高了查询效率。我们的视图不但可以对路径查询进行重写,而且还可以对树查询进行混合重写。我们设计了一个使用动态规划策略实现的视图重写算法。  相似文献   

9.
项重写系统是一种描述不确定计算的计算模型。近十年来,重写技术在计算机科学的许多重要领域得到广泛应用,表现出作为知识信息处理系统的良好性质,引起了人们对重写技术的重视,本文介绍重写技术的主要内容,着重强调了完全过程的思想。同时说明了目前重写技术几个活跃的研究课题。本文还介绍了重写技术在自动定理证明、逻辑程序设计和软件开发中的应用。  相似文献   

10.
用最小自由能法预测RNA二级结构是NP困难问题,其根本原因是假结的存在。近几年的预测算法都针具有一定结构特征的假结寻找多项式时间算法进行预测。论文针对RNA二级结构图提出一种图语法,该语法由初始结构图集和重写规则集构成,用重写规则在初始结构图上的不断重写得到的结构图都是该语法的语言。分析了5个主流RNA二级结构预测算法的目标集,给出它们的图语法,使得目标集的结构特征一目了然,目标集间的真包含关系也通过图语法直观地体现出来。  相似文献   

11.
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.  相似文献   

12.
nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.  相似文献   

13.
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.  相似文献   

14.
Multi-algebras allow to model nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results.We propose a simple inequational deduction system, based on term graphs, for inferring inclusions of derived relations in a multi-algebra, and we show that term graph rewriting provides a sound and complete implementation of it.  相似文献   

15.
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.  相似文献   

16.
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.  相似文献   

17.
Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite sequences. Proving termination of CSR has been recently recognized as an interesting problem with several applications in the fields of term rewriting and programming languages. Several methods have been developed for proving termination of CSR. Specifically, a number of transformations that permit treating this problem as a standard termination problem have been described. The main goal of this paper is to contribute to a better comprehension and practical use of transformations for proving termination of CSR. We provide new completeness results regarding the use of the transformations in two restricted (but relevant) settings: (a) proofs of termination of canonical CSR and (b) proofs of termination of CSR by using transformations together with simplification orderings. We have also made an experimental evaluation of the transformations, which complements the theoretical analysis from a practical point of view. This leads to new hierarchies of the transformations which are useful to guide their practical use when implementing tools for proving termination of CSR.  相似文献   

18.
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.  相似文献   

19.
The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号