重写系统

重写系统（rewriting systems），理学-计算机科学技术-计算机科学理论-可计算模型-形式化，一种非对称的等式逻辑（equation logic）。计算机科学领域大部分相关知识体系都可归到重写系统。重写系统可以看作是由一组对象及其上（子）对象上的代换关系组成。代换关系称为重写规则。项重写是指将公式中的某个子项代换为其他项。用模式匹配的方法进行表达式求值的机制通常称为项重写，即可以用规则对项进行代换或重写。项重写系统是由重写规则组成的集合，可以应用的领域有定理证明、（数据类型、程序等的）代数说明、计算机代数学、演算、声明语言的实现和程序设计语言的操作语义等。除了项重写系统还有字符串重写系统（string rewriting systems）、图重写系统（graph rewriting systems）和迹重写系统（trace rewriting systems）等。令为函数符号的集合，为变量符号的集合，并且和不相交，则和上的项的集合定义为：①每个元函数符号是项（称为常量符号）；②每个变量符号是项；③若是项，是元函数符号，则是项,其中。是一个项，令表示中所有出现的变量的集合。