Функциональные доказательства (Haskell)

Мне не удалось прочитать RWH; и не один, чтобы бросить курить, я заказал Haskell: Craft of Functional Programming. Теперь мне интересно об этих функциональных доказательствах на стр. 146. В частности, я пытаюсь доказать 8.5.1 sum (reverse xs) = sum xs. Я могу сделать некоторые доказательства индукции, но потом я застрял.

ССЫЛ:

sum ( reverse xs ) = sum xs

БАЗА:

sum ( reverse [] ) = sum []

Left  = sum ( [] ) (reverse.1)
      = 0          (sum.1)

Right = 0          (sum.1)

ИНДУКЦИЯ:

sum ( reverse (x:xs) ) = sum (x:xs) 

Left = sum ( reverse xs ++ [x] )    (reverse.2)

Right = sum (x:xs)   
      = x + sum xs                  (sum.2)

Итак, теперь я просто пытаюсь доказать, что Left sum ( reverse xs ++ [x] ) равно Right x + sum xs, но это не слишком далеко от того места, где я начал sum ( reverse (x:xs) ) = sum (x:xs).

Я не совсем уверен, почему это нужно доказать, кажется вполне разумным использовать символическое доказательство reverse x:y:z = z:y:x (через defn), а потому, что + является коммутативным (arth), то reverse 1+2+3 = 3+2+1,

Ответ 1

sum (reverse [])     = sum []                     -- def reverse
sum (reverse (x:xs)) = sum (reverse xs ++ [x])    -- def reverse
                     = sum (reverse xs) + sum [x] -- sum lemma below
                     = sum (reverse xs) + x       -- def sum
                     = x + sum (reverse xs)       -- commutativity assumption!
                     = x + sum xs                 -- inductive hypothesis
                     = sum (x:xs)                 -- definition of sum

Однако существуют основополагающие допущения ассоциативности и коммутативности, которые не являются строго обоснованными, и это не будет работать должным образом для ряда числовых типов, таких как Float и Double, где эти предположения нарушены.

Лемма: sum (xs ++ ys) == sum xs + sum ys, учитывая ассоциативность (+)

Доказательство:

sum ([] ++ ys)     = sum ys           -- def (++)
                   = 0 + sum ys       -- identity of addition
                   = sum [] ++ sum ys -- def sum

sum ((x:xs) ++ ys) = sum (x : (xs ++ ys))  -- def (++)
                   = x + sum (xs ++ ys)    -- def sum 
                   = x + (sum xs + sum ys) -- inductive hypothesis
                   = (x + sum xs) + sum ys -- associativity assumption!
                   = sum (x:xs) + sum ys   -- def sum

Ответ 2

В основном вам нужно показать, что

sum (reverse xs ++ [x]) = sum (reverse xs) + sum [x]

что затем легко приводит к

                        = x + sum (reverse xs)
                        = x + sum xs  -- by inductive hyp.

Проблема заключается в том, чтобы показать, что sum распределяет по конкатенации списка.

Ответ 3

Используйте определение суммы для разложения (суммирование обратного xs ++ [x]) в сумму x + (обратное (xs)) и используя вашу индуктивную гипотезу, вы знаете сумму (reverse (xs)) = sum ( хз). Но я согласен с тем, что индукция является излишней для такой проблемы.

Ответ 4

Здесь, где я думаю, ты застрял. Вам нужно доказать лемму, в которой говорится, что

sum (xs ++ ys) == sum xs + sum ys

Чтобы доказать этот закон, вам придется предположить, что сложение является ассоциативным, что справедливо только для целых чисел и рациональных чисел.

Тогда вам также нужно будет предположить, что добавление является коммутативным, что верно для целых чисел и рациональных чисел, но также и для float.

Отступление: стиль ваших доказательств выглядит очень странным для меня. Я думаю, вам будет легче писать такие доказательства, если вы используете стиль в книге Грэма Хаттона.