Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 101 - 120 of about 247 ／ All the affair displays >>

On Lemma Generation in Rewriting Induction for Constrained Term Rewriting Systems by Using Commutativity of Function Composition

Ryutaro Kuriki, Naoki Nishida, and Masahiko Sakai

Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( M4-1 ) page： 1 2014.9

On a Necessary and Sufficient Condition for Equations to Represent Equivalence of Functions in Constrained Term Rewriting

Takumi Kataoka, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( M4-4 ) page： 1 2014.9

On a Sufficient Condition for Argument Filterings to Preserve Equivalence between Functions in Term Rewriting

Yoshifumi Kawamoto, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( M4-2 ) page： 1 2014.9

On a Procedure for Proving Confluence of Conditional Term Rewriting Systems by Using Condition Elimination

Makishi Yanagisawa, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( M4-4 ) page： 1 2014.9

On Reducing the Frequency of Checking Validity of Presburger Formulas in the Dependency Pair Method for Constrained Term Rewriting Systems

Tomoya Ueyama, Naoki Nishida, Toshiki Sakabe, and Masahiko Sakai

Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( M4-5 ) page： 1 2014.9

On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants Reviewed

Naoki Nishida and Takumi Kataoka

Proceedings of the 14th International Workshop on Termination (WST 2014) page： 1-5 2014.7

Authorship：Lead author Language：English

Recently, to analyze procedural programs by using techniques in the field of term rewriting, several transformations of a program into a rewrite system have been developed. Such transformations are basically complete in the sense of computation, and e.g., termination of the rewrite system ensures termination of the program. However, in general, termination of the program is not preserved by the transformations and, thus, the preservation of termination is a common interesting problem. In this paper, we discuss the improvement of a transformation from a simple procedural program over integers into a constrained term rewriting system by appending loop invariants to loop conditions of "while" statements so as to preserve termination as much as possible.

Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems Reviewed

Karl Gmeiner and Naoki Nishida

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics Vol. 40 page： 3-14 2014.7

Language：English

Transforming conditional term rewrite systems (CTRSs) into unconditional systems (TRSs) is a common approach to analyze properties of CTRSs via the simpler framework of unconditional rewriting. In the past many different transformations have been introduced for this purpose. One class of transformations, so-called unravelings, have been analyzed extensively in the past. In this paper we provide an overview on another class of transformations that we call structure-preserving transformations. In these transformations the structure of the conditional rule, in particular their left-hand side is preserved in contrast to unravelings. We provide an overview of transformations of this type and define a new transformation that improves previous approaches.

DOI： 10.4230/OASIcs.WPTE.2014.3

On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation Reviewed

Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner

Proceedings of the 3rd International Workshop on Confluence (IWC 2014) page： 24-28 2014.7

Authorship：Lead author Language：English

This paper improves the existing criterion for proving confluence of a normal conditional term rewriting system (CTRS) via the Serbanuta-Rosu transformation, a computationally equivalent transformation of CTRSs into unconditional term rewriting systems (TRS), showing that a weakly left-linear normal CTRS is confluent if the transformed TRS is confluent. Then, we discuss usefulness of the optimization of the Serbanuta-Rosu transformation, which has informally been proposed in the literature.

Inverse Unfold Problem and Its Heuristic Solving Reviewed

Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, and Naoki Nishida

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics Vol. 40 page： 27-38 2014.7

Language：English

Unfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. This paper, by using an example, show that restoring an one-step unfolding is not easy, i.e., a challenging task, since some rules used by unfolding may be lost. We formalize this problem by regarding one-step program transformation as a relation. Next we discuss some issues on a specific framework, called pure-constructor systems, which constitute a subclass of conditional term rewriting systems. We show that the inverse of T preserves rewrite relations if T preserves rewrite relations and the signature. We propose a heuristic procedure to solve the problem, and show its successful examples. We improve the procedure, and show examples for which the improvement takes effect.

DOI： 10.4230/OASIcs.WPTE.2014.27

On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings Reviewed

Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics Vol. 40 page： 39-50 2014.7

Authorship：Lead author Language：English

In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is sound for weakly left-linear normal conditional term rewriting systems (CTRS). Here, soundness for a CTRS means that reduction of the transformed unconditional term rewriting system (TRS) creates no undesired reduction for the CTRS. We first show that every reduction sequence of the transformed TRS starting with a term corresponding to the one considered on the CTRS is simulated by the reduction of the TRS obtained by the simultaneous unraveling. Then, we use the fact that the unraveling is sound for weakly left-linear normal CTRSs.

DOI： 10.4230/OASIcs.WPTE.2014.39

Inverse Unfold Problem and Its Heuristic Solving

Tomofumi Kato, Masanori Nagashima, Masahiko Sakai, and Naoki Nishida

IEICE Technical Rerport Vol. 113 ( 489 ) page： 13-18 2014.3

On Detecting Useless Transition Rules of Constrained Tree Automata

Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Kenji Hashimoto

IEICE Technical Rerport Vol. 113 ( 489 ) page： 31-36 2014.3

Conversion to tail recursion in term rewriting Reviewed

Naoki Nishida and German Vidal

The Journal of Logic and Algebraic Programming Vol. 83 ( 1 ) page： 53-63 2014.1

Authorship：Lead author Language：English Publishing type：Research paper (scientific journal)

Tail recursive functions are a special kind of recursive functions where the last action in their body is the recursive call. Tail recursion is important for a number of reasons (e.g., they are usually more efficient). In this article, we introduce an automatic transformation of first-order functions into tail recursive form. Functions are defined using a (first-order) term rewrite system. We prove the correctness of the transformation for constructor-based reduction over constructor systems (i.e., typical first-order functional programs).

DOI： 10.1016/j.jlap.2013.07.001

On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms Reviewed

Naoki Nishida, Masahiko Sakai, and Yasuhiro Nakano

Proceedings of the 2nd International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2013), Electronic Proceedings in Theoretical Computer Science Vol. 134 page： 1-10 2013.10

Authorship：Lead author Language：English

An inductive theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for reduction-completeness of constrained terms. In addition, the sufficient complete property of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms. This paper proposes a method to construct deterministic, complete, and constraint-complete constrained tree automata recognizing ground instances of constrained terms.

DOI： 10.4204/EPTCS.134.1

On Reducibility of Word Problems for Equations to Those for Ground Equations

Toshimitsu Sakai, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari and Naoki Nishida

Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering ( M4-4 ) page： 1 2013.9

Generation of Loop Invariants Consisting of Non-Linear Inequalities for Programs with Arrays

Junichiro Higashino, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari and Naoki Nishida

Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering ( M4-6 ) page： 1 2013.9

On Local Strategies for Automated Inductive-Theorem Proving on Simply Typed Term Rewriting Systems

Hisashi Kamiya, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida

Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering ( M4-3 ) page： 1 2013.9

Designing Higher-order Lexicographic Path Ordering with Currying

Honami Matsubara, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida

Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering ( M4-5 ) page： 1 2013.9

Development of an Interpreter Dynamically Checking Assertions on Pointers in Programs

Yoshihiro Mokutani, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari and Naoki Nishida

Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering ( M4-7 ) page： 1 2013.9

Use of Loop Invariants for Improving Termination Preservability of Transformations from Procedural Programs to Rewriting Systems

Takumi Kataoka, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe and Keiichirou Kusakari

Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering ( M2-6 ) page： 1 2013.9

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki