右辺のみに現れる変数を持つ項書換え系の計算モデル A computation model of term rewriting systems with extra variables

Access this Article

Author(s)

Abstract

右辺のみに現れる変数を持つ書換え規則を含む項書換え系(EV-TRS) は,その変数に任意の項を代入して書き換えられるので,書換え関係が無限分岐となる.そのため,EV-TRS は計算モデルとして好ましくない.本稿では,ナローイングをEV-TRS の書換え(EV ナローイング) に自然に拡張し,これがEV-TRS の書換え関係を十分にシミュレーションすることを示す.さらに,EV ナローイングが停止するEV-TRS の1 つの条件を示す.

The reduction relation of a term rewriting system with extra variables,called EV-TRSs, is infinitely branching since terms are reduced bysubstituting an arbitrary term for each extra variable of an applicablerewrite rule. Therefore, EV-TRSs are undesirable as a computation model.In this paper, we propose EV-narrowing which is a new reduction ofEV-TRSs and a natural extension of narrowing. Then, we show thatEV-narrowing can sufficiently simulate the original reduction relationof any EV-TRS. Moreover, we show a condition on EV-TRSs such thatEV-narrowing terminates.

Journal

  • Conference Proceedings of Japan Society for Software Science and Technology

    Conference Proceedings of Japan Society for Software Science and Technology 19(0), 6F3-6F3, 2002

    Japan Society for Software Science and Technology

Codes

Page Top