haskell - Haskell 中的结构归纳

Question

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

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

有人可以给我一个 Haskell 结构归纳的例子吗？

Answer 1

您没有指定它，但我假设::是指 list concanation 和 use ++，因为那是 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

从而证明了我们的假设。