{"created":"2021-03-01T06:16:10.449451+00:00","id":9408,"links":{},"metadata":{"_buckets":{"deposit":"7e402a17-d8b0-4ad3-bcb1-3c7826a5ee9e"},"_deposit":{"id":"9408","owners":[],"pid":{"revision_id":0,"type":"depid","value":"9408"},"status":"published"},"_oai":{"id":"oai:nagoya.repo.nii.ac.jp:00009408","sets":["320:606:607"]},"author_link":["26892"],"item_12_alternative_title_19":{"attribute_name":"その他のタイトル","attribute_value_mlt":[{"subitem_alternative_title":"項書換えにおける逆計算へのプログラム変換アプローチ","subitem_alternative_title_language":"ja"}]},"item_12_biblio_info_6":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicIssueDates":{"bibliographicIssueDate":"2004-03-25","bibliographicIssueDateType":"Issued"}}]},"item_12_date_granted_64":{"attribute_name":"学位授与年月日","attribute_value_mlt":[{"subitem_dategranted":"2004-03-25"}]},"item_12_degree_grantor_62":{"attribute_name":"学位授与機関","attribute_value_mlt":[{"subitem_degreegrantor":[{"subitem_degreegrantor_language":"ja","subitem_degreegrantor_name":"名古屋大学"},{"subitem_degreegrantor_language":"en","subitem_degreegrantor_name":"Nagoya University"}],"subitem_degreegrantor_identifier":[{"subitem_degreegrantor_identifier_name":"13901","subitem_degreegrantor_identifier_scheme":"kakenhi"}]}]},"item_12_degree_name_61":{"attribute_name":"学位名","attribute_value_mlt":[{"subitem_degreename":"博士(工学)","subitem_degreename_language":"ja"}]},"item_12_description_4":{"attribute_name":"抄録","attribute_value_mlt":[{"subitem_description":"In this thesis, we approach by program transformation to inverse computation in term rewriting.Inverse computation of a given program (or function) is the calculation of the possible input of the program for a given output.  Inverse interpreters are algorithmic approaches to inverse computation, which computes the possible input from a given program and a given output.  Inverse compilers are transformational approaches, which generates from a given program a program computing the possible input of the given program for a given output. Such a generated program is called an inverse program of the given program.  Once the inverse program is generated for the given program, inverse computation can be done by the inverse program inputing a given output of the original program. In this thesis, we propose inverse compilers for term rewriting systems (TRSs, for short).  As the first step, we treat a class of TRSs, called PT-TRSs.  PT-TRSs can define pure treeless functions which are often used in program transformations and have the future that each argument of defined symbols appearing in the right-hand side is a variable.  While they can be easily treated in program transformation, their syntax is very restrictive and the class of functions defined as PT-TRSs is narrow.  Hence we extend the inverse compiler for PT-TRSs to that for constructor TRSs.  Constructor TRSs includes PT-TRSs properly, and it is known that their computation power is equivalent to that of Turing machines.Both of the inverse compilers proposed in this thesis are consisting of two parts.  The first part is an actual inverse compiler that generates from a given TRS a conditional TRS(CTRS) which computes inverse of the given TRS.  We show the correctness of our inverse compilers by proving that the generated CTRSs are inverse programs of the given TRSs.  The second part is a program transformation of the generated CTRS into a TRS with extra variables, which is considered to be equivalent to the generated CTRS.  TRSs with extra variables are called EV-TRSs, which can contain extra variables in the right-hand sides of their rewrite rules.  Extra variables are variables which appear in the conditional part or the right-hand side of a conditional rewrite rule but not in the left-hand side.  In order to show the correctness of the program transformation in the second part, we show soundness and completeness of the generated EV-TRSs with respect to the terms which are treated by the input CTRSs.We also show the general relationships between the syntactic properties of the input TRS and its inverse EV-TRS generated by our inverse compilers.  Three of such relationships are very important.  One is that the generated EV-TRSs are constructor systems.  A second is that the generated EV-TRS is a TRS if the input TRS is non-erasing.  The other is that the generated EV-TRS is right-linear (left-linear) if the input is left-linear (right-linear, respectively).EV-TRSs contain two serious problems for practical use of them.  One is that their one-step of rewrite relation by a rule which contains an extra variable is infinitely branching even if renamed terms are regarded as the same.  The other is that they are not terminating at all if extra variables are contained.  Therefore, EV-TRSs in general cannot be executed efficiently.  Unfortunately, the inverse programs generated by out inverse compilers are EV-TRSs.  Therefore a simulation method of rewrite relation of EV-TRS s is necessary.To simulate rewrite relation of EV-TRS s, we show that narrowing substituting a fresh variable for each extra variable can simulate, as a narrowing sequence starting from ground terms, a rewrite sequence of a given EV-TRS if the EV-TRS is right-linear or any redex which is reduced in the rewrite sequence is not introduced by means of extra variables.  Since narrowing is finitely branching up to renaming and those starting from ground terms are sometimes terminating, the above problems of EV-TRSs are avoided.  Since the narrowing of TRSs on ground terms is equal to the rewrite relation of them and every rewrite sequence of TRSs can be considered as a ground rewrite sequence, the computation of TRSs can be also done by the narrowing. Hence, the input and output programs of our inverse compilers can be worked on the same interpretation.　Termination is one of the important properties of computation.  Since the computation of our inverse EV-TRSs is simulated by narrowing, to guarantee the termination of the inverse computation by our approaches, we propose two termination proof methods of narrowing, especially starting from ground terms.  One is based on the notion of active chains, and another is based on the dependency pair method which is a termination proof method for rewrite relations of TRSs. Solutions of inverse computation are not always unique, and hence all solution search is necessary.  However, it is known that all solution search is expensive.  For the purpose of improving efficiency of inverse computation, we show that basic narrowing is sufficient to simulate rewrite sequences of right-linear EV-TRSs.  Since the left-linearity is often assumed in first-order functional programs and inverse EV-TRSs of linear constructor TRSs are right-linear, this result is useful for the efficience of our inverse computation.  We also show that for linear constructor EV-TRSs, all normal forms of a given terminating term can be obtained by innermost narrowing. To generate innermost-terminating inverse TRSs, we give a condition on the relationship between the depth of the both hand sides of each rewrite rules in the input non-erasing TRSs.  The condition for each rule is that the root symbol of the right-hand side is not a defined symbol,    the depth of the left-hand side is two or less if the right-hand side is a variable, or less than the number of constructors in the shortest path from the root to variables or defined symbols in the right-hand side.Since every redex is innermost in rewrite sequences representing inverse computation, innermost termination is sufficient as termination of  inverse computation. As an extension of the proposed inverse compilers, we tackle partial inverse computation.  Partial inverse computation is the calculation of some of the possible unknown input for a program, a given output and the known input.  We extend the inverse compiler for constructor TRS s into a compiler which generate a CTRS computing partial inverses of the input TRS. Finally, we give some examples as applications of the generated inverse compilers.  These shows that inverse compilers are advantageous over inverse interpreters.","subitem_description_language":"en","subitem_description_type":"Abstract"}]},"item_12_description_5":{"attribute_name":"内容記述","attribute_value_mlt":[{"subitem_description":"名古屋大学博士学位論文 学位の種類:博士(工学) (課程) 学位授与年月日:平成16年3月25日","subitem_description_language":"ja","subitem_description_type":"Other"}]},"item_12_dissertation_number_65":{"attribute_name":"学位授与番号","attribute_value_mlt":[{"subitem_dissertationnumber":"甲第6287号"}]},"item_12_identifier_60":{"attribute_name":"URI","attribute_value_mlt":[{"subitem_identifier_type":"HDL","subitem_identifier_uri":"http://hdl.handle.net/2237/11185"}]},"item_12_select_15":{"attribute_name":"著者版フラグ","attribute_value_mlt":[{"subitem_select_item":"publisher"}]},"item_12_text_14":{"attribute_name":"フォーマット","attribute_value_mlt":[{"subitem_text_value":"application/pdf"}]},"item_12_text_63":{"attribute_name":"学位授与年度","attribute_value_mlt":[{"subitem_text_value":"2003"}]},"item_access_right":{"attribute_name":"アクセス権","attribute_value_mlt":[{"subitem_access_right":"open access","subitem_access_right_uri":"http://purl.org/coar/access_right/c_abf2"}]},"item_creator":{"attribute_name":"著者","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Nishida, Naoki","creatorNameLang":"en"}],"nameIdentifiers":[{"nameIdentifier":"26892","nameIdentifierScheme":"WEKO"}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2018-02-20"}],"displaytype":"detail","filename":"ko6287.pdf","filesize":[{"value":"9.2 MB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","url":{"label":"ko6287.pdf","objectType":"fulltext","url":"https://nagoya.repo.nii.ac.jp/record/9408/files/ko6287.pdf"},"version_id":"147726cf-b80e-457b-aad1-402e64cfc957"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourcetype":"doctoral thesis","resourceuri":"http://purl.org/coar/resource_type/c_db06"}]},"item_title":"Transformational approach to inverse computation in term rewriting","item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Transformational approach to inverse computation in term rewriting","subitem_title_language":"en"}]},"item_type_id":"12","owner":"1","path":["607"],"pubdate":{"attribute_name":"PubDate","attribute_value":"2009-02-25"},"publish_date":"2009-02-25","publish_status":"0","recid":"9408","relation_version_is_last":true,"title":["Transformational approach to inverse computation in term rewriting"],"weko_creator_id":"1","weko_shared_id":-1},"updated":"2023-01-16T03:55:02.661225+00:00"}