研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 254 件中 161 - 180 件目／全件表示 >>

Program Inversion for Tail Recursive Functions 査読有り Open Access

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

Open Access

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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月

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月

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月

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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.

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

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

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

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

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

Open Access

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹