Структурная индукция в Haskell

Question

Является ли следующее определение структурной индукции?

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

Может ли кто-нибудь дать мне пример структурной индукции в Haskell?

Answer 1

Вы не указали, но я буду считать :: означает список concatention и использование ++, так что оператор используется в 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 

Таким образом доказывает нашу гипотезу.