Haskell'de Yapısal İndüksiyon

Question

Aşağıdaki yapısal indüksiyon tanımı mıdır?

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

Birisi bana Haskell'de yapısal indüksiyonun bir örneğini verebilir mi? Bu Haskell kullanılan operatörüdür beri

Answer 1

Bunu belirtmek yoktu, ama ben :: üstlenecek, liste concatention ve kullanımını ++ anlamına gelir. Bunu kanıtlamak için, xs'da indüksiyon gerçekleştireceğiz. İlk olarak, deyimi baz durumda (yani xs = [])

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

ve Şimdi

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 

, biz indüksiyon hipotezi foldr f a (xs ++ ys) = foldr f (foldr f a ys) xsxs için de geçerlidir varsayalım ve geçerli olduğunu göstermeye yönelik sahip olduğunu göstermektedir ayrıca x:xs listesi için.

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 

ve

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 

Şimdi, indüksiyon hipotezi tarafından, bu nedenle

x `f` k1 = x `f` k2 

Böylece hipotezimizi kanıtlayan k1 ve k2 eşit olduğunu biliyoruz.