4.2 操作語意
操作語意(operational semantics)談一個程式做什麼。
在操作語意中，我們通常不談符號的「意思」是什麼。
符號 Zero 只代表它本身，Suc Zero 也只代表它本身。
操作語意著重的是一串符號如何變成另一段符號。
在這個意義下，前述的 fact 定義：
fact :: Nat -> Nat
fact Zero = 1
fact (Suc n) = (Suc n) * fact n
從操作語意的觀點可被讀解成覆寫規則：看到 fact Zero, 均可改寫為 1; 看到 fact (Suc n), 均可改寫為 (Suc n) * fact n.
歸約 fact (Suc (Suc Zero)) 這個式子可被視為是不斷使用這兩條覆寫規則：
fact (Suc (Suc Zero))
= (Suc (Suc Zero)) * fact (Suc Zero)
= (Suc (Suc Zero)) * (Suc Zero) * fact Zero
= (Suc (Suc Zero)) * (Suc Zero) * 1
其中的每個等號都可讀解為「改寫成」。
操作語意中較容易談「執行」與「終止」的概念。
改寫一個式子相當於執行它，如果已經沒有可改寫之處，也就是碰到了範式，執行便終止了。
在操作語意中，兩個數值（例如 4+4 與 2*4）相等意謂它們可被歸約成同一個範式；
兩個函數 f 和 g 相等則意謂對於任何 x, f x 與 g x 都相等。
有了兩種談語意的方式，我們自然希望它們有些一致性。確實，我們有如下的定理：
定理 4.1
操作語意保持指稱語意。意即，給定一個有指稱語意的算式 e, 若算式 e 能在零步或多步之內依據操作語意改寫成 e', 則 e 與 e' 的指稱語意相同。
定理 4.2
給定一個遞迴的函數定義 f = F f。若在操作語意中，該函數對所有輸入都正常終止，則在指稱語意中，f 是 F 的唯一定點。
我們在下一節會