haskell 合并运算子的foldl与foldr

0vvn1miw  于 2022-11-14  发布在  其他
关注(0)|答案(4)|浏览(148)

以下语句是否等效?

foldr (++) [ ] = foldl (++) [ ]

我知道foldr (+) 0 = fold (+) 0是等价的,而对于运算符(-)则不是,但对于(++)运算符呢?我认为结果是一个内容相同但顺序不同的列表。列表的顺序相关吗?

zfciruhq

zfciruhq1#

像往常一样,一个视觉表示胜过一千个单词:

Source)(英文)

ny6fqffe

ny6fqffe2#

编辑:没有回答问题(抱歉)
foldl :: (b -> a -> b) -> b -> [a] -> b
foldr :: (a -> b -> b) -> b -> [a] -> b
(+)是可交换的,也就是说,如果改变参数顺序,则会产生相同的结果。例如,1+22+1相同。
请查看foldlfoldr的类型签名。
foldl接受函数(b->a->b),该函数的第二个参数是列表中的元素。
另一方面,foldr接受函数(a->b->b),该函数的第一个参数是列表中的元素。
对于foldl,左边有一个累积(第一个参数);对于foldr,右边有一个累积(第二个参数)。
foldl从左到右折叠,foldr从右到左折叠。
从技术上讲,它要比这复杂得多。

m0rkklqb

m0rkklqb3#

这两个表达式都返回最右边参数中所有子列表的有序连接,因此它们在 * 功能 * 上是相同的,至少对于有限子列表是如此。
让我们使用Haskell ghci解释器进行检查:

$ ghci
GHCi, version 8.10.5: https://www.haskell.org/ghc/  :? for help
 ...
 λ> 
 λ> xss = [[1,2], [3,4,5], [6,7,8,9]]
 λ>
 λ> foldr (++) [] xss == foldl (++) [] xss
 True
 λ> 
 λ> foldr (++) [] [[1,2], [3,4,5], [6,7,8,9]]
 [1,2,3,4,5,6,7,8,9]
 λ> 
 λ> foldl (++) [] [[1,2], [3,4,5], [6,7,8,9]]
 [1,2,3,4,5,6,7,8,9]
 λ>

但这还不是全部。例如,任何一个听过排序算法讲座的程序员都知道,冒泡排序和快速排序在功能上是等价的。两种算法都返回输入数组的有序版本。
但是QuickSort是实用的,气泡排序除了对小的输入数组外是无用的。
这里有点类似。
让我们在ghci解释器中打开统计信息:

λ> 
 λ> :set +s
 λ> 
 λ> length $ foldl (++) [] (replicate 5000 [1,2,3,4])
 20000
 (3.31 secs, 4,124,759,752 bytes)
 λ> 
 λ> length $ foldl (++) [] (replicate 10000 [1,2,3,4])
 40000
 (16.94 secs, 17,172,001,352 bytes)
 λ>

因此,如果我们将输入子列表的数量增加一倍,内存分配量将增加4倍,而不是2倍。这里的算法是 * 二次 * 的,因此速度非常慢,就像冒泡排序一样。
不,将foldl替换为它的严格同级foldl'将不会有帮助。()必须 * 复制 * 它的左操作数,因为在Haskell中不可能像在C/C中那样只改变它指向下一个节点的最后一个指针。但是,运算符(++)可以只使用一个指向其右操作数的简单指针,因为右操作数是 * 不可变 * 的,任何Haskell命名的值都是如此。
总之,对于左操作数,不变性对我们不利;对于右操作数,它对我们有利。
foldl的例子中,左边的操作数是 accumulator,所以我们必须重复我们的(大的和不断增长的)累加器,这就打破了foldlfoldr之间的 * 性能 * 对称性。
我们可以很容易地检查到foldr的性能要好得多:

λ> 
 λ> length $ foldr (++) [] (replicate 5000 [1,2,3,4])
 20000
 (0.02 secs, 1,622,304 bytes)
 λ> 
 λ> length $ foldr (++) [] (replicate 10000 [1,2,3,4])
 40000
 (0.02 secs, 3,182,304 bytes)
 λ>

因为这里的动态内存分配乘以2,而不是4。

erhoui1w

erhoui1w4#

我不知道这对你有多大用处,但我想以此作为学习阿格达的借口,所以这里有一个正式的证明:
进口

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

定义

data List (A : Set) : Set where
  [] : List A
  _::_ : (x : A) (xs : List A) -> List A

variable 
  A : Set
  B : Set

foldr : (A -> B -> B) -> B -> List A -> B
foldr k z [] = z
foldr k z (x :: xs) = k x (foldr k z xs)

foldl : (B -> A -> B) -> B -> List A -> B
foldl k z [] = z
foldl k z (x :: xs) = foldl k (k z x) xs

_++_ : List A -> List A -> List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

定理

++-assoc : ∀ (xs ys zs : List A)
        -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
++-assoc [] ys zs = refl
++-assoc (x :: xs) ys zs = cong (x ::_) (++-assoc xs ys zs)

++-[] : ∀ (xs : List A)
     -> xs ++ [] ≡ xs
++-[] [] = refl
++-[] (x :: xs) = cong (x ::_) (++-[] xs)

helper : ∀ (x : List A) (ys : List (List A))
      -> x ++ foldl _++_ [] ys ≡ foldl _++_ x ys
helper x [] = ++-[] x
helper x (y :: ys) =
  begin
    x ++ foldl _++_ [] (y :: ys)
  ≡⟨⟩
    x ++ foldl _++_ y ys
  ≡⟨ cong (x ++_) (sym (helper y ys)) ⟩
    x ++ (y ++ foldl _++_ [] ys)
  ≡⟨ ++-assoc x y (foldl _++_ [] ys) ⟩
    (x ++ y) ++ foldl _++_ [] ys
  ≡⟨ helper (x ++ y) ys ⟩
    foldl _++_ (x ++ y) ys
  ≡⟨⟩
    foldl _++_ x (y :: ys)
  ∎

proof : ∀ (xs : List (List A))
     -> foldr _++_ [] xs ≡ foldl _++_ [] xs
proof [] = refl
proof (x :: xs) =
  begin
    foldr _++_ [] (x :: xs)
  ≡⟨⟩
    x ++ foldr _++_ [] xs
  ≡⟨ cong (x ++_) (proof xs) ⟩
    x ++ foldl _++_ [] xs
  ≡⟨ helper x xs ⟩
    foldl _++_ x xs
  ≡⟨⟩
    foldl _++_ [] (x :: xs)
  ∎

我希望这是一种可读的,即使你只知道 haskell 。
这比我预期的要多,只知道_++_的结合性并不明显。
哦,我相信把它推广到任何带有恒等元素的结合运算并不难,我将把它作为练习留给读者。
最后,我应该注意到,这只适用于有限列表。

相关问题