文献

J-GLOBAL ID：201802211857775323   整理番号：18A1365213

関数プログラムにおける静的依存対法

Static Dependency Pair Method in Functional Programs

著者 (1件)： KUSAKARI Keiichirou (Informatics Course, Department of Electrical, Electronic and Computer Engineering, Faculty of Engineering, Gifu University)
資料名： IEICE Transactions on Information and Systems (Web)  (IEICE Transactions on Information and Systems (Web))
巻： E101.D  号： 6  ページ： 1491-1502(J-STAGE)  発行年： 2018年 
JST資料番号： U0469A  ISSN： 1745-1361  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 英語 (EN)

抄録/ポイント： 著者らは以前に,高階関数を扱うための項書き換えシステムの様々な拡張の静的再帰構造を解析することにより,終了を証明する静的依存性対法を紹介した。鍵は,強い計算可能性の概念に基づく再帰構造の形式化に成功することであり,タイプ化λ計算の終了にこれを導入した。著者らは,既存の汎関数プログラムに近い静的依存性対法をもたらすために,パターンによる関数抽象化が許される項書換えモデルにもこの方法を拡張した。静的依存性対法は一般的ではないので,著者らは,この方法が良く機能するクラスすなわちアクセシビリティを定式化した。静的依存性対法は非常に自然な推論であるので,著者らの拡張は以前の結果とわずかに異なるだけだった。一方,健全性の証明は甚だしく困難だった。(翻訳著者抄録)

シソーラス用語： *関数プログラミング ,  依存性 ,  *項書換え系 ,  再帰性 ,  アクセシビリティ ,  健全性 ,  計算可能性 ,  λ計算 ,  定式化 ,  汎関数 ,  停止
準シソーラス用語： *項書換えシステム

著者キーワード (5件)： 機能プログラム ,  項書き換えシステム ,  停止 ,  再帰的定義 ,  静的依存対法

分類 (2件)： その他のシステムプログラミング  (JD03070M) ,  計算理論  (JB02000A)

引用文献 (24件)：

• [1] T. Arts and J. Giesl, “Termination of Term Rewriting Using Dependency Pairs,” Theoretical Computer Science, vol.236, no.1-2, pp.133-178, 2000. 10.1016/s0304-3975(99)00207-8
• [2] K. Bimbó, Combinatory Logic: Pure, Applied and Typed, Chapman and Hall/CRC, 2011.
• [3] F. Blanqui, J.-P. Jouannaud, and M. Okada, “Inductive-Data-Type Systems,” Theoretical Computer Science, vol.272, no.1-2, pp.41-68, 2002. 10.1016/s0304-3975(00)00347-9
• [4] F. Blanqui, “Computability Closure: Ten Years Later,” In Essay in Honour of Jean-Pierre Jouannaud's 60 Birthday, LNCS 4600, pp.68-88, 2007.
• [5] F. Blanqui, J.-P. Jouannaud, and A. Rubio, “The Computability Path Ordering: The End of a Quest,” Proc. 17th EACSL Annual Conf. on Computer Science Logic, LNCS 5213 (CSL2008), pp.1-14, 2008.

タイトルに関連する用語 (2件)： 関数 ,  法