ルートE重なりな深さ保存項書き換えシステムのチャーチ・ロッサー性について

• GOMI HIROSHI

  Faculty of Engineering, Mie University Oki TechnoSystems Laboratory, Inc.

• OYAMAGUCHI MICHIO

  Faculty of Engineering,Mie University

• OHTA YOSHIKATSU

  Faculty of Engineering, Mie University

Bibliographic Information

Other Title

• On the Church-Rosser Property of Root-E-overlapping and Depth-Preserving Term Rewriting Systems

Abstract

項書き換えシステムが強深さ保存であるとは、すべての書き換え規則の両辺に現れる各変数において、その変数の左辺における出現位置の最小深さが右辺の最大深さ以上であるときである。本稿では強深さ保存項書き換えシステムのチャーチ・ロッサー性を保証する十分条件を与え、この条件の判定方法について述べる。各関数記号に対して正の整数(重みと呼ぶ)を割り当てることにより、強深さ保存の概念を強重み保存の概念に自然に拡張することができ、強重み保存項香き換えシステムのチャーチ・ロッサー性を保証する同様な十分条件を導くことができる。
A term rewriting system (TRS) is said to be strongly depth-preserving if for any rewrite rule and any variable appearing in the both sides, the minimal depth of the variable occurrences in the left-hand-side is greater than or equal to the maximal depth of the variable occurrences in the right-hand-side. This paper gives a sufficient condition for Church-Rosser of strongly depth-preserving TRS's and describes how to check this condition. By assigning a positive integer (called weight) to each function symbol, the notion of strongly depth-preserving is naturally extended to that of strongly weight-preserving and a similar sufficient condition for church-Rosser of strongly weigh-preserving TRS's is obtained.

Journal

• IPSJ SIG Notes

  IPSJ SIG Notes 97 (9), 109-116, 1997-01-23

  Information Processing Society of Japan (IPSJ)

Keywords

• Term Rewriting System
• Church-Rosser property
• non-linear
• depth-preserving
• weight-preserving
• E-overlapping

Details

• CRID: 1574231876937576704
• NII Article ID: 110002929354
• NII Book ID: AN10485570
• Text Lang: en
• Data Source:
  • CiNii Articles