在像 Haskell 这样的纯函数语言中,是否有一种算法来获取函数的逆(编辑),当它是双射的?
在某些情况下,是的!有一篇漂亮的论文叫做Bidirectionalization for Free!,它讨论了几种情况 — — 当你的函数足够多态时 — — 在可能的情况下,完全自动地导出反函数。(它还讨论了当函数不是多态时,是什么让问题变得困难。)
你在你的函数是可逆的情况下得到的是逆(具有虚假输入);在其他情况下,你会得到一个试图“合并”旧输入值和新输出值的函数。
不,一般来说是不可能的。
证明:考虑类型的双射函数
type F = [Bit] -> [Bit]
具有
data Bit = B0 | B1
假设我们有一个反相器inv :: F -> F
,使得inv f . f ≡ id
。假设我们已经测试了它的功能f = id
,通过确认
inv f (repeat B0) -> (B0 : ls)
由于输出中的第一个B0
必须在有限时间之后出现,因此我们在inv
实际评估测试输入以获得此结果的深度以及它可以调用的次数上都有一个上限n
现在定义一个函数族
g j (B1 : B0 : ... (n+j times) ... B0 : ls)
= B0 : ... (n+j times) ... B0 : B1 : ls
g j (B0 : ... (n+j times) ... B0 : B1 : ls)
= B1 : B0 : ... (n+j times) ... B0 : ls
g j l = l
显然,对于所有0<j≤n
,g j
都是双射,实际上是自逆的。所以我们应该能够确认
inv (g j) (replicate (n+j) B0 ++ B1 : repeat B0) -> (B1 : ls)
但要实现这一点,inv (g j)
需要
评估g j (B1 : repeat B0)
到n+j > n
的深度
评估head $ g j l
至少n
与replicate (n+j) B0 ++ B1 : ls
匹配的不同列表
到那时为止,g j
中至少有一个与f
没有区别,并且由于inv f
没有进行这些评估中的任何一个,因此inv
不可能将其分开-缺少自己进行一些运行时测量,这只能在IO Monad
中进行。
.
不是在大多数函数式语言中,而是在逻辑编程或关系编程中,您定义的大多数函数实际上不是函数,而是“关系”,这些函数可以在两个方向上使用。
本站系公益性非盈利分享网址,本文来自用户投稿,不代表码文网立场,如若转载,请注明出处
评论列表(51条)