此條目需要精通或熟悉相关主题的编者参与及协助编辑。 (2011年1月5日)
請邀請適合的人士改善本条目。更多的細節與詳情請參见討論頁。 |
重写逻辑是一种对绝大多数编程语言和系统进行规范描述的计算机逻辑。重写逻辑能把目标逻辑的抽象语法表示为代数结构。利用重写规则，目标逻辑的推理规则可以被描述出来。[1]
重写逻辑中的语法和结构化公理都由用户自己定义，这使其变得极为简单且通用。
1992年，José Meseguer在《作为统一并发模型的条件重写逻辑》一文中首先提出重写逻辑这一概念。[2]
基本公理 重写逻辑中的基本公理是形如 t→t'的重写规则。重写规则有计算性解读与逻辑性解读两种解读方式。这两种不同的解读方式对应重写逻辑的两种应用价值：语义框架和逻辑框架。[3]
计算性解读
把t、t'看作系统碎片的状态，把重写当作状态迁移（类似Petri网）。
语义框架
重写逻辑可以用来表达计算系统和编程语言。重写逻辑被设计成一种描述变化的逻辑，能对系统的迁移进行完备的推理。系统的基本变化用重写规则刻画。
逻辑性解读
把t、t'看作公式，t→t'表示t可以推导出t'。
逻辑框架
重写逻辑可以被用来表达其他逻辑（如等式逻辑、线性逻辑及霍尔逻辑等）。
与项重写系统
重写逻辑这一概念由José Meseguer等提出并定义，并作为他们自己开发的Maude的基础。 但计算机科学界一般把大部分相关知识体系归到“项重写系统”。 项重写和项重写系统的最早研究可以追溯到数理逻辑发展早期，如弗雷格，Herbrand，哥德尔等人的工作，虽然那时候并没有明确提出“项重写系统”这个概念。2003年，荷兰的klop等人出版了第一本研究项重写系统的专著《term rewriting systems》，系统阐述了项重写系统的历史起源和概念，主要内容，课题和应用。klop等的书中稍微提及重写逻辑，脚注为“实际上就是没有对称性的等式逻辑(equational logic without symmetry)”。 在列举基于项重写系统的软件系统时描述José Meseguer等开发的Maude为“可以按照等式逻辑和重写逻辑推理”，遵照了José Meseguer等自己对Maude的描述用词。20世纪80年代到90年代曾出现基于项重写系统的程序语言设计的热潮，其中Obj系列的项重写语言比较有名，而Maude是对Obj3的继承。基于项重写的程序语言的特点是匹配和替换(重写)，因此，函数式编程语言Haskell也属于这一类。而且，函数式编程语言的理论基础——lambda演算和组合逻辑——本身就被认为是典型的项重写系统。其它基于项重写的语言或系统包括：Isabella,Pure,Clean等。
Maude
Maude是José Meseguer等带领下开发的基于重写逻辑的软件。可以同时支持等式逻辑和重写逻辑推理。 Maude可以用关键字comm和assoc来指定模交换律和结合律的重写（rewriting modulo commutativity and associativity）。pure等语言同样可以使用 a+(b+c)=(a+b)+c的等式来指定“+”的结合律。不过，pure确实不能通过a+b=b+a来指定“+”的交换律，因为这样的等式会造成 a+b=b+a=a+b...无穷推理下去。这是因为a+b和b+a的匹配模式是一样的，而a+(b+c)和(a+b)+c的匹配模式不一样。后者不会造成无穷推理。而pure语言确实没有提供模交换律的重写。这一点上，Maude是占有优势的。
参考文献 - ^ Gabbay,D.M.,&Guenthner,F. Handbook of Philosophical Logic-vol 9. Kluwer Academic Publishers. [2011年1月]. （原始内容于2019-06-30） （英语）.
- ^ José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science. 1992: 73–155.
- ^ Rewriting Logic: Roadmap and Bibliography （英语）.
重写逻辑, 此條目需要精通或熟悉相关主题的编者参与及协助编辑, 2011年1月5日, 請邀請適合的人士改善本条目, 更多的細節與詳情請參见討論頁, 是一种对绝大多数编程语言和系统进行规范描述的计算机逻辑, 能把目标逻辑的抽象语法表示为代数结构, 利用重写规则, 目标逻辑的推理规则可以被描述出来, 中的语法和结构化公理都由用户自己定义, 这使其变得极为简单且通用, 1992年, josé, meseguer在, 作为统一并发模型的条件, 一文中首先提出这一概念, 目录, 基本公理, 计算性解读, 语义框架, 逻辑性解. 此條目需要精通或熟悉相关主题的编者参与及协助编辑 2011年1月5日 請邀請適合的人士改善本条目 更多的細節與詳情請參见討論頁 重写逻辑是一种对绝大多数编程语言和系统进行规范描述的计算机逻辑 重写逻辑能把目标逻辑的抽象语法表示为代数结构 利用重写规则 目标逻辑的推理规则可以被描述出来 1 重写逻辑中的语法和结构化公理都由用户自己定义 这使其变得极为简单且通用 1992年 Jose Meseguer在 作为统一并发模型的条件重写逻辑 一文中首先提出重写逻辑这一概念 2 目录 1 基本公理 1 1 计算性解读 1 1 1 语义框架 1 2 逻辑性解读 1 2 1 逻辑框架 1 3 与项重写系统 1 4 Maude 2 参考文献基本公理 编辑重写逻辑中的基本公理是形如 t t 的重写规则 重写规则有计算性解读与逻辑性解读两种解读方式 这两种不同的解读方式对应重写逻辑的两种应用价值 语义框架和逻辑框架 3 计算性解读 编辑 把t t 看作系统碎片的状态 把重写当作状态迁移 类似Petri网 语义框架 编辑 重写逻辑可以用来表达计算系统和编程语言 重写逻辑被设计成一种描述变化的逻辑 能对系统的迁移进行完备的推理 系统的基本变化用重写规则刻画 逻辑性解读 编辑 把t t 看作公式 t t 表示t可以推导出t 逻辑框架 编辑 重写逻辑可以被用来表达其他逻辑 如等式逻辑 线性逻辑及霍尔逻辑等 与项重写系统 编辑 重写逻辑这一概念由Jose Meseguer等提出并定义 并作为他们自己开发的Maude的基础 但计算机科学界一般把大部分相关知识体系归到 项重写系统 项重写和项重写系统的最早研究可以追溯到数理逻辑发展早期 如弗雷格 Herbrand 哥德尔等人的工作 虽然那时候并没有明确提出 项重写系统 这个概念 2003年 荷兰的klop等人出版了第一本研究项重写系统的专著 term rewriting systems 系统阐述了项重写系统的历史起源和概念 主要内容 课题和应用 klop等的书中稍微提及重写逻辑 脚注为 实际上就是没有对称性的等式逻辑 equational logic without symmetry 在列举基于项重写系统的软件系统时描述Jose Meseguer等开发的Maude为 可以按照等式逻辑和重写逻辑推理 遵照了Jose Meseguer等自己对Maude的描述用词 20世纪80年代到90年代曾出现基于项重写系统的程序语言设计的热潮 其中Obj系列的项重写语言比较有名 而Maude是对Obj3的继承 基于项重写的程序语言的特点是匹配和替换 重写 因此 函数式编程语言Haskell也属于这一类 而且 函数式编程语言的理论基础 lambda演算和组合逻辑 本身就被认为是典型的项重写系统 其它基于项重写的语言或系统包括 Isabella Pure Clean等 Maude 编辑 Maude是Jose Meseguer等带领下开发的基于重写逻辑的软件 可以同时支持等式逻辑和重写逻辑推理 Maude可以用关键字comm和assoc来指定模交换律和结合律的重写 rewriting modulo commutativity and associativity pure等语言同样可以使用 a b c a b c的等式来指定 的结合律 不过 pure确实不能通过a b b a来指定 的交换律 因为这样的等式会造成 a b b a a b 无穷推理下去 这是因为a b和b a的匹配模式是一样的 而a b c 和 a b c的匹配模式不一样 后者不会造成无穷推理 而pure语言确实没有提供模交换律的重写 这一点上 Maude是占有优势的 参考文献 编辑 Gabbay D M amp Guenthner F Handbook of Philosophical Logic vol 9 Kluwer Academic Publishers 2011年1月 原始内容存档于2019 06 30 英语 Jose Meseguer Conditional rewriting logic as a unified model of concurrency Theoretical Computer Science 1992 73 155 Rewriting Logic Roadmap and Bibliography 英语 使用 accessdate 需要含有 url 帮助 取自 https zh wikipedia org w index php title 重写逻辑 amp oldid 71251653, 维基百科，wiki，书籍，书籍，图书馆，
文章
，阅读，下载，免费，免费下载，mp3，视频，mp4，3gp， jpg，jpeg，gif，png，图片，音乐，歌曲，电影，书籍，游戏，游戏。