Haskell 中的结构归纳

Question

以下是结构归纳的定义吗？

foldr f a (xs::ys) = foldr f (foldr f a ys) xs

谁能给我一个 Haskell 结构归纳的例子？

Answer 1

您没有指定它，但我假设:: 表示列表连接和 使用 ++，因为那是 Haskell 中使用的运算符。 为了证明这一点，我们将对xs 进行归纳。首先，我们证明了 声明适用于基本情况（即xs = []）

foldr f a (xs ++ ys) 
{- By definition of xs -}
= foldr f a ([] ++ ys)
{- By definition of ++ -}
= foldr f a ys

和

foldr f (foldr f a ys) xs
{- By definition of xs -}
= foldr f (foldr f a ys) []
{- By definition of foldr -}
= foldr f a ys

现在，我们假设归纳假设 foldr f a (xs ++ ys) = foldr f (foldr f a ys) xs 适用于 xs 并表明它将适用于列表 x:xs 也是。

foldr f a (x:xs ++ ys)
{- By definition of ++ -}
= foldr f a (x:(xs ++ ys))
{- By definition of foldr -}
= x `f` foldr f a (xs ++ ys)
         ^------------------ call this k1
= x `f` k1

和

foldr f (foldr f a ys) (x:xs)
{- By definition of foldr -}
= x `f` foldr f (foldr f a ys) xs
         ^----------------------- call this k2
= x `f` k2

现在，根据我们的归纳假设，我们知道k1 和k2 是相等的， 因此

x `f` k1 =  x `f` k2

从而证明我们的假设。