Haskell：函数应用程序是否分布在列表级联上？

看完这个问题之后：Functional proofs (Haskell)Haskell：函数应用程序是否分布在列表级联上？

在看过Haskell音乐学院的forall xs ys. length (xs ++ ys) = length xs + length ys的归纳证明后（第164页）。

这在我看来，功能应用分布在连接列表。

因此，更一般的规律可能是forall f xs ys. f (xs ++ ys) = f xs ++ f ys。

但是，如何将一个证明/反驳这样的断言？

- 编辑 -

我做了一个错字，它的意思是：forall f xs ys. f (xs ++ ys) = f xs + f ys，它匹配什么前面的问题和Haskell的SOM系统使用。这就是说，由于这个错字，它不再是“分配”属性。但是，@leftaroundabout为我最初的打字问题做出了正确的答案。至于我的预期问题，法律仍然不正确，因为职能不需要保留结构性价值。根据所应用列表的长度，f可能会给出完全不同的答案。

来源

2016-02-16 CMCDragonkai

“但是，如何将一个证明/反驳这样的断言？”通过归纳，我假设。如果你是一个真正的天才，你可以通过检查来做到这一点，但对于我们其他人来说，归纳一直是几个世纪以来的方式。它实际上并不是真的 - 你可能想要的是较弱的陈述 - “foldr f x xs \'''foldr f x ys = foldr f x（xs ++ ys）'。 – user2407038

但是这个证明和'forall xs ys'的证明是一样的。长度（xs ++ ys）=长度xs +长度ys'？如何通过归纳来证明函数？从功能的角度来说，“n”和“n + 1”是什么？ – CMCDragonkai

你甚至是如何到达这个更一般的法律？它没有使用特定的类型（突然'f'需要返回一个列表），甚至连接级联通过将'tail'替换为'f'：tail（[1] ++ [2]）而被证明是不成立的== [2]'而'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

并且从Haskell音乐学院（第164页）看到forall xs ys. length (xs ++ ys) = length xs + length ys的归纳证明。

这在我看来，功能应用分布在连接列表。

好吧，很显然事实并非如此。例如：

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：函数应用程序是否分布在列表级联上？

回答

相关问题