2022-01-25T23:58:43Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001422942020-10-27T05:02:43Z00934:00935:08226:08227
A Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold ProblemA Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold Problemeng[発表概要]http://id.nii.ac.jp/1001/00142230/Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=142294&item_no=1&attribute_id=1&file_no=1Copyright (c) 2015 by the Information Processing Society of JapanGraduate School of Information Science, Nagoya UniversityGraduate School of Information Science, Nagoya UniversityGraduate School of Information Science, Nagoya UniversityGraduate School of Information Science, Nagoya UniversityMasanori, NagashimaTomofumi, KatoMasahiko, SakaiNaoki, NishidaUnfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. Unfolding expands a sub-expression of a program using its own definitions. Folding does the opposite, but restoring a one-step unfolding by folding is not easy as we expect because some rules used by unfolding may be lost. In our previous work, we proposed a heuristic procedure that solves the inverse problem of unfolding for conditional term rewriting systems, call pure-constructor systems. This paper reformulates it on term rewriting systems, and shows a simple sufficient condition for the completeness in the sense that the procedure always find a solution if it exists.Unfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. Unfolding expands a sub-expression of a program using its own definitions. Folding does the opposite, but restoring a one-step unfolding by folding is not easy as we expect because some rules used by unfolding may be lost. In our previous work, we proposed a heuristic procedure that solves the inverse problem of unfolding for conditional term rewriting systems, call pure-constructor systems. This paper reformulates it on term rewriting systems, and shows a simple sufficient condition for the completeness in the sense that the procedure always find a solution if it exists.AA11464814情報処理学会論文誌プログラミング（PRO）8117172015-06-021882-78022015-05-27