Haskell: Правда ли, что приложение-функция распределяет по конкатенации списка?

После прочтения этого вопроса: Functional proofs (Haskell)Haskell: Правда ли, что приложение-функция распределяет по конкатенации списка?

И после того, как глядя на индуктивного доказательства forall xs ys. length (xs ++ ys) = length xs + length ys из Haskell школы музыки (стр 164).

Мне показалось, что приложение-приложение распределяет по конкатенации списка.

Следовательно, более общим законом может быть то, что forall f xs ys. f (xs ++ ys) = f xs ++ f ys.

Но как бы доказать или опровергнуть такой предикат?

- EDIT -

Я сделал опечатку это должно было быть: forall f xs ys. f (xs ++ ys) = f xs + f ys, который соответствует тому, что использует предыдущий вопрос и Haskell SoM. При этом, из-за этой опечатки, это уже не свойство «дистрибутивности». Тем не менее, @leftaroundabout сделал правильный ответ для моего первоначального вопроса о типографии. И что касается моего предполагаемого вопроса, закон все еще не правильный, потому что функции не нуждаются в сохранении структурной ценности. f может дать совершенно другой ответ в зависимости от длины списка, к которому он применяется.

источник

2016-02-16 CMCDragonkai

"Но как бы один доказать/опровергнуть такой предикат?" По индукции, я полагаю. Если вы настоящий гений, вы, вероятно, можете сделать это путем осмотра, но для остальных из нас индукция - это путь, который выйдет уже несколько столетий. На самом деле это не так - то, что вам нужно, это более слабый оператор - 'foldr f x xs \' f \ 'foldr f x ys = foldr f x (xs ++ ys)'. – user2407038

Но это доказательство так же, как и доказательства для forall xs ys. длина (xs ++ ys) = длина xs + длина ys'? Как доказать индукцию для функций? Что означает 'n' и' n + 1' в терминах функций? – CMCDragonkai

Как вы дошли до этого более общего закона? Это не typecheck с конкретным (внезапно 'f' должен вернуть список), и даже с конкатенацией тривиально опровергается, заменяя' tail' для 'f':' tail ([1] ++ [2]) == [2] 'while' tail [1] ++ tail [2] == [] '. –

Нет, это явно не соответствует действительности в целом:

f [_] = [] 
f l = l

затем

f ([1] ++ [2]) = f [1,2] = [1,2]

но

f [1] ++ f [2] = [] ++ [] = []

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

источник

2016-02-16 11:27:28 leftaroundabout

Для записи такие функции называются [гомоморфизмами] (https://ncatlab.org/nlab/show/homomorphism) (гомоморфизмы магмы в этом случае). – gallais

И посмотрев на индуктивное доказательство forall xs ys. length (xs ++ ys) = length xs + length ys из Музыкальной школы Haskell (стр. 164).

Мне показалось, что приложение-приложение распределяет по конкатенации списка.

Хорошо, ясно, что это не так.Например:

reverse ([1..3] ++ [4..6]) /= reverse [1..3] ++ reverse [4..6]

Объект, который вы цитируете пример является частным случаем, который называется Моноид морфизм: функция f :: m -> n, что:

m и n являются моноиды с бинарной операцией <> и личность mempty;
f mempty = mempty
f (m <> m') == f m <> f m'

Так length :: [a] -> Int является Моноид морфизм, посылая [] в 0 и ++ к +:

length [] = 0 
length (xs ++ ys) = length xs + length ys

источник

2016-02-16 21:04:36

Haskell: Правда ли, что приложение-функция распределяет по конкатенации списка?

ответ

Смежные вопросы