研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 245 件中 61 - 80 件目／全件表示 >>

CauDEr: A Causal-Consistent Reversible Debugger for Erlang 査読有り

Ivan Lanese, Naoki Nishida, Adrian Palacios, and German Vidal

Proceedings of the 14th International Conference on Functional and Logic Programming, Lecture Notes in Computer Scienc 10818 巻頁： 247-263 2018年4月

記述言語：英語

Programming languages based on the actor model, such as Erlang, avoid some concurrency bugs by design. However, other concurrency bugs, such as message order violations and livelocks, can still show up in programs. These hard-to-find bugs can be more easily detected by using causal-consistent reversible debugging, a debugging technique that allows one to traverse a computation both forward and backward. Most notably, causal consistency implies that, when going backward, an action can only be undone provided that its consequences, if any, have been undone beforehand. To the best of our knowledge, we present the first causal-consistent reversible debugger for Erlang, which may help programmers to detect and fix various kinds of bugs, including message order violations and livelocks.

DOI： 10.1007/978-3-319-90686-7_16

Rewriting induction for constrained inequalities 査読有り

Takahiro Nagao and Naoki Nishida

Science of Computer Programming 155 巻頁： 76-102 2018年4月

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

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. Direct handling of inequalities enables us to utilize transitivity of binary predicates via application of induction hypotheses. Our framework succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations. For the sake of automated reasoning, we provide a strategy for applying inference rules and evaluate its performance by means of an implementation.

DOI： 10.1016/j.scico.2017.10.012

Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction 査読有り

Shinnosuke Mizutani and Naoki Nishida

Electronic Proceedings in Theoretical Computer Science 265 巻頁： 35-51 2018年2月

記述言語：英語

A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of the program w.r.t. the Hoare triple. The transformation enables us to apply techniques for proving termination of constrained rewriting to proving total correctness of programs together with proof tableaux for partial correctness.

DOI： 10.4204/EPTCS.265.4

Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers 査読有り

Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama

Electronic Proceedings in Theoretical Computer Science 265 巻頁： 83-97 2018年2月

記述言語：英語

In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences of integers, and they play an important role for the success of proving termination, especially for constrained rewriting systems. In this paper, we show sufficient conditions of linear polynomial interpretations for transforming dependency chains into bounded monotone (i.e., decreasing or increasing) sequences of integers. Such polynomial interpretations transform rewrite sequences of the original system into decreasing or increasing sequences independently of the transformation of dependency chains. When we transform rewrite sequences into increasing sequences, polynomial interpretations have non-positive coefficients for reducible positions of marked function symbols. We propose four DP processors parameterized by transforming dependency chains and rewrite sequences into either decreasing or increasing sequences of integers, respectively. We show that such polynomial interpretations make us succeed in proving termination of the McCarthy 91 function over the integers.

DOI： 10.4204/EPTCS.265.7

Reversible computation in term rewriting 査読有り

Naoki Nishida, Adrian Palacios, and German Vidal

Journal of Logical and Algebraic Methods in Programming 94 巻頁： 128-149 2018年1月

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

Essentially, in a reversible programming language, for each forward computation from state S to state S', there exists a constructive 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 work, 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 method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define two transformations, injectivization and inversion, to make a rewrite system reversible using standard term rewriting. We illustrate the usefulness of our transformations in the context of bidirectional program transformation.

DOI： 10.1016/j.jlamp.2017.10.003

CO3 (Version 1.4)

Naoki Nishida, Yoshiaki Kanazawa,, and Karl Gmeiner

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

A Reversible Semantics for Erlang 査読有り

Naoki Nishida, Adrian Palacios, and German Vidal

Revised Selected Papers of the 26th International Conference on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science (LOPSTR 2016) 10184 巻頁： 259-274 2017年7月

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

In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for debugging and for enforcing fault-tolerance, among others. In this paper, we consider a subset of Erlang, a concurrent language based on the actor model, and formally introduce a semantics for reversible computation. To the best of our knowledge, this is the first attempt to define a reversible semantics for Erlang.

DOI： 10.1007/978-3-319-63139-4_15

再帰呼び出しを持つC言語サブセットからMalbolgeへのコンパイラ

坂梨元軌，河邉翔平，酒井正彦，西田直樹，橋本健二

電子情報通信学会技術報告 117 巻 ( 136 ) 頁： 145-150 2017年7月

記述言語：日本語

難読プログラミング言語Malbolgeは，その解析困難性により知的財産権の保護などに役立つと考えられているが，命令が特殊であるためプログラムの作成は非常に困難である．そのため，Malbolgeプログラムを生成するための中間言語として制御付き疑似命令列が提案されているが，Cなどの通常の言語と比較すると依然としてプログラミングが困難である．本稿では，整数型と真偽型を扱え，while文などの基本的な制御構造と再帰関数を定義できるC言語のサブセットのプログラムからMalbolgeコードへのコンパイラの実現法を述べる．コンパイラの実現のために，まず，既存の制御付き疑似命令列に配列構文と関数構文を追加し，それにあわせて既存の制御付き疑似命令列からMalbolgeへの変換系を拡張する．さらにC言語のサブセットから制御付き疑似命令列へ変換する方法を提案する．

制約付き項書換え系の依存鎖を上限付き整数増加列に変換する多項式解釈

笹野智裕，西田直樹，酒井正彦，上山智也

電子情報通信学会技術報告 117 巻 ( 136 ) 頁： 139-144 2017年7月

記述言語：日本語

制約付き項書換え系の停止性証明の枠組みである依存対フレームワークでは，関数呼び出しの関係を表現した依存鎖を下限付き整数減少列に変換する多項式解釈が証明の成否を左右する重要な役割を果たす．本稿では，依存鎖を下限付き整数減少列に変換する一方で，書換え規則による書換え系列を整数増加列に変換する多項式解釈による停止性証明機能を依存対フレームワークに導入する．さらに，依存鎖を上限付き整数増加列に変換する多項式解釈による停止性証明機能を導入し，比較実験の結果を報告する．

Verifying Procedural Programs via Constrained Rewriting Induction 査読有り

Carsten Fuhs, Cynthia Kop, and Naoki Nishida

ACM Transactions on Computational Logic 18 巻 ( 2 ) 頁： 14:1-14:50 2017年6月

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

This article aims to develop a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend transformation methods based on integer term rewriting systems to handle arbitrary data types, global variables, function calls, and arrays, and to encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations; thus, in contrast to other works, we do not require an explicit specification in a separate specification language.

DOI： 10.1145/3060143

十分完全性を持たない階層的条件付き項書換え系の合流性証明

黒田貴之，西田直樹，関浩之

電子情報通信学会技術報告 116 巻 ( 512 ) 頁： 103-108 2017年3月

記述言語：日本語

条件付き項書換え系（CTRS）における合流性の検証手法として項書換え系への変換を経て証明する手法が知られているが，自然数リストの並び替えを行うCTRSの合流性は証明できていない．このCTRSは関数記号の振舞いが階層的に定義される階層的CTRSとなっており，十分完全性を持っていない．本稿では，十分完全性を持たない階層的CTRSの合流性を証明する手法を提案する．具体的には，条件付き等式に対する書換え帰納法を十分完全性を持たないTRSに拡張し，書換え帰納法を用いて条件付き危険対の条件から別の条件を導出することでその危険対が会同可能であることを示す．次に，書換え規則の条件部が成立することを考慮できる単純化順序を設計し，その単純化順序により階層的CTRSの停止性を証明する手法を提案する．

Relative Termination via Dependency Pairs 査読有り

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

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

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

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.

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

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

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

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹