代码之家 › 专栏 › 技术社区 › CMCDragonkai

Haskell:函数应用程序在列表连接上分布是真的吗?

proof functional-programming haskell

1

CMCDragonkai · 技术社区 · 10 年前

读完这个问题后: Functional proofs (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 根据所应用列表的长度,可能会给出完全不同的答案。

2 回复 | 直到 9 年前

1

8

leftaroundabout 10 年前

不,这显然不是事实:

f [_] = []
f l = l

然后

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

但是

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

我确信确实存在这个问题的函数形成了一个有趣的类,但一般函数可以对列表结构做任何事情,从而阻止这种不变量。

2

3

Luis Casillas 10 年前

在看了 forall xs ys. length (xs ++ ys) = length xs + length ys 来自哈斯克尔音乐学院(第164页)。

在我看来,函数应用程序分布在列表连接上。

很明显,事实并非如此。例如:

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

你引用的例子是一个特殊情况,称为 幺半态射 :a函数 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