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

从而证明了我们的假设.