ハスケルでの構造誘導

Question

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

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

誰かが私にハスケルの構造誘導の例を教えてもらえますか？

Answer 1

あなたはそれを指定していませんでしたが、::はリスト連結を意味し、 は++を使用します。これは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 

今、私たちはxsために帰納法の仮定foldr f a (xs ++ ys) = foldr f (foldr f a ys) 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 

今、私たちの帰納法の仮定により、我々は したがって

x `f` k1 = x `f` k2 

このように我々の仮説を証明し、​​とk2が等しいことを知っています。