研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 254 件中 141 - 160 件目／全件表示 >>

Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity 招待有り査読有り Open Access

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Logical Methods in Computer Science 8 巻 ( 3-4 ) 頁： 1-49 2012年8月

担当区分：筆頭著者記述言語：英語掲載種別：研究論文（学術雑誌）

Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for a deterministic CTRS is sound w.r.t. reduction if the corresponding unraveled TRS is left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling. Finally, we show that soundness of Ohlebusch's unraveling is the weakest in soundness of the other unravelings and a transformation, proposed by Serbanuta and Rosu, for (normal) deterministic CTRSs, i.e., soundness of them respectively implies that of Ohlebusch's unraveling.

DOI： 10.2168/LMCS-8(3:4)2012

Open Access

On Extending Matching Operation in Grammar Programs for Program Inversion

Minami Niwa, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe and Keiichirou Kusakari

IEICE Technical Rerport 112 巻 ( 164 ) 頁： 103-108 2012年7月

Constrained Tree Automata and their Closure Properties 査読有り

Naoki Nishida, Futoshi Nomura, Katsuhisa Kurahashi and Masahiko Sakai

Proceedings of the 1st International Workshop on Trends in Tree Automata and Tree Transducers 頁： 24-34 2012年6月

More Specific Term Rewriting Systems 査読有り

Naoki Nishida and German Vidal

Proceedings of the 21st International Workshop on Functional and (Constraint) Logic Programming 頁： 1-15 2012年5月

Malbolgeの高級アセンブリ言語への配列機能の追加

安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

電子情報通信学会技術報告 112 巻 ( 23 ) 頁： 43-49 2012年5月

A Sound Type System for Typing Runtime Errors 査読有り Open Access

Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, and Naoki Nishida

IPSJ Transactions on Programming, 5 巻 ( 2 ) 頁： 16-24 2012年3月

単純型付き項書換え系における書換え帰納法について Open Access

尾関朗, 草刈圭一朗, 坂田翼, 西田直樹, 酒井正彦, 坂部俊樹

電子情報通信学会技術報告 111 巻 ( 406 ) 頁： 51-56 2012年1月

語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて Open Access

坂井利光, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗

電子情報通信学会技術報告 111 巻 ( 406 ) 頁： 45-49 2012年1月

関数呼び出しを持つプログラムの非線形ループ不変式の自動生成 Open Access

鈴木英一, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

電子情報通信学会技術報告 111 巻 ( 406 ) 頁： 39-44 2012年1月

高階書換え系における引数切り落とし関数の下での実効規則について Open Access

大井一展, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹

電子情報通信学会技術報告 111 巻 ( 406 ) 頁： 57-62 2012年1月

2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み Open Access

日野善信, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

電子情報通信学会技術報告 111 巻 ( 268 ) 頁： 67-72 2011年10月

制約付き項書換え系における木準同型写像を用いた関数等価性検証

高桑一也, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗

日本ソフトウェア科学会第28回大会論文集 ( 7B-1 ) 頁： 1-12 2011年9月

多重文脈書換え帰納法における反証と補題追加

坂田翼, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹

日本ソフトウェア科学会第28回大会論文集 ( 1A-4 ) 頁： 1-12 2011年9月

Malbolgeの高級アセンブリ言語への加算命令の追加

安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

日本ソフトウェア科学会第28回大会論文集 ( 5A-3 ) 頁： 1-12 2011年9月

関数呼び出しを持つプログラムの不変式の自動生成について

鈴木英一, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

平成23年度電気関係学会東海支部連合大会論文集 ( H1-5 ) 頁： 1 2011年9月

線形左シャロー項書換え系の停止性の決定可能性について

服部達哉, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

平成23年度電気関係学会東海支部連合大会論文集 ( H1-6 ) 頁： 1 2011年9月

Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems 査読有り Open Access

Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

IPSJ Transactions on Programming, 4 巻 ( 4 ) 頁： 12-35 2011年9月

Decidability and Undecidability of Reachability for Right-Linear Left-Shallow Non-Erasing Term Rewriting Systems

Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

LA Symposium 2011 Summer ( 15 ) 頁： 1-10 2011年7月

On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs 査読有り

Tsubasa Sakata, Naoki Nishida, and Toshiki Sakabe

Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming, Lecture Notes in Computer Science 6816 巻頁： 138-155 2011年7月

記述言語：英語

In this paper, we propose methods for proving termination of constrained term rewriting systems, where constraints are interpreted by built-in semantics given by users, and rewrite rules are assumed to be sound for the interpretation. To this end, we extend the dependency pair framework for proving termination of unconstrained term rewriting systems to constrained term rewriting systems. Moreover, we extend the dependency pair framework so that dependency pair processors take a subgraph of the dependency graph as input and they output a finite set of graphs which can be obtained by eliminating nodes and/or edges from the input graph.

DOI： 10.1007/978-3-642-22531-4_9

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity 査読有り Open Access

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPICcs 10 巻頁： 267-282 2011年5月

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

Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound for every CTRS w.r.t. reduction, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling.

DOI： 10.4230/LIPIcs.RTA.2011.267

Open Access

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹