重寫邏輯

在數學、計算機科學和邏輯學中，重寫邏輯是把目標邏輯的抽象語法替換為代數結構，通過用其他術語表示公式子項的各種實現方法。利用重寫規則，目標邏輯的推理規則可以被描述出來。 重寫邏輯中的結構化公理和語法都由用戶自己定義，這使其變得極為簡單且通用。在最基本的形式中，一種重寫的規則可適用多個規則。因此，當與適當的算法結合時，重寫系統被視為絕大多數程式語言和系統應用程式進行規範描述的計算機邏輯，許多定理證明和宣告式程式語言是基於重寫的。

1992年，José Meseguer在《作為統一併發模型的條件重寫邏輯》一文中首先提出重寫邏輯這一概念。

基本公理

重寫邏輯中的基本公理是形如 t→t'的重寫規則。重寫規則涵蓋了計算性解讀與邏輯性解讀兩種解讀方式。這兩種不同的解讀方式能對應重寫邏輯的兩種應用價值：語義框架和邏輯框架。

計算性解讀

把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是佔有優勢的。

外部連結

• The Rewriting Home Page （頁面存檔備份，存於互聯網檔案館）
• IFIP Working Group 1.6 （頁面存檔備份，存於互聯網檔案館）
• 因斯布魯克大學Researchers in rewriting （頁面存檔備份，存於互聯網檔案館）
• Termination Portal
• Maude System （頁面存檔備份，存於互聯網檔案館） — 通用術語重寫系統的軟件實現。

參見

• 臨界對 (邏輯)
• 編譯器
• Knuth-Bendix 完成算法
• L系統指定並行完成的重寫。
• 計算機科學中的參考透明度
• Regulated rewriting
• Rho演算
• Interaction nets