التفاصيل البيبلوغرافية
| العنوان: |
Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting |
| المؤلفون: |
草刈, 圭一朗, 26678, Kusakari, Keiichirou, 26679, 酒井, 正彦, 26680, Sakai, Masahiko, 26681 |
| بيانات النشر: |
Springer-International |
| سنة النشر: |
2007 |
| المجموعة: |
Nagoya University: NAGOYA Repository / 名古屋大学学術機関リポジトリ |
| مصطلحات موضوعية: |
Termination, Simply-Typed Term Rewriting System, Plain Function-Passing, Dependency Pair, Strong Computability |
| الوصف: |
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 λ-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. ; journal article |
| نوع الوثيقة: |
other/unknown material |
| وصف الملف: |
application/pdf |
| اللغة: |
English |
| تدمد: |
09381279 |
| Relation: |
Applicable Algebra in Engineering, Communication and Computing; 18; 407; 431; http://hdl.handle.net/2237/11112; https://nagoya.repo.nii.ac.jp/record/9338/files/aaecc07.pdf |
| الاتاحة: |
http://hdl.handle.net/2237/11112
https://nagoya.repo.nii.ac.jp/record/9338/files/aaecc07.pdf |
| رقم الانضمام: |
edsbas.CAAAC365 |
| قاعدة البيانات: |
BASE |