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 

現在，我們歸納假設，我們知道​​和k2是相等的，因此

x `f` k1 = x `f` k2 

從而證明了我們的假設。