2.14 交互歸納

許多工作無法由一個函數獨立完成，而需要許多函數彼此呼叫。本章最後談談這類的交互歸納(mutual induction)定義。 下列函數定義中，even 判斷其輸入是否為偶數。第二個子句告訴我們：如果 n 是奇數， Suc n 便是偶數。但如何判斷一個數字是否為奇數？如果 n 是偶數，Suc n 便是奇數：

even :: Nat -> Bool
even Zero     = True
even (Suc n)  = odd n  

odd :: Nat -> Bool
odd Zero     = False
odd (Suc n)  = even n 

這類彼此呼叫的定義可以視為一整個大定義。 為讓讀者習慣，我們先把 even 與 odd 的定義改寫為 $\lambda$ 算式與 case:

even = \n ->  case n of
                Zero   -> True
                Suc n  -> odd n  

odd = \n ->  case n of
               Zero   -> False
               Suc n  -> even n 

上述的定義可以合併成一個：evenOdd 是一個序對，其中有兩個函數 Nat -> Bool，其中是 fst evenOdd 就是 even，snd evenOdd 就是 odd:

evenOdd :: ((Nat -> Bool) × (Nat -> Bool))
evenOdd = (  \n -> case n of{-"~~"-}  Zero   -> True
                                      Suc n  -> snd evenOdd n,
             \n -> case n of{-"~~"-}  Zero   -> False
                                      Suc n  -> fst evenOdd n) 

    all ((x:xs) ==) (zipWith (++) (inits (x:xs)) (tails (x:xs)))
<=> all ((x:xs) ==) (zipWith (++) ([]: map (x:) (inits xs)) ((x:xs):tails xs))
<=> all ((x:xs) ==) (([] ++ (x:xs)) : zipWith (++) (map (x:) (inits xs)) (tails xs))
<=> ((x:xs) == (x:xs)) ⋀
    all ((x:xs) ==) (zipWith (++) (map (x:) (inits xs)) (tails xs))