论文部分内容阅读
1.引言项重写系统是一种受到广泛研究和应用的形式计算模型.一个项重写系统由一组称为重写规则的定向等式组成.它的计算基于代入、匹配和替换,除具有方向性外,与等式推导一致.虽然项重写系统形式简单、计算单纯,但它同时又具有与λ计算及图灵机相同的计算能力.正是它的简洁性及计算能力使它受到广泛的研究和应用:项重写系统为抽象数据类型提供类型、为函数型语言提供操作语义、为定理自动证明提供推理工具.对于项重写系统本身也有大量的研究:如合流性、终止性、等价性等[1-5].