Haskell中的结构归纳 [英] Structural induction in Haskell

问题描述

下面是结构归纳的定义吗？

  foldr fa（xs :: ys）= foldr f（foldr fa ys）xs 
  

有人可以给我一个Haskell结构归纳的例子吗？

解决方案

您没有指定它，但我会假设 :: 表示列表连接和
使用 ++ ，因为那是Haskell中使用的运算符。
为了证明这一点，我们将在 xs 上进行归纳。首先，我们证明
语句适用于基本情况（即 xs = [] ）

<$ （xs ++ ys）
{ - 通过定义xs - }
= foldr fa（[] ++ ys）
{ - >根据定义++ - }
= foldr fa ys

和

  foldr f（foldr fa ys）xs 
 { - 通过定义xs  - } 
 = foldr f（foldr fa ys ）[] 
 { - 根据foldr的定义 - } 
 = foldr fa ys 
  

<现在，我们假设归纳假设 foldr fa（xs ++ ys）= foldr
f（foldr fa ys）xs 对于 xs ，并显示它也可以支持列表
x：xs 。

  foldr fa（x：xs ++ ys）
 { - 根据定义++  - } 
 = foldr fa（x：（xs ++ ys））
 { - 通过定义foldr  - } 
 = x`f` foldr fa（xs ++ ys）
 ^ ----------- -------调用这个k1 
 = x`f` k1 
  

和

  foldr f（foldr fa ys）（x：xs）
 { - 根据foldr的定义 - } 
 = x`f` foldr f ys）xs 
 ^ ----------------------- call this k2 
 = x`f` k2 
  

现在，通过我们的归纳假设，我们知道 k1 和 k2 是相等的，因此

  x`f` k1 = x`f` k2 
  

证明我们的假设。

Is the following a definition of structural induction?

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

Can someone give me an example of structural induction in Haskell?

解决方案

You did not specify it, but I will assume :: means list concatention and use ++, since that is the operator used in Haskell. To prove this, we will perform induction on xs. First, we show that the statement holds for the base case (i.e. xs = [])

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

and

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

Now, we assume that the induction hypothesis foldr f a (xs ++ ys) = foldr f (foldr f a ys) xs holds for xs and show that it will hold for the list x:xs as well.

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

and

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

Now, by our induction hypothesis, we know that k1 and k2 are equal, therefore

x `f` k1 =  x `f` k2

Thus proving our hypothesis.

这篇关于Haskell中的结构归纳的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！