2

我正在关注 Coursera 上的 Scala 函数式编程讲座，在视频 5.7 的结尾，Martin Odersky 要求通过归纳证明以下等式的正确性：

(xs ++ ys) map f = (xs map f) ++ (ys map f)

当涉及多个列表时如何处理归纳证明？

我检查了 xs 为 Nil 和 ys 为 Nil 的基本情况。我已经通过归纳证明，当 xs 被 x::xs 替换时，等式成立，但是我们是否还需要检查 ys 被 y::ys 替换的等式？

在那种情况下（不会过多地破坏练习......无论如何都没有评分）你如何处理：(xs ++ (y::ys)) map f？

这是我在类似示例中使用的方法，以证明

(xs ++ ys).reverse = ys.reverse ++ xs.reverse

证明（省略基本情况和简单的 x::xs 情况）：

(xs ++ (y::ys)).reverse
= (xs ++ (List(y) ++ ys)).reverse         //y::ys = List(y) ++ ys
= ((xs ++ List(y)) ++ ys).reverse         //concat associativity
= ys.reverse ++ (xs ++ List(y)).reverse   //by induction hypothesis (proven with x::xs)
= ys.reverse ++ List(y).reverse ++ xs.reverse //by induction hypothesis
= ys.reverse ++ (y::Nil).reverse ++ xs.reverse //List(y) = y :: Nil
= ys.reverse ++ Nil.reverse ++ List(y) ++ xs.reverse //reverse definition
= (ys.reverse ++ List(y)) ++ xs.reverse //reverse on Nil (base case)
= (y :: ys).reverse ++ xs.reverse         //reverse definition

这是正确的吗 ？

4

2 回答 2

4

该属性涉及多个列表，但++仅在其左侧参数上递归。这是一个提示，你可以通过对左论证的归纳来证明。一般来说，当证明一个关于某个递归函数的命题时，你首先尝试的是对函数递归的同一个参数进行归纳。

我会为你做一个例子：

索赔：(xs ++ ys) map f=(xs map f) ++ (ys map f)

证明：由归纳论xs。

  • 基本情况：xs=Nil

    • lhs =(Nil ++ ys) map f=ys map f

      （根据++的定义）

    • rhs =(Nil map f) ++ (ys map f)=Nil ++ ys map f=ys map f

      （由map's, then ++'s 定义）

    • 因此lhs = rhs

  • 归纳案例：xs=z :: zs

    • 假设：(zs ++ ys) map f=(zs map f) ++ (ys map f)
    • 目标：((z :: zs) ++ ys) map f=((z :: zs) map f) ++ (ys map f)

    • lhs =(z :: (zs ++ ys)) map f=f(z) :: ((zs ++ ys) map f) (1)

      （根据map的定义）

    • rhs =((z :: zs) map f) ++ (ys map f)=(f(z) :: (zs map f)) ++ (ys map f)

      （根据map的定义）

    • 反过来，rhs = f(z) :: ((zs map f) ++ (ys map f)) (2)

      （根据++的定义）

    • 根据假设，（1）和（2），我们已经证明了目标。

因此，我们已经证明该声明是真实的xs，无论ys、 和f。

于 2015-05-24T02:31:29.813 回答
0

正如@Phil 的评论所说，首先是很好地了解列表中的方法++和::正在做什么，更好的方法是文档

我们如何证明列表程序的性质？答案是结构归纳法！通过结构归纳证明列表属性 P(xs) 的证明规则：

所有 x,xs 的 P(Nil) （基本情况）： P(xs) => P(x::xs) （归纳步骤）

对于所有 xs：P(xs)（结果）

归纳步骤中的 P(xs) 称为归纳假设

因为唯一重要的是 xs，ys 是用长度 l 修复适当的 List，在证明 xs 之后，您可以证明 ys，或者看到它是可交换的

所以让我们应用归纳和函数的定义

P(xs): (xs ++ ys) 映射 f = (xs 映射 f) ++ (ys 映射 f)

基本情况我们用 nil 代替 xs

(nil ++ ys) map f [definition of ++ ] 
ys map f  on the other hand 
(xs map f) ++ (ys map p) [apply map over NIL] 
(NIL) ++ (ys map p) [definition pf ++] 
ys map p

感应步骤

((x::xs) ++ ys) map f [definition ++]
(x:: (xs ++ ys)) map f [definition map]
f(x) :: ((xs ++ ys) map f) [induction hypothesis]
f(x) :: ((xs map f) ++ (ys map f)) [definition ++]
(f(x) :: (xs map f)) ++ (ys map f) [definition map]
(x::xs) map f ++ ys map f

qed

例如scala工作表中的另一个案例

import scala.util.Random

// P : length ( append(as,bs) )) = length ( as ) + length (bs)

def length[T](as: List[T]): Int = as match {
    case Nil => 0
    case _::xs => 1 + length(xs)
}

def append[T](as: List[T], bs: List[T]): List[T] = as match {
  case Nil => bs
  case x :: xs => x :: append(xs, bs)
}

// base case  we substitute Nil for as in P

val a:List[Int] = Nil
val n = 10
val b:List[Int] = Seq.fill(n)(Random.nextInt).toList

length((append(a,b)))

length(a)

length(b)

导入 scala.util.Random

length: length[T](val as: List[T]) => Int




append: append[T](val as: List[T],val bs: List[T]) => List[T]






a: List[Int] = List()
n: Int = 10
b: List[Int] = List(1168053950, 922397949, -1884264936, 869558369, -165728826, -1052466354, -1696038881, 246666877, 1673332480, -975585734)

res0: Int = 10

res1: Int = 0

res2: Int = 10

在这里您可以找到更多示例

于 2015-05-23T10:30:33.020 回答