caa a22 4500 463203240 CHVBK 20180405153118.0 cr unu---uuuuu 170326e20071001xx s 000 0 eng 10.1007/s00200-007-0046-9 doi (NATIONALLICENCE)springer-10.1007/s00200-007-0046-9 Enhancing dependency pair method using strong computability in simply-typed term rewriting [Elektronische Daten] [Keiichirou Kusakari, Masahiko Sakai] 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. Springer-Verlag, 2007 Termination nationallicence Simply-typed term rewriting system nationallicence Plain function- passing nationallicence Dependency pair nationallicence Strong computability nationallicence Kusakari Keiichirou Graduate School of Information Science, Nagoya University, Nagoya-shi, Japan aut Sakai Masahiko Graduate School of Information Science, Nagoya University, Nagoya-shi, Japan aut Applicable Algebra in Engineering, Communication and Computing Springer-Verlag 18/5(2007-10-01), 407-431 0938-1279 18:5<407 2007 18 200 https://doi.org/10.1007/s00200-007-0046-9 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s00200-007-0046-9 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Kusakari Keiichirou Graduate School of Information Science, Nagoya University, Nagoya-shi, Japan aut NATIONALLICENCE 700 1- Sakai Masahiko Graduate School of Information Science, Nagoya University, Nagoya-shi, Japan aut NATIONALLICENCE 773 0- Applicable Algebra in Engineering, Communication and Computing Springer-Verlag 18/5(2007-10-01), 407-431 0938-1279 18:5<407 2007 18 200 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer