| 講演抄録／キーワード |
| 講演名 |
2004-08-02 13:00
高階書換え系の決定可能な計算戦略について
○粕谷英人（愛知県立大）・酒井正彦・阿草清滋（名大） |
| 抄録 |
（和） |
高階書換え系の正規化戦略である必須書換えを用いて計算を行う場合，項書換え系における場合と同様に一般的にその計算は決定可能ではない．本論文では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 / / / |
| 文献情報 |
信学技報, vol. 104, no. 242, SS2004-6, pp. 1-6, 2004年8月. |
| 資料番号 |
SS2004-6 |
| 発行日 |
2004-07-26 (SS) |
| ISSN |
Print edition: ISSN 0913-5685 |
| PDFダウンロード |
|