氏名: 洪 順姫 (289934257)

論文題目: メタ項書換え計算の合流性に関する研究


論文概要

メタ項書換え計算(Metaterm Rewriting Calculus,MRC)は, 項書換え系(TRS)を処理するアルゴリズムの設計・解析に対して 形式的な基礎を与えることを目的とする書換え型の計算モデルである. 書換え型の計算モデルの最も重要な性質として合流性がある. しかし,MRCではその定義から明らかなように,一般には項の合流性が保証されな い. 合流性の性質を持つMRCのサブセットを発見することは, それに基づく解析を行うためには必要不可欠である. 本研究では,メタ項が合流性を持つための十分条件を明らかにすることを 目的とし,直交性を持つ(左線形でかつ重なりがない)メタ項が合流性を持つことを示 した.

MRCは従来の項書換え系とは異なり,有効な書換え規則が項の出現の位置によって 異なること,書換え規則が別の書換え規則によって書き換わるという二つの特徴を持 つ ため,従来の項書換え系に対する合流性の証明をそのまま適用できない. そこで本研究では,項書換え系の合流性の証明に用いられている デベロップメントの概念をMRC向けに改良することによって, 直交性を持つメタ項が合流性を持つことを証明した.


目次に戻る


提出時刻:2001/02/08 14:29:19