研究者詳細 - 酒井　正彦

論文 - 酒井　正彦

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

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

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

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

Recognizability of Redexes for Higher-Order Rewrite Systems 査読有り

Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa

IPSJ Transactions of Programming 2 巻 ( 2 ) 頁： 166-175 2009年3月

Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes 査読有り

Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa

IPSJ Transactions of Programming 2 巻 ( 2 ) 頁： 144-165 2009年3月

Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques 査読有り

Keiichirou Kusakari, Masahiko Sakai

IEICE Trans. on Information and Systems E92-D 巻 ( 2 ) 頁： 235-247 2009年2月

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

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

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

*Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems 査読有り

Yoshiharu Kojima, Masahiko Sakai

Proc. of 19th Int'l Conference on Rewriting Techniqes and Applications, Hagenberg RTA2008, LNCS 5117 巻頁： 187-201 2008年7月

記述言語：英語

A reachability problem is a problem used to decide whether s is reachable to t by R or not for a given two terms s, t and a term rewriting system R. Since it is known that this problem is undecidable, effort has been devoted to finding subclasses of term rewriting systems in which the eachabilit
y is decidable. However few works on decidability exist for innermost reduction strategy or context-sensitive rewriting.

In this paper, we show that innermost reachability and
context-sensitive reachability are decidable for linear right-shallow term rewriting systems. Our approach is based on the tree automata technique that is commonly
used for analysis of reachability and its related properties.

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

Naoki Nishida, Masahiko Sakai

"Proc. of 8th International Workshop on Reduction Strategies in Rewriting and Programming, Hagenberg (WRS2008)" 頁： 61-75 2008年7月

Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems 査読有り

Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe

Electronic Notes in Theoretical Computer Science 204 巻 ( 4 ) 頁： 21-34 2008年4月

*Undecidable Properties on Length-Two String Rewriting Systems 査読有り

Masahiko Sakai and Wang Yi

Electronic Notes in Theoretical Computer Science 204 巻 ( 4 ) 頁： 53-69 2008年4月

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

Length-two string rewriting systems are length-preserving string rewriting systems that consist of length-two rules. This paper shows that confluence, termination, left-most termination and right-most termination are undecidable
properties for length-two string rewriting systems. These results mean that these properties are undecidable for
the class of linear term rewriting systems in which depth-two variables are allowed in both-hand sides of rules.

Error Detection with Soft Typing for Dynamically Typed Language

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

IEICE Technical Report 107 巻 ( 505 ) 頁： 7-12 2008年3月

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

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

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

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

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

電子情報通信学会技術研究報告 107 巻 ( 505 ) 頁： 25-30 2008年3月

Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques

"Keiichirou Kusakari, Masahiko Sakai"

IEICE Technical Report 107 巻 ( 505 ) 頁： 19-24 2008年3月

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

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

電子情報通信学会技術研究報告 107 巻 ( 392 ) 頁： 43-48 2007年12月

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

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

電子情報通信学会技術研究報告 107 巻 ( 392 ) 頁： 73-78 2007年12月

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

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

電子情報通信学会技術研究報告 107 巻 ( 275 ) 頁： 1-6 2007年10月

*Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting 査読有り

Keiichirou Kusakari, Masahiko Sakai

Applicable Algebra in Engineering, Communication and Computing 18 巻 ( 5 ) 頁： 407-431 2007年10月

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

We enhance the dependency pair method in order to prove termination using recursive structure analysis in simply-typed term rewriting systems, which is one of the computational models of functional programs. The primary advantage of our method is that one can exclude higher-order variables which are difficult to analyze theoretically, from recursive structure analysis. The key idea of our method is to analyze recursive structure from the viewpoint of strong computability. This property was introduced for proving termination in typed lambda-calculus, and is a stronger condition than the property of termination. The difficulty in incorporating this concept into recursive structure analysis is that because it is defined inductively over type structure, it is not closed under the subterm relation. This breaks the correspondence between strong computability and recursive structure. In order to guarantee the correspondence, we propose plain function-passing as a restriction, which is satisfied by
many non-artificial functional programs.

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

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

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

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

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

電子情報通信学会技術研究報告 107 巻 ( 176 ) 頁： 1-6 2007年8月

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

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

電子情報通信学会技術研究報告 107 巻 ( 176 ) 頁： 7-12 2007年8月

　前のページ - 次のページ　

<酒井 正彦>

論文 - 酒井 正彦

<酒井　正彦>

論文 - 酒井　正彦