Faculty Profiles - SAKAI, Masahiko

Papers - SAKAI, Masahiko

Division display 61 - 80 of about 218 ／ All the affair displays >>

Recognizability of Redexes for Higher-Order Rewrite Systems Reviewed

Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa

IPSJ Transactions of Programming Vol. 2 ( 2 ) page： 166-175 2009.3

Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes Reviewed

Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa

IPSJ Transactions of Programming Vol. 2 ( 2 ) page： 144-165 2009.3

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

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

情報処理学会論文誌プログラミング Vol. 2 ( 2 ) page： 80-96 2009.3

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

Keiichirou Kusakari, Masahiko Sakai

IEICE Trans. on Information and Systems Vol. E92-D ( 2 ) page： 235-247 2009.2

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

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

情報処理学会論文誌プログラミング Vol. 1 ( 2 ) page： 100-121 2008.9

*Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems Reviewed

Yoshiharu Kojima, Masahiko Sakai

Proc. of 19th Int'l Conference on Rewriting Techniqes and Applications, Hagenberg RTA2008, LNCS Vol. 5117 page： 187-201 2008.7

Language：English

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 Reviewed

Naoki Nishida, Masahiko Sakai

"Proc. of 8th International Workshop on Reduction Strategies in Rewriting and Programming, Hagenberg (WRS2008)" page： 61-75 2008.7

Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems Reviewed

Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe

Electronic Notes in Theoretical Computer Science Vol. 204 ( 4 ) page： 21-34 2008.4

*Undecidable Properties on Length-Two String Rewriting Systems Reviewed

Masahiko Sakai and Wang Yi

Electronic Notes in Theoretical Computer Science Vol. 204 ( 4 ) page： 53-69 2008.4

Authorship：Lead author Language：English Publishing type：Research paper (scientific journal)

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 Vol. 107 ( 505 ) page： 7-12 2008.3

A Type System for Analyzing Secure Information Flow in Object-Oriented Programs with Exception Handling Reviewed

IEICE Trans. on Information and Systems Vol. J91-D ( 3 ) page： 757-770 2008.3

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

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

電子情報通信学会技術研究報告 Vol. 107 ( 505 ) page： 25-30 2008.3

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

"Keiichirou Kusakari, Masahiko Sakai"

IEICE Technical Report Vol. 107 ( 505 ) page： 19-24 2008.3

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

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

電子情報通信学会技術研究報告 Vol. 107 ( 392 ) page： 43-48 2007.12

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

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

電子情報通信学会技術研究報告 Vol. 107 ( 392 ) page： 73-78 2007.12

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

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

電子情報通信学会技術研究報告 Vol. 107 ( 275 ) page： 1-6 2007.10

*Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting Reviewed

Keiichirou Kusakari, Masahiko Sakai

Applicable Algebra in Engineering, Communication and Computing Vol. 18 ( 5 ) page： 407-431 2007.10

Language：English Publishing type：Research paper (scientific journal)

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年度電気関係学会東海支部連合大会講演論文集 page： O-012 2007.9

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

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

電子情報通信学会技術研究報告 Vol. 107 ( 176 ) page： 1-6 2007.8

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

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

電子情報通信学会技術研究報告 Vol. 107 ( 176 ) page： 7-12 2007.8

　 PREV - NEXT 　

<SAKAI, Masahiko>

Papers - SAKAI, Masahiko