2024-03-29T11:32:10Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000168742020-10-27T05:02:43Z00934:00935:00973:00975
λ項を用いた抽象ナローイングとその完全性Completeness of Abstract Narrowing with Lambda Termsjpn発表概要http://id.nii.ac.jp/1001/00016874/Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=16874&item_no=1&attribute_id=1&file_no=1Copyright (c) 2001 by the Information Processing Society of Japan三重大学東北大学奥居, 哲鈴木, 太朗本稿は抽象的なナローイングを定式化し,その完全性を論じるものである.もともと一階の等式の求解法として提案されたナローイングは関数・論理型プログラミング言語の基礎として発展し,現在では高階項書き換え系を用いた高階の項におけるナローイングや,グラフ書き換え系を用いたナローイングも提案されている.前者はHaskelやMLのような高階関数を扱う機能を持つ言語の,後者は遅延評価機構の計算機上への実装のモデル化に適している.これらのナローイングに共通する最も重要な理論的性質は求解完全性であるが,その証明はそれぞれの定式化の枠組みで別個に行わざるをえなかった.そこで我々は,これらのナローイングを統一的に扱える抽象的な枠組みを提供し,種々のナローイングの求解完全性を簡潔に示すことを目指す.我々の定式化はvan Oostromによる高階項書き換え系を用いる.この定式化で特徴的なのは,代入を $エlambda$ 項上の計算として抽象化している点である.本稿では,ナローイングをこのように定式化することで,求解完全性の証明が従来のものと比べはるかに簡潔で見通し良くなることを示す.また一階のナローイングをこの枠組みでモデル化することで,抽象ナローイングにおける求解完全性から一階のナローイングの求解完全性を導けることを示す.Nipkowによる高階項書き換え系に基づくナローイングに対しても同様のことが示せると予想される.In this paper we propose an abstract form of narrowing and show its completeness. Narrowing has originally been a method for solving first-order equations. Now it is extended to the solving of higher-order or term graph equations. Due to their apparent difference, completeness, the most important theoretical property of narrowing, of these narrowing methods has been proved independently. Our goal is to propose a unified framework for narrowing and to show completeness of various narrowing concisely in this framework. Our formulation is based on higher-order rewriting a la van Oostrom. Here, substitution is performed by means of so-called substitution calculus, an operation on lambda terms. This yields a simple and clear completeness proof of the abstract narrowing. We present a rigorous proof of completeness and show that completeness of conventional first-order narrowing is an instance of the above completeness result.AA11464814情報処理学会論文誌プログラミング(PRO)42SIG07(PRO11)90902001-07-151882-78022009-06-30