WEKO3
AND
アイテム
{"_buckets": {"deposit": "7e402a17d8b04ad3bcb13c7826a5ee9e"}, "_deposit": {"id": "9408", "owners": [], "pid": {"revision_id": 0, "type": "depid", "value": "9408"}, "status": "published"}, "_oai": {"id": "oai:nagoya.repo.nii.ac.jp:00009408"}, "item_12_alternative_title_19": {"attribute_name": "\u305d\u306e\u4ed6\u306e\u8a00\u8a9e\u306e\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_alternative_title": "\u9805\u66f8\u63db\u3048\u306b\u304a\u3051\u308b\u9006\u8a08\u7b97\u3078\u306e\u30d7\u30ed\u30b0\u30e9\u30e0\u5909\u63db\u30a2\u30d7\u30ed\u30fc\u30c1"}]}, "item_12_biblio_info_6": {"attribute_name": "\u66f8\u8a8c\u60c5\u5831", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "20040325", "bibliographicIssueDateType": "Issued"}, "bibliographic_titles": [{}]}]}, "item_12_date_granted_64": {"attribute_name": "\u5b66\u4f4d\u6388\u4e0e\u5e74\u6708\u65e5", "attribute_value_mlt": [{"subitem_dategranted": "20040325"}]}, "item_12_description_4": {"attribute_name": "\u6284\u9332", "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 PTTRSs. PTTRSs 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 righthand 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 PTTRSs is narrow. Hence we extend the inverse compiler for PTTRSs to that for constructor TRSs. Constructor TRSs includes PTTRSs 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 EVTRSs, which can contain extra variables in the righthand sides of their rewrite rules. Extra variables are variables which appear in the conditional part or the righthand side of a conditional rewrite rule but not in the lefthand side. In order to show the correctness of the program transformation in the second part, we show soundness and completeness of the generated EVTRSs 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 EVTRS generated by our inverse compilers. Three of such relationships are very important. One is that the generated EVTRSs are constructor systems. A second is that the generated EVTRS is a TRS if the input TRS is nonerasing. The other is that the generated EVTRS is rightlinear (leftlinear) if the input is leftlinear (rightlinear, respectively).EVTRSs contain two serious problems for practical use of them. One is that their onestep 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, EVTRSs in general cannot be executed efficiently. Unfortunately, the inverse programs generated by out inverse compilers are EVTRSs. Therefore a simulation method of rewrite relation of EVTRS s is necessary.To simulate rewrite relation of EVTRS 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 EVTRS if the EVTRS is rightlinear 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 EVTRSs 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.\u3000Termination is one of the important properties of computation. Since the computation of our inverse EVTRSs 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 rightlinear EVTRSs. Since the leftlinearity is often assumed in firstorder functional programs and inverse EVTRSs of linear constructor TRSs are rightlinear, this result is useful for the efficience of our inverse computation. We also show that for linear constructor EVTRSs, all normal forms of a given terminating term can be obtained by innermost narrowing. To generate innermostterminating inverse TRSs, we give a condition on the relationship between the depth of the both hand sides of each rewrite rules in the input nonerasing TRSs. The condition for each rule is that the root symbol of the righthand side is not a defined symbol, the depth of the lefthand side is two or less if the righthand 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 righthand 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_type": "Abstract"}]}, "item_12_description_5": {"attribute_name": "\u5185\u5bb9\u8a18\u8ff0", "attribute_value_mlt": [{"subitem_description": "\u540d\u53e4\u5c4b\u5927\u5b66\u535a\u58eb\u5b66\u4f4d\u8ad6\u6587 \u5b66\u4f4d\u306e\u7a2e\u985e:\u535a\u58eb(\u5de5\u5b66) (\u8ab2\u7a0b) \u5b66\u4f4d\u6388\u4e0e\u5e74\u6708\u65e5:\u5e73\u621016\u5e743\u670825\u65e5", "subitem_description_type": "Other"}]}, "item_12_dissertation_number_65": {"attribute_name": "\u5b66\u4f4d\u6388\u4e0e\u756a\u53f7", "attribute_value_mlt": [{"subitem_dissertationnumber": "13901\u7532\u7b2c6287\u53f7"}]}, "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": "\u8457\u8005\u7248\u30d5\u30e9\u30b0", "attribute_value_mlt": [{"subitem_select_item": "publisher"}]}, "item_12_text_14": {"attribute_name": "\u30d5\u30a9\u30fc\u30de\u30c3\u30c8", "attribute_value_mlt": [{"subitem_text_value": "application/pdf"}]}, "item_12_text_63": {"attribute_name": "\u5b66\u4f4d\u6388\u4e0e\u5e74\u5ea6", "attribute_value_mlt": [{"subitem_text_value": "2003"}]}, "item_creator": {"attribute_name": "\u8457\u8005", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Nishida, Naoki"}], "nameIdentifiers": [{"nameIdentifier": "26892", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "\u30d5\u30a1\u30a4\u30eb\u60c5\u5831", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "20180220"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "ko6287.pdf", "filesize": [{"value": "9.2 MB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 9200000.0, "url": {"label": "ko6287.pdf", "url": "https://nagoya.repo.nii.ac.jp/record/9408/files/ko6287.pdf"}, "version_id": "147726cfb80e457baad1402e64cfc957"}]}, "item_language": {"attribute_name": "\u8a00\u8a9e", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "item_resource_type": {"attribute_name": "\u8cc7\u6e90\u30bf\u30a4\u30d7", "attribute_value_mlt": [{"resourcetype": "thesis", "resourceuri": "http://purl.org/coar/resource_type/c_46ec"}]}, "item_title": "Transformational approach to inverse computation in term rewriting", "item_titles": {"attribute_name": "\u30bf\u30a4\u30c8\u30eb", "attribute_value_mlt": [{"subitem_title": "Transformational approach to inverse computation in term rewriting"}]}, "item_type_id": "12", "owner": "1", "path": ["320/606/607"], "permalink_uri": "http://hdl.handle.net/2237/11185", "pubdate": {"attribute_name": "\u516c\u958b\u65e5", "attribute_value": "20090225"}, "publish_date": "20090225", "publish_status": "0", "recid": "9408", "relation": {}, "relation_version_is_last": true, "title": ["Transformational approach to inverse computation in term rewriting"], "weko_shared_id": 3}
Transformational approach to inverse computation in term rewriting
http://hdl.handle.net/2237/11185
97500376b5ff49beb5e5a82c9f07dda3
名前 / ファイル  ライセンス  アクション  

ko6287.pdf (9.2 MB)


Item type  学位論文 / Thesis or Dissertation(1)  

公開日  20090225  
タイトル  
タイトル  Transformational approach to inverse computation in term rewriting  
その他のタイトル  
その他のタイトル  項書換えにおける逆計算へのプログラム変換アプローチ  
著者 
Nishida, Naoki
× Nishida, Naoki 

抄録  
内容記述  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 PTTRSs. PTTRSs 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 righthand 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 PTTRSs is narrow. Hence we extend the inverse compiler for PTTRSs to that for constructor TRSs. Constructor TRSs includes PTTRSs 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 EVTRSs, which can contain extra variables in the righthand sides of their rewrite rules. Extra variables are variables which appear in the conditional part or the righthand side of a conditional rewrite rule but not in the lefthand side. In order to show the correctness of the program transformation in the second part, we show soundness and completeness of the generated EVTRSs 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 EVTRS generated by our inverse compilers. Three of such relationships are very important. One is that the generated EVTRSs are constructor systems. A second is that the generated EVTRS is a TRS if the input TRS is nonerasing. The other is that the generated EVTRS is rightlinear (leftlinear) if the input is leftlinear (rightlinear, respectively).EVTRSs contain two serious problems for practical use of them. One is that their onestep 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, EVTRSs in general cannot be executed efficiently. Unfortunately, the inverse programs generated by out inverse compilers are EVTRSs. Therefore a simulation method of rewrite relation of EVTRS s is necessary.To simulate rewrite relation of EVTRS 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 EVTRS if the EVTRS is rightlinear 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 EVTRSs 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 EVTRSs 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 rightlinear EVTRSs. Since the leftlinearity is often assumed in firstorder functional programs and inverse EVTRSs of linear constructor TRSs are rightlinear, this result is useful for the efficience of our inverse computation. We also show that for linear constructor EVTRSs, all normal forms of a given terminating term can be obtained by innermost narrowing. To generate innermostterminating inverse TRSs, we give a condition on the relationship between the depth of the both hand sides of each rewrite rules in the input nonerasing TRSs. The condition for each rule is that the root symbol of the righthand side is not a defined symbol, the depth of the lefthand side is two or less if the righthand 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 righthand 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.  
内容記述タイプ  Abstract  
内容記述  
内容記述  名古屋大学博士学位論文 学位の種類:博士(工学) (課程) 学位授与年月日:平成16年3月25日  
内容記述タイプ  Other  
言語  
言語  eng  
資源タイプ  
資源  http://purl.org/coar/resource_type/c_46ec  
タイプ  thesis  
書誌情報  発行日 20040325  
学位授与年度  
学位授与年度  2003  
学位授与年月日  
学位授与年月日  20040325  
学位授与番号  
学位授与番号  13901甲第6287号  
フォーマット  
application/pdf  
著者版フラグ  
値  publisher  
URI  
識別子  http://hdl.handle.net/2237/11185  
識別子タイプ  HDL 