重寫邏輯

重寫邏輯是一種對絕大多數程式語言和系統進行規範描述的計算機邏輯。重寫邏輯能把目標邏輯的抽象語法表示為代數結構。利用重寫規則，目標邏輯的推理規則可以被描述出來。

重寫邏輯中的語法和結構化公理都由用戶自己定義，這使其變得極為簡單且通用。

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

國內研究

國內有學者認為把“重寫邏輯”提升到一個單獨概念而與“項重寫系統”相分別可能是沒有必要的，其理由是：很多基於項重寫的系統和語言都具有跟Maude相近的機制和能力，但他們的作者並沒有提到自己的軟體是基於重寫邏輯。從項重寫的角度理解這些系統和語言（包括Maude）的運行機理是非常自然的。重寫邏輯的提法反而讓人感到困惑。所有項重寫語言使用等式邏輯運行時本來就是單向的（所謂的重寫邏輯！）
不過，上述考慮是基於Maude和其他語言（如Haskell以及Pure）中的規則被“計算性解讀”的情形下；如果考慮Meseguer提出的“邏輯性解讀”，非對稱推理的重寫和對稱推理的等式確實不一樣。考慮如下語句：

a=b；a=c；則可以得到 c=b a->b；a->c；得不到 c->b 

Maude在運行時並不會把c重寫到b,但如果使用Maude的search命令（不變數檢測）或LTL模型檢測工具來分析上述語句時，Maude確實把等式和重寫規則分別對待（如果是等式規則，search c => b是滿足的，重寫規則不滿足； => 表示可達或可推理得到）。此外，Maude的開發者開發了一些附帶工具用來檢測等式規則和重寫規則的其它性質。這包括終止性，合流性，而這些都是項重寫系統研究課題中的內容。而Pure和Haskell等語言並不集成search命令或LTL模型檢測工具。雖然程式設計師也可以自己開發這些不平凡的工具。
總體來說，Maude的語法雖然沒有Haskell優雅，但功能設計上Maude比Haskell更偏向對項重寫系統的分析。後者定位在一種通用（雖然是函式式，不是命令式）的程式語言。Maude使用reduce命令(可簡寫為red)完成Haskell那樣的計算任務(規則的計算性解讀)，使用search命令，LTL(連同red)checker，以及其他checker完成項重寫系統的其它分析任務（規則的邏輯性解讀）。
國內已經有學者把Maude用於模型檢測和預設邏輯研究。Maude一般不作為通用的程式語言，雖然它也可以完成簡單的計算任務。但它用於實用計算的庫太少了（數值計算，圖形和網路編程）。