haskell - Haskell での構造帰納法

Question

以下は構造誘導の定義ですか？

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

Haskell での構造誘導の例を教えてもらえますか?

Answer 1

あなたはそれを指定しませんでしたが、Haskellで使用される演算子であるため、 ::list concattention と use を意味すると仮定します。++これを証明するために、 について帰納法を実行し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

したがって、私たちの仮説を証明します。