講演抄録/キーワード |
講演名 |
2005-12-20 10:15
Enhancing Dependency Pair Method by Strong Computability in Simply-Typed Term Rewriting Systems ○Keiichirou Kusakari・Masahiko Sakai(Nagoya Univ.) |
抄録 |
(和) |
依存対法と呼ばれる再帰構造解析による停止性証明法を,型付き$\lambda$計算の停止性証明で導入された強計算性の概念を用いることにより改良する.取り扱いの困難な高階変数の解析を排除でき,強力でかつ効率的な手法を得る.強計算性は型の上で帰納的に定義され依存対は項の構造に従って定義されているので,型と項の構造の整合を保つために我々の手法は適切な制限を必要とする.このような制限として直接関数渡しの概念を提案する.ほとんどの人工的でない関数プログラムは直接関数渡しであるので我々の手法の汎用性は失われない. |
(英) |
We enhance the dependency pair method to prove termination by recursive structure analysis in the simply-typed term rewriting system, which is one of the computational models of functional programs. The primary advantage of our method is that one can avoid analyzing higher-order variables, which are difficult to analyze theoretically. The key idea of our method is to show its strong computability, which was introduced for proving termination of typed $\lambda$-calculus, and is a stronger property than the termination. This strong computability is not closed under the subterm relation, because it is inductively defined on type structure. This breaks a correspondence between the strong computability and the recursive structure of programs. As a restriction to guarantee the correspondence,
we provide the notion of plain function-passing, in which most non-artificial functional programs can still be represented. |
キーワード |
(和) |
停止性 / 単純型項書換え系 / 直接関数渡し / 依存対 / 強計算性 / / / |
(英) |
Termination / Simply-Typed Term Rewriting System / Plain Function-Passing / Dependency Pair / Strong Computability / / / |
文献情報 |
信学技報, vol. 105, no. 491, SS2005-65, pp. 13-18, 2005年12月. |
資料番号 |
SS2005-65 |
発行日 |
2005-12-13 (SS) |
ISSN |
Print edition: ISSN 0913-5685 |
PDFダウンロード |
|