研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 254 件中 81 - 100 件目／全件表示 >>

Relative Termination via Dependency Pairs 査読有り Open Access

Jose Iborra, Naoki Nishida, German Vidal, and Akihisa Yamada

Journal of Automated Reasoning 58 巻 ( 3 ) 頁： 391-411 2017年3月

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

A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.

DOI： 10.1007/s10817-016-9373-5

Open Access

Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems 査読有り

Ryota Nakayama, Naoki Nishida, and Masahiko Sakai

Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), Electronic Proceedings in Theoretical Computer Science 235 巻頁： 62-77 2017年1月

記述言語：英語

In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is a sound structure-preserving transformation for weakly-left-linear deterministic conditional term rewriting systems. More precisely, we show that every weakly-left-linear deterministic conditional term rewriting system can be converted to an equivalent weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting system and prove that the SR transformation is sound for weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting systems. Here, soundness for a conditional term rewriting system means that reduction of the transformed unconditional term rewriting system creates no undesired reduction sequence for the conditional system.

DOI： 10.4204/EPTCS.235.5

arXiv

Notes on Confluence of Ultra-WLL SDCTRSs via a Structure-Preserving Transformation 査読有り

Naoki Nishida

Proceedings of the 5th International Workshop on Confluence (IWC 2016) 頁： 60-64 2016年9月

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

A structure-preserving transformation proposed by Serbanuta and Rosu for strongly or syntactically deterministic conditional term rewriting systems (SDCTRSs) that are ultra-left-linear has been shown to be applicable to weakly-left-linear (WLL) and ultra-WLL SDCTRSs without any change, and sound for such DCTRSs even if they are not SDCTRSs. In this paper, we show a confluent, WLL, and ultra-WLL DCTRS that is not an SDCTRS such that the transformed TRS is not confluent. We also show that for a WLL and ultra-WLL SDCTRS, if the transformed TRS is confluent, then so is the SDCTRS.

CO3 (Version 1.3)

Naoki Nishida, Takayuki Kuroda, and Karl Gmeiner

Proceedings of the 5th International Workshop on Confluence (IWC 2016) 頁： 74 2016年9月

Proving inductive validity of constrained inequalities 査読有り

Takahiro Nagao and Naoki Nishida

Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016) 頁： 50-61 2016年9月

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

Rewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities within such frameworks, one may reduce inequalities to equations. However, it is often hard to prove inductive validity of such reduced equations within the existing RI frameworks due to their indirect handling of inequalities. In this paper, we adapt the notion of inductive theorems to inequalities and propose an RI framework for directly proving inductive validity of inequalities of constrained term rewriting systems. Within the framework, we handle inequalities that may contain function symbols defined in a given rewriting system but not necessarily interpreted by the built-in semantics. Direct handling of inequalities facilitates the utilization of transitivity of magnitude relations via inequalities obtained as induction hypotheses. Our approach succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations.

DOI： 10.1145/2967973.2968598

難読性の高いMalbolgeコードを生成するコンパイラのための中間言語

河邉翔平，酒井正彦，西田直樹，関浩之

電子情報通信学会技術報告 116 巻 ( 127 ) 頁： 105-110 2016年7月

Reversible Term Rewriting 査読有り Open Access

Naoki Nishida, Adrian Palacios, and German Vidal

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), LIPIcs 52 巻頁： 28:1-28:18 2016年6月

記述言語：英語

Essentially, in a reversible programming language, for each forward computation step from state S to state S', there exists a constructive and deterministic method to go backwards from state S' to state S. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few. In this paper, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step t1 -> t2, we do not always have a decidable and deterministic method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define a transformation to make a rewrite system reversible using standard term rewriting.

DOI： 10.4230/LIPIcs.FSCD.2016.28

Open Access

Reversible Term Rewriting in Practice 査読有り

Naoki Nishida, Adrian Palacios, and German Vidal

Informal Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016) 頁： 77-85 2016年6月

記述言語：英語

A computation is considered reversible if, for each step from state S to state S', there exists a deterministic and terminating method to compute S back from S'. Reversibilization aims at producing a reversible version of an originally irreversible computation principle. Recently, we have introduced a reversible extension of term rewriting. Furthermore, we have defined an appropriate reversibilization transformation for rewrite systems so that standard rewriting becomes reversible on the transformed systems. In this paper, we focus on the potential applications of the reversibilization transformation. In particular, we show its application in the context of bidirectional program transformation and the reversibilization of cellular automata.

配列を入力引数とする関数の検証のための分離論理の拡張 Open Access

水谷慎之介, 西田直樹, 酒井正彦

情報処理学会第109回プログラミング研究発表会頁： 1-8 2016年6月

組合せ最適化問題記述のためのSQLの拡張

内田佑作, 酒井正彦, 西田直樹

電子情報通信学会技術報告 115 巻 ( 508 ) 頁： 25-30 2016年3月

記述言語：日本語

近年，充足可能性判定ソルバの高速化がめざましい．しかしながらこれらのソルバを用いて組合せ最適化問題を解くための論理式へのコーディングは容易ではない．本稿では，組合せ最適化問題の定義の容易な記述を可能にするため，データベース問い合わせ言語SQLに対して組合せ最適化問題を記述するための構文を追加し，その記述から充足可能性判定ソルバを利用して問題の解を得るための手法について論ずる．

拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証

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

電子情報通信学会技術報告 115 巻 ( 508 ) 頁： 31-36 2016年3月

記述言語：日本語

ループ不変式を生成するための手法として，与えたテンプレートと事前条件と事後条件から得られる検証式をFarkas補題に基づき変換する手法が研究されている．Farkas補題に基づく変換では線形な多項式の不等式のみを原始論理式として含む論理式を等価変換する．それを変数や関数適用項の積を単項式とする多項式上に拡張した拡張Farkas補題が提案され，非線形なループ不変式を生成できる場合があることが示された．しかし，拡張Farkas補題を用いて生成したループ不変式がプログラム検証に有効かどうかについては議論されていない．本稿では，プロラム検証における拡張Farkas補題に基づくループ不変式の生成法の有効性を評価し，拡張Farkas補題を有効に利用する検証手法を提案する．具体的には，未知係数を含む複数の検証式の一部を拡張Farkas補題により変換し，それを充足する未知係数の割り当てを残りの検証式の未知係数に代入した後に恒真性を判定する．

ナローイングによる制約付き依存対の変換

笹野智裕, 西田直樹, 酒井正彦

電子情報通信学会技術報告 115 巻 ( 420 ) 頁： 123-128 2016年1月

記述言語：日本語

項書換え系の停止性証明の枠組みである依存対フレームワークは項書換え規則に制約を付随させた制約付き項書換え系を対象に拡張された．本論文では、拡張された依存対フレームワークにおけるナローイングによる依存対の変換の適用条件を緩和する．具体的には，先行研究における変換対象の依存対が直接接続可能でないという条件を満たさない場合にも変換が健全であることことを示す．

制約付き項書換え系における停止性と帰納的定理の同時証明

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

電子情報通信学会技術報告 115 巻 ( 420 ) 頁： 75-80 2016年1月

Constrained Term Rewriting tooL 査読有り

Cynthia Kop and Naoki Nishida

Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science ( 9450 ) 頁： 549-557 2015年11月

記述言語：英語

This paper discusses Ctrl, a tool to analyse - both automatically and manually - term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and automatically analyse various properties such as termination, confluence and quasi-reductivity. Ctrl also offers both a manual and automatic mode for equivalence tests using inductive theorem proving, giving support for and verification of "hand-written" term equivalence proofs.

DOI： 10.1007/978-3-662-48899-7_38

SATソルバへの基数制約節導入における学習節の最大保持数

塚本尚秀, 酒井正彦, 西田直樹, 橋本健二

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

Reducing Relative Termination to Dependency Pair Problems 査読有り Open Access

Jose Iborra, Naoki Nishida, German Vidal, and Akihisa Yamada

Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science 9195 巻頁： 163-178 2015年8月

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

Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce a new technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. The practical significance of our method is illustrated by means of an experimental evaluation.

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

CO3: a COnverter for proving COfluence of COnditional TRSs

Naoki Nishida, Takayuki Kuroda, Makishi Yanagisawa, and Karl Gmeiner

Proceedings of the 4th International Workshop on Confluence (IWC 2015) 頁： 42 2015年8月

Confluence Competition 2015

Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl

Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science 9195 巻頁： 101-104 2015年8月

パターン除去による制約付き項書換え系の等価変換

長尾貴浩, 西田直樹, 酒井正彦

電子情報通信学会技術報告 115 巻 ( 153 ) 頁： 167-172 2015年7月

記述言語：日本語

制約付き項書換え系は整数制約などにより規則の適用を制御できるように項書換え系を拡張した枠組みである．書換え規則の左辺に現れるパターンの一部を意味を変えることなく除去することにより，様々な性質の解析が容易となる．本稿では，左辺に解釈項のパターンのみを持つ制約付き項書換え系のパターン除去に基づく変換を提案し，この変換が十分完全性や最内停止性などの性質に関して等価変換となる十分条件を示す．また，変換の応用として書換え完全性の判定法を提案する．

制約付き項書換え系における関数合成の可換性を自動証明するためのヒューリスティック

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

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

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹