第 16 章：程序推理（Reasoning about programs）
原文：Graham Hutton, Programming in Haskell, Second Edition, Chapter 16。维护者已确认本书可翻译并发布用于学习研究。
本章介绍对 Haskell 程序进行推理的思想。我们先回顾等式推理的概念，然后考虑它如何应用于 Haskell，接着介绍重要的归纳技术，展示如何用归纳消除 append 运算符的使用，最后证明一个简单编译器的正确性。
16.1 等式推理（Equational reasoning）
在学校里，我们学习过数字的一些基本代数性质，例如乘法满足交换律，加法满足结合律，而乘法对加法在左右两侧都满足分配律：
x * y = y * x
x + (y + z) = (x + y) + z
x * (y + z) = x * y + x * z
(x + y) * z = x * z + y * z
例如，使用这些性质可以说明，形如 (x+a) * (x+b) 的乘积可以展开为求和 x^2 + (a+b)*x + a*b：
(x+a) * (x+b)
= { left distributivity }
x * (x+b) + a * (x+b)
= { right distributivity }
x*x + x*b + a*x + a*b
= { squaring }
x^2 + a*x + x*b + a*b
= { commutativity }
x^2 + a*x + b*x + a*b
= { right distributivity }
x^2 + (a+b)*x + a*b
注意，在这个计算中，我们遵循常见做法，隐式利用结合律性质。在这里，当连续使用多个加法时，我们省略了括号，也就是隐式使用了加法结合律。
代数性质除了本身很有趣，也可能具有计算意义。例如，表达式 x * (y+z) 需要两个操作（一次乘法和一次加法），而等价表达式 x*y + x*z 需要三个操作（两次乘法和一次加法）。因此，尽管这两个表达式在代数上相等，从效率角度看，前者优于后者。
16.2 关于 Haskell 的推理（Reasoning about Haskell）
同样风格的等式推理也可以用于 Haskell。例如，在这个语境中，等式 x * y = y * x 表示：对任意相同数值类型的表达式 x 和 y，求值 x * y 与 y * x 总会产生相同的数值结果。注意，在陈述这类性质时，我们使用数学中的相等关系，而不是 Haskell 自身提供的相等运算符 ==。这是因为我们的目标是把数学作为一门语言来推理 Haskell，而不是用 Haskell 作为语言来推理 Haskell 自身；后者多少有些循环。
对 Haskell 进行推理时，我们不仅会使用语言内置操作（例如加法和乘法）的性质，也会使用构造用户自定义函数时所依据的等式。例如，考虑下面这个把整数翻倍的函数：
double :: Int -> Int
double x = x + x
这个等式既可以看作函数定义，也可以看作推理该函数时可用的性质。特别是，作为逻辑性质，上面的等式说明，对于任意整数表达式 x，表达式 double x 可以自由替换为 x + x；反过来，表达式 x + x 也可以自由替换为 double x。这样一来，在对程序进行推理时，函数定义既可以从左到右应用，也可以从右到左取消应用。
不过，当函数使用多个等式定义时，需要更加小心。例如，考虑一个判断整数是否为零的函数，它由两个等式定义：
isZero :: Int -> Bool
isZero 0 = True
isZero n = False
第一个等式 isZero 0 = True 可以自由看作一个逻辑性质，并在两个方向上应用。然而，第二个等式 isZero n = False 并非如此。特别是，由于 Haskell 中等式书写顺序具有意义，只有在 n /= 0 时，形如 isZero n 的表达式才能替换为 False，因为当 n = 0 时会应用第一个等式。对偶地，也只有在 n /= 0 时，才能取消应用等式 isZero n = False，把 False 替换为形如 isZero n 的表达式，原因相同。
更一般地说，当函数由多个等式定义时，这些等式不能脱离彼此、孤立地看作逻辑性质，而需要根据各等式中模式匹配的顺序来解释。因此，最好用不依赖等式书写顺序的方式定义函数。例如，如果把上面的定义改写为使用守卫：
isZero 0 = True
isZero n | n /= 0 = False
现在就显式表明，只有当守卫 n /= 0 成立时，isZero n 才能替换为 False，反过来 False 也只能在这个条件成立时替换为 isZero n。不依赖匹配顺序的模式称为不重叠模式（non-overlapping patterns）。为了简化程序推理过程，定义函数时应尽可能使用不重叠模式。例如，附录 B 中给出的大多数标准 prelude 函数都是以这种方式定义的。
16.3 简单例子（Simple examples）
作为 Haskell 中等式推理的第一个简单例子，回忆下面这个反转列表的库函数定义：
reverse :: [a] -> [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
使用这个定义，可以说明 reverse 对单元素列表没有影响，也就是说，对于任意值 x 都有 reverse [x] = [x]：
reverse [x]
= { list notation }
reverse (x : [])
= { applying reverse }
reverse [] ++ [x]
= { applying reverse }
[] ++ [x]
= { applying ++ }
[x]
因此，程序中任何形如 reverse [x] 的表达式都可以自由替换为 [x]，含义不变，但效率会变化，因为这样避免了应用 reverse 函数。
等式推理经常与某种形式的情况分析结合使用。例如，考虑逻辑否定函数：
not :: Bool -> Bool
not False = True
not True = False
由于这个函数通过模式匹配定义，关于 not 的性质通常通过对其参数进行情况分析来证明。例如，not 是自身的逆函数，也就是说对所有逻辑值 b 都有 not (not b) = b，可以通过分别分析 b 的两个可能取值来说明。下面验证 b = False 的情况；b = True 的情况类似：
not (not False)
= { applying the inner not }
not True
= { applying not }
False
16.4 对数字归纳（Induction on numbers）
大多数有趣的 Haskell 程序都包含某种形式的递归。关于这类程序的推理通常使用一种简单但强大的技术：归纳。我们先回忆最简单的递归类型，也就是自然数类型：
data Nat = Zero | Succ Nat
这个声明说明 Zero 是类型 Nat 的值（基本情况），并且如果 n 是类型 Nat 的值，那么 Succ n 也是类型 Nat 的值（递归情况）。该声明还隐含说明，Zero 和 Succ 是类型 Nat 唯一的构造器。因此，Nat 的值可以列举如下：
Zero
Succ Zero
Succ (Succ Zero)
Succ (Succ (Succ Zero))
...
为简单起见，我们只考虑有限自然数，也就是从 Zero 开始、有限次应用 Succ 得到的自然数。特别是，我们不考虑无限值 Succ (Succ (Succ ...))，虽然它可以递归定义为 inf = Succ inf。本章考虑的所有其他递归类型也适用类似说明。
现在假设我们想证明某个性质（称为 p）对所有有限自然数成立。归纳原理说明，只需证明 p 对 Zero 成立（称为基本情况），并且 p 会被 Succ 保持（称为归纳情况）。更准确地说，在归纳情况中，需要证明：如果性质 p 对任意自然数 n 成立（称为归纳假设），那么它也对 Succ n 成立。
为什么归纳足以说明 p 对所有自然数成立？例如，如何推出 p 对 Succ (Succ Zero) 成立？从基本情况可知 p 对 Zero 成立；令 n = Zero，应用一次归纳情况，就可得出 p 对 Succ Zero 成立；再令 n = Succ Zero，第二次应用归纳情况，就可得出 p 对 Succ (Succ Zero) 成立。以类似方式，可以确立性质 p 对任意自然数成立。
把它类比成多米诺效应很有帮助。假设有一排立着的多米诺牌，并且你知道第一张牌会倒下，还知道只要某张牌倒下，它旁边下一张牌也会倒下。那么显然所有牌都会倒下：先用第一个事实启动过程，再反复使用第二个事实让过程继续。归纳中的推理模式与此相同：先验证所需性质对 Zero 成立（第一张多米诺倒下），再验证该性质会被 Succ 保持（如果任意一张多米诺倒下，它的邻居也会倒下），最后得出该性质对所有自然数成立（所有多米诺倒下）。
作为具体例子，考虑一个递归函数的定义，它接收两个自然数并把它们相加：
add :: Nat -> Nat -> Nat
add Zero m = m
add (Succ n) m = Succ (add n m)
由第一个等式可立即得到，对于任意自然数 m，add Zero m = m 成立。现在我们来说明对偶性质 add n Zero = n 也对所有自然数 n 成立。把这个性质简称为 p，并对 n 进行归纳。基本情况是说明 p Zero 成立，也就是说明 add Zero Zero = Zero，这是直接的：
add Zero Zero
= { applying add }
Zero
归纳情况需要说明，如果 p 对任意自然数 n 成立，那么 p (Succ n) 也成立。也就是说，以归纳假设 add n Zero = n 为前提，需要说明等式 add (Succ n) Zero = Succ n 成立，可验证如下：
add (Succ n) Zero
= { applying add }
Succ (add n Zero)
= { induction hypothesis }
Succ n
由于归纳证明通常包含不止一个计算，显式标明证明结束很有用。为此，我们在计算之后说明证明结束。
再看一个例子，说明自然数加法满足结合律。也就是说，对所有 x、y 和 z 都有：
add x (add y z) = add (add x y) z
这里有三个变量，那么应该对哪一个变量做归纳？注意，函数 add 是对第一个参数做模式匹配定义的，因此自然的尝试是对 x 做归纳。x 在结合律等式中两次作为 add 的第一个参数出现，而 y 只出现一次，z 从未以这种方式出现。对 x 使用归纳时，add 结合律的证明如下。
基本情况：
add Zero (add y z)
= { applying the outer add }
add y z
= { unapplying add }
add (add Zero y) z
归纳情况：
add (Succ x) (add y z)
= { applying the outer add }
Succ (add x (add y z))
= { induction hypothesis }
Succ (add (add x y) z)
= { unapplying the outer add }
add (Succ (add x y)) z
= { unapplying the inner add }
add (add (Succ x) y) z
注意，证明中的两个情况都先应用定义，最后取消应用定义。这种模式在归纳证明中很常见，但后一部分初看可能有些神秘。特别是，知道要取消应用哪个定义似乎需要一定预见。实践中，如果在某个计算点卡住，通常可以把注意力转向期望的最终结果，并试着从终点向后推回卡住的位置。
例如，在上面归纳情况中应用归纳假设得到 Succ (add (add x y) z) 之后，可能不清楚如何继续，因为没有更多定义可以应用。但如果我们关注目标表达式 add (add (Succ x) y) z，就可以先应用内层 add，再应用外层 add，生成先前卡住的表达式；把这个过程反过来（把应用变成取消应用）即可完成计算。
尽管我们使用递归类型 Nat 引入归纳，同样的原理也可以用于 Haskell 内置的整数类型。特别是，为了证明某个性质 p 对所有整数 n >= 0 成立，只需证明 p 对 0 成立（基本情况），并证明如果 p 对任意 n >= 0 成立，那么它也对 n+1 成立（归纳情况）。
例如，考虑库函数 replicate 的下面这个递归定义，它生成包含 n 个相同元素的列表：
replicate :: Int -> a -> [a]
replicate 0 _ = []
replicate n x = x : replicate (n-1) x
可以很容易通过对 n >= 0 归纳来说明，这个函数确实会产生一个包含 n 个元素的列表，也就是 length (replicate n x) = n。
基本情况：
length (replicate 0 x)
= { applying replicate }
length []
= { applying length }
0
归纳情况：
length (replicate (n+1) x)
= { applying replicate }
length (x : replicate n x)
= { applying length }
1 + length (replicate n x)
= { induction hypothesis }
1 + n
= { commutativity of + }
n + 1
16.5 对列表归纳（Induction on lists）
归纳并不局限于自然数，也可以用于推理其他递归类型，例如列表类型。正如自然数可以从零开始、通过反复应用后继函数递归构造出来，列表也可以从空列表开始、通过反复应用 cons 运算符递归构造出来。
假设我们想证明某个性质 p 对所有列表成立。列表的归纳原理说明，只需证明 p 对空列表 [] 成立（基本情况），并证明如果 p 对任意列表 xs 成立，那么对任意元素 x，p 也对 x:xs 成立（归纳情况）。当然，元素 x 和列表 xs 都必须具有适当类型。
作为第一个例子，我们对 xs 做归纳，说明本章前面定义的函数 reverse 是自身的逆函数，也就是 reverse (reverse xs) = xs。基本情况只需应用定义即可验证：
reverse (reverse [])
= { applying the inner reverse }
reverse []
= { applying reverse }
[]
归纳情况中，以假设 reverse (reverse xs) = xs 为前提，说明 reverse (reverse (x:xs)) = x:xs：
reverse (reverse (x:xs))
= { applying the inner reverse }
reverse (reverse xs ++ [x])
= { distributivity - see below }
reverse [x] ++ reverse (reverse xs)
= { singleton lists - see below }
[x] ++ reverse (reverse xs)
= { induction hypothesis }
[x] ++ xs
= { applying ++ }
x : xs
上面的计算使用了 reverse 函数的两个辅助性质：前面已得到的单元素列表性质 reverse [x] = [x]，以及一个新结果：reverse 会在 append 上分配，但两个参数列表的顺序会被交换：
reverse (xs ++ ys) = reverse ys ++ reverse xs
严格来说，这种分配是反变的。由于 append 运算符 ++ 是对第一个参数做模式匹配定义的，自然可以尝试对 xs 做归纳来验证这个性质。
基本情况：
reverse ([] ++ ys)
= { applying ++ }
reverse ys
= { identity for ++ }
reverse ys ++ []
= { unapplying reverse }
reverse ys ++ reverse []
归纳情况：
reverse ((x:xs) ++ ys)
= { applying ++ }
reverse (x : (xs ++ ys))
= { applying reverse }
reverse (xs ++ ys) ++ [x]
= { induction hypothesis }
(reverse ys ++ reverse xs) ++ [x]
= { associativity of ++ }
reverse ys ++ (reverse xs ++ [x])
= { unapplying the second reverse }
reverse ys ++ reverse (x:xs)
上面的计算又使用了 ++ 满足结合律并以 [] 为单位元这一事实。这可以用与先前关于 add 和 Zero 的结果类似的方式通过归纳验证（见练习部分）。
在第 12 章引入函子概念时，我们提到函数 fmap 需要满足两个等式定律：
fmap id = id
fmap (g . h) = fmap g . fmap h
作为对列表使用归纳的另一个例子，现在展示如何为列表函子验证这些定律。为此，我们使用下面这个列表上 fmap 的递归定义：
fmap :: (a -> b) -> [a] -> [b]
fmap g [] = []
fmap g (x:xs) = g x : fmap g xs
根据定义，同一类型的两个函数相等，当且仅当它们对相同参数总是返回相同结果。因此，为列表验证第一个函子定律 fmap id = id 时，这个等式是函数之间的相等性，我们必须说明对任意列表 xs 都有 fmap id xs = id xs。使用恒等函数的定义 id x = x，该等式可简化为 fmap id xs = xs，随后可通过对 xs 归纳验证。
基本情况：
fmap id []
= { applying fmap }
[]
归纳情况：
fmap id (x : xs)
= { applying fmap }
id x : fmap id xs
= { applying id }
x : fmap id xs
= { induction hypothesis }
x : xs
接下来，对于第二个函子定律，我们必须说明对任意 xs 都有：
fmap (g . h) xs = (fmap g . fmap h) xs
使用函数组合的定义 (f . g) x = f (g x)，该等式可简化为 fmap (g . h) xs = fmap g (fmap h xs)，随后可通过归纳验证。
基本情况：
fmap (g . h) []
= { applying fmap }
[]
= { unapplying fmap }
fmap g []
= { unapplying fmap }
fmap g (fmap h [])
归纳情况：
fmap (g . h) (x : xs)
= { applying fmap }
(g . h) x : fmap (g . h) xs
= { applying . }
g (h x) : fmap (g . h) xs
= { induction hypothesis }
g (h x) : fmap g (fmap h xs)
= { unapplying fmap }
fmap g (h x : fmap h xs)
= { unapplying fmap }
fmap g (fmap h (x : xs))
本章练习还包含若干其他例子，用于验证函子定律，以及 applicative 和 monad 定律。
16.6 让 append 消失（Making append vanish）
许多递归函数很自然地会使用列表上的 append 运算符 ++ 来定义，但在递归使用时，这个运算符会带来相当大的效率成本。本节展示如何用归纳消除这类 append 使用，从而让函数更高效。作为第一个例子，再次考虑下面这个简单递归定义：
reverse :: [a] -> [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
这个版本的 reverse 效率如何？首先，很容易说明，在假设 xs 和 ys 都已经完全求值的情况下，求值 xs ++ ys 所需的归约步数比 xs 的长度多一。因此，我们说 ++ 对其第一个参数的长度而言需要线性时间。进而可以说明，对长度为 n 的列表求值 reverse xs 所需的步数，是从 1 到 n+1 的整数之和，也就是 (n+1)(n+2)/2。使用本章开头验证的等式展开括号，可得 (n^2 + 3*n + 2)/2。因此，我们说 reverse 对其参数长度而言需要平方时间。
平方时间很糟糕。例如，反转一个包含一万个元素的列表，大约需要五千万个归约步骤。幸运的是，通过使用归纳，很容易消除 reverse 定义中对 append 的使用，从而改善其效率。
诀窍是尝试定义一个更一般的函数，把 reverse 和 ++ 的行为结合起来。特别是，我们想定义一个递归函数 reverse'，它满足下面的等式：
reverse' xs ys = reverse xs ++ ys
也就是说，把 reverse' 应用于两个列表，应当得到“反转第一个列表，再与第二个列表拼接”的结果。如果能定义这样的函数，那么利用空列表是 append 的单位元这一事实，就可以把 reverse 自身重新定义为 reverse xs = reverse' xs []。
事实上，我们不必先给出 reverse' 的定义再证明它满足上述等式，而是可以用这个等式本身驱动定义的构造。具体而言，我们尝试对 xs 归纳来验证该等式。基本情况会产生一个给出 reverse' [] ys 定义的等式，归纳情况则会产生一个给出 reverse' (x:xs) ys 定义的等式。
基本情况：
reverse' [] ys
= { specification of reverse' }
reverse [] ++ ys
= { applying reverse }
[] ++ ys
= { applying ++ }
ys
归纳情况：
reverse' (x:xs) ys
= { specification of reverse' }
reverse (x:xs) ++ ys
= { applying reverse }
(reverse xs ++ [x]) ++ ys
= { associativity of ++ }
reverse xs ++ ([x] ++ ys)
= { induction hypothesis }
reverse' xs ([x] ++ ys)
= { applying ++ }
reverse' xs (x : ys)
由这个证明可得，下面的定义足以通过归纳说明 reverse' xs ys = reverse xs ++ ys：
reverse' :: [a] -> [a] -> [a]
reverse' [] ys = ys
reverse' (x:xs) ys = reverse' xs (x : ys)
注意，reverse' 的定义并未引用原来的 reverse 函数，也未引用 append。因此，现在可以把 reverse 重新定义如下：
reverse :: [a] -> [a]
reverse xs = reverse' xs []
例如：
reverse [1,2,3]
= { applying reverse }
reverse' [1,2,3] []
= { applying reverse' }
reverse' [2,3] (1:[])
= { applying reverse' }
reverse' [3] (2:(1:[]))
= { applying reverse' }
reverse' [] (3:(2:(1:[])))
= { applying reverse' }
3:(2:(1:[]))
也就是说，列表通过一个额外参数累积最终结果而被反转。新的 reverse 定义或许不如原始版本清晰，但效率高得多。特别是，使用新定义对长度为 n 的列表求值 reverse xs 所需的归约步数只是 n+2，因此 reverse 现在对其参数长度而言需要线性时间。例如，反转包含一万个元素的列表现在大约只需要一万步，而原始定义需要约五千万步，这确实是很大的改进。
注意，我们已经在第 7 章和第 15 章通过函数 foldl 见过用累积改善函数效率的做法。例如，reverse 的累积器版本也可以通过定义 reverse = foldl (\xs x -> x:xs) [] 得到。不过，看到同样的行为如何借助归纳获得，仍然很有启发。
作为另一个消除 append 的例子，同时展示如何对树状类型使用归纳，考虑下面的二叉树类型，以及把这种树展平成列表的函数：
data Tree = Leaf Int | Node Tree Tree
flatten :: Tree -> [Int]
flatten (Leaf n) = [n]
flatten (Node l r) = flatten l ++ flatten r
由于使用了 append，函数 flatten 效率不高。现在使用与 reverse 相同的技巧，构造一个更高效的版本。也就是说，我们想定义一个更一般的函数 flatten'，把 flatten 和 ++ 的行为结合起来：
flatten' t ns = flatten t ++ ns
为了证明某个性质对所有树成立，类型 Tree 的归纳原理说明，只需证明该性质对所有形如 Leaf n 的树成立，并证明如果该性质对任意树 l 和 r 成立，那么它也对 Node l r 成立。使用这个原理，我们如下构造满足上述等式的 flatten' 定义。
基本情况：
flatten' (Leaf n) ns
= { specification of flatten' }
flatten (Leaf n) ++ ns
= { applying flatten }
[n] ++ ns
= { applying ++ }
n : ns
归纳情况：
flatten' (Node l r) ns
= { specification of flatten' }
(flatten l ++ flatten r) ++ ns
= { associativity of ++ }
flatten l ++ (flatten r ++ ns)
= { induction hypothesis for l }
flatten' l (flatten r ++ ns)
= { induction hypothesis for r }
flatten' l (flatten' r ns)
由此可知，下面的定义满足 flatten' 的规约：
flatten' :: Tree -> [Int] -> [Int]
flatten' (Leaf n) ns = n : ns
flatten' (Node l r) ns = flatten' l (flatten' r ns)
因此，原函数 flatten 现在可以重新定义如下：
flatten :: Tree -> [Int]
flatten t = flatten' t []
再一次，新的 flatten 定义或许不如原始版本清晰，但效率高得多。它使用额外参数来累积最终结果，而不是使用 append。
16.7 编译器正确性（Compiler correctness）
本章最后给出一个较长的例子。回忆第 8 章中，我们定义了一种简单算术表达式类型，它由整数和加法运算符构成，同时还定义了一个函数（这里称为 eval），可以把表达式直接求值为整数：
data Expr = Val Int | Add Expr Expr
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x + eval y
这种表达式也可以通过在栈上执行的代码间接求值。在这个语境中，栈只是一个整数列表，而代码由对栈执行的 push 和 add 操作组成：
type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD
deriving Show
这类代码的含义由一个函数给出：它使用一个初始栈执行一段代码，得到最终栈：
exec :: Code -> Stack -> Stack
exec [] s = s
exec (PUSH n : c) s = exec c (n : s)
exec (ADD : c) (m : n : s) = exec c (n+m : s)
也就是说，push 操作会把一个新整数放到栈顶，而 add 会把栈顶的两个整数替换为它们的和。借助这些操作，现在很容易定义一个把表达式编译成代码的函数。一个整数值会被编译为简单地推入该值，而一个加法会先编译两个参数表达式 x 和 y，然后把栈上得到的两个整数相加：
comp :: Expr -> Code
comp (Val n) = [PUSH n]
comp (Add x y) = comp x ++ comp y ++ [ADD]
注意，执行 add 操作时，表达式 y 的值会在栈顶，表达式 x 的值会在第二个位置，因此 exec 的定义中会交换这两个值。
为了展示上面三个函数的行为，如果考虑表示 (2+3)+4 的表达式，就有：
> let e = Add (Add (Val 2) (Val 3)) (Val 4)
> eval e
9
> comp e
[PUSH 2, PUSH 3, ADD, PUSH 4, ADD]
> exec (comp e) []
[9]
从这个例子推广开来，我们的表达式编译器的正确性可以用下面的等式表示：
exec (comp e) [] = [eval e]
也就是说，编译一个表达式，然后用空初始栈执行所得代码，与先求值该表达式、再把得到的整数转换为单元素栈，二者会得到相同的最终栈。不过，为了证明这个结果，我们会看到有必要把空初始栈推广为任意初始栈：
exec (comp e) s = eval e : s
使用类型 Expr 的归纳原理（它与上一节类型 Tree 的归纳原理相同，只是构造器名称不同），可以如下验证编译器正确性等式。
基本情况：
exec (comp (Val n)) s
= { applying comp }
exec [PUSH n] s
= { applying exec }
n : s
= { unapplying eval }
eval (Val n) : s
归纳情况：
exec (comp (Add x y)) s
= { applying comp }
exec (comp x ++ comp y ++ [ADD]) s
= { associativity of ++ }
exec (comp x ++ (comp y ++ [ADD])) s
= { distributivity - see below }
exec (comp y ++ [ADD]) (exec (comp x) s)
= { induction hypothesis for x }
exec (comp y ++ [ADD]) (eval x : s)
= { distributivity again }
exec [ADD] (exec (comp y) (eval x : s))
= { induction hypothesis for y }
exec [ADD] (eval y : eval x : s)
= { applying exec }
(eval x + eval y) : s
= { unapplying eval }
eval (Add x y) : s
注意，如果没有把结果推广到任意栈，第二次使用归纳假设就无法应用，因为此时栈已经变为非空。归纳情况中使用的分配性质说明，执行两段拼接在一起的代码，与依次执行这两段代码得到相同结果：
exec (c ++ d) s = exec d (exec c s)
这个性质可通过对代码 c 做归纳来证明，其中归纳情况根据代码中第一个操作是 push 还是 add 分成两个子情况。
基本情况：
exec ([] ++ d) s
= { applying ++ }
exec d s
= { unapplying exec }
exec d (exec [] s)
归纳情况：
exec ((PUSH n : c) ++ d) s
= { applying ++ }
exec (PUSH n : (c ++ d)) s
= { applying exec }
exec (c ++ d) (n : s)
= { induction hypothesis }
exec d (exec c (n : s))
= { unapplying exec }
exec d (exec (PUSH n : c) s)
归纳情况：
exec ((ADD : c) ++ d) s
= { applying ++ }
exec (ADD : (c ++ d)) s
= { assume s of the form m : n : s' }
exec (ADD : (c ++ d)) (m : n : s')
= { applying exec }
exec (c ++ d) (n+m : s')
= { induction hypothesis }
exec d (exec c (n+m : s'))
= { unapplying exec }
exec d (exec (ADD : c) (m : n : s'))
第二个归纳情况中，如果栈不具有所假定的形式，就对应栈下溢错误。实践中这永远不会发生，因为编译器的结构会确保每次执行 add 操作时，栈中总是至少包含两个整数。
不过，事实上，可以通过应用上一节的技术消除 append 的使用，从而完全避免分配性质及其随后的下溢问题。特别是，我们想定义一个广义函数 comp'，它具有下面的性质：
comp' e c = comp e ++ c
通过对 e 做归纳，可以构造出定义：
comp' :: Expr -> Code -> Code
comp' (Val n) c = PUSH n : c
comp' (Add x y) c = comp' x (comp' y (ADD : c))
由此可得，我们可以把 comp e 重新定义为 comp' e []。进而，相对于表达式语义而言，新版编译器的正确性现在可以陈述如下：
exec (comp' e c) s = exec c (eval e : s)
也就是说，编译一个表达式，然后把所得代码与任意额外代码一起执行，与先在原栈顶部放上表达式的值、再执行这段额外代码，结果相同。这个结果通过对表达式 e 做归纳来证明。
基本情况：
exec (comp' (Val n) c) s
= { applying comp' }
exec (PUSH n : c) s
= { applying exec }
exec c (n:s)
= { unapplying eval }
exec c (eval (Val n) : s)
归纳情况：
exec (comp' (Add x y) c) s
= { applying comp' }
exec (comp' x (comp' y (ADD : c))) s
= { induction hypothesis for x }
exec (comp' y (ADD : c)) (eval x : s)
= { induction hypothesis for y }
exec (ADD : c) (eval y : eval x : s)
= { applying exec }
exec c ((eval x + eval y) : s)
= { unapplying eval }
exec c (eval (Add x y) : s)
注意，当 s = [] 且 c = [] 时，这个新的编译器正确性结果会简化为 exec (comp e) [] = [eval e]，也就是我们最初的正确性陈述。除了避免正确性证明中的栈下溢问题之外，编译器的累积器版本还有两个额外好处。第一，它避免使用 ++，因此效率更高。第二，新证明长度不到先前两个证明合计长度的一半。正如形式化推理中常见的那样，以恰当方式推广结果可以大幅简化证明。数学是引导高效程序和简单证明开发的绝佳工具！
16.8 章注（Chapter remarks）
关于函数式程序的推理本身足以写成一本书，这里只是触及表面。进一步阅读的主题包括：关于部分结构和无限结构的推理 [33, 34]，程序性质的自动化测试 [35]，关于计算效果的推理 [36]，以及避免归纳的技术 [10]。编译器例子改编自文献 [37]，而“让 append 消失”这一说法受文献 [38] 启发。
16.9 练习（Exercises）
- 通过对
n做归纳，说明：
add n (Succ m) = Succ (add n m)
- 使用上面的性质以及
add n Zero = n，通过对n做归纳，说明加法满足交换律：
add n m = add m n
- 使用下面这个库函数定义，它判断列表中的所有元素是否都满足某个谓词：
all p [] = True
all p (x:xs) = p x && all p xs
补全 replicate 正确性的证明：通过对 n >= 0 归纳，说明它会产生包含相同元素的列表，也就是 all (== x) (replicate n x)。提示：说明该性质始终为 True。
- 使用下面的
++定义：
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
通过对 xs 做归纳，验证下面两个性质：
xs ++ [] = xs
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
提示：这些证明与 add 函数的证明类似。
- 使用上面的
++定义，以及：
take 0 _ = []
take _ [] = []
take n (x:xs) = x : take (n-1) xs
drop 0 xs = xs
drop _ [] = []
drop n (_:xs) = drop (n-1) xs
通过对整数 n >= 0 和列表 xs 同时归纳，说明：
take n xs ++ drop n xs = xs
提示：共有三种情况，分别对应 take 和 drop 定义中的三种参数模式。
- 给定类型声明：
data Tree = Leaf Int | Node Tree Tree
通过对树归纳，说明这种树中的叶子数量总是比节点数量多一。提示：先定义函数来计算一棵树中的叶子数和节点数。
-
验证
Maybe类型的函子定律。提示：证明通过情况分析进行，不需要使用归纳。 -
给定下面的类型和实例声明，通过对树归纳，验证
Tree类型的函子定律。
data Tree a = Leaf a | Node (Tree a) (Tree a)
instance Functor Tree where
-- fmap :: (a -> b) -> Tree a -> Tree b
fmap g (Leaf x) = Leaf (g x)
fmap g (Node l r) = Node (fmap g l) (fmap g r)
- 验证
Maybe类型的 applicative 定律。 - 验证列表类型的 monad 定律。提示：这些证明可以使用列表推导式的简单性质完成。
- 给定等式
comp' e c = comp e ++ c，说明如何通过对e做归纳来构造comp'的递归定义。
练习 1-5 的解答见附录 A。