研究者詳細 - 西田　直樹

論文 - 西田　直樹

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

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

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

電子情報通信学会技術報告 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 査読有り

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

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言語プログラムを対象としており，ビット数が異なる基本データ型や構造体，共用体を扱っていない．本稿では，構造体や共用体などのサイズの異なるデータ構造を論理制約付き項書換えの枠組みで扱うための，構造体や共用体のビットベクトルを用いた表現，およびそれらのメンバへアクセスするための書換え規則の構成法を提案する．

項書換えにおけるナローイング計算木のベーシックナローイングへの拡張

前田侑也，西田直樹，酒井正彦，小林倫也

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

Loop Detection by Logically Constrained Term Rewriting 査読有り

Naoki Nishida and Sarah Winkler

Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018), Lecture Notes in Computer Science 11294 巻頁： 309-321 2018年11月

記述言語：英語

Logically constrained rewrite systems constitute a very general rewriting formalism that can capture simplification processes in various domains as well as computation in imperative programs. In both of these contexts, nontermination is a critical source of errors. We present new criteria to find loops in logically constrained rewrite systems which are implemented in the tool Ctrl. We illustrate the usefulness of these criteria in three example applications: to find loops in LLVM peephole optimizations, to detect looping program executions of C programs, and to establish nontermination of integer transition systems.

DOI： 10.1007/978-3-030-03592-1_18

A theory of reversibility for Erlang 査読有り

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

Journal of Logical and Algebraic Methods in Programming 100 巻頁： 71-97 2018年11月

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

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 testing and verifica- tion, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint.

DOI： 10.1016/j.jlamp.2018.06.004

書換え解析ツールを利用した漸近的計算量解析のためのC言語プログラムの簡易化について

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

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

ベーシックナローイングへのナローイング計算木の拡張について

前田侑也, 西田直樹, 酒井正彦

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

Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs 査読有り

Naoki Nishida, Yuta Tsuruta, and Yoshiaki Kanazawa

Proceedings of the 7th International Workshop on Confluence (IWC 2018) 頁： 51-55 2018年7月

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

Unravelings, which are transformations of a conditional term rewriting system (CTRS, for short) into an unconditional term rewriting system (TRS, for short), are useful to prove confluence and operational termination of some CTRSs. A simultaneous unraveling has been proposed for normal 1-CTRSs and a sequential one has been proposed for deterministic 3-CTRSs, the class of which includes normal 1-CTRSs. In this paper, we first show that for a normal 1-CTRS, the simultaneously unraveled TRS is orthogonal iff so is the sequentially unraveled one. Then, we show that for a normal 1-CTRS, if the simultaneously unraveled TRS is terminating, then so is the sequentially unraveled one. Finally, we show that for a normal 1-CTRS with termination of the unraveled TRS, the simultaneously unraveled TRS is locally confluent iff so is the sequentially unraveled one.

CO3 (Version 1.5)

Naoki Nishida, Yuta Tsuruta, and Yoshiaki Kanazawa

Proceedings of the 7th International Workshop on Confluence (IWC 2018) 頁： 64 2018年7月

Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems 査読有り

Naoki Nishida and Yuya Maeda

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs 108 巻頁： 26:1-26:20 2018年6月

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

A narrowing tree for a constructor term rewriting system and a pair of terms is a finite representation for the space of all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. Narrowing trees have grammar representations that can be considered regular tree grammars. Innermost narrowing is a counterpart of constructor-based rewriting, and thus, narrowing trees can be used in analyzing constructor-based rewriting to normal forms. In this paper, using grammar representations, we extend narrowing trees to syntactically deterministic conditional term rewriting systems that are constructor systems. We show that narrowing trees are useful to prove two properties of a normal conditional term rewriting system: one is infeasibility of conditional critical pairs and the other is quasi-reducibility.

DOI： 10.4230/LIPIcs.FSCD.2018.26

Confluence Competition 2018

Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs 108 巻頁： 32:1-32:5 2018年6月

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹