Strukturelle Induktion in Haskell

Question

Ist die folgende Definition der strukturellen Induktion?

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

Kann mir jemand ein Beispiel für strukturelle Induktion in Haskell geben?

Answer 1

Sie haben es nicht geben, aber ich werde davon ausgehen, :: bedeutet Liste concatention und Verwendung ++, da, dass der Betreiber in Haskell verwendet wird. Um dies zu beweisen, führen wir Induktion auf xs. Zunächst zeigen wir, dass die Erklärung für den Basisfall hält (dh xs = [])

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

und

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 

Jetzt gehen wir davon aus, dass die Induktionsvoraussetzung foldr f a (xs ++ ys) = foldr f (foldr f a ys) xs für xs hält und zeigen, dass es halten wird für die Liste x:xs auch.

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 

und

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 

nun durch unsere Induktionsvoraussetzung wissen wir, dass k1 und k2 gleich sind, daher

x `f` k1 = x `f` k2 

So ist unsere Hypothese zu beweisen.