研究者詳細 - 西田　直樹

論文 - 西田　直樹

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

木構造データを扱う関数の逆Unfold問題の発見的解法

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

電子情報通信学会技術報告 114 巻 ( 510 ) 頁： 85-90 2015年3月

A framework for computing finite SLD trees 査読有り Open Access

Naoki Nishida and German Vidal

Journal of Logical and Algebraic Methods in Programming 84 巻 ( 2 ) 頁： 197-217 2015年3月

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

The search space of SLD resolution, usually represented by means of a so-called SLD tree, is often infinite. However, there are many applications that must deal with possibly infinite SLD trees, like partial evaluation or some static analyses. In this context, being able to construct a finite representation of an infinite SLD tree becomes useful.

In this work, we introduce a framework to construct a finite data structure representing the (possibly infinite) SLD derivations for a goal. This data structure, called closed SLD tree, is built using four basic operations: unfolding, flattening, splitting, and subsumption. We prove some basic properties for closed SLD trees, namely that both computed answers and calls are preserved. We present a couple of simple strategies for constructing closed SLD trees with different levels of abstraction, together with some examples of its application. Finally, we illustrate the viability of our approach by introducing a test case generator based on exploring closed SLD trees.

DOI： 10.1016/j.jlamp.2014.11.006

Open Access

制約付き項書換え系の停止性証明におけるナローイングの効果について

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

電子情報通信学会技術報告 114 巻 ( 416 ) 頁： 43-48 2015年1月

例外処理を含む関数型プログラムの停止性証明のための条件付き依存対法の実現

太田浩一, 濱口毅, 酒井正彦, 山田晃久, 西田直樹, 坂部俊樹

電子情報通信学会技術報告 114 巻 ( 416 ) 頁： 55-60 2015年1月

A Finite Representation of the Narrowing Space 査読有り

Naoki Nishida and German Vidal

Revised Selected Papers of the 23rd International Conference on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science 8901 巻頁： 54-71 2014年12月

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

Narrowing basically extends rewriting by allowing free vari- ables in terms and by replacing matching with unification. As a con- sequence, the search space of narrowing becomes usually infinite, as in logic programming. In this paper, we introduce the use of some operators that allow one to always produce a finite data structure that still rep- resents all the narrowing derivations. Furthermore, we extract from this data structure a novel, compact equational representation of the (pos- sibly infinite) answers computed by narrowing for a given initial term. Both the finite data structure and the equational representation of the computed answers might be useful in a number of areas, like program comprehension, static analysis, program transformation, etc.

DOI： 10.1007/978-3-319-14125-1

Automatic Constrained Rewriting Induction towards Verifying Procedural Programs 査読有り

Cynthia Kop and Naoki Nishida

Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014) ( 8858 ) 頁： 334-353 2014年11月

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

This paper aims at developing a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can handle realistic functions, involving, e.g., integers and arrays. An implementation is provided.

DOI： 10.1007/978-3-319-12736-1_18

A Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold Problem

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

IPSJ Special Interest Group on Programming ( 2014-3-(9) ) 頁： 1-7 2014年11月

制約付き項書換え系の書換え帰納法における関数合成の可換性を利用した補題生成について

栗木隆太朗, 西田直樹, 酒井正彦

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

条件除去変換を用いた条件付き項書換え系の合流性証明手続きについて

柳澤真志, 西田直樹, 酒井正彦, 坂部俊樹

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

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

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

平成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 査読有り Open Access

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

Open Access

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

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

Open Access

On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings 査読有り Open Access

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

Open Access

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

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

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

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

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

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

Conversion to tail recursion in term rewriting 査読有り Open Access

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

Open Access

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹