2024-03-29T21:30:32Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000166482020-10-27T05:02:43Z00934:00935:00954:00958
木準同型写像を用いた項パターンマッチングTerm Pattern Matching with Tree Homomorphismjpn発表概要http://id.nii.ac.jp/1001/00016648/Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=16648&item_no=1&attribute_id=1&file_no=1Copyright (c) 2005 by the Information Processing Society of Japan東北大学電気通信研究所東北大学電気通信研究所東北大学電気通信研究所千葉, 勇輝青戸, 等人外山, 芳人ラムダ計算のパターンマッチングに基づくプログラム自動変換法の枠組みがHuet-Lang (1978) によって提案されている.本発表では,項書き換えシステムに基づくパターンマッチングを実現するために木準同形写像の概念を導入する.はじめに,項パターンマッチングを実現するためのアルゴリズムを提案し,アルゴリズムの正当性を示す.さらに,項パターンマッチングアルゴリズムを項書き換えシステムに適用し,木準同形写像がリダクション関係を保存することを証明する.また,正規形が保存されるべきクラスを示し,木準同形写像によってそのクラスの正規形が保存されるための十分条件を示す.本発表におけるパターンマッチングアルゴリズムは,操作的意味論に基づくプログラム変換の正当性を示す第一歩となると期待される.Huet and Lang (1978) developed a framework of automated program transformation using second-order matching algorithm of lambda terms. In this paper, we present a second-order matching algorithm based on term rewriting in which higher-order substitutions are represented by tree homomorphisms. We present term pattern matching algorithm and show its correctness; we then apply the algorithm to match term rewriting systems on term patterns with term rewriting systems. We then show reduction is preserved by tree homomorphisms and give a sufficient condition of tree homomorphisms that map suitable normal patterns to normal terms. Our matching algorithm is a first step to study the correctness of program transformations based on the operational semantics.AA11464814情報処理学会論文誌プログラミング(PRO)46SIG1(PRO24)1511512005-01-151882-78022009-06-30