Induzione strutturale in Haskell

Question

È la seguente definizione di induzione strutturale?

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

Qualcuno può darmi un esempio di induzione strutturale in Haskell?

Answer 1

Non è stato specificato, ma mi assumerà :: significa elenco concatenazione e uso ++, dal momento che è l'operatore usato in Haskell. Per provarlo, eseguiremo l'induzione su xs. In primo luogo, dimostriamo che l'affermazione vale per il caso base (cioè xs = [])

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

e

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 

Ora, supponiamo che l'ipotesi di induzione foldr f a (xs ++ ys) = foldr f (foldr f a ys) xs vale per xs e mostrare che si terrà per la lista x:xs pure.

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 

e

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 

Ora, con la nostra ipotesi di induzione, sappiamo che k1 e k2 sono uguali, quindi

x `f` k1 = x `f` k2 

Così dimostrando la nostra ipotesi.