共查询到19条相似文献,搜索用时 156 毫秒
1.
2.
归纳法推理中的项重写策略 总被引:2,自引:2,他引:0
本文介绍归纳法推理系统中的项重写策略,该策略根据不同的待重写项term,分别运用公理、重写引理、函数定义、项重写规则等重写项term,以期得到一个更接近推理目标的已重写项,这一策略已在微机上用编译LISP语言实现。 相似文献
3.
4.
本文着重研究重写系统的合流性,通过引入符号测度的概念,本文定义了半正则重写系统,并证明了半正则重写系统的合流性。 相似文献
5.
Knuth-Bendix完备过程不终止的起因研究得很少,本文研究引起不终止的重写规则的结构性质,提出了相容交叉规则对的概念,推广了文献6的结论,并提出了为构造系统检验该过程是否不终止的方法。 相似文献
6.
项重写系统弱基终止性的归纳证明 总被引:3,自引:2,他引:1
1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。例如,下面的R是一个由五个重写规则组成的、定义用({0,s})表示的自然数集N上的两倍函数d(x)=2×n:N→N的项重写系统: 相似文献
7.
Knuth-Bendix完备过程不终止的起因研究得很少.本文研究引起不终止的重写规则的结构性质,提出了相容交叉规则对的概念,推广了文献[6]的结论,并提出了为构造系统检验该过程是否不终止的方法. 相似文献
8.
9.
10.
11.
《Journal of Symbolic Computation》1994,17(1):23-50
We investigate proving termination of term rewriting systems by interpretation of terms in a well-founded monotone algebra. The well-known polynomial interpretations can be considered as a particular case in this framework. A classification of types of termination, including simple termination, is proposed based on properties in the semantic level. A transformation on term rewriting systems eliminating distributive rules is introduced. Using this distribution elimination a new termination proof of the system SUBST of Hardin and Laville (1986) is given. This system describes explicit substitution in λ-calculus.Another tool for proving termination is based on introduction and removal of type restrictions. A property of many-sorted term rewriting systems is called persistent if it is not affected by removing the corresponding typing restriction. Persistence turns out to be a generalization of direct sum modularity, but is more powerful for both proving confluence and termination. Termination is proved to be persistent for the class of term rewriting systems for which not both duplicating rules and collapsing rules occur, generalizing a similar result of Rusinowitch for modularity. This result has nice applications, in particular in undecidability proofs. 相似文献
12.
In this paper we study the non-determinism between the inference rules of the lazy narrowing calculusLNC(Middeldorpet al., 1996,Theoret. Comput. Sci.,167, 95–130. We show that all non-determinism can be removed without losing the important completeness property by restricting the underlying term rewriting systems to left-linear confluent constructor systems and interpreting equality as strict equality. For the subclass of orthogonal constructor systems the resulting narrowing calculus is shown to have the nice property that solutions computed by different derivations starting from the same goal are incomparable. 相似文献
13.
《Journal of Symbolic Computation》1995,20(1):1-41
In this paper we prove several new modularity results for unconditional and conditional term rewriting systems. Most of the known modularity results for the former systems hold for disjoint or constructor-sharing combinations. Here we focus on a more general kind of combination: so-called composable systems. As far as conditional term rewriting systems are concerned, all known modularity result but one apply only to disjoint systems. Here we investigate conditional systems which may share constructors. Furthermore, we refute a conjecture of Middeldorp (1990, 1993). 相似文献
14.
《Information Processing Letters》1987,25(3):141-143
The direct sum of two term rewriting systems is the union of systems having disjoint sets of function symbols. It is shown that the direct sum of two term rewriting systems is not terminating, even if these systems are both terminating. 相似文献
15.
In this paper, we propose the notion of reducibility of symbols in term rewriting systems (TRSs). For a given algebraic specification, operation symbols can be classified on the basis of their denotations: the operation symbols for functions and those for constructors. In a model, each term constructed by using only constructors should denote an element, and functions are defined on sets formed by these elements. A term rewriting system provides operational semantics to an algebraic specification. Given a TRS, a term is called reducible if some rewrite rule can be applied to it. An irreducible term can be regarded as an answer in a sense. In this paper, we define the reducibility of operation symbols as follows: an operation symbol is reducible if any term containing the operation symbol is reducible. Non-trivial properties of context-sensitive rewriting, which is a simple restriction of rewriting, can be obtained by restricting the terms on the basis of variable occurrences, its sort, etc. We confirm the usefulness of the reducibility of operation symbols by applying them to behavioral specifications for proving the behavioral coherence property. 相似文献
16.
《Journal of Symbolic Computation》1996,21(1):15-39
Currying is a transformation of term rewrite systems which may contain symbols of arbitrary arity into systems which contain only nullary symbols, together with a single binary symbol called application. We show that for all term rewrite systems (whether orthogonal or not) the following properties are preserved by this transformation: strong normalization, weak normalization, weak Church-Rosser, completeness, semi-completeness, and the non-convertibility of distinct normal forms. Under the condition of left-linearity we show preservation of the properties NF (if a term is reducible to a normal form,then its reducts are all reducible to the same normal form) and UN→ (a term is reducible to at most one normal form).We exhibit counterexamples to the preservation of NF and UN→ for non-left-linear systems.The results extend to partial currying(where some subset of the symbols are curried),and imply some modularity properties for unions of applicative systems. 相似文献
17.
Naoki Nishida Tomohiro Mizutani Masahiko Sakai 《Electronic Notes in Theoretical Computer Science》2007,174(10):75
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. 相似文献
18.
Jean-Pierre Jouannau Yoshihito Toyama 《International Journal of Software and Informatics》2008,2(1):61-75
In Ref.[19], Toyama proved that the union of two confluent term-rewriting systems that share absolutely no function symbols or constants is likewise confluent, a property called modularity. The proof of this beautiful modularity result, technically based on slicing terms into an homogeneous cap and a so called alien, possibly heterogeneous substitution,was later substantially simplified in Refs.[8,12]. In this paper, we present a further simplification of the proof of Toyama's result for confluence, which shows that the crux of the problem lies on two di?erent properties: a cleaning lemma, whose goal is to anticipate the application of collapsing reductions and a modularity property of ordered completion that allows to pairwise match the caps and alien substitutions of two equivalent terms obtained from the cleaning lemma. The approach allows for arbitrary kinds of rules, and scales up to rewriting modulo arbitrary sets of equations. 相似文献
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. 相似文献