编辑:没有回答问题(抱歉) foldl :: (b -> a -> b) -> b -> [a] -> b foldr :: (a -> b -> b) -> b -> [a] -> b个 (+)是可交换的,也就是说,如果改变参数顺序,则会产生相同的结果。例如,1+2与2+1相同。 请查看foldl和foldr的类型签名。 foldl接受函数(b->a->b),该函数的第二个参数是列表中的元素。 另一方面,foldr接受函数(a->b->b),该函数的第一个参数是列表中的元素。 对于foldl,左边有一个累积(第一个参数);对于foldr,右边有一个累积(第二个参数)。 foldl从左到右折叠,foldr从右到左折叠。 从技术上讲,它要比这复杂得多。
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)
∎
4条答案
按热度按时间zfciruhq1#
像往常一样,一个视觉表示胜过一千个单词:
(Source)(英文)
ny6fqffe2#
编辑:没有回答问题(抱歉)
foldl :: (b -> a -> b) -> b -> [a] -> b
foldr :: (a -> b -> b) -> b -> [a] -> b
个(+)
是可交换的,也就是说,如果改变参数顺序,则会产生相同的结果。例如,1+2
与2+1
相同。请查看
foldl
和foldr
的类型签名。foldl
接受函数(b->a->b)
,该函数的第二个参数是列表中的元素。另一方面,
foldr
接受函数(a->b->b)
,该函数的第一个参数是列表中的元素。对于
foldl
,左边有一个累积(第一个参数);对于foldr
,右边有一个累积(第二个参数)。foldl
从左到右折叠,foldr
从右到左折叠。从技术上讲,它要比这复杂得多。
m0rkklqb3#
这两个表达式都返回最右边参数中所有子列表的有序连接,因此它们在 * 功能 * 上是相同的,至少对于有限子列表是如此。
让我们使用Haskell
ghci
解释器进行检查:但这还不是全部。例如,任何一个听过排序算法讲座的程序员都知道,冒泡排序和快速排序在功能上是等价的。两种算法都返回输入数组的有序版本。
但是QuickSort是实用的,气泡排序除了对小的输入数组外是无用的。
这里有点类似。
让我们在
ghci
解释器中打开统计信息:因此,如果我们将输入子列表的数量增加一倍,内存分配量将增加4倍,而不是2倍。这里的算法是 * 二次 * 的,因此速度非常慢,就像冒泡排序一样。
不,将
foldl
替换为它的严格同级foldl'
将不会有帮助。()必须 * 复制 * 它的左操作数,因为在Haskell中不可能像在C/C中那样只改变它指向下一个节点的最后一个指针。但是,运算符(++)可以只使用一个指向其右操作数的简单指针,因为右操作数是 * 不可变 * 的,任何Haskell命名的值都是如此。总之,对于左操作数,不变性对我们不利;对于右操作数,它对我们有利。
在
foldl
的例子中,左边的操作数是 accumulator,所以我们必须重复我们的(大的和不断增长的)累加器,这就打破了foldl
和foldr
之间的 * 性能 * 对称性。我们可以很容易地检查到
foldr
的性能要好得多:因为这里的动态内存分配乘以2,而不是4。
erhoui1w4#
我不知道这对你有多大用处,但我想以此作为学习阿格达的借口,所以这里有一个正式的证明:
进口
定义
定理
我希望这是一种可读的,即使你只知道 haskell 。
这比我预期的要多,只知道
_++_
的结合性并不明显。哦,我相信把它推广到任何带有恒等元素的结合运算并不难,我将把它作为练习留给读者。
最后,我应该注意到,这只适用于有限列表。