Abstracts

• Masahiko Sakai and Hidetomo Nabeshima,
  Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers,
  IEICE Transaction on Information and Systems, Vol. E98-D, No. 6, pp. 1121-1127, Jun 2015.
  
  ABSTRACT
  Pseudo-Boolean (PB) problems are Integer Linear Problem restricted to 0-1 variables. This paper discusses on acceleration techniques of PB-solvers that employ SAT-solving of combined CNFs each of which is produced from each PB-constraint via a binary decision diagram (BDD). Specifically, we show
  (i) an efficient construction of a reduced ordered BDD (ROBDD) from a constraint in band form ℓ <= 〈Linear term〉 <= h,
  (ii) a CNF coding that produces two clauses for some nodes in an ROBDD obtained by (i), and
  (iii) an incremental SAT-solving of the binary/alternative search for minimizing values of a given goal function.
  We implemented the proposed constructions and report on experimental results.
  e98-d_6_1121.pdf Copyright(C) 2015 IEICE, on line transaction
  
  
  
  
• Masanori Nagashima, Masahiko Sakai and Toshiki Sakabe
  Determinization of Conditional Term Rewriting Systems,
  Theoretical Computer Science, Vol.464, pp.72-89, 2012, DOI. 10.1016/j.tcs.2012.09.005.
  
  ABSTRACT
  This paper discusses determinization of conditional term rewriting systems with oriented constructor rules. We present a rule-based transformation system, which transforms a non-deterministic one into a deterministic one, together with examples of the transformation. We prove that the transformation system is simulation sound and simulation complete. We also prove that the transformation system is complete for some class by introducing a strategy for the transformation system.
  pre-print
  
  
• Masahiko Sakai, Mizuhito Ogawa
  Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent,
  Information Processing Letters, Vol.110, Issues 18-19, pp.810--814 (2010 Sep).
  
  ABSTRACT
  This paper shows that weakly-non-overlapping, non-collapsing and shallow term rewriting systems are confluent, which is a new sufficient condition on confluence for non-left-linear systems.
  IPL2010.pdf
  
  
• Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe
  Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs
  IEICE Trans. on Information and Systems, Vol.E93-D, No.5, pp.953-962(2010,5).
  
  ABSTRACT
  In this paper, we show that (1) the termination and the innermost termination properties are decidable for the class of term rewriting systems (TRSs for short) all of whose dependency pairs are right-linear and right-shallow, (2) the innermost termination is decidable for the class of TRSs all of whose dependency pairs are shallow, and (3) the termination and the innermost termination of a given term are decidable for the class of TRSs all of whose dependency pairs are right-shallow. The key observation common to these two classes is as follows: for every TRS in the class, we can construct, by using the dependency-pairs information, a finite set of terms such that if the TRS is non-terminating then there is a looping sequence beginning with a term in the finite set. This fact is obtained by modifying the analysis of argument propagation in shallow dependency pairs proposed by Wang and Sakai in 2006. However we gained a great benefit that the resulted procedures do not require any decision procedure of reachability problem, because known decidable classes of reachability problem is not larger than classes discussing in this paper.
  e93-d_5_953.pdf Copyright(C) 2010 IEICE, on line transaction
  
  
• 馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗: 基本対象関数に基づく節を持つCNF論理式の充足可能性判定, 電子情報通信学会論文誌, Vol.J93-D, No.1, pp.1--9(2010,1).
  Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari
  Solving Satisfiability of CNF Formulas with Clauses based on Elementary Symmetric Functions, IEICE Trans. on Information and Systems, Vol.J93-D, No.1, pp.1-9(2010) (in Japanese).
  
  概要
  近年，高速な充足可能性判定ツール（SATソルバ）の開発が進んでいる． これらのツールでは，BCPと呼ばれる変数値の推論とそのバックトラックが実行時間の大半を占めていることが多く，その処理を効率化できればSATソルバの高速化が可能となる． 本論文では，「$n$個の変数のうち，ちょうど$k$個が真」という基本対称関数に基づく節を導入することにより入力する論理式の大きさが減少することに注目し，SATソルバの効率化を目指す． 実際にSATソルバでよく用いられるDPLLアルゴリズムを、基本対称関数に基づく節を導入したCNFを扱えるよう拡張し，その有効性を実験により確かめた．
  ABSTRACT
  In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulas, have been developed. Since most of execution time of these solvers is used for value-inferences of variables, called boolean constraint propagation (BCP), and their backtracking, improvements of BCP contribute the efficiency. This paper attempts to improve the efficiency of SAT solvers, focusing on the fact that the number of clauses of a CNF formula decreases by introducing clauses based on elementary symmetric functions. By extending DPLL algorithm, often used in SAT solvers, to treat CNFs having clauses based on elementary symmetric functions, the effectiveness of the approach is shown by experiments.
  j93-D-1.pdf Copyright(C) 2010 IEICE, on line transaction
  
  
• Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Frederic Blanqui
  Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems, IEICE Trans. on Information and Systems, Vol.E92-D, No.10, pp.2007-2015(2009,10).
  
  ABSTRACT
  Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include lambda-abstraction but STRSs do not, we restructure the static dependency pair method to allow lambda-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.
  e92-d_10_2007.pdf Copyright(C) 2009 IEICE, on line transaction
  
  
• Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari and Toshiki Sakabe
  Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems, IPSJ Transactions on Programming, Vol.2, No.3, pp.162-174(2009,7).
  
  ABSTRACT
  The reachability problem for given an initial term, a goal term, and a term rewriting system (TRS) is to decide whether the initial one is reachable to the goal one by the TRS or not. A term is shallow if each variable in the term occurs at depth 0 or 1. Innermost reduction is a strategy that rewrites innermost redexes, and context-sensitive reduction is a strategy in which rewritable positions are indicated by specifying arguments of function symbols. In this paper, we show that the reachability problem under context-sensitive innermost reduction is decidable for linear right-shallow TRSs. Our approach is based on the tree automata technique that is commonly used for analysis of reachability and its related properties. We show a procedure to construct tree automata accepting the sets of terms reachable from a given term by context-sensitive innermost reduction of a given linear right-shallow TRS.
  IPSJ-TPRO0203003.pdf All Rights Reserved, Copyright (C) Information Processing Society of Japan.
  
  
• Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa
  Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes, IPSJ Transactions on Programming, Vol.2, No.2, pp.144-165(2009,3).
  
  ABSTRACT
  The present paper discusses a head-needed strategy and its decidable classes of higher-order rewrite systems (HRSs), which is an extension of the head-needed strategy of term rewriting systems (TRSs). We discuss strong sequential and NV-sequential classes having the following three properties, which are mandatory for practical use: (1) the strategy reducing a head-needed redex is head normalizing (2) whether a redex is head-needed is decidable, and (3) whether an HRS belongs to the class is decidable. The main difficulty in realizing (1) is caused by the beta-reductions induced from the higher-order reductions. Since beta-reduction changes the structure of higher-order terms, the definition of descendants for HRSs becomes complicated. In order to overcome this difficulty, we introduce a function, PV, to follow occurrences moved by beta-reductions. We present a concrete definition of descendants for HRSs by using PV and then show property (1) for orthogonal systems. We also show properties (2) and (3) using tree automata techniques, a ground tree transducer (GTT), and recognizability of redexes.
  IPSJ09-1.pdf All Rights Reserved, Copyright (C) Information Processing Society of Japan.
  
  
• Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa
  Recognizability of Redexes for Higher-Order Rewrite Systems, IPSJ Transactions on Programming, Vol.2, No.2, pp.166-175(2009,3).
  
  ABSTRACT
  It is known that the set of all redexes for a left-linear term rewriting system is recognizable by a tree automaton, which means that we can construct a tree automaton that accepts redexes. The present paper extends this result to Nipkow's higher-order rewrite systems, in which every left-hand side is a linear fully-extended pattern. A naive extension of the first-order method causes the automata to have infinitely many states in order to distinguish bound variables in lambda-terms, even if they are closed. To avoid this problem, it is natural to adopt de Bruijn notation, in which bound variables are represented as natural numbers (possibly finite symbols, such as 0, s(0), and s(s(0))). We propose a variant of de Bruijn notation in which only bound variables are represented as natural numbers because it is not necessary to represent free variables as natural numbers.
  IPSJ09-2.pdf  All Rights Reserved, Copyright (C) Information Processing Society of Japan.
  
  
• Keiichirou Kusakari, Masahiko Sakai:
  Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting Systems, Applicable Algebra in Engineering, Communication and Computing, Vol.18, No.5, pp.407-431(2007,10).
  
  ABSTRACT
  We enhance the dependency pair method in order to prove termination using recursive structure analysis in simply-typed term rewriting systems, which is one of the computational models of functional programs. The primary advantage of our method is that one can exclude higher-order variables which are difficult to analyze theoretically, from recursive structure analysis. The key idea of our method is to analyze recursive structure from the view point of strong computability. This property was introduced for proving termination in typed lambda-calculus, and is a stronger condition than the property of termination. The difficulty in incorporating this concept into recursive structure analysis is that because it is defined inductively over type structure, it is not closed under the subterm relation. This breaks the correspondence between strong computability and recursive structure. In order to guarantee the correspondence, we propose plain function-passing as a restriction, which is satisfied by many non-artificial functional programs.
  aaecc07.pdf
  
  
• Keita Sakurai, Keiichirou Kusakari, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
  Usable Rules and Labeling Product-Typed Terms for Dependency Pair Method in Simply-Typed Term Rewriting Systems, IEICE Transactions on Information and Systems, Vol.J90-D, No.4, pp.978-989(2007,4) (in Japanese).
  
  
• Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe
  Primitive Indeuctive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting, IEICE Trans. on Information and Systems, Vol.E88-D, No.12, pp.2715-2726(2005,12).
  
  ABSTRACT
  Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems.
  ieice05.pdf  copyright(C)2005 IEICE   on line transaction
  
  
• Keita Sakurai, Keiichirou Kusakari, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe
  Proving Sufficient Completeness of Functional Programs based on Recursive Structure Analysis and Strong Computability, In Proceedings of the Forum on Information Technology 2005 (FIT2005), Information Technology Letters, LA-001, pp.1-4(2005) (in Japanese).
  
  
• Naoki Nishida, Masahiko Sakai, Toshiki Sakabe: Generation of Inverse Computation Programs for Constructor Term Rewriting Systems, Tran. of IEICE, Vol.J88-D-I-8(2005), pp,1171-1183 (in Japanese).
  
  
• Masahiko Sakai, Keiichirou Kusakari: On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems, IEICE Trans. on Information and Systems, Vol.E88-D, No.3, pp.583-593(2005).
  
  ABSTRACT
  This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. In the first order case, the termination of term rewriting systems are proved by showing the non-existence of an infinite R-chain of the dependency pairs. However, the termination and the non-existence of an infinite R-chain do not coincide in the higher-order case. We introduce a new notion of dependency forest that characterize infinite reductions and infinite R-chains, and show that the termination property of higher-order rewrite systems R can be checked by showing the non-existence of an infinite R-chain, if R is strongly linear or non-nested.
  IEICE04.pdf   copyright(C)2005 IEICE   on line transaction
  
  
• Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari: Program Generation by Transformation from Quantified Equational Specifications, Computer Software, Japan Society for Software Science and Technology, Vol.21, No.4, pp.49-54(2004) (in Japanese).
  
  
• Naoki Nishida, Masahiko Sakai, Toshiki Sakabe: Improving Efficiency of Linear Constructor Term Rewriting Systems with Extra Variables, Computer Software, Japan Society for Software Science and Technology, Vol.21, No.3, pp.40-47(2004) (in Japanese).
  
  
• Naoki Nishida, Masahiko Sakai, Toshiki Sakabe: A Computation Model of Term Rewriting Systems with Extra Variables, Computer Software, Japan Society for Software Science and Technology, Vol.20, No.5, pp.85-89(2003) (in Japanese).
  
  
• Mihoko Horie, Masahiko Sakai, Toshiki Sakabe: Typing Exceptions in an Object Calculus, Computer Software, Japan Society for Software Science and Technology, Vol.20, No.2, pp.54-58(2003) (in Japanese).
  
  
• Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Generation of a TRS Implementing the Imverses of Pure Treeless Function, Computer Software, Japan Society for Software Science and Technology, Vol.19, No.1, pp.29-33(2002) (in Japanese).
  
  
• Masahiko Sakai, Yoshitsugu Watanabe, Toshiki Sakabe: An Extension of Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems, IEICE Trans. on Information and Systems, Vol.E84-D, No.8, pp.1025-1032(2001,8).
  
  ABSTRACT
  This paper explores how to extend the dependency pair technique for proving termination of higher-order rewrite systems. We show that the termination property of higher-order rewrite systems can be checked by the non-existence of an infinite $R$-chain, which is an extension of Arts' and Giesl's result for the first-order case. It is clarified that the subterm property of the quasi-ordering, used for proving termination automatically, is indispensable.
  IEICE-E84-D-8.pdf   copyright(C)2001 IEICE   on line transaction
  
  
• Sun Hui Hong, Masahiko Sakai, Toshiki Sakabe, Confluence of Orthogonal Metaterm Rewriting Calculus with Rules Containing rules, Computer Software, Japan Society for Software Science and Technology, Vol.17,No.6, pp.47-51(2000) (in Japanese).
  
  
• Masahiko Sakai, Yoshihito Toyama: Semantics and Strong Sequentiality of Priority Term Rewriting Systems, Theoretical Computer Science, Vol.208, pp.87-110(1998).
  
  ABSTRACT
  This paper gives an operational semantics of priority term rewriting systems (PRSs) by using conditional systems, whose reduction relation is decidable and stable under substitution. We also define the class of strongly sequential PRSs and show that this class is decidable. Moreover, we show that the index rewriting of strongly sequential PRSs gives a normalizing strategy.
  
  
• Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama: An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems, IEICE Trans. on Information and Systems, Vol.E81-D, No.9, pp.988-996(1998,9).
  
  ABSTRACT
  Simplification orderings, like the recursive path ordering and the improved recursive decomposition ordering, are widely used for proving the termination property of term rewriting systems. The improved recursive decomposition ordering is known as the most powerful simplification ordering. Recently Jouannaud and Rubio extended the recursive path ordering to higher-order rewrite systems by introducing an ordering on type structure. In this paper we extend the improved recursive decomposition ordering for proving termination of higher-order rewrite systems. The key idea of our ordering is a new concept of pseudo-terminal occurrences.
  
  
• Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama: Index Reduction of Overlapping Strongly Sequential Systems, IEICE Trans. on Information and Systems, Vol.E81-D, No.5, pp.419-426(1998,5).
  
  ABSTRACT
  Huet and Levy showed that index reduction is a normalizing strategy for every orthogonal strongly sequential term rewriting system. Toyama extended this result to root balanced joinable strongly sequential systems. In this paper, we present a class including all root balanced joinable strongly sequential systems and show that index reduction is normalizing for this class. We also propose a class of left-linear (possibly overlapping) NV-sequential systems having a normalizing strategy.
  PDF   copyright(C)1998 IEICE   on line transaction
  
  
  
• Masahiko Sakai, Left-Incompatible Term Rewriting Systems and Functional Strategy, IEICE Trans. on Information and System E80-D 12(1997), 1176-1182.
  
  ABSTRACT
  This paper extends left-incompatible term rewriting systems defined by Toyama et al. It is also shown that the functional strategy is normalizing in the class, where the functional strategy is the reduction strategy that finds index by some rule selection method and top-down and left-to-right lazy pattern matching method.
  PDF   copyright(C)1997 IEICE   on line transaction
  
  
• H.Kasuya, M.Sakai, S.Yamamoto, K.Agusa, Term Set Rewriting Systems and their Confluent Property, Tran. of IEICE J80-D-I 4(1997), 325-334 (in Japanese).
  
  
• Y.Takahasi, M.Sakai, Y.Toyama, On the Confluence Property of Conditional Term Rewriting Systems, Trans. of IEICE J79-D-I 11(1996), 1-6 (in japanese).
  
  
• S.Yamamoto, R.Ishikawa, M.Sakai, K.Agusa, An Implementation of TRS on Shared Memory Multiprocessors, Trans. of IEICE J78-D-I 6(1995), 559-562 (in Japanese).
  
  
• M.Kawakita, M.Sakai, S.Yamamoto, K.Agusa, A model for reuse based on formal specifications, Trans. of IPSJ 36 5(1995), 1050-1058 (in Japanese).
  
  
• Y.Hamaguchi, M.Sakai, S.Yamamoto, K.Agusa, Error Description on Algebraic Specification and its Automatic Addition, Trans. of IEICE J78-D-I 3 (1995) 323-330 (in japanese).
  
  
• M.Sakai, T.Sakabe, Y.Inagaki, Cover Set Induction for Verifying Algebraic Specifications, Trans. of IEICE J75-D-I 3 (1992), 170-179 (in japanese).
  
  
• M.Sakai, T.Sakabe, Y.Inagaki, Algebraic Specification and Automatic Generation of Compilers, Trans. of IEICE J73-D-I 12 (1990), 979-989 (in japanese).
  
  
• M.Sakai, T.Sakabe, Y.Inagaki, LASS, Language Processor Generator based on Algebraic Specification Method, Trans. of IEICE J73-D-I 10 (1990), 829-838 (in japanese).
  
  
• M.Sakai, T.Sakabe, Y.Inagaki, Direct Implementation System of Algebraic Specification of Abstract Data Types, Computer Software, Japan Society for Software Science and Technology, Vol.3, No.4 pp.16-27 (1988) (in japanese).
  
  
• Yoshiharu Kojima and Masahiko Sakai:
  Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems,
  Proc. of 19th Int'l Conference on Rewriting Techniqes and Applications, Hagenberg, 2008(RTA2008), LNCS 5117, pp.187-201.
  
  ABSTRACT
  A reachability problem is a problem used to decide whether s is reachable to t by R or not for a given two terms s, t and a term rewriting system R. Since it is known that this problem is undecidable, effort has been devoted to finding subclasses of term rewriting systems in which the reachabiliy is decidable. However few works on decidability exist for innermost reduction strategy or context-sensitive rewriting.
  In this paper, we show that innermost reachability and context-sensitive reachability are decidable for linear right-shallow term rewriting systems. Our approach is based on the tree automata technique that is commonly used for analysis of reachability and its related properties.
  pre-print(pdf)
  
  
• Naoki Nishida and Masahiko Sakai
  Completion as Post-Process in Program Inversion of Injective Functions, Proc. of 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS2007), Hagenberg, pp.61-75 (2008).
  ABSTRACT
  Given a constructor term rewriting system defining injective functions, the inversion compiler in [19.20] generates a confluent conditional term rewriting system defining completely the inverse relations of the injective functions, and then the compiler unravels the conditional system into an unconditional term rewriting system. In general, the unconditional system is not confluent and thus not computationally equivalent to the conditional system. In this paper, we propose a modification of Knuth-Bendix completion procedure as a post-process of the inversion compiler. Given a confluent and operationally terminating conditional system, the procedure takes the unraveled one of the conditional system as input, and it returns a convergent system that is computationally equivalent to the conditional system if it halts successfully. We also adapt the modification to the conditional systems that are not confluent but innermost-confluent. The implementation of our method succeeds in generating innermost-convergent inverse systems for all examples shown by Kawabe et al. where all main and axillary functions are injective.
  pre-print (proceeding version in pdf) 
  
  
• Masahiko Sakai and Wang Yi
  Undecidable Properties on Length-Two String Rewriting Systems, Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS2007), Paris, pp.43-57 (2007).
  Electric Notes in Theoretical Computer Science, Vol.204, No.4, pp.53-69 (2008,4).
  
  ABSTRACT
  Length-two string rewriting systems are length preserving string rewriting systems that consist of length-two rules. This paper shows that confluence, termination, left-most termination and right-most termination are undecidable properties for length-two string rewriting systems. This results mean that these properties are undecidable for the class of linear term rewriting systems in which depth-two variables are allowed in both-hand sides of rules.
  pre-print (proceeding version in pdf)  pre-print (post proceeding version in pdf) 
  
  
• Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe
  Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems,
  Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS2007), Paris, pp.16-27 (2007).
  Electric Notes in Theoretical Computer Science, Vol.204, No4, pp.21-34 (2008,4).
  ABSTRACT
  Wang and Sakai showed that the termination problem is a d ecidable property for the class of semi-constructor term rewriting systems, which is a superclass of the class of right ground term rewriting systems. The decidability was shown by the fact that every non-terminating TRS in the class has a loop. In this paper we modify the Wang and Sakai's proof to show that both innermost termination and mu-termination are decidable properties for the class of semi-constructor TRSs.
  pre-print (proceeding version in pdf)  pre-print (post proceeding version in pdf) 
  
  
• Naoki Nishida, Masahiko Sakai, and Terutoshi Kato. Convergent Term Rewriting Systems for Inverse Computation of Injective Functions, Proc. of the 9th International Workshop on Termination, Paris, 2007(WST'07)
  
  ABSTRACT
  This paper shows a sufficient syntactic condition for constructor TRSs whose inverse-computation CTRSs generated by Nishida, Sakai and Sakabe's inversion compiler are confluent and operationally terminating. By replacing the unravelling at the second phase of the compiler with Sebanuta and Rosu's transformation, we generate convergent TRSs for inverse computation of injective functions satisfying the sufficient condition.
  full version 
  
  
• Wang Yi and Masahiko Sakai: Decidability of Termination for Semi-Constructor TRSs, Left-Linear Shallow TRSs and Related Systems, Proc. of 17th Int'l Conference on Rewriting Techniqes and Applications, Seattle, 2006(RTA2006), LNCS 4098, pp.343-356.
  
  ABSTRACT
  We consider several classes of term rewriting systems and prove that termination is decidable for these classes. By showing the cycling property of infinite dependency chains, we prove that termination is decidable for semi-constructor case, which is a superclass of right-ground TRSs. By analyzing argument propagation cycles in the dependency graph, we show that termination is also decidable for left-linear shallow TRSs. Moreover we extend these by combining these two techniques.
  (rta06.ps.gz)  (rta06.pdf)  (errata)
  (bug fixed version ps.gz)  (bug fixed version pdf)
  
  
• Wang Yi and Masahiko Sakai: On Non-looping Term Rewriting, Proc. of Eighth International Workshop on Termination, Seattle, 2006(WST2006), pp.17-21.
  
  ABSTRACT
  Proving non-termination is important for instance if one wants to decide termination for given TRSs. Although the usual method is to find looping reduction sequences, there are non-looping infinite reduction sequences. We find some new interesting non-looping examples and propose new definitions of inner-looping sequence and normal sequence to classify them. We also show the undecidability of the existence of inner-looping sequence.
  (wst06.ps.gz)  (wst06.pdf)
  
  
• Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai: Transformation for Refining Unraveled Conditional Term Rewriting Systems, Proc. of 6th International Workshop on Reduction Strategies in Rewriting and Programming, Seattle, 2006(WRS2006), pp.34-48
  
  ABSTRACT
  Unravelings, which transform conditional term rewriting systems (CTRSs) into unconditional term rewriting systems, are useful for analyzing properties of CTRSs. To compute reduction sequences of CTRSs, the restriction by a particular context-sensitive and membership condition is imposed on reductions of the unraveled CTRSs. The condition is determined by extra function symbols introduced due to the unravelings. In this paper, we propose a method to weaken the restriction, that is, to reduce the number of extra symbols. We first improve the unraveling for deterministic CTRSs, and then propose a transformation that folds two successively used rewrite rules in the unraveled CTRSs, which satisfy a condition, to a rewrite rule that simulates reductions by the two rules.
  (wrs06.ps.gz)  (wrs06.pdf)
  
  
• Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe: Partial Inversion of Constructor Term Rewriting Systems, 16th Int'l Conference on Rewriting Techniqes and Applications, Nara, 2005(RTA2005), Springer, LNCS 3467, pp.264-278.
  
  ABSTRACT
  Partial-inversion compilers generate programs which compute some unknown inputs of given programs from a given output and the rest of inputs whose values are already given. In this paper, we propose a partial-inversion compiler of constructor term rewriting systems. The compiler automatically generates a conditional term rewriting system, and then unravels it to an unconditional system. To improve the efficiency of inverse computation, we show that innermost strategy is usable to obtain all solutions if the generated system is right-linear.
  (rta05.ps.gz)  (rta05.pdf)
  
  
• Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe: Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof, 12th Int'l Workshop on Functional and (Constraint) Logic Programming Valencia, Spain, June 12-13, 2003(WFLP'03).
  
  ABSTRACT
  Term rewriting systems (TRSs) are extended by allowing to contain extra variables in their rewrite rules. We call the extended systems EV-TRSs. They are ill-natured since every one-step reduction by their rules with extra variables is infinitely branching and they are not terminating. To solve these problems, this paper extends narrowing on TRSs into that on EV-TRSs and show that it simulates the reduction sequences of EV-TRSs as the narrowing sequences starting from ground terms. We prove the soundness of ground narrowing-sequences for the reduction sequences . We prove the completeness for the case of right-linear systems, and also for the case that no redex in terms substituted for extra variables is reduced in the reduction sequences. Moreover, we give a method to prove the termination of the simulation, extending the termination proof of TRSs using dependency pairs, to that of narrowing on EV-TRSs starting from ground terms.
  (wflp03.ps.gz)  (wflp03.pdf)
  
  
• Masahiko Sakai, Kouji Okamoto, Toshiki Sakabe: Innermost Reductions Find All Normal Forms on Right-Linear Terminating Overlay TRSs, Proc. of 3rd Int'l Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain, June 8, 2003 (WRS'03). (wrs03.ps.gz)  (wrs03.pdf)
  
  
• Hideto Kasuya, Masahiko Sakai and Kiyoshi Agusa: Descendants and Head Normalization of Higher-Order Rewrite Systems, Sixth International Symposium on Functional and Logic Programming, Aizu, Japan, September 15-17, in LNCS 2441, pp.198-211(2002). (flops02_13.ps.gz)  (flops02_13.pdf)
  
  
• Masahiko Sakai and Keiichirou Kusakari: On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique, The First International Workshop on Higher-Order Rewriting (HOR'02), Copenhagen, Denmark, July 21, p.25(2002). (HOR02.ps.gz)  (HOR02.pdf)
  
  
• Masahiko Sakai and Keiichirou Kusakari: On New Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems, The International Workshop on Rewriting in Proof and Computation (RPC'01), Sendai, Japan, October 25-27, pp.176-187(2001). (rpc01a.ps.gz)  (rpc01a.pdf)
  
  
• Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe: Generation of Inverse Term Rewriting Systems for Pure Treeless Functions, The International Workshop on Rewriting in Proof and Computation (RPC'01), Sendai, Japan, October 25-27, pp.188-198(2001). (rpc01b.ps.gz)  (rpc01b.pdf)
  
  
• M.Sakai, Y.Toyama, Semantics and Strong Sequentiality of Priority Term Rewriting Systems, Proc. on Rewriting Techniques and Applications at New Brunswick NJ USA (RTA'96), LNCS 1103 (1996), 377-391. (rta96.ps.gz)
  
  
• Yasuyoshi Inagaki, Hidehiko Kita, Masahiko Sakai, Toshiki Sakabe: An Algebraic Approach to Specification of Programming Languages and Automatic Generation of Language Processors, Proc. Regional Symp. on Computer Sci. and its Applications, in Thai, pp.35-1--35-25(1987).
  
  
• Keita Uchiyama，Masahiko Sakai，Toshiki Sakabe，Keiichirou kusakari， Naoki Nishida
  Decidability of Termination Properties for Term Rewriting Systems consisting of Shallow Dependency Pairs, Tech. Rep. of IEICE (SS2008-45), Vol.108, No.362, pp.37-42(2008).
  
  ABSTRACT
  In this paper, we show some decidable properties: termination, innermost termination and context-sensitive termination for the class of term rewriting systems (TRSs for short) whose dependency pairs are right-ground or right-linear shallow. Here, the right-linearity is not required for innermost termination. By analyzing argument propagation in the dependency pairs proposed by Wang and Sakai \cite{wang:2006}, we show that there exists a looping sequence if a TRS in the class is not terminating. One of benefit of our approach is that decision of reachability and joinability is not necessary in the decision procedure.
  (IEICE-SS08-45.pdf)   copyright(C)2008 IEICE
  
  
• M.Sakai, H.Kasuya, S.Yamamoto, K.Agusa, On Term Set Rewriting System, Workshop on foundation of information theory at Tateshina, LA symposium (1994), 45-48. (LA94.ps.gz)
  
  
• M.Sakai, The functional strategy, The Extended Left-incompatible Systems, Tech. Rep. of IEICE SS95-17 (1995), 55-62. (SS95-17.ps.gz)
  
  
• Masahiko Sakai : Innermost Terminating Right-Linear Overlay Term Rewriting Systems are Terminating, note, Oct. 2003(sin-sn-031015.pdf)