研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 254 件中 41 - 60 件目／全件表示 >>

On Transforming Inductive Definition Sets into Term Rewrite Systems 査読有り

Shujun Zhang and Naoki Nishida

Informal Proceedings of the 8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2021) 頁： 1 - 10 2021年7月

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

In this paper, we transform an inductive definition set—a set of productions for inductive predicates—into a term rewrite system (TRS, for short) such that a quantifier-free sequent over the first-order logic with the inductive definition set is valid if and only if its corresponding equation is an inductive theorem of the TRS. The resulting TRS is composed of three parts: Rewrite rules for logical connectives and a binary symbol for sequents; rewrite rules for productions; rewrite rules for the co-patterns of the second part. For correctness of the resulting TRS, we assume a certain property of the inductive definition set, which is a sufficient condition for ground termination and ground confluence of the resulting TRS. The transformation aims at comparing cyclic proof systems and rewriting induction.

計数セマフォを含むプログラムから論理制約付き項書換え系への変換 Open Access

小嶋美咲，西田直樹，酒井正彦

情報処理学会第83回全国大会講演論文集頁： 229 - 230 2021年3月

擬ブール制約の導入による組合せ最適化ソルバCombSQL+の高速化

岸潤一郎，酒井正彦，西田直樹，橋本健二

電子情報通信学会技術報告 120 巻 ( 343 ) 頁： 66-71 2021年1月

記述言語：日本語

著者らはこれまでに，拡張したSQLで組合せ最適化問題を簡単に記述でき，かつ効率的に解くことのできる求解系CombSQL+を提案した．CombSQL+はシステム内部で，入力のSQL式からプログラム変換によって得られるSQL式をDBエンジンで実行することでいくつかの線形整数制約（QFLIA）を生成し，SMTソルバを利用してそれらの解を求めている．本稿では，変換後のSQL式で用いられる制約生成関数を工夫することで，擬ブール制約として表現できる制約を直接，擬ブール制約として生成する方法を提案する．この改良により問題によっては7倍以上の高速化が達成できたことを報告する．

Reversible CSP Computations 査読有り Open Access

Carlos Galindo, Naoki Nishida, Josep Silva, and Salvador Tamarit

IEEE Transactions on Parallel and Distributed Systems 32 巻 ( 6 ) 頁： 1425-1436 2021年1月

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

Reversibility enables a program to be executed both forwards and backwards. This ability allows programmers to backtrack the execution to a previous state. This is essential if the computation is not deterministic because re-running the program forwards may not lead to that state of interest. Reversibility of sequential programs has been well studied and a strong theoretical basis exists. Contrarily, reversibility of concurrent programs is still very young, especially in the practical side. For instance, in the particular case of the Communicating Sequential Processes (CSP) language, reversibility is practically missing. In this article, we present a new technique, including its formal definition and its implementation, to reverse CSP computations. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. The technique proposes different forms of reversibility, including strict reversibility and causal-consistent reversibility. On the practical side, we provide an implementation of a system to reverse CSP computations that is able to highlight the source code that is being executed in each forwards/backwards computation step, and that has been optimized to be scalable to real systems.

DOI： 10.1109/TPDS.2021.3051747

ReverCSP: Time-Travelling in CSP Computations 査読有り Open Access

Carlos Galindo, Naoki Nishida, Josep Silva, and Salvador Tamarit

Proceedings of the 12th International Conference on Reversible Computation, Lecture Notes in Computer Science 12227 巻頁： 239-245 2020年7月

記述言語：英語

This paper presents reverCSP, a tool to animate both forward and backward CSP computations. This ability to reverse computations can be done step by step or backtracking to a given desired state of interest. reverCSP allows us to reverse computations exactly in the same order in which they happened, or also in a causally-consistent way. Therefore, reverCSP is a tool that can be especially useful to comprehend, analyze, and debug computations. reverCSP is an open-source project publicly available for the community. We describe the tool and its functionality, and we provide implementation details so that it can be reimplemented for other languages.

DOI： 10.1007/978-3-030-52482-1_14

Open Access

Confluence Competition 2020 国際共著

Aart Middeldorp, Naoki Nishida, Kiraku Shintani, and Johannes Waldmann

Proceedings of the 9th International Workshop on Confluence 頁： 53 2020年6月

CO3 (Version 2.1)

Naoki Nishida

Proceedings of the 9th International Workshop on Confluence 頁： 67 2020年6月

Transforming Concurrent Programs with Semaphores into Logically Constrained Term Rewrite Systems 査読有り

Misaki Kojima, Naoki Nishida, and Yutaka Matsubara

Informal Proceedings of the 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2020) 頁： 1-12 2020年6月

A Case Study for Reversible Computing: Reversible Debugging of Concurrent Programs 査読有り

James Hoey, Ivan Lanese, Naoki Nishida, Irek Ulidowski, and German Vidal

Reversible Computation: Extending Horizons of Computing, Lecture Notes in Computer Science 12070 巻頁： 108-127 2020年5月

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

Reversible computing allows one to run programs not only in the usual forward direction, but also backward. A main application area for reversible computing is debugging, where one can use reversibility to go backward from a visible misbehaviour towards the bug causing it. While reversible debugging of sequential systems is well understood, reversible debugging of concurrent and distributed systems is less settled. We present here two approaches for debugging concurrent programs, one based on backtracking, which undoes actions in reverse order of execution, and one based on causal consistency, which allows one to undo any action provided that its consequences, if any, are undone beforehand. The first approach tackles an imperative language with shared memory, while the second one considers a core of the functional message-passing language Erlang. Both the approaches are based on solid formal foundations.

DOI： 10.1007/978-3-030-47361-7_5

排他制御を含むプログラムから論理制約付き項書換え系への変換

小嶋美咲，西田直樹，松原豊，酒井正彦

電子情報通信学会技術報告 119 巻 ( 451 ) 頁： 31-36 2020年3月

記述言語：日本語

計算モデルである論理制約付き項書換え系（LCTRS）をプログラムの検証に用いる先行研究では，逐次実行される命令型プログラムを対象としている．現実の計算機の利用状況を考えると，逐次実行されるプログラムとそれを並行化したプログラムが等価であることを検証したいという要求がある．本稿では，並行実行されるプログラムをLCTRSで表現すること目的として，セマフォによる排他制御を含むプログラムをLCTRSで表現する方法を提案する．そのためにまず，先行研究で導入された実行環境を表す関数記号の引数を，実行されるプロセスの数だけ増やすことで，プロセスの並行実行を表現する．次に，セマフォに対する操作を書換え規則で表現し，セマフォによる排他制御を含むプログラムをLCTRSに変換する．セマフォに対する待ち行列を番号札を使って管理することで，リストなどの再帰データ構造を導入せずにセマフォの操作を表現する．

存在限量子付き等式を証明するための書換え帰納法の拡張

西江一志，西田直樹，酒井正彦

電子情報通信学会技術報告 119 巻 ( 246 ) 頁： 25-30 2019年10月

記述言語：日本語

本稿では，等式を証明するための書換え帰納法を存在限量子付き等式を証明できるように拡張する．具体的にはまず，論理制約付き項書換え系の書換え規則の右辺に存在限量子を持つ項を許すように拡張する．次に，存在限量子付き等式を形式化し，書換え帰納法を拡張する．最後に，不等式を存在限量子付き等式に帰着して証明する例を示す．

CO3 (Version 2.0)

Naoki Nishida and Yuya Maeda

Proceedings of the Joint Proceedings of HOR 2019 and IWC 2019 (with system descriptions from CoCo 2019) 頁： 50 2019年6月

Characterizing Compatible View Updates in Syntactic Bidirectionalization 査読有り

Naoki Nishida and German Vidal

Proceedings of the 11th International Conference on Reversible Computation, Lecture Notes in Computer Science 11497 巻頁： 67-83 2019年6月

記述言語：英語

Given a function that takes a source data and returns a view, bidirectionalization aims at producing automatically a new function that takes a modified view and returns the corresponding, modified source. In this paper, we consider simple first-order functional programs specified by (conditional) term rewrite systems. Then, we present a bidirectionalization technique based on the injectivization and inversion transformations from. We also prove a number of relevant properties which ensure that changes in both the source and the view are correctly propagated and that no undesirable side-effects are introduced. Furthermore, we introduce the use of narrowing---an extension of rewriting that replaces matching with unification---to precisely characterize compatible (also called in-place) view updates so that the resulting bidirectional transformations are well defined. Finally, we discuss some directions for dealing with view updates that are not compatible.

DOI： 10.1007/978-3-030-21500-2_5

On Determinization of Inverted Grammar Programs via Context-Free Expressions 査読有り

Naoki Nishida and Minami Niwa

Informal Proceedings of the 6th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018) 頁： 1-15 2019年6月

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

In this paper, we propose a determinization method of inverted grammar programs by means of context-free expressions which are straightforward extensions of regular expressions to context-free languages. Grammar programs are context-free grammars that an inversion method proposed by Glueck and Kawabe uses as intermediate results. We use conditional term rewriting systems (CTRSs, for short) as target programs, and our determinization method aims at transforming a given CTRS into a non-overlapping one that is semantically equivalent to the given one. To this end, we first translate a grammar program into an equivalent context-free expression. Then, by using some simple equalities of expressions, we transform the expression to a desired form. Finally, we translate the resulting expression back into an equivalent grammar program which can be translated back into a non-overlapping CTRS.

On Formalizing a Transformation of IMP Programs into Logically Constrained Term Rewriting Systems in Isabelle/HOL 査読有り

Ryota Nakayama and Naoki Nishida

Informal Proceedings of the 6th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018) 頁： 1-15 2019年6月

Proving Program Equivalence with Constrained Rewriting Induction and Ctrl 査読有り

Caarsten Fuhs, Cynthia Kop, and Naoki Nishida

Informal Proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning 頁： 1-2 2019年4月

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

We prove equivalence of imperative programs by an automatic conversion of the functions in the input program to an equivalent Logically Constrained Term Rewrite System (LCTRS), followed by constrained rewriting induction (either fully automatically or guided by the user) to analyze equivalence of the corresponding functions in the LCTRS. Our approach is implemented in the tool Ctrl.

組合せ最適化問題の記述からSMTソルバの入力式を生成するSQL問合せ

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

電子情報通信学会技術報告 118 巻 ( 471 ) 頁： 85-90 2019年3月

記述言語：日本語

著者らはこれまでに，組合せ最適化問題を簡単に記述でき，かつ効率的に解く手法を開発すること目的として，SQLを基礎とした言語CombSQL+を提案し，SMTソルバを利用した問題解法を示した．この手法の特長は，通常のSQL問い合わせをそのまま制約の記述に用いることができ，直観的な記述ができることにある．CombSQL+で書かれた問題記述からのSMTソルバに入力するための制約を生成するために，テーブルの集合を表す制約付きテーブル上に拡張したSQL問合せを利用している．しかしながらSQLのすべての問い合わせ機能には対応しておらず，対応のためには制約付きテーブル上に拡張した複雑なSQLエンジンを拡充する必要がある．本稿では，拡張SQLエンジンを拡充するのではなく，既存のSQLエンジンで実行するだけでSMTソルバに与える制約式を生成できるSQL問い合わせを生成する方法を提案する．ここで，データベースシステムSQLiteが備える，副作用をもつ関数が定義できるという機能を利用することが，SMTソルバに与える制約式の生成における鍵となっている．

On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems 査読有り Open Access

Yoshiaki Kanazawa and Naoki Nishida

Electronic Proceedings in Theoretical Computer Science 289 巻頁： 34-52 2019年2月

記述言語：英語

In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The resulting system represents transitions of the whole execution environment with a call stack. More precisely, we prepare a function symbol for the whole environment, which stores values for global variables and a call stack as its arguments. For a function call, we prepare rewrite rules to push the frame to the stack and to pop it after the execution. Any running frame is located at the top of the stack, and statements accessing global variables are represented by rewrite rules for the environment symbol. We show a precise transformation based on the approach and prove its correctness.

DOI： 10.4204/EPTCS.289.3

Open Access

arXiv

On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions 査読有り

Naoki Nishida and Yuya Maeda

Electronic Proceedings in Theoretical Computer Science 289 巻頁： 68-87 2019年2月

記述言語：英語

The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with particular non-narrowable terms. In this paper, under a certain syntactic condition, we show a transformation of the grammar representation of a narrowing tree into another regular tree grammar that overapproximately generates the ranges of ground substitutions generated by the grammar representation. In our previous work, such a transformation is restricted to the ranges w.r.t. a given single variable, and thus, the usefulness is limited. We extend the previous transformation by representing the range of a ground substitution as a tuple of terms, which is obtained by the coding for finite trees. We show a precise definition of the transformation and prove that the language of the transformed regular tree grammar is an overapproximation of the ranges of ground substitutions generated by the grammar representation. We leave an experiment to evaluate the usefulness of the transformation as future work.

DOI： 10.4204/EPTCS.289.35

arXiv

論理制約付き書換えにおける構造体および共用体の表現について

金澤慶明，西田直樹，酒井正彦

電子情報通信学会技術報告 118 巻 ( 385 ) 頁： 67-72 2019年1月

記述言語：日本語

近年，項書換え系への変換に基づいた手続き型のプログラムの検証について研究が行われており，実行の中間状態を表現する項から制御フローをモデル化するための論理制約を分離して表現できる論理制約付き項書換え系への変換が注目されている．しかし，既存手法ではデータ型として整数とその1次元配列のみをデータとして扱うC言語プログラムを対象としており，ビット数が異なる基本データ型や構造体，共用体を扱っていない．本稿では，構造体や共用体などのサイズの異なるデータ構造を論理制約付き項書換えの枠組みで扱うための，構造体や共用体のビットベクトルを用いた表現，およびそれらのメンバへアクセスするための書換え規則の構成法を提案する．

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹