Improving rewriting induction approach for proving ground confluence

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.


Ground confluence proof with pattern complementation

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.


Decision method of reachability based on rewrite rule overlapping

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.


書き換え規則の重なりに基づく到達可能性判定法

項書き換えシステムの到達可能性は合流性の解析や正規化戦略の解析などで重要であり, 木オートマトンの完備化は到達可能性を解析するために広く用いられている手法である. 完備化手続きの要点は,その停止性を保証することであり, 成長項書き換えシステムや有限経路重なり項書き換えシステムのクラスに対する完備化手続きは停止することが知られている. 本論文では,成長項書き換えシステムや有限経路重なり項書き換えシステムのクラスとは独立な, 非左右重なり項書き換えシステムという新しいクラスを提案する. 書き換え規則間の左辺と右辺の重なりを解析することで, 非左右重なり項書き換えシステムに対する完備化手続きが停止するための十分条件を与える. この十分条件をみたす項書き換えシステムのクラスに対して到達可能性問題は決定可能である.


A rule-based equivariant unification procedure

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 confluence tool

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 prover based on rewriting induction

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.


Critical pair analysis in nominal rewriting

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.


Correctness of context-moving transformations for term rewriting 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.


Context-moving transformation for 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 Competition 2015

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.


Correctness of context-moving transformations for term rewriting 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.


Confluence of orthogonal nominal rewriting systems revisited

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)が提案されている.これらの手法は, 末尾再帰プログラムを自動検証に適した単純再帰プログラムへと変換する. 本論文では,項書き換えシステムに対する文脈移動法・文脈分割法の正当性を証明し, それらが書き換え帰納法による帰納的定理の証明に有効であることを明らかにする.


Automated inductive theorem proving using transformations of term rewriting systems

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.


Decision procedures for proving inductive theorems without induction

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つのアプローチを組み合わせることにより, 従来保証されていた決定可能な帰納的定理のクラスを拡張する.


Decidability of inductive theorems based on rewriting induction

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.


Proving confluence of term rewriting systems via persistency and decreasing diagrams

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-ボトムアップ最内システムか否かが決定可能であることを証明する.


Innermost Reachability of Bottom-Up Innermost Term Rewriting Systems

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.


Disproving confluence of term rewriting systems by interpretation and ordering

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.


Confluence proofs of term rewriting systems based on persistency

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 も合流性をもつ. しかし,型付けによって部分システムへ分解できない場合には, このような判定方法は使えない.本論文では, 部分システムに分解できない非左線形項書き換えシステムに対して適用可能となる, 永続性に基づく新しい合流性証明法を提案する.


Disproving confluence of term rewriting systems by interpretation and ordering (extended abstract)

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.


Termination of rule-based calculi for uniform semi-unification

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 of term rewriting systems based on one side decreasing diagrams

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.


Rational term rewriting revisited: decidability and confluence

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.


Transformations by templates for simply-typed term rewriting

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.


Reduction-preserving completion for proving confluence of non-terminating term rewriting systems

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.


Disproving strong head normalization and general productivity automatically in infinitary term rewriting systems

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)は無限項書き換えシステムの部分クラスであるストリーム項書き換えシステムを提案し, ある十分条件のもとでのストリームの生成性判定手続きを報告している. 本論文では,強頭部正規化可能性および一般生成性に対する反証手続きを提案する. 提案する手続きの基本的なアイデアは, 有限表現をもつ無限項である正則項の反例を構成する点にある. 反証手続きの正しさを示すとともに,手続きの実装を報告する. 実験の結果,自動反証法が従来知られていない例について自動反証に成功することを確認した.


A path ordering for term rewriting systems with polynomial size normal forms

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)は多項式サイズ正規形を保証する軽多重集合経路順序を提案し, この順序により方向付け可能な項書き換えシステムにおいては, 任意の項は多項式時間で評価可能であることを示した. また,多項式時間で計算可能な任意の関数は, この軽多重集合経路順序によって方向付けが可能であるような項書き換えシステムによって記述できることも示されている. しかしながら,一般に項書き換えシステムを与えたとき, 多項式サイズ正規形が保証される場合でも, 軽多重集合経路順序で方向付けができないことがある. このため,より一般的な経路順序によって多項式サイズ正規形を保証できることが望ましい. 本論文では,軽多重集合経路順序を拡張し, より一般的な項書き換えシステムに対して多項式サイズ正規形を保証する新しい経路順序を提案する.


Natural inductive theorems for higher-order rewriting

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).


Reduction-preserving completion for proving confluence of non-terminating term rewriting systems

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.


Automated confluence proof by decreasing diagrams based on rule-labelling

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.


Program transformation templates for tupling based on term rewriting

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.


Argument filterings and usable rules for simply typed dependency pairs

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.


Proving confluence of term rewriting systems automatically

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.


項書き換えシステムの合流性自動判定

本論文では, 複数の判定方法を組み合わせた項書き換えシステムの合流性自動判定システムを提案する. 我々の提案するシステムでは, 判定条件が直接適用できない複雑な項書き換えシステムに対して, 直和分解や可換分解といった分解法を適用し, 分解により得られた部分システムに対して合流性判定法を適用することによって, 全体の合流性を自動判定する. このような合流性自動判定システムは,従来ほとんど知られていない. 合流性自動判定システムを実装し,実験を行なった結果, 従来の合流性判定条件が直接適用出来ない項書き換えシステムに対しても, 合流性の自動判定に成功した.また, 項書き換えシステムの合流性を扱った論文等から抜粋した例題集を構成し, 合流性判定実験を試みる.


Automating confluence check of term rewriting systems

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)に置き換えることにより, 単相項書き換えシステムに対して適用可能な,健全な発散鑑定法を提案する. また,これらの補題自動生成法を反証機能付き書き換え帰納法上に実装し, 補題生成能力の比較実験を行う. これにより,(健全)発散鑑定法と健全一般化法が異なる有効範囲を持つことを明らかにし, 従来から知られていた健全一般化法と我々の提案する健全発散鑑定法を組み合わせることにより, 書き換え帰納法のためのより強力な健全補題自動生成法が実現できることを示す.


Automated lemma generation for rewriting induction with disproof

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.


Sound lemma generation for proving inductive validity of equations

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.


Designing a rewriting induction prover with an increased capability of non-orientable theorems

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.


Soundness of rewriting induction based on an abstract principle

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.


Automatic construction of program transformation templates

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.


Program Transformation by Templates: A Rewriting Framework

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.


RAPT: A program transformation system based on term rewriting

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.


Dealing with non-orientable equations in rewriting induction

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.


Program transformation by templates based on term rewriting

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.


Dependency pairs for simply typed term rewriting

Simply typed term rewriting proposed by Yamada (RTA, 2001) is a framework of higher-order term rewriting without bound variables. In this paper, the dependency pair method of first-order term rewriting introduced by Arts and Giesl (TCS, 2000) is extended in order to show termination of simply typed term rewriting systems. Basic concepts such as dependency pairs and estimated dependency graph in the simply typed term rewriting framework are clarified. The subterm criterion introduced by Hirokawa and Middeldorp (RTA, 2004) is successfully extended to the case where terms of function type are allowed. Finally, an experimental result for a collection of simply typed term rewriting systems is presented. Our method is compared with the direct application of the first-order dependency pair method to a first-order encoding of simply typed term rewriting systems.

Inductive theorems for higher-order rewriting

Based on the simply typed term rewriting framework, inductive reasoning in higher-order rewriting is studied. The notion of higher-order inductive theorems is introduced to reflect higher-order feature of simply typed term rewriting. Then the inductionless induction methods in first-order term rewriting are incorporated to verify higher-order inductive theorems. In order to ensure that higher-order inductive theorems are closed under contexts, the notion of higher-order sufficient completeness is introduced. Finally, the decidability of higher-order sufficient completeness is discussed.

Termination of simply-typed applicative term rewriting systems

Applicative term rewriting system handles terms having a tree structure with a function symbol or a variable at every leaf node and a unique application symbol at every internal node. Because of this term structure, direct application of standard termination proof methods, such as recursive path orderings, are often ineffective for applicative term rewriting systems. In this paper, we introduce a simply-typed version of applicative term rewriting systems and present a termination proof method for simply-typed applicative term rewriting systems.

Termination of simply typed term rewriting systems by translation and labelling

Simply typed term rewriting proposed by Yamada (RTA 2001) is a framework of term rewriting allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed term rewriting dispenses with bound variables. This paper presents a method for proving termination of simply typed term rewriting systems (STTRSs, for short). We first give a translation of STTRSs into many-sorted first-order TRSs and show that termination problem of STTRSs is reduced to that of many-sorted first-order TRSs. Next, we introduce a labelling method which is applied to first-order TRSs obtained by the translation to facilitate termination proof of them; our labelling employs an extension of semantic labelling where terms are interpreted on a many-sorted algebra.

単純型付き項書換え系における停止性の自動証明

単純型付き項書換え系は,山田 (RTA'01, 2001) によって提案された, 高階関数を利用できる項書換え系である. 通常の高階項書換え系と異なり,この項書換え系は束縛変数を組み込んでいない. 本論文では,単純型付き項書換え系の停止性証明法を提案する. まず,項書換え系の変換法を導入し,単純型付き項書換え系の停止性が, 変換により得られる第一階項書換え系の停止性から導かれることを示す. 次に,変換で得られた第一階項書換え系の停止性証明を容易にする ラベリングを提案する. 山田 (RTA'01, 2001) が与えた意味論的な停止性証明法とは対照的に, 本論文で提案する停止性証明法は構文論的なため,停止性証明の自動化が容易である.

Proving termination of simply typed term rewriting systems automatically

Simply typed term rewriting proposed by Yamada (RTA'01, 2001) is a framework of term rewriting allowing higher-order functions. In contrast to the usual higher-order term rewriting frameworks, simply typed term rewriting dispenses with bound variables. In this paper, we present a method to prove termination of simply typed term rewriting systems. We first give a transformation on term rewriting systems and show that termination of simply typed term rewriting systems is induced from that of the first-order term rewriting systems obtained by this transformation. We next introduce a labelling technique which facilitates termination proof of the first-order term rewriting systems obtained by our transformation. Contrary to the semantic method proposed by Yamada (RTA'01, 2001), our technique is based on a syntactic approach; and thus one can easily automate termination proof of simply typed term rewriting systems.

Solution to the problem of Zantema on a persistent property of term rewriting systems

A property $P$ of term rewriting systems is persistent if for any many-sorted term rewriting system $R$, $R$ has the property $P$ if and only if its underlying term rewriting system $\Theta(R)$, which results from $R$ by omitting its sort information, has the property $P$. It is shown that termination is a persistent property of many-sorted term rewriting systems that contain only variables of the same sort.

On the finite model property of intuitionistic modal logics over MIPC

MIPC is a well-known intuitionistic modal logic of Prior (1957) and Bull(1966). It is shown that every normal intuitionistic modal logic $L$ over MIPC has the finite model property whenever $L$ is Kripke-complete and universal.

Solution to the problem of Zantema on a persistent property of term rewriting systems

A property $P$ of term rewriting systems is persistent if for any many-sorted term rewriting system $R$, $R$ has the property $P$ iff its underlying term rewriting system $\Theta(R)$, which results from $R$ by omitting its sort information, has the property $P$. It is shown that termination is a persistent property of many-sorted term rewriting systems that contain only variables of the same sort. This is the positive solution to a problem of Zantema, which has been appeared as Rewriting Open Problem 60 in literature.

Uniqueness of normal proofs in implicational intuitionistic logic

A minimal theorem in a logic $L$ is an $L$-theorem which is not a nontrivial substitution instance of another $L$-theorem. Komori (1986) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem $A$ in intuitionistic logic has a unique $\beta$-normal proof in NJ whenever $A$ is provable without non-prime contraction. The non-prime contraction rule in NJ is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. Our result improves the known partial positive solutions to Komori's problem. Also, we present another simple example of a minimal implicational theorem in intuitionistic logic which does not have a unique $\beta\eta$-normal proof in NJ.

Termination transformation by tree lifiting ordering

An extension of a modular termination result for term rewriting systems (TRSs, for short) by A.~Middeldorp (1989) is presented. We intended to obtain this by adapting the dummy elimination transformation by M.~C.~F.~Ferreira and H.~Zantema (1995) under the presence of a non-collapsing non-duplicating terminating TRS whose function symbols are all to be eliminated. We propose a tree lifting ordering induced from a reduction order and a set $G$ of function symbols, and use this ordering to transform a TRS $R$ into $R'$; termination of $R'$ implies that of $R \cup S$ for any non-collapsing non-duplicating terminating TRS $S$ whose function symbols are contained in $G$, provided that for any $l \to r$ in $R$ (1) the root symbol of $r$ is in $G$ whenever that of $l$ is in $G$; and (2) no variable appears directly below a symbol from $G$ in $l$ when $G$ contains a constant. Because of conditions (1) and (2), our technique covers only a part of the dummy elimination technique; however, even when $S$ is empty, there are cases that our technique has an advantage over the dummy elimination technique.

Persistency of confluence

A property $P$ of term rewriting systems (TRSs, for short) is said to be persistent if for any many-sorted TRS $R$, $R$ has the property $P$ if and only if its underlying unsorted TRS $\Theta(R)$ has the property $P$. This notion was introduced by H.~Zantema (1994). In this paper, it is shown that confluence is persistent.

On composable properties of term rewriting systems

A property of term rewriting system (TRS, for short) is said to be composable if it is preserved under unions. We present composable properties of TRSs on the base of modularity results for direct sums of TRSs. We propose a decomposition by a naive sort attachment, and show that modular properties for direct sums of TRSs are $\tau$-composable for a naive sort attachment $\tau$. Here, a decomposition of a TRS $R$ is a pair $\langle R_1, R_2 \rangle$ of (not necessary disjoint) subsets of $R$ such that $R = R_1 \cup R_2$; and for a naive sort attachment $\tau$ a property $\phi$ of TRSs is said to be $\tau$-composable if for any TRS $R$ such that $\tau$ is consistent with $R$, $\phi(R_1) \land \phi(R_2)$ implies $\phi(R)$, where $\langle R_1, R_2 \rangle$ is the decomposition of $R$ by $\tau$.

Non-uniqueness of normal proofs for minimal formulas in implication-conjunction fragment of BCK

A minimal formula of a given logic $L$ is a formula which is provable in $L$ and is not a non-trivial substitution instance of other provable formulas in $L$. Y.~Komori (1986) asked whether normal proofs of minimal formulas are unique in the implicational fragments of natural deduction systems for the intuitionistic logic and the logic BCK. It was already shown that the answer is positive for BCK, while it is negative for the intuitionistic logic. The present paper shows normal proofs for minimal formulas are not necessarily unique for the implication-conjunction fragment of BCK. This result contrasts sharply with the uniqueness of normal proofs of balanced formulas for the implication-conjunction fragment of the intuitionistic logic.
Aoto