研究者詳細 - 西田　直樹

論文 - 西田　直樹

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

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

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

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

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

Open Access

書換え解析ツールを利用した漸近的計算量解析のための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 査読有り Open Access

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

Open Access

Confluence Competition 2018 Open Access

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月

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

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

Open Access

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

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

Open Access

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

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

Open Access

Reversible computation in term rewriting 査読有り Open Access

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

Open Access

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

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

Open Access

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

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

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

記述言語：日本語

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

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹