2024/05/20 更新

写真a

ニシダ ナオキ
西田 直樹
NISHIDA Naoki
所属
大学院情報学研究科 情報システム学専攻 計算論 准教授
大学院担当
大学院情報科学研究科
大学院情報学研究科
学部担当
工学部
情報学部 コンピュータ科学科
職名
准教授
連絡先
メールアドレス

学位 1

  1. 博士(工学) ( 2004年3月   名古屋大学 ) 

研究キーワード 5

  1. 定理自動証明

  2. プログラム変換

  3. 項書換え系

  4. 関数型プログラム

  5. 逆計算

研究分野 1

  1. その他 / その他  / 情報学基礎

現在の研究課題とSDGs 2

  1. 制約付き書換え系の定理自動証明を利用した命令型プログラムの検証に関する研究

  2. 関数型プログラムの逆計算プログラムの生成に関する研究

経歴 4

  1. 名古屋大学   大学院情報学研究科情報システム学専攻   准教授

    2017年4月 - 現在

      詳細を見る

    国名:日本国

    備考:改組

  2. 名古屋大学   大学院情報科学研究科情報システム学専攻   准教授

    2013年4月 - 2017年3月

      詳細を見る

    国名:日本国

  3. 名古屋大学   大学院情報科学研究科情報システム学専攻   助教

    2007年4月 - 2013年3月

      詳細を見る

    国名:日本国

    備考:職名変更

  4. 名古屋大学   大学院情報科学研究科情報システム学専攻   助手

    2004年4月 - 2007年3月

      詳細を見る

    国名:日本国

学歴 3

  1. 名古屋大学   大学院工学研究科   情報工学専攻

    2002年4月 - 2004年3月

      詳細を見る

    国名: 日本国

  2. 名古屋大学   大学院工学研究科   計算理工学専攻

    2000年4月 - 2002年3月

      詳細を見る

    国名: 日本国

  3. 名古屋大学   工学部   電気電子・情報工学科(情報工学コース)

    1996年4月 - 2000年3月

      詳細を見る

    国名: 日本国

所属学協会 3

  1. 情報処理学会

    2011年11月 - 現在

  2. 電子情報通信学会

    2002年11月 - 現在

  3. 日本ソフトウェア科学会

    2002年9月 - 現在

委員歴 42

  1. 2023年度電子情報通信学会ソサイエティ大会   現地開催校委員  

    2022年9月 - 2023年9月   

  2. IFIP WG 1.6: Rewriting   Member  

    2022年8月 - 現在   

      詳細を見る

    団体区分:その他

  3. 第25回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)   プログラム委員  

    2022年8月 - 2023年3月   

      詳細を見る

    団体区分:その他

  4. 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)   PC member  

    2022年2月 - 2022年9月   

      詳細を見る

    団体区分:その他

  5. 11th International Workshop on Confluence   PC member  

    2022年1月 - 2022年8月   

      詳細を見る

    団体区分:その他

  6. 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)   PC member  

    2021年2月 - 2021年9月   

      詳細を見る

    団体区分:その他

  7. 情報処理学会プログラミング研究会   運営委員  

    2020年4月 - 2024年3月   

      詳細を見る

    団体区分:学協会

  8. 情報処理学会論文誌プログラミング編集委員会   編集委員  

    2020年4月 - 2024年3月   

      詳細を見る

    団体区分:学協会

  9. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)   PC member  

    2019年11月 - 2021年7月   

      詳細を見る

    団体区分:その他

  10. Confluence Competition   SC member  

    2019年9月 - 現在   

      詳細を見る

    団体区分:その他

  11. 情報処理学会   代表会員  

    2019年4月 - 2021年3月   

      詳細を見る

    団体区分:学協会

  12. 2019年度LAシンポジウム   事務局員  

    2019年4月 - 2020年3月   

      詳細を見る

    団体区分:その他

  13. 第81回情報処理学会全国大会実行委員会   プログラム編成WG委員  

    2019年1月   

      詳細を見る

    団体区分:学協会

  14. 電子情報通信学会ソフトウェアサイエンス研究専門委員会   専門委員  

    2018年6月 - 2024年6月   

      詳細を見る

    団体区分:学協会

  15. 情報処理学会プログラミング研究会   主査  

    2018年4月 - 2020年3月   

  16. 情報処理学会論文誌プログラミング編集委員会   編集委員長  

    2018年4月 - 2020年3月   

      詳細を見る

    団体区分:学協会

  17. 情報処理学会   コンピュータサイエンス領域委員会委員  

    2018年4月 - 2019年3月   

      詳細を見る

    団体区分:学協会

  18. Confluence Competition 2018 (CoCo 2018)   OC member  

    2017年10月 - 2018年7月   

      詳細を見る

    団体区分:その他

  19. 19th International Symposium on Principles and Practice of Declarative Programming (PPDP 2017)   PC member  

    2016年12月 - 2017年10月   

  20. Confluence Competition 2017 (CoCo 2017)   OC member  

    2016年10月 - 2017年9月   

      詳細を見る

    団体区分:その他

  21. 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017)   Steering Committee, Organization Committee, and Program Committee members  

    2016年9月 - 2017年9月   

      詳細を見る

    団体区分:その他

  22. 8th International Symposium on Symbolic Computation in Software Science (SCSS 2017)   PC member  

    2016年8月 - 2017年4月   

      詳細を見る

    団体区分:その他

  23. 第79回情報処理学会全国大会実行委員会   実行委員  

    2016年8月 - 2017年3月   

      詳細を見る

    団体区分:学協会

  24. 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)   PC member  

    2016年4月 - 2016年9月   

      詳細を見る

    団体区分:その他

  25. Confluence Competition 2016 (CoCo 2016)   OC member  

    2015年9月 - 2016年9月   

      詳細を見る

    団体区分:その他

  26. 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016)   Steering Committee, Organization Committee, and Program Committee members  

    2015年9月 - 2016年7月   

      詳細を見る

    団体区分:その他

  27. Confluence Competition 2015 (CoCo 2015)   OC member  

    2014年10月 - 2015年8月   

      詳細を見る

    団体区分:その他

  28. 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)   Organization Committee co-chair and PC co-chair  

    2014年9月 - 2015年7月   

      詳細を見る

    団体区分:その他

  29. 情報処理学会プログラミング研究会   運営委員  

    2014年4月 - 2018年3月   

      詳細を見る

    団体区分:学協会

  30. 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2014)   PC member  

    2014年4月 - 2014年9月   

  31. 3rd International Workshop on Confluence (IWC 2014)   PC member  

    2014年4月 - 2014年7月   

      詳細を見る

    団体区分:その他

  32. 第16回プログラミングおよびプログラミング言語ワークショップ(PPL 2014)   プログラム委員  

    2014年3月   

      詳細を見る

    団体区分:その他

  33. 情報処理学会論文誌プログラミング編集委員会   編集委員  

    2013年4月 - 2017年3月   

      詳細を見る

    団体区分:学協会

  34. 情報処理学会   代表会員  

    2013年4月 - 2014年4月   

      詳細を見る

    団体区分:学協会

  35. 平成24年度電気関係学会東海支部大会   実行委員  

    2012年9月   

      詳細を見る

    団体区分:学協会

  36. 23rd International Conference on Rewriting Techniques and Applications (RTA 2012)   Member of Organizing Committee  

    2012年5月 - 2012年6月   

      詳細を見る

    団体区分:その他

  37. 1st International Workshop on Confluence (IWC 2012)   Member of Organizing Committee  

    2012年5月   

      詳細を見る

    団体区分:その他

  38. 情報処理学会東海支部   幹事  

    2012年4月 - 2014年5月   

      詳細を見る

    団体区分:学協会

  39. 2011年度LAシンポジウム   事務局員  

    2011年4月 - 2013年3月   

      詳細を見る

    団体区分:その他

  40. 第12回プログラミングおよびプログラミング言語ワークショップ(PPL 2010)   プログラム委員  

    2010年3月   

      詳細を見る

    団体区分:その他

  41. ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2009)   PC member  

    2009年1月   

      詳細を見る

    団体区分:その他

  42. 名報会(名大工学部情報コース同窓会)   幹事  

    2008年5月 - 現在   

      詳細を見る

    団体区分:その他

▼全件表示

受賞 7

  1. 情報処理学会論文編集貢献賞

    2020年5月   情報処理学会  

    西田直樹

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

  2. 情報処理学会研究会活動貢献賞

    2020年2月   情報処理学会  

    西田直樹

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

  3. 平成24年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞

    2013年5月   電子情報通信学会ソフトウェアサイエンス研究会   Malbolge低級アセンブリプログラミングにおける制御命令の配置設計のためのSATソルバの利用

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

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

  4. 平成23年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞

    2012年5月   電子情報通信学会ソフトウェアサイエンス研究会   2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み

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

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

  5. 平成23年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞

    2012年5月   電子情報通信学会ソフトウェアサイエンス研究会   語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて

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

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

  6. 第67回(平成22年度)電子情報通信学会論文賞

    2011年5月   電子情報通信学会   基本対称関数に基づく節をもつCNF論理式の充足可能性判定

    馬野洋平,酒井正彦,西田直樹,坂部俊樹,草刈圭一朗

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

  7. 平成14年度電気関係学会東海支部連合大会 奨励賞

    2003年1月   電気関係学会東海支部連合  

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

▼全件表示

 

論文 236

  1. A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations 査読有り 国際誌

    Misaki Kojima and Naoki Nishida

    Journal of Information Processing   32 巻   頁: 417 - 435   2024年5月

     詳細を見る

    担当区分:最終著者, 責任著者   記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元:Information Processing Society of Japan  

    An all-path reachability (APR, for short) problem of a logically constrained term rewrite system (LCTRS, for short) is a pair of constrained terms representing state sets. An APR problem is demonically valid if every finite execution path from any state in the first set to an irreducible state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by an LCTRS to an APR problem with irreducible constant destinations. In this paper, by focusing on quasi-termination of constrained narrowing, we characterize a class of LCTRSs of which APR problems with constant destinations are decidable. Quasi-termination of a (constrained) term w.r.t. narrowing is the finiteness of the set of reachable narrowed (constrained) terms from the initial (constrained) term up to variable renaming (and equivalence of constraints). To this end, we first introduce an inference rule for disproofs to a proof system for APR problems with constant destinations and formulate (dis)proof trees of APR problems in the style of cyclic proofs. Secondly, to prove correctness of disproof trees, we adapt constrained narrowing to LCTRSs and show soundness of constrained narrowing of LCTRSs w.r.t. constrained rewriting. Thirdly, we show a sufficient condition of LCTRSs for quasi-termination of constrained narrowing starting from linear constrained terms that have no nesting of defined symbols: Rewrite rules are right-linear and nesting-free w.r.t. defined symbols, and the application of rewrite rules for (mutually) recursive defined symbols does not increase the height of resulting constrained terms of narrowing. Finally, we show that if a constrained term is quasi-terminating w.r.t. narrowing of an LCTRS over a sort-wise finite signature with a decidable theory, then the APR problem consisting of the constrained term and an irreducible constant is decidable.

    DOI: 10.2197/ipsjjip.32.417

  2. Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting 査読有り 国際誌

    Misaki Kojima and Naoki Nishida

    Journal of Logical and Algebraic Methods in Programming   135 巻   頁: 1 - 19   2023年10月

     詳細を見る

    担当区分:最終著者, 責任著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    A concurrent program with semaphore-based exclusive control can be modeled by a logically constrained term rewrite system. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem of the system is a pair of state sets and is demonically valid if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, we propose a weakened but easily-implementable variant of an existing proof system for all-path reachability problems. As a case study, we deal with the race freedom of concurrent programs with semaphore-based exclusive control.

    DOI: 10.1016/j.jlamp.2023.100903

  3. On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic 査読有り

    Ayuka Mastumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin

    Proceedings of the 19th International Workshop on Termination     頁: 1 - 6   2023年8月

     詳細を見る

    担当区分:最終著者, 責任著者   記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

    As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV-LCTRSs to solve a singleton DP problem consisting of a dependency pair forming a self-loop. The processor is based on an acyclic directed graph such that the nodes are bit-vectors and any dependency chain of the problem is projected to a path of the graph. We show a sufficient condition for the existence of such an acyclic graph, and simplify it for a specific case.

    DOI: 10.48550/arXiv.2307.14094

  4. CO3 (Version 2.4)

    Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

    Proceedings of the 12th International Workshop on Confluence     頁: 67   2023年8月

     詳細を見る

    担当区分:筆頭著者, 責任著者   記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  5. A New Format for Rewrite Systems 査読有り 国際共著

    Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, Rene Thiemann, and Akihisa Yamada

    Proceedings of the 12th International Workshop on Confluence     頁: 32 - 37   2023年8月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  6. On Representations of Waiting Queues for Semaphores in Logically Constrained Term Rewrite Systems 査読有り

    Misaki Kojima and Naoki Nishida

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

     詳細を見る

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

    A transformation of concurrent programs with semaphore-based exclusive control and waiting queues into logically constrained term rewrite systems (LCTRSs, for short) has been proposed. To represent waiting queues, the transformation adopts a turn waiting system with number tickets, while the use of usual lists is a straightforward approach. In this abstract, we show a list-based approach to waiting queues and compare the two approaches by means of verification of race freedom of a simple reader-writer example.

  7. A Nesting-Preserving Transformation of SIMP Programs into Logically Constrained Term Rewrite Systems 査読有り

    Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

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

     詳細を見る

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

    In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must be often useful in analyzing the transformed LCTRS, but, to use such features, we have to know how to transform the program into the LCTRS, e.g., we keep the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C integer program) into an LCTRS. The transformation is almost based on previous work and introduces the nesting of function symbols that correspond to statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness of the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.

  8. ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて

    松見 歩佳,西田 直樹,小嶋 美咲,申 東訓

    電子情報通信学会技術報告   122 巻 ( 432 ) 頁: 85 - 90   2023年3月

     詳細を見る

    担当区分:責任著者   記述言語:日本語   掲載種別:研究論文(研究会,シンポジウム資料等)  

    ビットベクトル制約付き項書換え系(BV-LCTRS)はC言語などのプログラムのモデルとして有用である.等価性検証に書換え帰納法を用いる際には,与えられた書換え系に帰納法の仮定となる書換え規則を加えて得られる書換え系の停止性が何度も証明される. LCTRSの停止性証明には項書換え系と同様に依存対プロセッサを使用して証明する枠組みの依存対フレームワークが用いられるが,整数制約を持つLCTRSの停止性証明において最も強力なプロセッサの1つである多項式解釈プロセッサはBV-LCTRSには適用できない.本稿では,BV-LCTRSの停止性証明を強化することを目的として,新たな依存対プロセッサとしてビットベクトル上の多項式解釈プロセッサと単一自己ループ除去プロセッサを提案する.

  9. From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting 査読有り 国際誌

    Misaki Kojima and Naoki Nishida

    Proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages, Lecture Notes in Computer Science   13880 巻   頁: 161 - 179   2023年1月

     詳細を見る

    担当区分:最終著者, 責任著者   記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Springer, Cham  

    An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by a logically constrained term rewrite system to an all-path reachability problem of the system. In this paper, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.

    DOI: 10.1007/978-3-031-24841-2_11

  10. CO3 (Version 2.3)

    Naoki Nishida and Misaki Kojima

    Proceedings of the 11th International Workshop on Confluence     頁: 63   2022年8月

     詳細を見る

    担当区分:筆頭著者, 責任著者   記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  11. Confluence Competition 2022 国際共著

    Raul Gutierrez, Aart Middeldorp, Naoki Nishida, and Kiraku Shintani

    Proceedings of the 11th International Workshop on Confluence     頁: 54   2022年8月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  12. On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms 査読有り

    Naoki Nishida, Misaki Kojima, and Takumi Kato

    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022)     頁: 1 - 16   2022年7月

     詳細を見る

    担当区分:筆頭著者, 責任著者   記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work converts a statement list to rewrite rules in a stepwise manner, and proves the correctness along such a conversion and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language comprises of inference rules that define transition steps of configurations. Partial instances of such inference rules are almost the same as rewrite rules in the transformed LCTRS. In this paper, we aim at establishing a framework for plain definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work, we show an injective function from configurations to terms, and reformulate the transformation by means of the injective function. The injective function maps a transition step to a reduction step, and results in a plain correctness proof.

  13. On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting 査読有り

    Misaki Kojima and Naoki Nishida

    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022)     頁: 1 - 16   2022年7月

     詳細を見る

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

    A concurrent program with semaphore-based exclusive control can be transformed into a logically constrained term rewrite system that is computationally equivalent to the program. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem is a pair of state sets and is true if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, as a case study, we show how to apply the framework to the race-freeness of semaphore-based exclusive control in the program. Finally, we show a simplified variant of a proof system for all-path reachability problems.

  14. On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs 査読有り

    Shujun Zhang and Naoki Nishida

    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022)     頁: 1 - 14   2022年7月

     詳細を見る

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

    A GSC-terminating and orthogonal inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. Under certain assumptions, it has been shown that a quantifier- and cut-free cyclic proof of a sequent can be transformed into a rewriting-induction (RI, for short) proof of the corresponding term equation. The RI proof can be transformed back into the cyclic proof, but it is not known how to transform arbitrary RI proofs into cyclic proofs. In this paper, we show that for a quantifier- and logical-connective-free sequent, if there exists an RI proof of the corresponding term equation, then there exists a cyclic proof of some sequent w.r.t. some IDS such that the cyclic proof ensures the validity of the initial sequent. To this end, we show a transformation of the RI proof into such a cyclic proof, a sequent, and an IDS.

  15. Transforming orthogonal inductive definition sets into confluent term rewrite systems 査読有り 国際誌

    Shujun Zhang and Naoki Nishida

    Journal of Logical and Algebraic Methods in Programming   127 巻   頁: 1 - 17   2022年6月

     詳細を見る

    担当区分:最終著者, 責任著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    In this paper, we transform an orthogonal inductive definition set, which is a set of productions for inductive predicates, into a confluent term rewrite system such that a quantifier-free sequent is valid w.r.t. the inductive definition set if and only if an equation representing the sequent is an inductive theorem of the term rewrite system. To this end, we first propose a transformation of an orthogonal inductive definition set into a confluent term rewrite system that is equivalent to the inductive definition set in the sense of evaluating ground formulas. Then, we show that termination of the inductive definition set is proved by the generalized subterm criterion if and only if termination of the transformed term rewrite system is so. Finally, we show that the transformed term rewrite system with some rewrite rules for sequents has the expected property. In addition, we show a termination criterion for the union of term rewrite systems whose termination is proved by the generalized subterm criterion.

    DOI: 10.1016/j.jlamp.2022.100779

  16. On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs 査読有り 国際誌

    Shujun Zhang and Naoki Nishida

    Proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), Lecture Notes in Computer Science   13215 巻   頁: 262 - 281   2022年5月

     詳細を見る

    担当区分:責任著者   記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Springer  

    An inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. In this paper, to compare rewriting induction (RI, for short) with cyclic proof systems, under certain assumptions, we show that if a sequent has a cut- and quantifier-free cyclic proof, then there exists an RI proof for a term equation of the sequent. To this end, we propose a transformation of a cut- and quantifier-free cyclic proof of the sequent into an RI proof for the corresponding equation.

    DOI: 10.1007/978-3-030-99461-7_15

  17. プログラム逆化のための文脈自由表現の等価関係に基づく項書換え系決定化手法の実装

    熊谷 妃美香,西田 直樹

    情報処理学会第84回全国大会講演論文集     頁: 271 - 272   2022年3月

     詳細を見る

    担当区分:責任著者   記述言語:日本語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  18. LLVM中間表現の意味論規則を表現する制約付き書換え規則について

    加藤 拓洋,西田 直樹,酒井 正彦

    電子情報通信学会技術報告   121 巻 ( 318 ) 頁: 89 - 94   2022年1月

     詳細を見る

    担当区分:責任著者   記述言語:日本語   掲載種別:研究論文(研究会,シンポジウム資料等)  

    C言語に沿った簡易プログラミング言語を論理制約付き項書換え系(LCTRS)に変換し,元のプログラムの性質をLCTRSの性質に帰着して検証する手法が研究されている.本稿では,LCTRSへ変換できるプログラミング言語を増やすことをめざし,LLVM中間表現からLCTRSへの変換を提案する.一般に,LLVM中間表現の意味論ではメモリ及び変数への割当てが写像として計算状態に含まれる.一方,写像をデータとして扱わないLCTRSへの既存の変換では写像の値域を関数記号の引数として保持させることになり正当性証明を複雑にする.本稿ではメモリ及び割当てに相当する写像をデータとして扱うLCTRSを用いることで,変換とその正当性証明を簡潔にする.具体的には,プログラムの計算状態から項への単射関数を定義し,LLVM中間表現の各命令とそれに適用可能な各意味論規則に対して,1つの制約付き書換え規則を生成する.

  19. 制約付き書換え帰納法におけるラグランジュ補間を用いた補題生成

    比嘉 慎哉,西田 直樹,酒井 正彦

    日本ソフトウェア科学会第38回大会講演論文集     頁: 1 - 13   2021年9月

     詳細を見る

    担当区分:責任著者   記述言語:日本語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  20. Determinization of inverted grammar programs via context-free expressions 査読有り 国際誌

    Naoki Nishida and Minami Niwa

    Journal of Logical and Algebraic Methods in Programming   122 巻   頁: 1 - 26   2021年8月

     詳細を見る

    担当区分:筆頭著者, 責任著者   記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.2021.100688

    その他リンク: http://hdl.handle.net/2237/0002001914

  21. Confluence Competition 2021 国際共著

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

    Proceedings of the 10th International Workshop on Confluence     頁: 51   2021年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  22. CO3 (Version 2.2)

    Naoki Nishida

    Proceedings of the 10th International Workshop on Confluence     頁: 61   2021年7月

     詳細を見る

    担当区分:筆頭著者, 責任著者   記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  23. 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.

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

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

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

     詳細を見る

    担当区分:責任著者   記述言語:日本語   掲載種別:研究論文(研究会,シンポジウム資料等)  

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

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

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

     詳細を見る

    記述言語:日本語  

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

  26. Reversible CSP Computations 査読有り

    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

  27. ReverCSP: Time-Travelling in CSP Computations 査読有り

    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

  28. Confluence Competition 2020 国際共著

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

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

     詳細を見る

    記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  29. CO3 (Version 2.1)

    Naoki Nishida

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

     詳細を見る

    担当区分:筆頭著者, 責任著者   記述言語:英語   掲載種別:研究論文(研究会,シンポジウム資料等)  

  30. 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月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

  31. 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

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

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

     詳細を見る

    記述言語:日本語  

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

  34. 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月

     詳細を見る

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

  35. 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

  36. 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.

  37. 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月

     詳細を見る

    記述言語:英語  

    In this paper, we aim at formalizing a transformation of an IMP program into a logically constrained term rewriting system (LCTRS, for short) in Isabelle/HOL. To this end, we formalize LCTRSs and the transformation in Isabelle/HOL.

  38. 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.

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

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

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

     詳細を見る

    記述言語:日本語  

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

  40. 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

  41. 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

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

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

     詳細を見る

    記述言語:日本語  

  44. 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

  45. 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

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

  48. 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.

  49. CO3 (Version 1.5)

    Naoki Nishida, Yuta Tsuruta, and Yoshiaki Kanazawa

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

     詳細を見る

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

  50. 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

  51. 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月

     詳細を見る

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

    We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.

    DOI: 10.4230/LIPIcs.FSCD.2018.32

  52. 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

  53. 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

  54. 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

  55. 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

  56. 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

  57. CO3 (Version 1.4)

    Naoki Nishida, Yoshiaki Kanazawa,, and Karl Gmeiner

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

     詳細を見る

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

  58. 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

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

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

     詳細を見る

    記述言語:日本語  

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

  61. 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

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

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

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

     詳細を見る

    記述言語:日本語  

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

  63. 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

  64. 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

  65. 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.

  66. CO3 (Version 1.3)

    Naoki Nishida, Takayuki Kuroda, and Karl Gmeiner

    Proceedings of the 5th International Workshop on Confluence (IWC 2016)     頁: 74   2016年9月

     詳細を見る

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

  67. 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

  68. 難読性の高いMalbolgeコードを生成するコンパイラのための中間言語

    河邉 翔平,酒井 正彦,西田 直樹,関 浩之

    電子情報通信学会技術報告   116 巻 ( 127 ) 頁: 105-110   2016年7月

     詳細を見る

    記述言語:日本語  

  69. 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

  70. 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.

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

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

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

     詳細を見る

    記述言語:日本語  

  72. 組合せ最適化問題記述のためのSQLの拡張

    内田 佑作, 酒井 正彦, 西田 直樹

    電子情報通信学会技術報告   115 巻 ( 508 ) 頁: 25-30   2016年3月

     詳細を見る

    記述言語:日本語  

    近年,充足可能性判定ソルバの高速化がめざましい.しかしながらこれらのソルバを用いて組合せ最適化問題を解くための論理式へのコーディングは容易ではない.本稿では,組合せ最適化問題の定義の容易な記述を可能にするため,データベース問い合わせ言語SQLに対して組合せ最適化問題を記述するための構文を追加し,その記述から充足可能性判定ソルバを利用して問題の解を得るための手法について論ずる.

  73. 拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証

    柳澤 真志, 西田 直樹, 酒井 正彦

    電子情報通信学会技術報告   115 巻 ( 508 ) 頁: 31-36   2016年3月

     詳細を見る

    記述言語:日本語  

    ループ不変式を生成するための手法として,与えたテンプレートと事前条件と事後条件から得られる検証式をFarkas補題に基づき変換する手法が研究されている.Farkas補題に基づく変換では線形な多項式の不等式のみを原始論理式として含む論理式を等価変換する.それを変数や関数適用項の積を単項式とする多項式上に拡張した拡張Farkas補題が提案され,非線形なループ不変式を生成できる場合があることが示された.しかし,拡張Farkas補題を用いて生成したループ不変式がプログラム検証に有効かどうかについては議論されていない.本稿では,プロラム検証における拡張Farkas補題に基づくループ不変式の生成法の有効性を評価し,拡張Farkas補題を有効に利用する検証手法を提案する.具体的には,未知係数を含む複数の検証式の一部を拡張Farkas補題により変換し,それを充足する未知係数の割り当てを残りの検証式の未知係数に代入した後に恒真性を判定する.

  74. ナローイングによる制約付き依存対の変換

    笹野 智裕, 西田 直樹, 酒井 正彦

    電子情報通信学会技術報告   115 巻 ( 420 ) 頁: 123-128   2016年1月

     詳細を見る

    記述言語:日本語  

    項書換え系の停止性証明の枠組みである依存対フレームワークは項書換え規則に制約を付随させた制約付き項書換え系を対象に拡張された.本論文では、拡張された依存対フレームワークにおけるナローイングによる依存対の変換の適用条件を緩和する.具体的には,先行研究における変換対象の依存対が直接接続可能でないという条件を満たさない場合にも変換が健全であることことを示す.

  75. 制約付き項書換え系における停止性と帰納的定理の同時証明

    川本 佳史, 西田 直樹, 酒井 正彦

    電子情報通信学会技術報告   115 巻 ( 420 ) 頁: 75-80   2016年1月

     詳細を見る

    記述言語:日本語  

  76. Constrained Term Rewriting tooL 査読有り

    Cynthia Kop and Naoki Nishida

    Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science   ( 9450 ) 頁: 549-557   2015年11月

     詳細を見る

    記述言語:英語  

    This paper discusses Ctrl, a tool to analyse - both automatically and manually - term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and automatically analyse various properties such as termination, confluence and quasi-reductivity. Ctrl also offers both a manual and automatic mode for equivalence tests using inductive theorem proving, giving support for and verification of "hand-written" term equivalence proofs.

    DOI: 10.1007/978-3-662-48899-7_38

  77. SATソルバへの基数制約節導入における学習節の最大保持数

    塚本 尚秀, 酒井 正彦, 西田 直樹, 橋本 健二

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

     詳細を見る

    記述言語:日本語  

  78. Reducing Relative Termination to Dependency Pair Problems 査読有り

    Jose Iborra, Naoki Nishida, German Vidal, and Akihisa Yamada

    Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science   9195 巻   頁: 163-178   2015年8月

     詳細を見る

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

    Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce a new 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. The practical significance of our method is illustrated by means of an experimental evaluation.

    DOI: 10.1007/978-3-319-21401-6_11

  79. CO3: a COnverter for proving COfluence of COnditional TRSs

    Naoki Nishida, Takayuki Kuroda, Makishi Yanagisawa, and Karl Gmeiner

    Proceedings of the 4th International Workshop on Confluence (IWC 2015)     頁: 42   2015年8月

     詳細を見る

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

  80. Confluence Competition 2015

    Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl

    Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science   9195 巻   頁: 101-104   2015年8月

     詳細を見る

    記述言語:英語  

    Confluence is one of the central properties of rewriting. Our competition aims to foster the development of techniques for proving/disproving confluence of various formalisms of rewriting automatically. We explain the background and setup of the 4th Confluence Competition.

    DOI: 10.1007/978-3-319-21401-6_5

  81. パターン除去による制約付き項書換え系の等価変換

    長尾 貴浩, 西田 直樹, 酒井 正彦

    電子情報通信学会技術報告   115 巻 ( 153 ) 頁: 167-172   2015年7月

     詳細を見る

    記述言語:日本語  

    制約付き項書換え系は整数制約などにより規則の適用を制御できるように項書換え系を拡張した枠組みである.書換え規則の左辺に現れるパターンの一部を意味を変えることなく除去することにより,様々な性質の解析が容易となる.本稿では,左辺に解釈項のパターンのみを持つ制約付き項書換え系のパターン除去に基づく変換を提案し,この変換が十分完全性や最内停止性などの性質に関して等価変換となる十分条件を示す.また,変換の応用として書換え完全性の判定法を提案する.

  82. 制約付き項書換え系における関数合成の可換性を自動証明するためのヒューリスティック

    栗木隆太朗, 西田直樹, 酒井正彦, 坂部俊樹

    電子情報通信学会技術報告   114 巻 ( 510 ) 頁: 91-96   2015年3月

     詳細を見る

    記述言語:日本語  

  83. 木構造データを扱う関数の逆Unfold問題の発見的解法

    加藤友郁, 長島正憲, 酒井正彦, 西田直樹, 坂部俊樹

    電子情報通信学会技術報告   114 巻 ( 510 ) 頁: 85-90   2015年3月

     詳細を見る

    記述言語:日本語  

  84. A framework for computing finite SLD trees 査読有り

    Naoki Nishida and German Vidal

    Journal of Logical and Algebraic Methods in Programming   84 巻 ( 2 ) 頁: 197-217   2015年3月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    The search space of SLD resolution, usually represented by means of a so-called SLD tree, is often infinite. However, there are many applications that must deal with possibly infinite SLD trees, like partial evaluation or some static analyses. In this context, being able to construct a finite representation of an infinite SLD tree becomes useful.

    In this work, we introduce a framework to construct a finite data structure representing the (possibly infinite) SLD derivations for a goal. This data structure, called closed SLD tree, is built using four basic operations: unfolding, flattening, splitting, and subsumption. We prove some basic properties for closed SLD trees, namely that both computed answers and calls are preserved. We present a couple of simple strategies for constructing closed SLD trees with different levels of abstraction, together with some examples of its application. Finally, we illustrate the viability of our approach by introducing a test case generator based on exploring closed SLD trees.

    DOI: 10.1016/j.jlamp.2014.11.006

  85. 制約付き項書換え系の停止性証明におけるナローイングの効果について

    上山智也, 西田直樹, 酒井正彦, 坂部俊樹

    電子情報通信学会技術報告   114 巻 ( 416 ) 頁: 43-48   2015年1月

     詳細を見る

    記述言語:日本語  

  86. 例外処理を含む関数型プログラムの停止性証明のための条件付き依存対法の実現

    太田浩一, 濱口毅, 酒井正彦, 山田晃久, 西田直樹, 坂部俊樹

    電子情報通信学会技術報告   114 巻 ( 416 ) 頁: 55-60   2015年1月

     詳細を見る

    記述言語:日本語  

  87. A Finite Representation of the Narrowing Space 査読有り

    Naoki Nishida and German Vidal

    Revised Selected Papers of the 23rd International Conference on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science   8901 巻   頁: 54-71   2014年12月

     詳細を見る

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

    Narrowing basically extends rewriting by allowing free vari- ables in terms and by replacing matching with unification. As a con- sequence, the search space of narrowing becomes usually infinite, as in logic programming. In this paper, we introduce the use of some operators that allow one to always produce a finite data structure that still rep- resents all the narrowing derivations. Furthermore, we extract from this data structure a novel, compact equational representation of the (pos- sibly infinite) answers computed by narrowing for a given initial term. Both the finite data structure and the equational representation of the computed answers might be useful in a number of areas, like program comprehension, static analysis, program transformation, etc.

    DOI: 10.1007/978-3-319-14125-1

  88. Automatic Constrained Rewriting Induction towards Verifying Procedural Programs 査読有り

    Cynthia Kop and Naoki Nishida

    Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014)   ( 8858 ) 頁: 334-353   2014年11月

     詳細を見る

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

    This paper aims at developing a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can handle realistic functions, involving, e.g., integers and arrays. An implementation is provided.

    DOI: 10.1007/978-3-319-12736-1_18

  89. A Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold Problem

    Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, and Naoki Nishida

    IPSJ Special Interest Group on Programming   ( 2014-3-(9) ) 頁: 1-7   2014年11月

     詳細を見る

    記述言語:英語  

  90. 制約付き項書換え系の書換え帰納法における関数合成の可換性を利用した補題生成について

    栗木 隆太朗, 西田 直樹, 酒井 正彦

    平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集   ( M4-1 ) 頁: 1   2014年9月

     詳細を見る

    記述言語:日本語  

  91. 条件除去変換を用いた条件付き項書換え系の合流性証明手続きについて

    柳澤 真志, 西田 直樹, 酒井 正彦, 坂部 俊樹

    平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集   ( M4-4 ) 頁: 1   2014年9月

     詳細を見る

    記述言語:日本語  

  92. 制約付き項書換え系の依存対法におけるプレスブルガー算術式の恒真性判定の回数削減について

    上山 智也, 西田 直樹, 坂部 俊樹, 酒井 正彦

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

     詳細を見る

    記述言語:日本語  

  93. 項書換え系における関数の等価性を保存する引数切り落としの十分条件について

    川本 佳史, 西田 直樹, 酒井 正彦, 坂部 俊樹

    平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集   ( M4-2 ) 頁: 1   2014年9月

     詳細を見る

    記述言語:日本語  

  94. 制約付き項書換えにおいて等式が関数等価性を表現するための必要十分条件について

    片岡 巧, 西田 直樹, 酒井 正彦, 坂部 俊樹

    平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集   ( M4-4 ) 頁: 1   2014年9月

     詳細を見る

    記述言語:日本語  

  95. On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants 査読有り

    Naoki Nishida and Takumi Kataoka

    Proceedings of the 14th International Workshop on Termination (WST 2014)     頁: 1-5   2014年7月

     詳細を見る

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

    Recently, to analyze procedural programs by using techniques in the field of term rewriting, several transformations of a program into a rewrite system have been developed. Such transformations are basically complete in the sense of computation, and e.g., termination of the rewrite system ensures termination of the program. However, in general, termination of the program is not preserved by the transformations and, thus, the preservation of termination is a common interesting problem. In this paper, we discuss the improvement of a transformation from a simple procedural program over integers into a constrained term rewriting system by appending loop invariants to loop conditions of "while" statements so as to preserve termination as much as possible.

  96. Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems 査読有り

    Karl Gmeiner and Naoki Nishida

    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics   40 巻   頁: 3-14   2014年7月

     詳細を見る

    記述言語:英語  

    Transforming conditional term rewrite systems (CTRSs) into unconditional systems (TRSs) is a common approach to analyze properties of CTRSs via the simpler framework of unconditional rewriting. In the past many different transformations have been introduced for this purpose. One class of transformations, so-called unravelings, have been analyzed extensively in the past. In this paper we provide an overview on another class of transformations that we call structure-preserving transformations. In these transformations the structure of the conditional rule, in particular their left-hand side is preserved in contrast to unravelings. We provide an overview of transformations of this type and define a new transformation that improves previous approaches.

    DOI: 10.4230/OASIcs.WPTE.2014.3

  97. On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation 査読有り

    Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner

    Proceedings of the 3rd International Workshop on Confluence (IWC 2014)     頁: 24-28   2014年7月

     詳細を見る

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

    This paper improves the existing criterion for proving confluence of a normal conditional term rewriting system (CTRS) via the Serbanuta-Rosu transformation, a computationally equivalent transformation of CTRSs into unconditional term rewriting systems (TRS), showing that a weakly left-linear normal CTRS is confluent if the transformed TRS is confluent. Then, we discuss usefulness of the optimization of the Serbanuta-Rosu transformation, which has informally been proposed in the literature.

  98. Inverse Unfold Problem and Its Heuristic Solving 査読有り

    Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, and Naoki Nishida

    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics   40 巻   頁: 27-38   2014年7月

     詳細を見る

    記述言語:英語  

    Unfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. This paper, by using an example, show that restoring an one-step unfolding is not easy, i.e., a challenging task, since some rules used by unfolding may be lost. We formalize this problem by regarding one-step program transformation as a relation. Next we discuss some issues on a specific framework, called pure-constructor systems, which constitute a subclass of conditional term rewriting systems. We show that the inverse of T preserves rewrite relations if T preserves rewrite relations and the signature. We propose a heuristic procedure to solve the problem, and show its successful examples. We improve the procedure, and show examples for which the improvement takes effect.

    DOI: 10.4230/OASIcs.WPTE.2014.27

  99. On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings 査読有り

    Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner

    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics   40 巻   頁: 39-50   2014年7月

     詳細を見る

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

    In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is sound for weakly left-linear normal conditional term rewriting systems (CTRS). Here, soundness for a CTRS means that reduction of the transformed unconditional term rewriting system (TRS) creates no undesired reduction for the CTRS. We first show that every reduction sequence of the transformed TRS starting with a term corresponding to the one considered on the CTRS is simulated by the reduction of the TRS obtained by the simultaneous unraveling. Then, we use the fact that the unraveling is sound for weakly left-linear normal CTRSs.

    DOI: 10.4230/OASIcs.WPTE.2014.39

  100. 逆Unfold問題とその発見的解法

    加藤 友郁, 長島 正憲, 酒井 正彦, 西田 直樹

    電子情報通信学会技術報告   113 巻 ( 489 ) 頁: 13-18   2014年3月

     詳細を見る

    記述言語:日本語  

  101. 制約付き木オートマトンにおける不用な遷移規則の発見法について

    中野 靖大, 西田 直樹, 酒井 正彦, 坂部 俊樹, 草刈 圭一朗, 橋本 健二

    電子情報通信学会技術報告   113 巻 ( 489 ) 頁: 31-36   2014年3月

     詳細を見る

    記述言語:日本語  

  102. Conversion to tail recursion in term rewriting 査読有り

    Naoki Nishida and German Vidal

    The Journal of Logic and Algebraic Programming   83 巻 ( 1 ) 頁: 53-63   2014年1月

     詳細を見る

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

    Tail recursive functions are a special kind of recursive functions where the last action in their body is the recursive call. Tail recursion is important for a number of reasons (e.g., they are usually more efficient). In this article, we introduce an automatic transformation of first-order functions into tail recursive form. Functions are defined using a (first-order) term rewrite system. We prove the correctness of the transformation for constructor-based reduction over constructor systems (i.e., typical first-order functional programs).

    DOI: 10.1016/j.jlap.2013.07.001

  103. On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms 査読有り

    Naoki Nishida, Masahiko Sakai, and Yasuhiro Nakano

    Proceedings of the 2nd International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2013), Electronic Proceedings in Theoretical Computer Science   134 巻   頁: 1-10   2013年10月

     詳細を見る

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

    An inductive theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for reduction-completeness of constrained terms. In addition, the sufficient complete property of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms. This paper proposes a method to construct deterministic, complete, and constraint-complete constrained tree automata recognizing ground instances of constrained terms.

    DOI: 10.4204/EPTCS.134.1

  104. 等式集合の語問題から基底等式集合の語問題への帰着可能性について

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

    平成25年度電気関係学会東海支部連合大会論文集   ( M4-4 ) 頁: 1   2013年9月

     詳細を見る

    記述言語:日本語  

  105. 配列を含むプログラムの検証のための非線形不等式型ループ不変式の生成

    東野 惇一郎, 坂部 俊樹, 酒井 正彦, 草刈 圭一朗, 西田 直樹

    平成25年度電気関係学会東海支部連合大会論文集   ( M4-6 ) 頁: 1   2013年9月

     詳細を見る

    記述言語:日本語  

  106. 単純型付き項書換え系における帰納的定理自動証明の局所戦略について

    神谷 尚史, 草刈 圭一朗, 酒井 正彦, 坂部 俊樹, 西田 直樹

    平成25年度電気関係学会東海支部連合大会論文集   ( M4-3 ) 頁: 1   2013年9月

     詳細を見る

    記述言語:日本語  

  107. カリー化を組み込んだ高階辞書式経路順序の設計

    松原 穂波, 草刈 圭一朗, 酒井 正彦, 坂部 俊樹, 西田 直樹

    平成25年度電気関係学会東海支部連合大会論文集   ( M4-5 ) 頁: 1   2013年9月

     詳細を見る

    記述言語:日本語  

  108. プログラム中のポインタに関する表明式を動的に検査するインタプリタの開発

    杢谷 孔皓, 坂部 俊樹, 酒井 正彦, 草刈 圭一朗, 西田 直樹

    平成25年度電気関係学会東海支部連合大会論文集   ( M4-7 ) 頁: 1   2013年9月

     詳細を見る

    記述言語:日本語  

  109. 手続き型プログラムから書換え系への変換における停止性をより保存するためのループ不変式の利用

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

    平成25年度電気関係学会東海支部連合大会論文集   ( M2-6 ) 頁: 1   2013年9月

     詳細を見る

    記述言語:日本語  

  110. 幅優先探索型完備化手続きのErlangによる実装の並列実行の評価

    栗木 隆太朗, 西田 直樹, 坂部 俊樹, 酒井 正彦, 草刈 圭一朗

    平成25年度電気関係学会東海支部連合大会論文集   ( M2-5 ) 頁: 1   2013年9月

     詳細を見る

    記述言語:日本語  

  111. Term Rewriting with Logical Constraints 査読有り

    Cynthia Kop and Naoki Nishida

    Proceedings of the 9th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence   ( 8152 ) 頁: 343-358   2013年9月

     詳細を見る

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

  112. Malbolgeのワード長の拡大とそのプログラミング支援ツール

    加藤 起騎, 酒井 正彦, 坂部 俊樹, 草刈 圭一朗, 西田 直樹

    電子情報通信学会技術報告   113 巻 ( 159 ) 頁: 73-78   2013年7月

     詳細を見る

    記述言語:日本語  

  113. Proving Confluence of Conditional Term Rewriting Systems via Unravelings 査読有り

    Karl Gmeiner, Naoki Nishida and Bernhard Gramlich

    Proceedings of the 2nd International Workshop on Confluence     頁: 35-39   2013年6月

     詳細を見る

    記述言語:英語  

  114. Computing More Specific Versions of Conditional Rewriting Systems 査読有り

    Naoki Nishida and German Vidal

    Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science   7844 巻   頁: 137-154   2013年4月

     詳細を見る

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

  115. Improving Determinization of Grammar Programs for Program Inversion 査読有り

    Minami Niwa, Naoki Nishida, and Masahiko Sakai

    Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science   7844 巻   頁: 155-175   2013年4月

     詳細を見る

    記述言語:英語  

  116. 整数解を導出するための単体法とゴモリーカットの合成について

    伏見 政晃, 西田 直樹, 酒井 正彦, 草刈 圭一朗, 坂部 俊樹

    電子情報通信学会技術報告   112 巻 ( 458 ) 頁: 109-114   2013年3月

     詳細を見る

    記述言語:日本語  

  117. 制約付き項のインスタンスを受理する制約付き木オートマトンの構成法

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

    電子情報通信学会技術報告   112 巻 ( 373 ) 頁: 7-12   2013年1月

     詳細を見る

    記述言語:日本語  

  118. Malbolge低級アセンブリプログラミングにおける制御命令の配置設計のためのSATソルバの利用

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

    電子情報通信学会技術報告   112 巻 ( 373 ) 頁: 25-30   2013年1月

     詳細を見る

    記述言語:日本語  

  119. 三値関数を実現するMalbolge命令列の発見のためのSATエンコーディング

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

    電子情報通信学会技術報告   112 巻 ( 275 ) 頁: 7-12   2012年11月

     詳細を見る

    記述言語:日本語  

  120. Cooperの限量子除去アルゴリズムと単体法を逐次合成するための論理式変換

    伏見 政晃, 西田 直樹, 坂部 俊樹, 酒井 正彦, 草刈 圭一朗

    平成24年度電気関係学会東海支部連合大会論文集   ( A4-2 ) 頁: 1   2012年9月

     詳細を見る

    記述言語:日本語  

  121. 制約付き項のインスタンスを受理する制約付き木オートマトンの構成について

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

    平成24年度電気関係学会東海支部連合大会論文集   ( A4-4 ) 頁: 1   2012年9月

     詳細を見る

    記述言語:日本語  

  122. 単純型付き項書換え系の停止性証明におけるカリー化の利用

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

    平成24年度電気関係学会東海支部連合大会論文集   ( A4-3 ) 頁: 1   2012年9月

     詳細を見る

    記述言語:日本語  

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

    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

  124. 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月

     詳細を見る

    記述言語:英語  

  125. 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月

     詳細を見る

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

  126. 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月

     詳細を見る

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

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

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

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

     詳細を見る

    記述言語:日本語  

  128. A Sound Type System for Typing Runtime Errors 査読有り

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

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

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:日本語  

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

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

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

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

  140. 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月

     詳細を見る

    記述言語:英語  

  141. 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

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

    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

  143. Program Inversion for Tail Recursive Functions 査読有り

    Naoki Nishida and German Vidal

    Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs   10 巻   頁: 283-298   2011年5月

     詳細を見る

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

    Program inversion is a fundamental problem that has been addressed in many different programming settings and applications. In the context of term rewriting, several methods already exist for computing the inverse of an injective function. These methods, however, usually return non-terminating inverted functions when the considered function is tail recursive. In this paper, we propose a direct and intuitive approach to the inversion of tail recursive functions. Our new technique is able to produce good results even without the use of an additional post-processing of determinization or completion. Moreover, when combined with a traditional approach to program inversion, it constitutes a promising approach to define a general method for program inversion. Our experimental results confirm that the new technique compares well with previous approaches.

    DOI: 10.4230/LIPIcs.RTA.2011.283

  144. 制約付き木オートマトンとその閉包性

    倉橋 克尚, 酒井 正彦, 西田 直樹, 野村 太志, 坂部 俊樹, 草刈 圭一朗

    電子情報通信学会技術報告   110 巻 ( 458 ) 頁: 61-66   2011年3月

     詳細を見る

    記述言語:日本語  

  145. 順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について

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

    信学技報 SS2010-44   110 巻 ( 336 ) 頁: 31-36   2010年12月

     詳細を見る

    記述言語:日本語  

  146. 等式理論を法とするDPLL遷移系について

    馬場達也, 坂部俊樹, 西田直樹, 草刈圭一朗, 酒井正彦

    信学技報 SS2010-36   110 巻 ( 227 ) 頁: 49-54   2010年10月

     詳細を見る

    記述言語:日本語  

  147. 難解言語Malbolgeのチューリング完全性について

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

    信学技報 SS2010-37   110 巻 ( 227 ) 頁: 55-60   2010年10月

     詳細を見る

    記述言語:日本語  

  148. 2カウンタ法に基づく基本対称節を持つCNF論理式のSATソルバ

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

    平成22年度電気関係学会東海支部連合大会論文集   ( D3-5 ) 頁: 1   2010年8月

     詳細を見る

    記述言語:日本語  

  149. 等式理論を法とする抽象DPLLアルゴリズムの提案

    馬場達也, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

    平成22年度電気関係学会東海支部連合大会論文集   ( D3-4 ) 頁: 1   2010年8月

     詳細を見る

    記述言語:日本語  

  150. 制約付き項書換え系における関数の効率的な等価性検証

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

    平成22年度電気関係学会東海支部連合大会論文集   ( D3-6 ) 頁: 1   2010年8月

     詳細を見る

    記述言語:日本語  

  151. Termination of Narrowing via Termination of Rewriting 査読有り

    Naoki Nishida and Germán Vidal

    Applicable Algebra in Engineering, Communication and Computing   21 巻 ( 3 ) 頁: 177-225   2010年5月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

  152. Goal-directed and Relative Dependency Pairs for Proving the Termination of Narrowing 査読有り

    José Iborra, Naoki Nishida, and Germán Vidal

    Postproceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009), Lecture Notes in Computer Science   6037 巻   頁: 52-66   2010年4月

     詳細を見る

    記述言語:英語  

  153. Proving Injectivity of Functions via Program Inversion in Term Rewriting 査読有り

    Naoki Nishida and Masahiko Sakai

    Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science   6009 巻   頁: 288-303   2010年4月

     詳細を見る

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

  154. 基本対象関数に基づく節を持つCNF論理式の充足可能性判定 査読有り

    馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗

    電子情報通信学会論文誌 D   J93-D 巻 ( 1 ) 頁: 1-9   2010年1月

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  155. 条件付き等式の変換に基づくプログラム生成

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

    信学技報 SS2009-41   109 巻 ( 343 ) 頁: 37-42   2009年12月

     詳細を見る

    記述言語:日本語  

  156. 高階書換え系における引数切り落とし法と実効規則

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

    信学技報 SS2009-39   109 巻 ( 343 ) 頁: 25-30   2009年12月

     詳細を見る

    記述言語:日本語  

  157. 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について

    御宿義勝, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

    信学技報 SS2009-40   109 巻 ( 343 ) 頁: 31-36   2009年12月

     詳細を見る

    記述言語:日本語  

  158. Improving the Termination Analysis of Narrowing in Left-Linear Constructor Systems 査読有り

    José Iborra, Naoki Nishida, and Germán Vidal

    Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009)     頁: 9 pages   2009年9月

     詳細を見る

    記述言語:英語  

    In this extended abstract, we introduce an extension of a previous technique
    for proving the termination of narrowing. Basically, given a rewrite system
    and an argument filtering, the previous technique required the filtered
    program to be free of extra-variables. In this work, we transform the original
    rewrite system so that, in some cases (namely when the filtered rewrite system
    is left-shallow), termination can still be proved despite the occurrence of
    extra-variables in the filtered system.

  159. 制約付き項書換え系の書換え帰納法における補題等式の自動生成法

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

    日本ソフトウェア科学会第26回大会講演論文集   ( 7B-2 ) 頁: 1-14   2009年9月

     詳細を見る

    記述言語:日本語  

  160. Context-Sensitive Innermost Reachability is Decidable for Linear Right-Shallow Term Rewriting Systems 査読有り

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

    IPSJ Transactions on Programming,   2 巻 ( 3 ) 頁: 20-32   2009年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

  161. Completion after Program Inversion of Injective Functions 査読有り

    Naoki Nishida and Masahiko Sakai

    Electronic Notes in Theoretical Computer Science   237 巻   頁: 39-56   2009年4月

     詳細を見る

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

    Given a constructor term rewriting system that defines injective functions, the inversion compiler proposed
    by Nishida, Sakai and Sakabe generates a conditional term rewriting system that defines the inverse relations
    of the injective functions, and then the compiler unravels the conditional system into an unconditional term
    rewriting system. In general, the resulting unconditional system is not (innermost-)confluent even if the
    conditional system is (innermost-)confluent. In this paper, we propose a modification of the Knuth-Bendix
    completion procedure, which is used as a post-processor of the inversion compiler. Given a confluent and
    operationally terminating conditional system, the procedure takes the resulting unconditional systems as
    input. When the procedure halts successfully, it returns convergent systems that are computationally
    equivalent to the conditional systems. To adapt the modified procedure to the conditional systems that are
    not confluent but innermost-confluent, we propose a simplified variant of the modified procedure. We report
    that the implementations of the procedures succeed in generating innermost-convergent inverse systems for
    all the examples we tried.

  162. 制約付き項書換え系における書換え帰納法 査読有り

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

    情報処理学会論文誌プログラミング   2 巻 ( 2 ) 頁: 80-96   2009年3月

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    帰納的定理の証明原理の1 つである潜在帰納法が制約付き項書換え系に対応するよ
    うに拡張され,命令型プログラムの等価性検証に応用されている.本論文では,別の
    証明原理である書換え帰納法を制約付き項書き換え系に対応するように拡張するとと
    もに,その正しさを証明する.また,拡張された書換え帰納法に基づいた帰納的定理
    の証明法を提案する.さらに,帰納的定理でないことを示す反証の手法についても議
    論する.

  163. 基本対称関数を付加したCNF論理式の充足可能性判定

    馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗

    信学技報 SS2008-44   108 巻 ( 362 ) 頁: 31-36   2008年12月

     詳細を見る

    記述言語:日本語  

  164. シャローな依存対から構成される項書換え系の停止性の決定可能性

    内山敬太, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

    信学技報 SS2008-45   108 巻 ( 362 ) 頁: 37-42   2008年12月

     詳細を見る

    記述言語:英語  

  165. ビットエラー通信路におけるスケーラブルCANの動作解析

    鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹

    信学技報 SS2008-37   108 巻 ( 242 ) 頁: 61-66   2008年10月

     詳細を見る

    記述言語:日本語  

  166. 制約付き項書換え系における書換え帰納法

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

    第71回情報処理学会・プログラミング研究会 配布資料     頁: 1-12   2008年10月

     詳細を見る

    記述言語:日本語  

  167. スケーラブルCANプロトコルの動作解析に関する予備的考察

    鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹

    平成20年度電気関係学会東海支部連合大会論文集   ( O-262 ) 頁: 1   2008年9月

     詳細を見る

    記述言語:日本語  

  168. 制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み 査読有り

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

    情報処理学会論文誌プログラミング   1 巻 ( 2 ) 頁: 100-121   2008年9月

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    手続き型プログラムの検証手法として,モデル検査やホーア論理に基づく検証手法
    が代表的である.一方,項書換えの分野では帰納的定理の証明手法として潜在帰納法
    や書換え帰納法などが広く研究されている.本論文では,帰納的定理の証明法を利用
    して手続き型プログラムの等価性の検証を試みる.具体的には,自然数上のwhile 言
    語で定義された手続き型関数からプレスブルガー文を規則の制約として持つことが許
    された制約付き項書換え系への変換を与え,その変換により手続き型プログラムの等
    価性を書換え系の関数の等価性に帰着させ,潜在帰納法を用いて等価性検証を試みる.
    この手法を実現するために,合流性を保証するための危険対定理および完備化手続き
    を制約付き書換えに対応するように拡張する.

  169. Completion as Post-Process in Program Inversion of Injective Functions 査読有り

    Naoki Nishida and Masahiko Sakai

    Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'08)     頁: 61-75   2008年7月

     詳細を見る

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

  170. 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序

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

    信学技報 SS2008-20   108 巻 ( 173 ) 頁: 43-48   2008年7月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  171. プレスブルガー文付き項書換え系における書換え帰納法について

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

    信学技報 SS2008-1   108 巻 ( 64 ) 頁: 1-6   2008年5月

     詳細を見る

    記述言語:日本語  

  172. 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム 査読有り

    黒川翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

    電子情報通信学会論文誌 D   J91-D 巻 ( 3 ) 頁: 757-770   2008年3月

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  173. 潜在帰納法を利用した手続き型プログラム検証の試み

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

    第68回情報処理学会・プログラミング研究会 配布資料     頁: 1-22   2008年3月

     詳細を見る

    記述言語:日本語  

  174. 等式を規則化する変換の停止条件

    水野清貴, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗

    信学技報 SS2007-61   107 巻 ( 505 ) 頁: 25-30   2008年3月

     詳細を見る

    記述言語:日本語  

  175. 動的型言語への柔らかい型付けによるエラー検出

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

    信学技報 SS2007-58   107 巻 ( 505 ) 頁: 7-12   2008年3月

     詳細を見る

    記述言語:英語  

  176. プログラム生成系GeneSysにおける等式仕様への否定の導入

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

    信学技報 SS2007-45   107 巻 ( 392 ) 頁: 43-48   2007年12月

     詳細を見る

    記述言語:日本語  

  177. 対話型埋込みによる数独問題の設計ツール

    馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗

    信学技報 SS2007-50   107 巻 ( 392 ) 頁: 73-78   2007年12月

     詳細を見る

    記述言語:日本語  

  178. 導出木からのループ検出による論理プログラムの非停止性証明法

    水谷知博, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗

    信学技報 SS2007-30   107 巻 ( 275 ) 頁: 1-6   2007年10月

     詳細を見る

    記述言語:日本語  

  179. 論理式への変換に基づく魔方陣の発見

    伊藤寛之, 酒井正彦, 草刈圭一朗, 坂部俊樹, 西田直樹

    平成19年度電気関係学会東海支部連合大会論文集   ( O-012 ) 頁: 1   2007年9月

     詳細を見る

    記述言語:日本語  

  180. 左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン

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

    信学技報 SS2007-16   107 巻 ( 176 ) 頁: 1-6   2007年8月

     詳細を見る

    記述言語:日本語  

  181. 振舞等価性の証明のための等式付き書換えに基づく潜在帰納法

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

    信学技報 SS2007-17   107 巻 ( 176 ) 頁: 7-12   2007年8月

     詳細を見る

    記述言語:日本語  

  182. * Transformation for Refining Unraveled Conditional Term Rewriting Systems 査読有り

    Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai

    Electronic Notes in Theoretical Computer Science   174 巻 ( 10 ) 頁: 75-95   2007年7月

     詳細を見る

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

    Unravelings, transformations from conditional term rewriting systems (CTRSs, for short) into unconditional
    term rewriting systems, are valuable for analyzing properties of CTRSs. In order to completely simulate
    rewrite sequences of CTRSs, the restriction by a particular context-sensitive and membership condition that
    is determined by extra function symbols introduced due to the unravelings, must be imposed on the rewrite
    relations of the unraveled CTRSs. In this paper, in order to weaken the context-sensitive and membership
    condition, we propose a transformation applied to the unraveled CTRSs, that reduces the number of the
    extra symbols. In the transformation, updating the context-sensitive condition properly, we remove the
    extra symbols that satisfy a certain condition. If the transformation succeeds in removing all of the extra
    symbols, we obtain the TRSs that are computationally equivalent with the original CTRSs.

  183. Static Dependeycy Pair Method for Proving Termination of Higher-Order Rewriting Systems

    Keiichirou Kusakari, Yasuo Isogai, , Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida

    IEICE Technical Report SS2007-12   107 巻 ( 99 ) 頁: 17-22   2007年6月

     詳細を見る

    記述言語:英語  

  184. Convergent Term Rewriting Systems for Inverse Computation of Injective Functions 査読有り

    Naoki Nishida, Masahiko Sakai, and Terutoshi Kato

    Proceedings of the 9th International Workshop on Termination (WST'07)     頁: 77-81   2007年6月

     詳細を見る

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

  185. 二階の書換え系における引数切り落とし法

    磯谷泰巨, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹

    信学技報 SS2007-13   107 巻 ( 99 ) 頁: 23-28   2007年6月

     詳細を見る

    記述言語:日本語  

  186. Decidability of Innermost Termination for Semi-Constructor Term Rewriting Systems

    Keita Uchiyama, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

    Theory of Computer Science and Its Applications, RIMS Kokyuroku (LA Symposium 2006 Winter)   1554 巻   頁: 166-170   2007年5月

     詳細を見る

    記述言語:英語  

  187. Confluence of Length Preserving String Rewriting Systems is Undecidable

    Yi Wang, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

    Theory of Computer Science and Its Applications, RIMS Kokyuroku (LA Symposium 2006 Winter)   1554 巻   頁: 171-177   2007年5月

     詳細を見る

    記述言語:英語  

  188. 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け 査読有り

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

    電子情報通信学会論文誌 D   J90-D 巻 ( 4 ) 頁: 978-989   2007年4月

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  189. 単純型項書換え系における定理自動証明系HOPSYS

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

    信学技報 SS2006-57   106 巻 ( 426 ) 頁: 7-12   2006年12月

     詳細を見る

    記述言語:日本語  

  190. 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み

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

    信学技報 SS2006-41 (KBSE2006-17)   106 巻 ( 324 ) 頁: 7-12   2006年10月

     詳細を見る

    記述言語:日本語  

  191. GeneSysによるプログラム生成例とIntroduction規則の追加

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

    信学技報 SS2006-46 (KBSE2006-22)   106 巻 ( 324 ) 頁: 37-42   2006年10月

     詳細を見る

    記述言語:日本語  

  192. 例外処理付きオブジェクト指向言語における情報流の安全性解析

    黒川翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

    信学技報 SS2006-42 (KBSE2006-18)   106 巻 ( 324 ) 頁: 13-18   2006年10月

     詳細を見る

    記述言語:日本語  

  193. 高階関数機能を持つ項書換え系のコンパイル

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

    平成18年度電気関係学会東海支部連合大会論文集   ( O-437 ) 頁: 1   2006年9月

     詳細を見る

    記述言語:日本語  

  194. 所属制約を持つ条件付き項書換え系の紐解き変換

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

    平成18年度電気関係学会東海支部連合大会論文集   ( O-438 ) 頁: 1   2006年9月

     詳細を見る

    記述言語:日本語  

  195. Transformation for Refining Unraveled Conditional Term Rewriting Systems 査読有り

    Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai

    Proceedings of the 6th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'06)     頁: 34-48   2006年8月

     詳細を見る

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

  196. Dependency Graph Method for Proving Termination of Narrowing 査読有り

    Naoki Nishida and Koichi Miura

    Proceedings of the 8th International Workshop on Termination (WST'06)     頁: 12-16   2006年8月

     詳細を見る

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

  197. 等式付き書換え系の等式数を削減する変換

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

    信学技報 SS2006-14   106 巻 ( 120 ) 頁: 7-12   2006年6月

     詳細を見る

    記述言語:日本語  

  198. 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け

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

    信学技報 SS2006-15   106 巻 ( 120 ) 頁: 13-18   2006年6月

     詳細を見る

    記述言語:日本語  

  199. 項正規表現に基づくSpi計算の機密性検証

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

    信学技報 SS2005-82   105 巻 ( 596 ) 頁: 35-40   2006年2月

     詳細を見る

    記述言語:日本語  

  200. 関数プログラムの停止性証明のための辞書式経路順序

    星野由美, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹

    信学技報 SS2005-85   105 巻 ( 597 ) 頁: 13-18   2006年2月

     詳細を見る

    記述言語:日本語  

  201. 暗号プロトコル記述からカラーペトリネットへの変換による機密性検証

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

    信学技報 SS2005-58   105 巻 ( 490 ) 頁: 19-24   2005年12月

     詳細を見る

    記述言語:日本語  

  202. 左線形シャローなどの項書換え系の停止性の決定性

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

    信学技報 COMP2005-50   105 巻 ( 499 ) 頁: 9-13   2005年12月

     詳細を見る

    記述言語:英語  

  203. 分散JoinJAVAプログラムの通信エラーに対する型判定システム

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

    信学技報 SS2005-67   105 巻 ( 491 ) 頁: 25-30   2005年12月

     詳細を見る

    記述言語:日本語  

  204. 重なりを持つTRSにおける最外戦略の完全性について

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

    信学技報 SS2005-46   105 巻 ( 331 ) 頁: 39-44   2005年10月

     詳細を見る

    記述言語:日本語  

  205. 関数プログラムの再帰構造解析と強計算性に基づく十分完全性の証明法 査読有り

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

    第4回情報科学技術フォーラム (FIT2005) 論文集, 情報科学技術レターズ   ( LA-001 ) 頁: 1-4   2005年9月

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  206. カラーペトリネットを用いた暗号プロトコルの安全性検証

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

    平成17年度電気関係学会東海支部連合大会論文集   ( O-198 ) 頁: 1   2005年9月

     詳細を見る

    記述言語:日本語  

  207. 分散JoinJAVAプログラムの正常実行性判定のための型システム

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

    平成17年度電気関係学会東海支部連合大会論文集   ( O-306 ) 頁: 1   2005年9月

     詳細を見る

    記述言語:日本語  

  208. 構成子項書換え系の逆計算プログラムの生成 査読有り

    西田直樹, 酒井正彦, 坂部俊樹

    電子情報通信学会論文誌 D-I   J88-D-I 巻 ( 8 ) 頁: 1171-1183   2005年8月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  209. 準構成子項書換え系における停止性の決定問題

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

    信学技報 SS2005-46   105 巻 ( 228 ) 頁: 13-18   2005年8月

     詳細を見る

    記述言語:英語  

  210. 難読プログラミング言語Malbolgeにおけるプログラム構成手法

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

    信学技報 SS2005-22   105 巻 ( 129 ) 頁: 25-30   2005年6月

     詳細を見る

    記述言語:日本語  

  211. ナローイング計算の停止性証明のための依存グラフ法

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

    信学技報 SS2005-23   105 巻 ( 129 ) 頁: 31-36   2005年6月

     詳細を見る

    記述言語:日本語  

  212. 強計算性に基づいた単純型項書換え系の停止性証明法

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

    信学技報 SS2005-21   105 巻 ( 129 ) 頁: 19-24   2005年6月

     詳細を見る

    記述言語:日本語  

  213. Partial Inversion of Constructor Term Rewriting Systems 査読有り

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 16th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science   3467 巻   頁: 264-278   2005年4月

     詳細を見る

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

  214. 配列を扱う非線形先頭再帰プログラムからの再帰除去

    高須洋平, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2004年度冬のLAシンポジウム)   1426 巻   頁: 39-44   2005年4月

     詳細を見る

    記述言語:日本語  

  215. 到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係

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

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2004年度冬のLAシンポジウム)   1426 巻   頁: 106-112   2005年4月

     詳細を見る

    記述言語:日本語  

  216. 変換と部分評価に基づく非左辺正規なメタ項の停止性証明

    蛸島洋明, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2004年度冬のLAシンポジウム)   1426 巻   頁: 113-118   2005年4月

     詳細を見る

    記述言語:日本語  

  217. 弱最内戦略を完全にする項書換え系の等価変換

    岡本晃治, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2004年度冬のLAシンポジウム)   1426 巻   頁: 119-125   2005年4月

     詳細を見る

    記述言語:日本語  

  218. 融合変換を模倣するプログラム生成変換の戦略

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

    信学技報 SS2004-33   104 巻 ( 466 ) 頁: 43-48   2004年11月

     詳細を見る

    記述言語:日本語  

  219. On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report SS 2004-18   104 巻 ( 243 ) 頁: 25-30   2004年8月

     詳細を見る

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

  220. On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    LA Symposium 2004 Summer   ( 7 ) 頁: 1-6   2004年7月

     詳細を見る

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

  221. 右辺のみに現れる変数を持つ線形構成子項書換え系の計算の効率化 査読有り

    西田直樹, 酒井正彦, 坂部俊樹

    コンピュータソフトウェア   21 巻 ( 3 ) 頁: 40-47   2004年5月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  222. Narrowing-Based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof 査読有り

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Electronic Notes in Theoretical Computer Science   86 巻 ( 3 ) 頁: 1-18   2003年11月

     詳細を見る

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

  223. 右辺のみに現れる変数を持つ項書換え系の計算モデル 査読有り

    西田直樹, 酒井正彦, 坂部俊樹

    コンピュータソフトウェア   20 巻 ( 5 ) 頁: 85-89   2003年9月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  224. 右辺のみに現れる変数を持つ右線形構成子項書換え系の計算の効率化

    西田直樹, 酒井正彦, 坂部俊樹

    日本ソフトウェア科学会第20回記念大会講演論文集   ( 5B-3 ) 頁: 1-5   2003年9月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  225. 右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算

    西田直樹, 酒井正彦, 坂部俊樹

    2003年度夏のLAシンポジウム   ( 24 ) 頁: 1-6   2003年7月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  226. Narrowing-Based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof 査読有り

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming (WFLP'03)     頁: 198-211   2003年6月

     詳細を見る

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

  227. 右辺のみに現れる変数を持つ項書換え系のナローイングに基づく実効的書換えとその停止性

    西田直樹, 酒井正彦, 坂部俊樹

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2002年度冬のLAシンポジウム)   1325 巻   頁: 238-243   2003年5月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  228. 右辺のみに現れる変数を持つ項書換え系のナローイングに基づく実効的書換えとその停止性

    西田直樹, 酒井正彦, 坂部俊樹

    信学技報 COMP2003-68   102 巻 ( 593 ) 頁: 45-52   2003年1月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  229. 右辺のみに現れる変数を持つ項書換え系のナローイングに基づく書換え

    西田直樹, 酒井正彦, 坂部俊樹

    平成14年度電気関係学会東海支部連合大会論文集     頁: 292   2002年9月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  230. 右辺のみに現れる変数を持つ項書換え系の計算モデル

    西田直樹, 酒井正彦, 坂部俊樹

    日本ソフトウェア科学会第19回大会講演論文集   ( 6F-3 ) 頁: 1-5   2002年9月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  231. PT関数の逆関数を定義するTRSの生成 査読有り

    西田直樹, 酒井正彦, 坂部俊樹

    コンピュータソフトウェア   19 巻 ( 1 ) 頁: 29-33   2002年1月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語   掲載種別:研究論文(学術雑誌)  

  232. 指定した引数を固定した逆関数を定義するTRSの生成

    西田直樹, 酒井正彦, 坂部俊樹

    信学技報 COMP2001-67   101 巻 ( 488 ) 頁: 33-40   2001年12月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  233. Generation of Inverse Term Rewriting Systems for Pure Treeless Functions 査読有り

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the International Workshop on Rewriting in Proof and Computation (RPC'01)     頁: 188-198   2001年10月

     詳細を見る

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

  234. PT関数の逆関数を定義するTRSの生成

    西田直樹, 酒井正彦, 坂部俊樹

    日本ソフトウェア科学会第18回大会講演論文集   ( 6C-3 ) 頁: 1-5   2001年9月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  235. PT関数の逆関数を定義する条件付きTRSの生成

    西田直樹, 酒井正彦, 坂部俊樹

    信学技報 COMP2001-14   101 巻 ( 133 ) 頁: 9-16   2001年6月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

  236. ユーザにごみ集めを意識させないCライブラリの設計法

    西田直樹, 酒井正彦, 坂部俊樹

    信学技報 SS2000-9   100 巻 ( 64 ) 頁: 25-32   2000年5月

     詳細を見る

    担当区分:筆頭著者   記述言語:日本語  

▼全件表示

講演・口頭発表等 47

  1. A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-Path Reachability Problems with Constant Destinations

    Misaki Kojima and Naoki Nishida

    th 146th Workshop on IPSJ Special Interest Group on Programming  2023年10月31日  IPSJ Special Interest Group on Programming

     詳細を見る

    開催年月日: 2023年10月 - 2023年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Tokyo   国名:日本国  

  2. On Constrained Narrowing of Logically Constrained Term Rewrite Systems

    Naoki Nishida

    the 59th TRS Meeting  2023年9月28日 

     詳細を見る

    開催年月日: 2023年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:New Welcity Izumo   国名:日本国  

  3. Unravelings and Narrowing Trees Towards Confluence of Deterministic CTRSs 招待有り 国際会議

    Naoki Nishida

    12th International Workshop on Confluence  2023年8月23日  Cyrille Chenavier and Sarah Winkler

     詳細を見る

    開催年月日: 2023年8月

    記述言語:英語   会議種別:口頭発表(招待・特別)  

    開催地:Obergurgl, Austria   国名:オーストリア共和国  

  4. On Transforming Imperative Programs into LCTRSs via Injective Functions from Configurations to Terms

    Naoki Nishida

    the 57th TRS Meeting  2022年9月28日 

     詳細を見る

    開催年月日: 2022年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:hybrid (Eiheiji / onlien)   国名:日本国  

  5. Inversion and Determinization in Term Rewriting 招待有り 国際会議

    Naoki Nishida

    the meeting of IFIP Working Group 1.6: Rewriting  2022年7月31日  IFIP Working Group 1.6: Rewriting

     詳細を見る

    開催年月日: 2022年7月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Haifa, Israel   国名:イスラエル国  

    As a transformational approach, inversion is formulated in several settings, and the basic ideas are naive and similar. To generate a better form, e.g., non-overlapping systems if possible, determinization is used as a post-process of inversion for injective functions, and is the most challenging part in developing an inversion framework. In this talk, I introduce a framework of inversion and determinization in term rewriting. First, I explain a direct inversion of deterministic CTRSs, and a direct MSV-based determinization. Next, I explain the framework proposed by Gluck and Kawabe, which uses context-free grammars as intermediate representations of CTRSs. Finally, I explain a framework based on context-free expressions.

  6. On Semantically Equivalent Operations for Inversion of DCTRSs

    Naoki Nishida

    the 56th TRS Meeting  2022年2月24日 

     詳細を見る

    開催年月日: 2022年2月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:hybrid (Nagoya University / onlien)   国名:日本国  

  7. On Improving Confluence and Infeasibility Proofs in CO3

    Naoki Nishida

    the 55th TRS Meeting  2021年9月29日 

     詳細を見る

    開催年月日: 2021年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:online   国名:日本国  

  8. Transformation of Concurrent Programs with Semaphores into LCTRSs

    Naoki Nishida

    the 54th TRS Meeting  2021年3月16日 

     詳細を見る

    開催年月日: 2021年3月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:online   国名:日本国  

  9. Proving Infeasibility by Basic Narrowing

    Naoki Nishida

    the 50th TRS Meeting 

     詳細を見る

    開催年月日: 2019年2月 - 2019年3月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Ikaho, Gunma   国名:日本国  

  10. Proving Infeasibility by Narrowing Trees

    Naoki Nishida

    the 49th TRS Meeting 

     詳細を見る

    開催年月日: 2018年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Ikaho, Gunma   国名:日本国  

  11. 組合せ最適化問題を記述するための関係代数の集合上への拡張

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

    第20回プログラミングおよびプログラミング言語ワークショップ 

     詳細を見る

    開催年月日: 2018年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:皆生グランドホテル天水   国名:日本国  

    組合せ最適化問題は様々な分野に応用できるが,効率良く解くためには専門知識を必要とするという問題がある.本研究では,組合せ最適化問題を簡潔に記述できなおかつ効率的に解くことができるシステムの構築を目指して,理論的な枠組として関係の集合上に拡張した関係代数を提案し,それに基づく拡張SQL構文とその汎用ソルバによる解法を議論する.

  12. 配列を含むC言語サブセットから難解言語Malbolgeへのコンパイラ

    岩金カナン,坂梨元軌,酒井正彦,西田直樹,橋本健二

    第20回プログラミングおよびプログラミング言語ワークショップ 

     詳細を見る

    開催年月日: 2018年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:皆生グランドホテル天水   国名:日本国  

    難解プログラミング言語とは意図的に読解が困難になるように設計された言語であり、中でも難解な言語としてMalbolgeがある。現在では低級アセンブリ言語と制御付き疑似命令列を経てC言語に制限を設けた高級言語からのコンパイラが実現されている。しかしこの高級言語では配列を扱うことができず、複雑なプログラムが書けなかった。本研究では配列を含む高級言語を処理してMalbolgeへ変換する手法を実装した。この変換にはメモリの空き領域をスタックとして用いることで実現した。

  13. From Dependency Chains to Bounded Monotone Sequences of Integers

    Naoki Nishida

    the 47th TRS Meeting 

     詳細を見る

    開催年月日: 2017年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Matsue, Shimane   国名:日本国  

  14. On Proving Infeasibility of Conditional Critical Pairs via Narrowing Trees

    Naoki Nishida

    the 46th TRS Meeting 

     詳細を見る

    開催年月日: 2017年2月 - 2017年3月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Shinojima, Aichi   国名:日本国  

  15. Heuristics for Proving Termination of Constrained Rewriting Systems via Rule Duplication 国際会議

    Naoki Nishida

    4th Austria - Japan Summer Workshop on Term Rewriting 

     詳細を見る

    開催年月日: 2016年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:オーストリア共和国  

  16. On Uninterpreted Functions in Proving Termination of Constrained Rewriting

    Naoki Nishida

    the 41st TRS Meeting 

     詳細を見る

    開催年月日: 2014年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Jozankei, Sapporo   国名:日本国  

  17. On Soundness for Reduction of TRSs Obtained by Condition Elimination for Normal CTRSs

    Naoki Nishida

    the 40th TRS Meeting 

     詳細を見る

    開催年月日: 2014年3月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  18. A Finite Representation of the Narrowing Space and its Application 国際会議

    Naoki Nishida

    COMPUTER SCIENCE COLLOQUIUM, IMADA, University of Southern Denmark 

     詳細を見る

    開催年月日: 2014年3月

    記述言語:英語  

    国名:デンマーク王国  

  19. Automated Verification of C Programs via Rewriting Induction of Constrained TRSs 国際会議

    Naoki Nishida

    Seminar at Research Group "Verification meets Algorithm Engineering", the Institute for Theoretical Computer Science, Karlsruhe Institute of Technology 

     詳細を見る

    開催年月日: 2013年7月

    記述言語:英語   会議種別:口頭発表(招待・特別)  

    国名:ドイツ連邦共和国  

    In this talk, we introduce an automated theorem proving method based on rewriting induction of constrained TRSs, and show how to apply it to the verification of C programs over integers. Especially, we show a technique to automatically generate (a candidate of) lamma equations that are necessary for the proof.

  20. Computing More Specific Versions of Conditional Rewriting Systems

    Naoki Nishida

    the 37th TRS Meeting 

     詳細を見る

    開催年月日: 2012年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  21. Program Inversion and MSV Transformation in Term Rewriting 国際会議

    Naoki Nishida

    Master Seminar 1, Institute of Computer Science, University of Innsbruck 

     詳細を見る

    開催年月日: 2012年10月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:オーストリア共和国  

    In this talk, I present two principles of program inversion
    in term rewriting setting, a classical one and another one for tail
    recursion. Rewrite rules generated by inversion methods based on the
    principles are often non-deterministic w.r.t. application of rules to
    redexes even if given functions are injective. For this reason,
    determinization of inverted programs is one of the most challenging
    topics in program inversion of injective functions. To make inverted
    programs deterministic, I present an MSV transformation of term
    rewriting systems, which converts a rewrite system to a more specific
    version. The notion of MSV originated from the context of logic
    programs.

  22. Program Inversion for Tail Recursive Functions 国際会議

    Naoki Nishida

    Seminar at DSIC, Technical University of Valencia 

     詳細を見る

    開催年月日: 2011年12月

    記述言語:英語   会議種別:口頭発表(招待・特別)  

    国名:スペイン  

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

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

    日本ソフトウェア科学会第28回大会 

     詳細を見る

    開催年月日: 2011年9月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:沖縄産業支援センター   国名:日本国  

  24. On Soundness of CTRS Transformations

    Naoki Nishida

    the 35th TRS Meeting 

     詳細を見る

    開催年月日: 2011年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  25. On Verifying Equivalence between Functions in Constrained TRSs via Tree Homomorphisms

    Naoki Nishida

    the 35th TRS Meeting 

     詳細を見る

    開催年月日: 2011年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  26. 難解言語Malbolgeにおける高級アセンブリ言語への加算命令の追加

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

    第13回プログラミングおよびプログラミング言語ワークショップ 

     詳細を見る

    開催年月日: 2011年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:定山渓ビューホテル   国名:日本国  

  27. 難解言語Malbolgeにおけるプログラミング環境の構築と改良

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

    第13回プログラミングおよびプログラミング言語ワークショップ 

     詳細を見る

    開催年月日: 2011年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:定山渓ビューホテル   国名:日本国  

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

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

    第13回プログラミングおよびプログラミング言語ワークショップ 

     詳細を見る

    開催年月日: 2011年3月

    記述言語:日本語   会議種別:ポスター発表  

    開催地:定山渓ビューホテル   国名:日本国  

  29. On Inverting Tail Recursive Functions

    Naoki Nishida

    the 34th TRS Meeting 

     詳細を見る

    開催年月日: 2011年2月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  30. 例外処理を持つ関数型プログラムの停止性証明法

    馬場正貴, 酒井正彦, 濱口毅, 西田直樹, 坂部俊樹, 草刈圭一朗

    第12回プログラミングおよびプログラミング言語ワークショップ 

     詳細を見る

    開催年月日: 2010年3月

    記述言語:日本語   会議種別:ポスター発表  

    国名:日本国  

  31. SATソルバを利用したお絵かきロジックの問題作成支援ツール

    長坂哲, 伊藤寛之, 酒井正彦, 草刈圭一朗, 西田直樹, 坂部俊樹

    組合せゲーム・パズル ミニプロジェクト 第5回ミニ研究集会 

     詳細を見る

    開催年月日: 2010年3月

    記述言語:日本語   会議種別:口頭発表(一般)  

    国名:日本国  

  32. On Improving Lemma Generation Framework for Constrained Term Rewriting Systems

    the 33rd TRS Meeting 

     詳細を見る

    開催年月日: 2010年2月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  33. On Automating Theorem Proving for Constrained Equations

    the 32nd TRS Meeting 

     詳細を見る

    開催年月日: 2009年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  34. 制約付き等式の定理自動証明器の試作

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

    日本ソフトウェア科学会第26回大会 

     詳細を見る

    開催年月日: 2009年9月

    記述言語:日本語   会議種別:ポスター発表  

    国名:日本国  

  35. 潜在帰納法を利用した手続き型プログラム検証の試み

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

    第68回情報処理学会・プログラミング研究会 

     詳細を見る

    開催年月日: 2008年3月

    記述言語:日本語  

    国名:日本国  

  36. Comparison of Unraveling Techniques for Deterministic Conditional Term Rewriting Systems 国際会議

    2nd Austria - Japan Summer Workshop on Term Rewriting 

     詳細を見る

    開催年月日: 2007年8月

    記述言語:英語   会議種別:口頭発表(一般)  

  37. Convergent Term Rewriting Systems for Computing Inverses of Injective Functions

    the 28th TRS Meeting 

     詳細を見る

    開催年月日: 2007年2月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  38. On Reachability of Oriented Conditional Term Rewriting Systems

    the 27th TRS Meeting 

     詳細を見る

    開催年月日: 2006年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  39. Improving Unraveling for Deterministic Conditional Term Rewriting Systems

    the 26th TRS Meeting 

     詳細を見る

    開催年月日: 2006年2月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  40. Dependency Graph Method for Proving Termination of Narrowing 国際会議

    Austria - Japan Summer Workshop on Term Rewriting 

     詳細を見る

    開催年月日: 2005年8月

    記述言語:英語   会議種別:口頭発表(一般)  

  41. Partial Inversion of Constructor Term Rewriting Systems

    the 25th TRS Meeting 

     詳細を見る

    開催年月日: 2004年11月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  42. Transformational Approach to Inverse Computation in Term Rewriting

    the 18th Tokyo Programming Seminar (ToPS) 

     詳細を見る

    開催年月日: 2004年10月

    記述言語:英語   会議種別:口頭発表(招待・特別)  

    国名:日本国  

  43. Completeness of Unraveling Transformation for Left-Linear Conditional Term Rewriting Systems

    the 24th TRS Meeting 

     詳細を見る

    開催年月日: 2004年4月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  44. Basic Narrowing Improves Efficiency of Computation of Right-Linear Term Rewriting Systems with Extra Variables

    the 23rd TRS Meeting 

     詳細を見る

    開催年月日: 2003年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  45. Condition for Generation of Terminating Inverse TRSs from Constructor TRSs

    the 22nd TRS Meeting 

     詳細を見る

    開催年月日: 2003年3月

    記述言語:英語   会議種別:口頭発表(一般)  

    国名:日本国  

  46. Narrowing-Based Reduction of Term Rewriting Systems with Extra Variables

    the 21st TRS Meeting 

     詳細を見る

    開催年月日: 2002年10月

    記述言語:英語   会議種別:口頭発表(一般)  

  47. On Generating Inverse Systems of Constructor TRSs

    the 20th TRS Meeting 

     詳細を見る

    開催年月日: 2002年3月

    記述言語:英語   会議種別:口頭発表(一般)  

▼全件表示

共同研究・競争的資金等の研究課題 5

  1. 組込み制御システムの検証手法に関する研究

    2019年4月 - 2020年3月

    学内共同研究 

  2. 組込み制御システムの検証手法に関する研究

    2017年9月 - 2019年3月

    学内共同研究 

  3. 組込み制御システムの検証手法に関する研究

    2016年9月 - 2017年8月

    学内共同研究 

  4. 左線形構成子項書換え系におけるナローイング計算の停止性証明の手法に関する研究

    2009年9月

    研究等助成(海外渡航援助) 

      詳細を見る

    資金種別:競争的資金

  5. 条件付き項書換え系から等価な条件無し項書換え系への変換とその応用に関する研究

    2007年4月 - 2009年3月

    栢森情報科学振興財団研究助成金 

      詳細を見る

    資金種別:競争的資金

科研費 7

  1. 書換え帰納法を利用したプログラム等価性検証技術の開発

    2018年4月 - 2023年3月

    科学研究費補助金  基盤研究(C)

    西田直樹

      詳細を見る

    担当区分:研究代表者 

    本研究では制約付き項書換えシステムに対する書換え帰納法に基づく定理自動証明ツールを開発し,命令型プログラミング言語のプログラム等価性検証の新たな手法の確立をめざす.具体的には,関数型プログラミング言語だけでなく命令型プログラミング言語の計算モデルとしての利用を期待できる制約付き項書換えシステムに対する書換え帰納法に基づく帰納的定理証明法を命令型プログラミング言語から得られた書換えシステム向けに自動化することで,命令型プログラム向けの定理自動証明ツールを開発する.特に,関数の等価性など等式で表現できる性質の検証への応用をめざす.命令型プログラム向けの自動化を実現するために,書換え帰納法の推論規則の適用戦略の改良,補題等式の生成法の開発に取り組む.また,不等式も同時に扱う,等式付き書換えに対応するなど理論の拡張にも取り組む.

  2. 実時間性を持つ並行プログラムに対するデバッグのための逆方向計算モデル

    2017年4月 - 2021年3月

    科学研究費補助金  基盤研究(B)

    結縁 祥治

      詳細を見る

    担当区分:研究分担者 

  3. 単射性を持つ関数型プログラムの逆計算プログラム生成に関する研究

    2009年4月 - 2013年3月

    科学研究費補助金  若手研究(B)

    西田直樹

      詳細を見る

    担当区分:研究代表者 

  4. 高階関数プログラムの停止性判定に関する研究

    2008年4月 - 2012年3月

    科学研究費補助金  基盤研究(C)

    草刈圭一朗

      詳細を見る

    担当区分:研究分担者 

  5. 関数型プログラムの逆計算プログラム生成に関する研究

    2005年4月 - 2008年3月

    科学研究費補助金  若手研究(B)

    西田 直樹

      詳細を見る

    担当区分:研究代表者 

  6. 書換えに基づく例外型を持つオブジェクト指向プログラムの型推論

    2004年4月 - 2008年3月

    科学研究費補助金  基盤研究(B)

    坂部俊樹

      詳細を見る

    担当区分:研究分担者 

  7. 関数型言語の解析・検証・効率的実行のための書換え理論の研究

    2003年4月 - 2010年3月

    科学研究費補助金  基盤研究(C)

    酒井正彦

      詳細を見る

    担当区分:研究分担者 

▼全件表示

 

担当経験のある科目 (本学) 38

  1. 計算論基礎特論A

    2022

  2. アルゴリズム2

    2022

  3. アルゴリズム1

    2022

  4. 基礎セミナーB

    2020

  5. アルゴリズム2

    2020

  6. アルゴリズム1

    2020

  7. 計算論基礎特論A

    2020

  8. 基礎セミナー

    2019

  9. 計算モデル特論

    2019

  10. アルゴリズム2

    2019

  11. アルゴリズム1

    2019

  12. アルゴリズム及び演習

    2018

  13. アルゴリズム2

    2018

  14. アルゴリズム1

    2018

  15. 計算論基礎特論A

    2018

  16. 計算モデル特論

    2017

  17. 基礎セミナー

    2017

  18. アルゴリズム及び演習

    2017

  19. 基礎セミナー

    2016

  20. ソフトウェア基礎論特論

    2016

  21. アルゴリズム及び演習

    2016

  22. アルゴリズム及び演習

    2015

  23. ソフトウェア基礎論特論

    2015

  24. ソフトウェア基礎論特論

    2014

  25. 電気・電子・情報工学序論

    2014

  26. 計算機プログラミング基礎及び演習

    2014

  27. 基礎セミナー

    2014

  28. 電気・電子・情報工学序論

    2013

  29. 計算機プログラミング基礎及び演習

    2013

  30. 基礎セミナー

    2013

  31. コンパイラおよび演習

    2012

  32. プログラミングおよび演習

    2012

  33. 情報工学実験第2

    2012

  34. 情報工学実験第1

    2012

  35. 情報基礎論第1および演習

    2011

  36. 情報工学実験第2

    2011

  37. 情報工学実験第1

    2011

  38. プログラミングおよび演習

    2011

▼全件表示