We present a framework for proving inductive theorems of first-order equational theories, using techniques of implicit induction developed in the field of term rewriting. In this framework, we make use of automated confluence provers, which have recently been developed intensively, as well as a novel condition of sufficient completeness, called local sufficient completeness. The condition is a key to automated proof of inductive theorems of term rewriting systems that include non-terminating functions. We also apply the technique to showing the correctness of program transformation that is realised as an equivalence transformation of term rewriting systems.
The notion of normal forms is ubiquitous in various equivalent transformations. Confluence (CR), one of the central properties of term rewriting systems (TRSs), concerns uniqueness of normal forms. Yet another such property, which is weaker than confluence, is the property of unique normal forms w.r.t.\ conversion (UNC). Recently, automated confluence proof of TRSs has caught attentions; some powerful confluence tools integrating multiple methods for (dis)proving the CR property of TRSs have been developed. In contrast, there have been little efforts on (dis)proving the UNC property automatically yet. In this paper, we report on a UNC prover combining several methods for (dis)proving the UNC property. We present an equivalent transformation of TRSs preserving UNC, as well as some new criteria for (dis)proving UNC.
Inductive validity is an important characterization of term rewriting systems (TRSs). The notion of inductive validity is also adapted in conditional term rewriting systems (CTRSs). Rewriting induction is a method for proving inductive validity of TRSs originally intended for proving equational conjectures. In this paper, we propose an automated method to prove inductive validity of Horn-clauses (conditional equations) of deterministic oriented CTRSs of type 3. We first show how to deal with proving inductive validity of CTRSs via unraveling transformation from oriented CTRSs to TRSs, and reveal the class of CTRSs for which this approach works. Then, we give an extension of rewriting induction to deal with Horn-clause conjectures, and prove the correctness of the proposed method. We also report on an implementation of the automated inductive theorem prover based on the proposed method, and a preliminary experiment to evaluate the effectiveness of our approach.
帰納的定理は項書き換えシステム(TRS)における重要な特徴付けの一つであり， 帰納的妥当性は条件付き項書き換えシステム(CTRS)においても自然に定義される． 書き換え帰納法は帰納的定理の証明法であり， 従来知られている基本的な書き換え帰納法は， 項書き換えシステムにおける等式帰納的定理を対象としている． 本論文では，決定的な3型指向式CTRSにおける ホーン節(条件付き等式)帰納的定理の自動証明法を提案する． まず，条件付き項書き換えシステムを扱うために， 指向式CTRSからTRSへの変換であるアンラベリング変換を利用する手法を提案し，そのアプローチが 適用可能なCTRSのクラスを明らかにする． 次に，帰納的定理についても，等式だけでなく，等式のホーン節を扱えるように書き換え帰納法の 拡張を行い，提案手法の正当性を証明する． 提案手法に基づく帰納的定理自動証明システムの実装および帰納的定理証明の実験結果を報告し， 提案手法の有効性を明らかにする．
We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically
In (Aoto&Toyama, FSCD 2016), a method to prove ground confluence of many-sorted term rewriting systems based on rewriting induction is given. In this paper, we give several methods that add wider flexibility to the rewriting induction approach for proving ground confluence. Firstly, we give a method to deal with the case in which suitable rules are not presented in the input system. Our idea is to construct additional rewrite rules that supplement or replace existing rules in order to obtain a set of rules that is adequate for applying rewriting induction. Secondly, we give a method to deal with non-orientable constructor rules. This is accomplished by extending the inference system of rewriting induction and giving a sufficient criterion for the correctness of the system. Thirdly, we give a method to deal with disproving ground confluence. The presented methods are implemented in our ground confluence prover AGCP and experiments are reported. Our experiments reveal the presented methods are effective to deal with problems for which state-of-the-art ground confluence provers can not handle.
In (Aoto&Toyama, FSCD 2016), we gave a procedure for proving ground confluence of many-sorted TRSs based on rewriting induction for proving bounded ground convertibility. The procedure needs to find a strongly quasi-reducible terminating set of rules from the given input TRS to make the rewriting induction work. It turns out, however, that such a subset of rewrite rules is often not present in the input TRS. In this note, we propose an improvement of the procedure; in the new procedure, firstly the lack of defining patterns is detected using pattern complementation procedure (Lazrek et al., I&C 1990), and then possible defining rules that can be appended to obtain a strongly quasi-reducible terminating TRS are searched. The new procedure is useful to prove ground confluence of some TRSs automatically which have been failed in the previous procedure.
Tree automata completion is a popular method for reachability analysis over term rewriting systems, which has many applications such as con uence analysis and normalizing strategy analysis. The point of this method is to ensure termination of the completion procedure, and it is known that the completion procedure terminates for the classes of growing term rewriting systems and finite path overlapping term rewriting systems. In this paper, we propose a new class of term rewriting systems, named non-left-right-overlapping term rewriting systems, which is incompatible with the classes of growing systems and nite path overlapping systems. Analyzing the overlapping relation between the left-hand side and the right-hand side of the rewrite rules, we give a sufficient condition for termination of the tree automata completion procedure for non-left-right-overlapping term rewriting systems. The reachability problem is decidable for the class of term rewriting systems satisfying this sufficient condition.
項書き換えシステムの到達可能性は合流性の解析や正規化戦略の解析などで重要であり， 木オートマトンの完備化は到達可能性を解析するために広く用いられている手法である． 完備化手続きの要点は，その停止性を保証することであり， 成長項書き換えシステムや有限経路重なり項書き換えシステムのクラスに対する完備化手続きは停止することが知られている． 本論文では，成長項書き換えシステムや有限経路重なり項書き換えシステムのクラスとは独立な， 非左右重なり項書き換えシステムという新しいクラスを提案する． 書き換え規則間の左辺と右辺の重なりを解析することで， 非左右重なり項書き換えシステムに対する完備化手続きが停止するための十分条件を与える． この十分条件をみたす項書き換えシステムのクラスに対して到達可能性問題は決定可能である．
Nominal rewriting is a rewriting formalism that deals with variable binding. An equivariant nominal unification is a basic ingredient of nominal rewriting for computing rewrite steps and critical pairs. We present a rule-based procedure for the equivariant nominal unification.
Nominal rewriting is a framework of higher-order rewriting introduced in (Fernández, Gabbay & Mackie, 2004; Fernández & Gabbay, 2007). Recently, (Suzuki et al., 2015) revisited confluence of nominal rewriting in the light of feasibility. We report on an implementation of a confluence tool for (non-closed) nominal rewriting, based on (Suzuki et al., 2015) and succeeding studies.
Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Recently, interests in proving confluence of term rewriting systems automatically has grown, and confluence provers have been developed. But they mainly focus on confluence and not ground confluence. In fact, little interest has been paid to developing tools for proving ground confluence automatically. We report an implementation of a ground confluence prover based on rewriting induction, which is a method originally developed for proving inductive theorems.
Nominal rewriting systems (Fernández, Gabbay & Mackie, 2004; Fernández & Gabbay, 2007) is a framework that extends first-order term rewriting by a binding mechanism based on the nominal approach (Gabbay & Pitts, 2002; Pitts, 2003). In this paper, we investigate confluence properties of nominal rewriting, following the study of orthogonal systems in (Suzuki et al., 2015), but here we treat systems in which overlaps of the rewrite rules exist. First we present an example where choice of bound variables (atoms) of rules affects joinability of the induced critical pairs. Then we give a proof of the critical pair lemma, and illustrate some of its applications including confluence results for non-terminating systems.
Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for functional programs transform tail-recursive programs into non tail-recursive ones which are more suitable for proofs by induction and thus for verification. In this paper, we formulate context-moving and context-splitting transformations in the framework of term rewriting systems, and prove their correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed. The conditions for the correctness with respect to initial algebra semantics can be checked by automated methods for inductive theorem proving developed in the field of term rewriting systems.
Proofs by induction are often incompatible with tail-recursive definitions as the accumulator changes in the course of unfolding the definitions. Context-moving (Giesl, 2000) for functional programs transforms tail-recursive programs into non tail-recursive ones which are more suitable for verification. In this work, we formulate a context-moving transformation for term rewriting systems, and prove the correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed.
Confluence is one of the central properties of rewriting. Our competition aims to foster the development of techniques for proving/disproving confluence of various formalisms of rewriting automatically. We explain the background and setup of the 4th Confluence Competition.
Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for functional programs transform tail-recursive programs into non tail-recursive ones which are more suitable for proofs by induction and thus for verification. In this paper, we formulate context-moving and context-splitting transformations in the framework of term rewriting systems, and prove their correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed. The conditions for the correctness with respect to initial algebra semantics can be checked by automated methods for inductive theorem proving developed in the field of term rewriting systems.
Nominal rewriting systems (Fernández, Gabbay & Mackie, 2004; Fernández & Gabbay, 2007) have been introduced as a new framework of higher-order rewriting systems based on the nominal approach (Gabbay & Pitts, 2002; Pitts, 2003), which deals with variable binding via permutations and freshness conditions on atoms. Confluence of orthogonal nominal rewriting systems has been shown in (Fernández & Gabbay, 2007). However, their definition of (non-trivial) critical pairs has a serious weakness so that the orthogonality does not actually hold for most of standard nominal rewriting systems in the presence of binders. To overcome this weakness, we divide the notion of overlaps into the self-rooted and proper ones, and introduce a notion of α-stability which guarantees α-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and α-stability. The new definition of orthogonality and the criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.
項書き換えシステム上の帰納的定理の自動証明手法として書き換え帰納法(Reddy, 1989)が提案されている． しかし，書き換え帰納法は末尾再帰による関数定義が含まれると有効に働かない場合が多い． 一方，プログラムの自動検証を容易にすることを目的としたプログラム変換法として， 文脈移動法および文脈分割法(Giesl, 2000)が提案されている．これらの手法は， 末尾再帰プログラムを自動検証に適した単純再帰プログラムへと変換する． 本論文では，項書き換えシステムに対する文脈移動法・文脈分割法の正当性を証明し， それらが書き換え帰納法による帰納的定理の証明に有効であることを明らかにする．
Rewriting induction (Reddy, 1989) is proposed as an automated theorem proving method on term rewriting systems. In general, rewriting induction does not work well for the term rewriting systems with tail recursion. On the other hand, context moving and splitting (Giesl, 2000) are proposed as program transformation techniques intended to facilitate automated verification for functional programs. These techniques transform tail recursive programs into simple recursive programs suitable for automated verification. In this paper, we prove that the correctness of these techniques for term rewriting systems, and show that the combination of rewriting induction and these techniques are useful in proving inductive theorems on term rewriting systems with tail recursion.
Automated inductive reasoning for term rewriting has been extensively studied in the literature. Classes of equations and term rewriting systems (TRSs) with decidable inductive validity have been identified and used to automatize the inductive reasoning. We give procedures for deciding the inductive validity of equations in some standard TRSs on natural numbers and lists. Contrary to previous decidability results, our procedures can automatically decide without involving induction reasoning the inductive validity of arbitrary equations for these TRSs, that is, without imposing any syntactical restrictions on the form of equations. We also report on the complexity of our decision procedures. These decision procedures are implemented in our automated provers for inductive theorems of TRSs and experiments are reported.
等式論理において，自然数やリストなどのデータ構造上で成立する等式を帰納的定理とよぶ． 与えられた等式が等式論理の帰納的定理であるか否かは一般に決定不能であるが， いくつかの部分クラスに対する決定手続きが知られている． FalkeとKapur(2006)が与えた決定手続きは書き換え帰納法に基づく．一方，外山 (2002)は， 帰納的定理判定問題を2つの抽象リダクションシステムの等価性判定問題としてとらえることで， 書き換え帰納法が帰納的定理の決定手続きとなるための十分条件を示した． しかし，この両者が保証している決定可能な帰納的定理のクラス間には包含関係がない． そこで，本論文ではこれら2つのアプローチを組み合わせることにより， 従来保証されていた決定可能な帰納的定理のクラスを拡張する．
In equational logics, validity of equations on data structures such as natural numbers or lists is formalized as inductive validity; and the equations inductively valid are called inductive theorems. In general, it is undecidable whether an equation is an inductive theorem of an equational logic. Thus, several decision procedures of inductive validity for some subclasses of conjectures have been known. A decision procedure given by Falke and Kapur (2006) is based on rewriting induction. Toyama (2002) gives a sufficient criterion of conjectures for which the rewriting induction procedure becomes a decision procedure for inductive validity, by reducing the problem of inductive validity to a problem of equivalence of two abstract reduction systems. However, the classes of conjectures having decidable inductive validity obtained by Falke and Kapur and obtained by Toyama are incomparable. In this paper, we extend known classes of conjectures having decidable inductive validity, combining these two approaches.
The decreasing diagrams technique (van Oostrom, 1994) has been successfully used to prove confluence of rewrite systems in various ways; using rule-labelling (van Oostrom, 2008), it can also be applied directly to prove confluence of some linear term rewriting systems (TRSs) automatically. Some efforts for extending the rule-labelling are known, but non-left-linear TRSs are left beyond the scope. Two methods for automatically proving confluence of non-(left-)linear TRSs with the rule-labelling are given. The key idea of our methods is to combine the decreasing diagrams technique with persistency of confluence (Aoto \& Toyama, 1997).
DurandとSénizergues(2007)によってボトムアップ線形項書き換えシステム の到達可能性が決定可能であることが示されている．本論文では，ボトムアッ プ書き換えをボトムアップ最内書き換えに変更したボトムアップ最内シス テムのクラスを提案し，ボトムアップ最内左線形項書き換えシステムの最内到 達可能性が決定可能であることを示す．また，ボトムアップ最内システムを 制限した強k-ボトムアップ最内システムを提案し，左線形項書き換えシステムが 強k-ボトムアップ最内システムか否かが決定可能であることを証明する．
Durand and Sénizergues (2007) showed that reachability of bottom-up linear term rewriting systems is decidable. In this paper we propose the class of bottom-up innermost systems by replacing "bottom-up rewriting" with "bottom-up innermost rewriting", and show that innermost reachability is decidable for bottom-up innermost left-linear term rewriting systems. Furthermore, we give a class of bottom-up innermost systems-the class of strongly k-bottom-up innermost systems-and show that it is decidable whether a left-linear term rewriting system belongs to the class.
In order to disprove confluence of term rewriting systems, we develop new criteria for ensuring non-joinability of terms based on interpretation and ordering. We present some instances of the criteria which are amenable for automation, and report on an implementation of a confluence disproving procedure based on these instances. The experiments reveal that our method is successfully applied to automatically disprove confluence of some term rewriting systems, on which state-of-the-art automated confluence provers fail. A key idea to make our method effective is the introduction of usable rules - this allows one to decompose the constraint on rewrite rules into smaller components that depend on starting terms.
Since the confluence property of term rewrite systems is persistent, a term rewriting system R is confluent if it is decomposed into small subsystems by introducing appropriate many-sorted types and each of them is confluent. However, if introducing types does not decompose R into small subsystems, this proof method does not work. In this paper we propose a new method for confluence proof based on persistency, which can be applied to non-left-linear term rewriting systems not decomposed into subsystems by introducing types.
項書き換えシステムの合流性は永続性をもつので， 適当な多ソート型付けにもとづいて項書き換えシステム R を部分システムに分解し， それぞれの部分システムが合流性をもつなら，R も合流性をもつ． しかし，型付けによって部分システムへ分解できない場合には， このような判定方法は使えない．本論文では， 部分システムに分解できない非左線形項書き換えシステムに対して適用可能となる， 永続性に基づく新しい合流性証明法を提案する．
We present new criteria for ensuring non-joinability of terms based on interpretation and ordering, and report on an implementation of confluence disproving procedure based on some instances of the criteria. The experiment reveals that our methods can be applied to automatically disprove confluence of some term rewriting systems, on which state-of-the-art automated confluence provers fail.
Uniform semi-unification is a generalization of unification; its efficient algorithms have been extensively studied in (Kapur et al., 1994) and (Oliart&Snyder, 2004). For (uniform) semi-unification, several variants of rule-based calculi are known. But, some of these calculi in the literature lack the termination property, i.e. not all derivations are terminating. We revisit symbolic semi-unification whose solvability coincides with that of uniform semi-unification. We give an abstract criterion of the strategy on which a general rule-based calculus for symbolic semi-unification terminates. Based on this, we give an alternative and robust correctness proof of a rule-based uniform semi-unification algorithm.
項書き換えシステムの可換性は合流性を一般化した性質であり，可換性に基づく項書 き換えシステムの分解は項書き換えシステムの合流性の証明に利用できる．項書き換 えシステムの可換性を示す方法がいくつか知られているが，これらはみな危険対解析 に基づく条件に基づいている．一方，抽象リダクションシステムの可換性証明法とし て減少ダイアグラム法が知られている．しかし，減少ダイアグラム法を項書き換えシ ステムの可換性証明へ応用した研究はほとんど報告されていない．本論文では，片側 減少ダイアグラム法を提案し，片側減少ダイアグラム法に基づく項書き換えシステム の可換性証明法を示す．
Commutativity is a generalization of confluence. Furthermore, decompositions of term rewriting systems based on the commutativity is useful to prove confluence of term rewriting systems. Several methods for showing commutativity of term rewriting systems are known, where all of them are based on conditions imposed from critical pairs analysis. Apart from this, a sufficient condition of commutativity based on decreasing diagrams has been studied in the framework of abstract rewriting. Decreasing diagrams, however, have not been applied for proving commutativity of term rewriting systems. In this paper, we introduce one side decreasing diagrams, and give a method to prove commutativity of term rewriting systems based on one side decreasing diagrams.
We consider a variant of rational term rewriting as first introduced by Corradini et al., i.e., we consider rewriting of (infinite) terms with a finite number of different subterms. Motivated by computability theory, we show a number of decidability results related to the rewrite relation and prove an effective version of a confluence theorem for orthogonal systems.
We extend a framework of program transformation by templates based on first order term rewriting (Chiba et al., 2005) to simply typed term rewriting (Yamada, 2001), which is a framework of higher order term rewriting. A pattern matching algorithm to apply templates for transforming a simply typed term rewriting system is given and the correctness of the algorithm is shown.
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also (partially) works even if the system is not terminating modulo E. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.
Infinitary term rewriting has been proposed to model functional programs that deal with virtually infinite data structures such as streams or lazy lists. Strong head normalization is a fundamental property of infinitary term rewriting systems and methods for proving this property have been proposed by Zantema (2008) and Endrullis et al. (2009). Endrullis et al. (2010) have proposed a class of infinitary term rewriting systems-stream term rewriting systems-and they have given a decision procedure of the productivity of streams for a class of stream term rewriting systems. In this paper, we present procedures for disproving these two properties of infinitary term rewriting systems-the strong head normalization and the productivity. The basic idea of our procedure is to construct rational counterexamples which are infinitary terms but have finite representations. The correctness of our procedures is proved and an implementation is reported. Our experiments reveal that our procedures successfully disprove the strong head normalization and the productivity automatically for some examples for which no automated disproving procedure is known.
遅延リストやストリームといった仮想的に無限長とみなされるデータを扱う関数型プログラムの計算モデルとして， 無限項書き換えシステムが提案されている． 項書き換えシステムにおける停止性に対応する基本的な性質として， 無限項書き換えシステムにおける強頭部正規化可能性があり， その証明法がZantema(2008)やEndrullisら(2009)によって報告されている． また，Endrullisら(2010)は無限項書き換えシステムの部分クラスであるストリーム項書き換えシステムを提案し， ある十分条件のもとでのストリームの生成性判定手続きを報告している． 本論文では，強頭部正規化可能性および一般生成性に対する反証手続きを提案する． 提案する手続きの基本的なアイデアは， 有限表現をもつ無限項である正則項の反例を構成する点にある． 反証手続きの正しさを示すとともに，手続きの実装を報告する． 実験の結果，自動反証法が従来知られていない例について自動反証に成功することを確認した．
Numbers of methods have been proposed to guarantee polynomial time computability of programs represented by term rewriting systems. Marion (2003) proposes the light multiset path ordering to guarantee polynomial size normal forms and shows that in term rewriting systems which can be oriented by this ordering any term can be evaluated in polynomial time. It is also shown that any polynomial time computable function can be encoded by term rewriting systems that can be oriented by this ordering. In general, however, there are term rewriting systems whose normal forms can be evaluated in polynomial time but which can not be oriented by this ordering. Thus a more general path ordering which guarantees polynomial time normal form is preferred. In this paper, we give an extension of the light multiset path ordering so that polynomial size normal form is guaranteed for more general class of term rewriting systems.
項書き換えシステムを用いて記述したプログラムが， 多項式時間で計算可能であることを示す様々な手法が知られている． Marion (2003)は多項式サイズ正規形を保証する軽多重集合経路順序を提案し， この順序により方向付け可能な項書き換えシステムにおいては， 任意の項は多項式時間で評価可能であることを示した． また，多項式時間で計算可能な任意の関数は， この軽多重集合経路順序によって方向付けが可能であるような項書き換えシステムによって記述できることも示されている． しかしながら，一般に項書き換えシステムを与えたとき， 多項式サイズ正規形が保証される場合でも， 軽多重集合経路順序で方向付けができないことがある． このため，より一般的な経路順序によって多項式サイズ正規形を保証できることが望ましい． 本論文では，軽多重集合経路順序を拡張し， より一般的な項書き換えシステムに対して多項式サイズ正規形を保証する新しい経路順序を提案する．
The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of inductive theorems for higher-order rewriting, natural inductive theorems. This allows to incorporate properties such as extensionality and extensibility, based on simply typed S-expression rewriting (Yamada, 2001).
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and usual termination. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into terminating part and possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.
Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams technique to prove confluence of rewrite systems, rule-labelling heuristic has been proposed by van Oostrom (2008). We show how constraints for ensuring confluence of term rewriting systems constructed based on the rule-labelling heuristic are encoded as linear arithmetic constraints suitable for solving the satisfiability of them by external SMT solvers. We point out an additional constraint omitted in (van Oostrom, 2008) that is needed to guarantee the soundness of confluence proofs based on the rule-labelling heuristic extended to deal with non-right-linear rules. We also present several extensions of the rule-labelling heuristic by which the applicability of the technique is enlarged.
Chiba et al. (2006) proposed a framework of program transformation of term rewriting systems by developed templates. Contrast to the previous framework of program transformation by templates based on lambda calculus, this framework provides a method to verify the correctness of transformation automatically. Tupling (Bird, 1980) is a well-known technique to eliminate redundant recursive calls for improving efficiency of programs. In Chiba et al.'s framework, however, one can not use tuple symbols to construct developed templates. Thus their framework is not capable of tupling transformations. In this paper, we propose a more flexible notion of templates so that a wider variety of transformations, including tupling transformations, can be handled.
Simply typed term rewriting (Yamada, 2001) is a framework of higher-order term rewriting without bound variables based on Lisp-like syntax. The dependency pair method for the framework has been obtained by extending the first-order dependency pair method and subterm criterion in (Aoto \& Yamada, 2005). In this paper, we incorporate termination criteria using reduction pairs and related refinements into the simply typed dependency pair framework using recursive path orderings for S-expression rewriting systems (Toyama, 2008). In particular, we incorporate the usable rules criterion with respect to argument filterings, which is a key ingredient to prove the termination in a modular way. The proposed technique has been implemented in a termination prover and an experimental result is reported.
We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide--and--conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown.
本論文では， 複数の判定方法を組み合わせた項書き換えシステムの合流性自動判定システムを提案する． 我々の提案するシステムでは， 判定条件が直接適用できない複雑な項書き換えシステムに対して， 直和分解や可換分解といった分解法を適用し， 分解により得られた部分システムに対して合流性判定法を適用することによって， 全体の合流性を自動判定する． このような合流性自動判定システムは，従来ほとんど知られていない． 合流性自動判定システムを実装し，実験を行なった結果， 従来の合流性判定条件が直接適用出来ない項書き換えシステムに対しても， 合流性の自動判定に成功した．また， 項書き換えシステムの合流性を扱った論文等から抜粋した例題集を構成し， 合流性判定実験を試みる．
We propose an automated confluence checker for term rewriting systems (TRSs) that combines several criteria for proving the confluence property of TRSs. For a TRS to which none of confluence criteria directly applies, our checker automatically decomposes it into small components using direct sum decomposition and commutative decomposition, and applies the confluence criteria to each component so that the confluence of the whole system is checked by combining these results. For the best of our knowledge, an automated confluence checker based on such an approach has been unknown. We have implemented our checker, and have successfully applied our checker to automatically check the confluence of a complex TRS, to which none of known confluence criteria applies directly. We also construct a collection of sample TRSs mainly extracted from papers on confluence of TRSs and perform an experiment to this collection.
書き換え帰納法(Reddy, 1989)は， 項書き換えシステムにもとづく帰納的定理の自動証明法である． 一般に，補題自動生成法において生成される補題はいつも正しい(定理である)とは限らないが， 正しい補題のみを生成する補題自動生成法を健全であるという． 発散鑑定法(Walsh, 1996)は書き換え帰納法のために提案された補題自動生成法であるが， 健全ではない． 本論文では，発散鑑定法の手続きの一部を健全一般化法 (UrsoとKounalis, 2004)に置き換えることにより， 単相項書き換えシステムに対して適用可能な，健全な発散鑑定法を提案する． また，これらの補題自動生成法を反証機能付き書き換え帰納法上に実装し， 補題生成能力の比較実験を行う． これにより，(健全)発散鑑定法と健全一般化法が異なる有効範囲を持つことを明らかにし， 従来から知られていた健全一般化法と我々の提案する健全発散鑑定法を組み合わせることにより， 書き換え帰納法のためのより強力な健全補題自動生成法が実現できることを示す．
Rewriting induction (Reddy, 1989) is an automated inductive theorem proving method for term rewriting systems. An automated lemma generation method for automated inductive theorem proving is said to be sound if it does not produce incorrect lemmas. Divergence critic (Walsh, 1996) is a well-known automated lemma generation method for the rewriting induction, but it is unsound. In this paper, we propose a sound variant of the divergence critic applicable for monomorphic term rewriting systems by incorporating sound generalization (Urso and Kounalis, 2004) in a part of its procedure. We implement these three automated lemma generation methods on a rewriting induction system with disproof to evaluate effectiveness of these methods. Our experiment reveals that the (sound) divergence critic and the sound generalization are often effective for different kinds of conjectures. Thus, the sound divergence critic can be combined with the sound generalization to obtain a more powerful automated sound lemma generation method for rewriting induction.
In many automated methods for proving inductive theorems, finding a suitable generalization of a conjecture is a key for the success of proof attempts. On the other hand, an obtained generalized conjecture may not be a theorem, and in this case hopeless proof attempts for the incorrect conjecture are made, which is against the success and efficiency of theorem proving. Urso and Kounalis (2004) proposed a generalization method for proving inductive validity of equations, called sound generalization, that avoids such an over-generalization. Their method guarantees that if the original conjecture is an inductive theorem then so is the obtained generalization. In this paper, we revise and extend their method. We restore a condition on one of the characteristic argument positions imposed in their previous paper and show that otherwise there exists a counterexample to their main theorem. We also relax a condition imposed in their framework and add some flexibilities to some of other characteristic argument positions so as to enlarge the scope of the technique.
Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order and the original rewriting induction is not capable of proving theorems which are not orientable by that reduction order. To deal with such theorems, Bouhoula (1995) as well as Dershowitz \& Reddy (1993) used the ordered rewriting. However, even using ordered rewriting, the weak capability of non-orientable theorems is considered one of the weakness of rewriting induction approach compared to other automated methods for proving inductive theorems. We present a refined system of rewriting induction with an increased capability of non-orientable theorems and a capability of disproving incorrect conjectures. Soundness for proving/disproving are shown and effectiveness of our system is demonstrated through some examples.
Rewriting induction (Reddy, 1990) is a method to prove inductive theorems of term rewriting systems automatically. Koike and Toyama (2000) extracted an abstract principle of rewriting induction in terms of abstract reduction systems. Based on their principle, the soundness of the original rewriting induction system can be proved. It is not known, however, whether such an approach can be adapted also for more powerful rewriting induction systems. In this paper, we give a new abstract principle that extends Koike and Toyama's abstract principle. Using this principle, we show the soundness of a rewriting induction system extended with an inference rule of simplification by conjectures. Inference rules of simplification by conjectures have been used in many rewriting induction systems. Replacement of the underlying rewriting mechanism with ordered rewriting is an important refinement of rewriting induction---with this refinement, rewriting induction can handle non-orientable equations. It is shown that, based on the introduced abstract principle, a variant of our rewriting induction system based on ordered rewriting is sound, provided that its base order is ground-total. In our system based on ordered rewriting, the simplification rule extends those of the equational fragment of some major systems from the literature.
Program transformation by templates (Huet and Lang, 1978) is a technique to improve the efficiency of programs. In this technique, programs are transformed according to a given program transformation template. To enhance the variety of program transformation, it is important to introduce new transformation templates. Up to our knowledge, however, few works discuss about the construction of transformation templates. Chiba et al.\ (2006) proposed a framework of program transformation by template based on term rewriting and automated verification of its correctness. Based on this framework, we propose a method that automatically constructs transformation templates from similar program transformations. The key idea of our method is a second-order generalization, which is an extension of Plotkin's first-order generalization (1969). We give a second-order generalization algorithm and prove the soundness of the algorithm. We then report about an implementation of the generalization procedure and an experiment on the construction of transformation templates.
We propose a framework in this paper for transforming programs with templates based on term rewriting. The programs are given by term rewriting systems. We discuss how to validate the correctness of program transformation within our framework. We introduce a notion of developed templates and a simple method of constructing such templates without explicit use of induction. We then show that in any transformation of programs using the developed templates, their correctness can be verified automatically. The correctness of program transformation within our framework is discussed based on operational semantics. We also present some examples of program transformations in our framework.
Chiba et al. (2005) proposed a framework of program transformation by template based on term rewriting in which correctness of the transformation is verified automatically. This paper describes RAPT (Rewriting-based Automated Program Transformation system) which implements this framework.
Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of term rewriting systems. Reasoning by the rewriting induction is based on the noetherian induction on some reduction order. Thus, when the given conjecture is not orientable by the reduction order in use, any proof attempts for that conjecture fails; also conjectures such as a commutativity equation are out of the scope of the rewriting induction because they can not be oriented by any reduction order. In this paper, we give an enhanced rewriting induction which can deal with non-orientable conjectures. We also present an extension which intends an incremental use of our enhanced rewriting induction.
Huet and Lang (1978) presented a framework of automated program transformation based on lambda calculus in which programs are transformed according to a given program transformation template. They introduced a second-order matching algorithm of simply-typed lambda calculus to verify whether the input program matches the template. They also showed how to validate the correctness of the program transformation using the denotational semantics.
We propose in this paper a framework of program transformation by templates based on term rewriting. In our new framework, programs are given by term rewriting systems. To automate our program transformation, we introduce a term pattern matching problem and present a sound and complete algorithm that solves this problem.
We also discuss how to validate the correctness of program transformation in our framework. We introduce a notion of developed templates and a simple method to construct such templates without explicit use of induction. We then show that in any program transformation by developed templates the correctness of the transformation can be verified automatically. In our framework the correctness of the program transformation is discussed based on the operational semantics. This is a sharp contrast to Huet and Lang's framework.