Haskell中的结构归纳和归纳假设

Question

我试图用结构归纳法用下面的陈述来证明'ns'。所有列表 'ns' 的类型都是 [Int] 并且所有 'm'类型为 Int.

foldl (+) m ns = m + (sum ns)

定义：

sum :: [Int] -> Int         -- summation of an Int list
sum []     = 0              -- s.1
sum (x:xs) = x + (sum xs)   -- s.2

foldl :: (a -> b -> a) -> a -> [b] -> a    -- fold left
foldl _ s []     = s                       -- fl.1
foldl f s (x:xs) = foldl f (f s x) xs      -- fl.2

如果有人能帮我解决这个问题，我将不胜感激。

Answer 1

我们想证明对于所有 ns 和 m，foldl (+) m ns = m + sum ns。我们将在 ns 上进行归纳。换句话说，我们证明属性对空列表成立，并且只要它对 ns 成立就对 n:ns 成立。

首先，让我们看一下空列表，让m为任意数字。我们的目标是证明 foldl (+) m [] = m + sum []。有很多方法可以做到这一点，但我们将通过等式推理将等式左侧转换为右侧。

foldl (+) m []  -- by definition of foldl
m               -- by right identity of addition
m + 0           -- by the definition of sum
m + sum []      -- QED

现在是 (:) 案例。让我们的列表为 n:ns。假设属性对于任何 m 都适用于 ns（这是归纳假设）。我们的目标是证明 foldl (+) m (n:ns) = m + sum (n:ns)。同样，我们使用等式推理。

foldl (+) m (n:ns)    -- by the definition of foldl
foldl (+) (m + n) ns  -- by the induction hypothesis, applied to (m + n)
(m + n) + sum ns      -- by associativity of addition
m + (n + sum ns)      -- by the definition of sum
m + sum (n:ns)        -- QED

我们完成了。

校对新生的一个普遍问题是，他们不确定自己所做的事情是否真的有意义，这让他们感到紧张。我建议看看 Agda or Coq 等证明助手。它们非常适合培养校对写作技巧。作为 Agda 的一个小例子，上面的证明可以在那里写得非常相似，只是有一些语法差异：

-- imports omitted

prop : forall m ns → foldl (_+_) m ns ≡ m + sum ns

prop m [] = begin
  foldl (_+_) m []     ≡⟨⟩ 
  m                    ≡⟨ sym $ +-right-identity m ⟩
  m + 0                ≡⟨⟩
  m + sum []           ∎

prop m (x ∷ ns) = begin 
  foldl _+_ m (x ∷ ns)     ≡⟨⟩
  foldl _+_ (m + x) ns     ≡⟨ prop (m + x) ns ⟩  
  (m + x) + sum ns         ≡⟨ +-assoc m x (sum ns) ⟩ 
  m + (x + sum ns)         ≡⟨⟩
  m + sum (x ∷ ns)         ∎

Haskell中的结构归纳和归纳假设

Structural Induction and Induction Hypothesis in Haskell

haskell

induction