研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 245 件中 101 - 120 件目／全件表示 >>

制約付き項書換え系の依存対法におけるプレスブルガー算術式の恒真性判定の回数削減について

上山智也, 西田直樹, 坂部俊樹, 酒井正彦

平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集 ( M4-5 ) 頁： 1 2014年9月

項書換え系における関数の等価性を保存する引数切り落としの十分条件について

川本佳史, 西田直樹, 酒井正彦, 坂部俊樹

平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集 ( M4-2 ) 頁： 1 2014年9月

制約付き項書換えにおいて等式が関数等価性を表現するための必要十分条件について

片岡巧, 西田直樹, 酒井正彦, 坂部俊樹

平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集 ( M4-4 ) 頁： 1 2014年9月

On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants 査読有り

Naoki Nishida and Takumi Kataoka

Proceedings of the 14th International Workshop on Termination (WST 2014) 頁： 1-5 2014年7月

担当区分：筆頭著者記述言語：英語

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 査読有り

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 40 巻頁： 3-14 2014年7月

記述言語：英語

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 査読有り

Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner

Proceedings of the 3rd International Workshop on Confluence (IWC 2014) 頁： 24-28 2014年7月

担当区分：筆頭著者記述言語：英語

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 査読有り

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 40 巻頁： 27-38 2014年7月

記述言語：英語

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 査読有り

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 40 巻頁： 39-50 2014年7月

担当区分：筆頭著者記述言語：英語

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

逆Unfold問題とその発見的解法

加藤友郁, 長島正憲, 酒井正彦, 西田直樹

電子情報通信学会技術報告 113 巻 ( 489 ) 頁： 13-18 2014年3月

制約付き木オートマトンにおける不用な遷移規則の発見法について

中野靖大, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗, 橋本健二

電子情報通信学会技術報告 113 巻 ( 489 ) 頁： 31-36 2014年3月

Conversion to tail recursion in term rewriting 査読有り

Naoki Nishida and German Vidal

The Journal of Logic and Algebraic Programming 83 巻 ( 1 ) 頁： 53-63 2014年1月

担当区分：筆頭著者記述言語：英語掲載種別：研究論文（学術雑誌）

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 査読有り

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 134 巻頁： 1-10 2013年10月

担当区分：筆頭著者記述言語：英語

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

等式集合の語問題から基底等式集合の語問題への帰着可能性について

坂井利光, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

平成25年度電気関係学会東海支部連合大会論文集 ( M4-4 ) 頁： 1 2013年9月

配列を含むプログラムの検証のための非線形不等式型ループ不変式の生成

東野惇一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

平成25年度電気関係学会東海支部連合大会論文集 ( M4-6 ) 頁： 1 2013年9月

単純型付き項書換え系における帰納的定理自動証明の局所戦略について

神谷尚史, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹

平成25年度電気関係学会東海支部連合大会論文集 ( M4-3 ) 頁： 1 2013年9月

カリー化を組み込んだ高階辞書式経路順序の設計

松原穂波, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹

平成25年度電気関係学会東海支部連合大会論文集 ( M4-5 ) 頁： 1 2013年9月

プログラム中のポインタに関する表明式を動的に検査するインタプリタの開発

杢谷孔皓, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

平成25年度電気関係学会東海支部連合大会論文集 ( M4-7 ) 頁： 1 2013年9月

手続き型プログラムから書換え系への変換における停止性をより保存するためのループ不変式の利用

片岡巧, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗

平成25年度電気関係学会東海支部連合大会論文集 ( M2-6 ) 頁： 1 2013年9月

幅優先探索型完備化手続きのErlangによる実装の並列実行の評価

栗木隆太朗, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗

平成25年度電気関係学会東海支部連合大会論文集 ( M2-5 ) 頁： 1 2013年9月

Term Rewriting with Logical Constraints 査読有り

Cynthia Kop and Naoki Nishida

Proceedings of the 9th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence ( 8152 ) 頁： 343-358 2013年9月

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹