Доказательство по индукции с несколькими списками

Question

Я слежу за лекцией "Функциональное программирование в Scala" на Coursera, и в конце видео 5.7 Мартин Одерский просит индуктивно доказать правильность следующего уравнения:

(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

Это правильно?

Answer 1

Свойство включает в себя несколько списков, но ++ только рекурсы на свой левый аргумент. Это подсказка, которую вы можете доказать по индукции в этом левом аргументе. В общем, при доказательстве утверждения о какой-то рекурсивной функции первое, что вы пытаетесь сделать, - это индуцировать тот же аргумент, что и функция.

Я сделаю это для вас в качестве примера:

Требовать: (xs ++ ys) map f знак равно (xs map f) ++ (ys map f)

Доказательство: по индукции на xs,

• Базовый вариант: xs знак равно Nil

  • лс = (Nil ++ ys) map f знак равно ys map f

    (от ++определение)

  • rhs = (Nil map f) ++ (ys map f) знак равно Nil ++ ys map f знак равно ys map f

    (от mapх, тогда ++определения)

  • Следовательно, 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)

  • лс = (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,

Answer 2

Как говорится в комментарии @Phil, во-первых, это хорошее понимание того, что методы ++ а также :: делать в списках лучший способ документации

Как мы можем доказать свойства списка программ? Ответ по структурной индукции! Правило доказательства для доказательства свойства списка P (xs) посредством структурной индукции:

P (Nil) (базовый случай) для всех x,xs: P(xs) => P(x::xs) (шаг индукции)

для всех xs: P(xs) (следствие)

P (xs) на этапе индукции называется гипотезой индукции

поскольку единственной важной вещью является xs, ys исправляет правильный список с длиной l, после доказательства для xs вы можете проверить для ys или увидеть, что коммутативно

Итак, давайте применим индукцию и определения функций

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

Базовый случай подставляем xs по nil

(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

здесь вы можете найти больше примеров