講演名 2004-08-02
高階書換え系の決定可能な計算戦略について
粕谷 英人, 酒井 正彦, 阿草 清滋,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 高階書換え系の正規化戦略である必須書換えを用いて計算を行う場合,項書換え系における場合と同様に一般的にその計算は決定可能ではない.本論文ではNipkowによる高階書換え系を対象とし,線形な高階パターンの具体項を受理する木オートマトンの構成法を示す.また,両辺に自由変数を共有しないよう近似した高階書換え系の書換え関係を認識するGTTの構成法を与えるこれらにより,高階書換え系の強逐次戦略とNV逐次戦略が決定可能であることを示す.
抄録(英) Needed redexes whose reduction yield is a normalizing strategy are not decidable in higher-order rewrite systems as well as in term rewriting. In this paper we focus on Nipkow's system. We present a construction of tree automata that recognize the instances of linear higher-order patterns. We give a construction of ground tree tranducers that recognize rewrite relation of a higher-order rewrite system whose rules are linear. From these results, we show that the strong sequential strategy and the NV-sequential strategy of higher order rewrite systems are decidable.
キーワード(和) 高階書換え系 / 正規化戦略 / 必須書換え / 木オートマトン / GTT
キーワード(英) higher-order rewrite system / normalizing strategy / needed reduction / tree automaton / GTT
資料番号 SS2004-6
発行日

研究会情報
研究会 SS
開催期間 2004/7/26(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Software Science (SS)
本文の言語 JPN
タイトル(和) 高階書換え系の決定可能な計算戦略について
サブタイトル(和)
タイトル(英) A Decidable Strategy for Higher-Order Rewrite Systems
サブタイトル(和)
キーワード(1)(和/英) 高階書換え系 / higher-order rewrite system
キーワード(2)(和/英) 正規化戦略 / normalizing strategy
キーワード(3)(和/英) 必須書換え / needed reduction
キーワード(4)(和/英) 木オートマトン / tree automaton
キーワード(5)(和/英) GTT / GTT
第 1 著者 氏名(和/英) 粕谷 英人 / Hideto KASUYA
第 1 著者 所属(和/英) 愛知県立大学情報科学部
Faculty of Information Science and Technology, Aichi Prefectural University
第 2 著者 氏名(和/英) 酒井 正彦 / Masahiko SAKAI
第 2 著者 所属(和/英) 名古屋大学大学院情報科学研究科
Graduate School of Information Science, Nagoya University
第 3 著者 氏名(和/英) 阿草 清滋 / Kiyoshi AGUSA
第 3 著者 所属(和/英) 名古屋大学大学院情報科学研究科
Graduate School of Information Science, Nagoya University
発表年月日 2004-08-02
資料番号 SS2004-6
巻番号(vol) vol.104
号番号(no) 242
ページ範囲 pp.-
ページ数 6
発行日