掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：ACM  

DOI： 10.1145/3354166.3354178

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik  

DOI： 10.4230/LIPIcs.FSCD.2018.32

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing  

In (Aoto&amp
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.

DOI： 10.4230/LIPIcs.FSCD.2017.7

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer Verlag  

Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet’s parallel closure theorem and its generalisation on confluence of left-linear term rewriting systems to the case of nominal rewriting. The proof of the theorem follows a previous inductive confluence proof for orthogonal uniform nominal rewriting systems, but the presence of critical pairs requires a much more delicate argument. The results include confluence of left-linear uniform nominal rewriting systems that are not α-stable and thus are not represented by any systems in traditional higher-order rewriting frameworks.

DOI： 10.1007/978-3-319-66167-4_7

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing  

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.

DOI： 10.4230/LIPIcs.FSCD.2016.33

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：EasyChair  

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：ソフトウェア科学会  

DOI： 10.11309/jssst.33.3_93

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer Verlag  

Nominal rewriting is a framework of higher-order rewriting introduced in (Fernández, Gabbay &amp
Mackie, 2004
Fernández &amp
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.

DOI： 10.1007/978-3-319-40229-1_12

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing  

Nominal rewriting systems (Fernández, Gabbay &amp
Mackie, 2004
Fernández &amp
Gabbay, 2007) have been introduced as a new framework of higher-order rewriting systems based on the nominal approach (Gabbay &amp
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 &amp
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.

DOI： 10.4230/LIPIcs.RTA.2015.301

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SPRINGER INT PUBLISHING AG  

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.

DOI： 10.1007/978-3-319-27436-2_20

Web of Science

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

DOI： 10.11309/jssst.32.1_179

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

DOI： 10.1007/978-3-319-21401-6_5

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Association for Computing Machinery, Inc  

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.

DOI： 10.1145/2643135.2643156

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer Verlag  

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 &amp
Toyama, 1997). © 2014 Springer International Publishing Switzerland.

DOI： 10.1007/978-3-319-08918-8_4

Scopus

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

DOI： 10.11309/jssst.31.3_294

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会 ; 1984-  

DOI： 10.11309/jssst.31.1_75

CiNii Article

CiNii Books

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

DOI： 10.1007/978-3-642-40885-4_22

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

Uniform semi-unification is a generalization of unification
its efficient algorithms have been extensively studied in (Kapur et al., 1994) and (Oliart&amp
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. © 2013 Springer-Verlag Berlin Heidelberg.

DOI： 10.1007/978-3-642-37064-9-7

Scopus

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

DOI： 10.11309/jssst.30.1_187

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

DOI： 10.11309/jssst.30.3_148

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

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. © 2012 Springer-Verlag.

DOI： 10.1007/978-3-642-33654-6_12

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

We give a method to prove con uence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, con uence 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 con uence 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 con uence of the original system is inferred from that of the completed system. © A REDUCTION-PRESERVING COMPLETION FOR PROVING CONFLUENCE.

DOI： 10.2168/LMCS-8(1:31)2012

Scopus

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

DOI： 10.11309/jssst.29.1_176

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

DOI： 10.11309/jssst.29.1_211

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

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

DOI： 10.4230/LIPIcs.RTA.2011.107

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

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.

DOI： 10.4230/LIPIcs.RTA.2011.91

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG  

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.

DOI： 10.1587/transinf.E93.D.963

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

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.

DOI： 10.4230/LIPIcs.RTA.2010.7

Web of Science

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Japan Society for Software Science and Technology  

書き換え帰納法(Reddy, 1989)は，項書き換えシステムにもとづく帰納的定理の自動証明法である．一般に，補題自動生成法において生成される補題はいつも正しい(定理である)とは限らないが，正しい補題のみを生成する補題自動生成法を健全であるという．発散鑑定法(Walsh, 1996)は書き換え帰納法のために提案された補題自動生成法であるが，健全ではない．本論文では，発散鑑定法の手続きの一部を健全一般化法(UrsoとKounalis, 2004)に置き換えることにより，単相項書き換えシステムに対して適用可能な，健全な発散鑑定法を提案する．また，これらの補題自動生成法を反証機能付き書き換え帰納法上に実装し，補題生成能力の比較実験を行う．これにより，(健全)発散鑑定法と健全一般化法が異なる有効範囲を持つことを明らかにし，従来から知られていた健全一般化法と我々の提案する健全発散鑑定法を組み合わせることにより，書き換え帰納法のためのより強力な健全補題自動生成法が実現できることを示す．

DOI： 10.11309/jssst.26.2_41

CiNii Article

CiNii Books

researchmap

その他リンク： https://jlc.jst.go.jp/DN/JALC/00334310578?from=CiNii

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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

DOI： 10.1007/978-3-642-02348-4_7

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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 sub-term 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.

DOI： 10.1007/978-3-642-04222-5_7

Web of Science

researchmap

記述言語：日本語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Japan Society for Software Science and Technology  

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

DOI： 10.11309/jssst.26.2_76

CiNii Article

CiNii Books

researchmap

その他リンク： https://jlc.jst.go.jp/DN/JALC/00334310592?from=CiNii

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.4230/LIPIcs.FSTTCS.2008.1737

researchmap

researchmap

researchmap

researchmap

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

DOI： 10.1007/11805618_18

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

DOI： 10.1007/11805618_20

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

DOI： 10.1007/978-3-540-32033-3_10

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1145/1069774.1069780

researchmap

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

DOI： 10.1007/978-3-540-25979-4_19

Web of Science

researchmap

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

DOI： 10.1007/3-540-44881-0_27

Web of Science

researchmap

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：WILEY-V C H VERLAG GMBH  

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.

DOI： 10.1002/malq.19990450402

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Springer Netherlands  

A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) 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 β-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 βη-normal proof in NJ. © 1999 Kluwer Academic Publishers.

DOI： 10.1023/A:1008254111992

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：SPRINGER-VERLAG BERLIN  

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 RUS for any non-collapsing non-duplicating terminating TRS S whose function symbols are contained in G, provided that for any l --> 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.

DOI： 10.1007/BFb0052375

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

DOI： 10.1007/BFb0056618

researchmap

記述言語：英語   掲載種別：学位論文（博士）  

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer Verlag  

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 τ-composable for a naive sort attachment τ. Here, a decomposition of a TRS R is a pair (R 1,R 2) of (not necessary disjoint) subsets of R such that R = R 1 U R 2
and for a naive sort attachment T a property ø of TRSs is said to be τ-composable if for any TRS R such that τ is consistent withR, ø(R1) Λ φ(R2) implies φ(R) where (R 1, R 2) is the decomposition of R by τ.

DOI： 10.1007/BFb0027006

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）  

DOI： 10.3217/jucs-003-11-1134

researchmap

researchmap

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Article

CiNii Books

researchmap

記述言語：英語   出版者・発行元：ELSEVIER SCIENCE BV  

DOI： 10.1016/j.tcs.2012.09.009

Web of Science

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Article

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Article

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Article

CiNii Books

researchmap

researchmap

researchmap

記述言語：英語  

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. © 2012 Springer-Verlag.

DOI： 10.1007/978-3-642-33654-6_12

Scopus

researchmap

DOI： 10.11309/jssst.29.1_211

researchmap

DOI： 10.11309/jssst.29.1_211

researchmap

DOI： 10.11309/jssst.29.1_176

researchmap

記述言語：英語   出版者・発行元：TECH UNIV BRAUNSCHWEIG  

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-criticalpairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also(partially) work seven 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.

DOI： 10.2168/LMCS-8(1:31)2012

Web of Science

researchmap

記述言語：英語   出版者・発行元：TECH UNIV BRAUNSCHWEIG  

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-criticalpairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also(partially) work seven 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.

DOI： 10.2168/LMCS-8(1:31)2012

Web of Science

researchmap

researchmap

DOI： 10.11309/jssst.29.1_176

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Article

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Article

CiNii Books

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

記述言語：英語   出版者・発行元：SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

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

DOI： 10.4230/LIPIcs.RTA.2011.107

Web of Science

researchmap

researchmap

記述言語：英語   出版者・発行元：SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

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

DOI： 10.4230/LIPIcs.RTA.2011.107

Web of Science

researchmap

DOI： 10.4230/LIPIcs.RTA.2011.91

researchmap

記述言語：英語   出版者・発行元：SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

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.

DOI： 10.4230/LIPIcs.RTA.2011.91

Web of Science

researchmap

researchmap

researchmap

記述言語：英語   出版者・発行元：IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG  

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.

DOI： 10.1587/transinf.E93.D.963

Web of Science

researchmap

researchmap

researchmap

記述言語：英語   出版者・発行元：Institute of Electronics, Information and Communication, Engineers, IEICE  

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. Copyright © 2010 The Institute of Electronics, Information and Communication Engineers.

DOI： 10.1587/transinf.E93.D.963

Scopus

researchmap

記述言語：日本語   出版者・発行元：Japan Society for Software Science and Technology  

書き換え帰納法(Reddy, 1989)は，項書き換えシステムにもとづく帰納的定理の自動証明法である．一般に，補題自動生成法において生成される補題はいつも正しい(定理である)とは限らないが，正しい補題のみを生成する補題自動生成法を健全であるという．発散鑑定法(Walsh, 1996)は書き換え帰納法のために提案された補題自動生成法であるが，健全ではない．本論文では，発散鑑定法の手続きの一部を健全一般化法(UrsoとKounalis, 2004)に置き換えることにより，単相項書き換えシステムに対して適用可能な，健全な発散鑑定法を提案する．また，これらの補題自動生成法を反証機能付き書き換え帰納法上に実装し，補題生成能力の比較実験を行う．これにより，(健全)発散鑑定法と健全一般化法が異なる有効範囲を持つことを明らかにし，従来から知られていた健全一般化法と我々の提案する健全発散鑑定法を組み合わせることにより，書き換え帰納法のためのより強力な健全補題自動生成法が実現できることを示す．

DOI： 10.11309/jssst.26.2_41

CiNii Article

CiNii Books

researchmap

その他リンク： https://jlc.jst.go.jp/DN/JALC/00334310578?from=CiNii

記述言語：英語   出版者・発行元：SPRINGER-VERLAG BERLIN  

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 sub-term 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.

DOI： 10.1007/978-3-642-04222-5_7

Web of Science

researchmap

記述言語：英語  

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 &amp
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. © 2009 Springer Berlin Heidelberg.

DOI： 10.1007/978-3-642-04222-5_7

Scopus

researchmap

記述言語：英語   出版者・発行元：SPRINGER-VERLAG BERLIN  

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

DOI： 10.1007/978-3-642-02348-4_7

Web of Science

researchmap

記述言語：日本語   出版者・発行元：Japan Society for Software Science and Technology  

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

DOI： 10.11309/jssst.26.2_76

CiNii Article

CiNii Books

researchmap

その他リンク： https://jlc.jst.go.jp/DN/JALC/00334310592?from=CiNii

DOI： 10.11309/jssst.26.2_76

researchmap

記述言語：英語  

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 &amp
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. © 2009 Springer Berlin Heidelberg.

DOI： 10.1007/978-3-642-02348-4_7

Scopus

researchmap

DOI： 10.11309/jssst.26.2_41

researchmap

researchmap

researchmap

researchmap

researchmap

記述言語：英語   出版者・発行元：情報処理学会  

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 firstorder 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 (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 firstorder 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.

CiNii Article

CiNii Books

researchmap

その他リンク： http://hdl.handle.net/10119/8515

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

ラムダ計算のパターンマッチングに基づくプログラム自動変換法の枠組みがHuet-Lang (1978) によって提案されている．本発表では，項書き換えシステムに基づくパターンマッチングを実現するために木準同形写像の概念を導入する．はじめに，項パターンマッチングを実現するためのアルゴリズムを提案し，アルゴリズムの正当性を示す．さらに，項パターンマッチングアルゴリズムを項書き換えシステムに適用し，木準同形写像がリダクション関係を保存することを証明する．また，正規形が保存されるべきクラスを示し，木準同形写像によってそのクラスの正規形が保存されるための十分条件を示す．本発表におけるパターンマッチングアルゴリズムは，操作的意味論に基づくプログラム変換の正当性を示す第一歩となると期待される．Huet and Lang (1978) developed a framework of automated program transformation using second-order matching algorithm of lambda terms. In this paper, we present a second-order matching algorithm based on term rewriting in which higher-order substitutions are represented by tree homomorphisms. We present term pattern matching algorithm and show its correctness; we then apply the algorithm to match term rewriting systems on term patterns with term rewriting systems. We then show reduction is preserved by tree homomorphisms and give a sufficient condition of tree homomorphisms that map suitable normal patterns to normal terms. Our matching algorithm is a first step to study the correctness of program transformations based on the operational semantics.

CiNii Article

CiNii Books

researchmap

記述言語：英語  

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. Copyright 2005 ACM.

DOI： 10.1145/1069774.1069780

Scopus

researchmap

researchmap

researchmap

researchmap

記述言語：英語   出版者・発行元：SPRINGER-VERLAG BERLIN  

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.

Web of Science

researchmap

記述言語：英語  

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. Copyright 2005 ACM.

DOI： 10.1145/1069774.1069780

Scopus

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

記述言語：英語   出版者・発行元：Wiley-VCH Verlag  

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.

DOI： 10.1002/malq.19990450402

Scopus

researchmap

researchmap

記述言語：英語   出版者・発行元：WILEY-V C H VERLAG GMBH  

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.

Web of Science

researchmap

researchmap

researchmap

researchmap

DOI： 10.1007/BFb0052375

researchmap

記述言語：英語   出版者・発行元：SPRINGER-VERLAG BERLIN  

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 RUS for any non-collapsing non-duplicating terminating TRS S whose function symbols are contained in G, provided that for any l --> 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.

DOI： 10.1007/BFb0052375

Web of Science

researchmap

記述言語：英語   出版者・発行元：Springer Verlag  

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 τ-composable for a naive sort attachment τ. Here, a decomposition of a TRS R is a pair (R 1,R 2) of (not necessary disjoint) subsets of R such that R = R 1 U R 2
and for a naive sort attachment T a property ø of TRSs is said to be τ-composable if for any TRS R such that τ is consistent withR, ø(R1) Λ φ(R2) implies φ(R) where (R 1, R 2) is the decomposition of R by τ.

DOI： 10.1007/BFb0027006

Scopus

researchmap

researchmap

researchmap

DOI： 10.1007/BFb0027006

researchmap

記述言語：英語   出版者・発行元：北陸先端科学技術大学院大学  

CiNii Article

CiNii Books

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

researchmap

会議種別：ポスター発表  

researchmap

researchmap

researchmap

researchmap

会議種別：ポスター発表  

researchmap

researchmap