1

我正在尝试使用结构归纳来证明以下语句中的“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

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

4

1 回答 1

3

我们想证明所有ns和m, foldl (+) m ns = m + sum ns。我们将在 上进行归纳ns。换句话说，我们证明该属性对于空列表成立，并且n:ns只要它成立就成立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。假设该属性适用ns于任何m（这是归纳假设）。我们的目标是证明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或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)         ∎
于 2015-01-20T20:27:22.937 回答