flo*_*poe 4 haskell equality proof function-composition map-function
我经历了理查德·伯德的"哈斯克尔功能的思考"一书,并且存在在那里他证明了滤波方法的属性我无法理解的部分.他证明的是:
filter p . map f = map f . filter (p . f)
Run Code Online (Sandbox Code Playgroud)
在本书的前面,他将过滤器定义为:
filter p = concat . map (test p)
test p x = if p x then [x] else []
Run Code Online (Sandbox Code Playgroud)
这就是他证明第一个等式的方法:
filter p . map f
= {second definition of filter} -- He's referring to the definition I gave above
concat . map (test p) . map f
= {functor property of map}
concat . map (test p . f)
= {since test p . f = map f . test (p . f)}
concat . map (map f . test (p . f))
= {functor property of map}
concat . map (map f) . map (test (p . f))
= {naturality of concat}
map f . concat . map (test (p . f))
= {second definition of filter}
map f . filter (p . f)
Run Code Online (Sandbox Code Playgroud)
我无法理解的是如何test p . f
等于map f . test (p . f)
.
这是我试图测试它的方式:
test :: (a -> Bool) -> a -> [a]
test p x = if p x then [x] else []
test ((<15) . (3*)) 4 -- test p .f, returns [4]
(map (3*) . test((<15) . (3*))) 4 -- map f . test (p . f), returns [12]
Run Code Online (Sandbox Code Playgroud)
任何人都可以解释我在这里缺少的东西吗?
你测试过了
test (p . f) = map f . test (p . f)
Run Code Online (Sandbox Code Playgroud)
这确实是假的.该物业实际上是
test p . f = map f . test (p . f)
Run Code Online (Sandbox Code Playgroud)
LHS关联的地方
test p . f = (test p) . f
Run Code Online (Sandbox Code Playgroud)
请记住,函数应用程序比任何用户可定义的运算符都更紧密地绑定,就像它一样infixl 10
.彼此相邻的两个标识符始终是前缀函数应用程序的一部分.(在as-patterns的情况下除外:f xs@ys zs
表示f (xs@ys) zs
.)
证明财产:
test p . f
={definition of (.)}
\x -> test p (f x)
={definition of test}
\x -> if p (f x) then [f x] else []
={definition of map, multiple times}
\x -> if p (f x) then map f [x] else map f []
={float map f out of cases}
\x -> map f (if p (f x) then [x] else [])
={definition of (.)}
\x -> map f (if (p . f) x then [x] else [])
={definition of test}
\x -> map f (test (p . f) x)
={definition of (.)}
map f . test (p . f)
Run Code Online (Sandbox Code Playgroud)
调整你的例子test (<15) . (*3)
意味着"乘以3
,确保结果小于15
".map (*3) . test ((<15) . (*3))
表示"确保输入的三次小于15
,如果是,则返回三次输入."