在像 Haskell 这样的纯函数式语言中,当它是双射的时,是否有一种算法来获得函数的逆(编辑)?有没有一种特定的方法来编程你的功能呢?
10 回答
在某些情况下,是的!有一篇漂亮的论文叫做免费双向化!它讨论了一些情况——当你的函数足够多态时——在可能的情况下,完全自动地推导出一个反函数。(它还讨论了当函数不是多态时是什么使问题变得困难。)
如果你的函数是可逆的,你得到的是逆函数(带有虚假输入);在其他情况下,您会得到一个尝试“合并”旧输入值和新输出值的函数。
不,一般来说是不可能的。
证明:考虑类型的双射函数
type F = [Bit] -> [Bit]
和
data Bit = B0 | B1
假设我们有一个inv :: F -> F
这样的逆变器inv f . f ≡ id
。假设我们已经测试了它的功能f = id
,通过确认
inv f (repeat B0) -> (B0 : ls)
由于B0
输出中的第一个必须在某个有限时间之后出现,因此我们对实际评估我们的测试输入以获得此结果n
的深度inv
以及它可以调用的次数都有一个上限f
。现在定义一个函数族
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
.
⬜</p>
你可以在 wikipedia 上查找它,它被称为Reversible Computing。
通常,您不能这样做,并且没有任何功能语言具有该选项。例如:
f :: a -> Int
f _ = 1
该函数没有逆函数。
不是在大多数函数式语言中,而是在逻辑编程或关系编程中,您定义的大多数函数实际上不是函数而是“关系”,并且可以双向使用。参见例如 prolog 或 kanren。
像这样的任务几乎总是无法确定的。您可以为某些特定功能提供解决方案,但不是一般的。
在这里,您甚至无法识别哪些函数具有逆函数。引用Barendregt,HP Lambda 演算:它的语法和语义。北荷兰,阿姆斯特丹(1984):
如果一组 lambda 项既不是空集也不是满集,则它是非平凡的。如果 A 和 B 是在 (beta) 等式下封闭的两个非平凡的、不相交的 lambda 项集,则 A 和 B 是递归不可分的。
让我们将 A 视为表示可逆函数的 lambda 项的集合,而 B 是其余的。两者都是非空的,并且在 beta 相等下是封闭的。所以不可能决定一个函数是否可逆。
(这适用于无类型的 lambda 演算。TBH 当我们知道要反转的函数的类型时,我不知道参数是否可以直接适应有类型的 lambda 演算。但我很确定它会是相似的。)
如果您可以枚举函数的域并可以比较范围内的元素是否相等,那么您可以 - 以一种相当直接的方式。枚举我的意思是拥有所有可用元素的列表。我会坚持使用 Haskell,因为我不知道 Ocaml(甚至不知道如何正确地大写它;-)
你想要做的是遍历域的元素,看看它们是否等于你试图反转的范围的元素,然后取第一个有效的元素:
inv :: Eq b => [a] -> (a -> b) -> (b -> a)
inv domain f b = head [ a | a <- domain, f a == b ]
既然你已经说过这f
是一个双射,那么肯定只有一个这样的元素。当然,诀窍是确保您的域枚举实际上在有限时间内到达所有元素。如果您试图将双射从 to 反转Integer
,则Integer
using[0,1 ..] ++ [-1,-2 ..]
将不起作用,因为您永远不会得到负数。具体来说,inv ([0,1 ..] ++ [-1,-2 ..]) (+1) (-3)
永远不会产生价值。
但是,0 : concatMap (\x -> [x,-x]) [1..]
将起作用,因为它按以下顺序遍历整数[0,1,-1,2,-2,3,-3, and so on]
。确实inv (0 : concatMap (\x -> [x,-x]) [1..]) (+1) (-3)
及时退货-4
!
Control.Monad.Omega包可以帮助您以一种很好的方式遍历元组列表等;我敢肯定还有更多这样的包——但我不知道。
当然,这种方法是相当低俗和蛮力的,更不用说丑陋和低效了!因此,我将以对您问题的最后一部分的一些评论结束,即如何“编写”双射。Haskell 的类型系统不能证明一个函数是双射的——你真的想要像 Agda 这样的东西——但它愿意相信你。
(警告:未经测试的代码如下)
那么你可以在类型和Bijection
之间定义 s的数据类型吗:a
b
data Bi a b = Bi {
apply :: a -> b,
invert :: b -> a
}
以及任意数量的常量(您可以说“我知道它们是双射!”),例如:
notBi :: Bi Bool Bool
notBi = Bi not not
add1Bi :: Bi Integer Integer
add1Bi = Bi (+1) (subtract 1)
和几个智能组合器,例如:
idBi :: Bi a a
idBi = Bi id id
invertBi :: Bi a b -> Bi b a
invertBi (Bi a i) = (Bi i a)
composeBi :: Bi a b -> Bi b c -> Bi a c
composeBi (Bi a1 i1) (Bi a2 i2) = Bi (a2 . a1) (i1 . i2)
mapBi :: Bi a b -> Bi [a] [b]
mapBi (Bi a i) = Bi (map a) (map i)
bruteForceBi :: Eq b => [a] -> (a -> b) -> Bi a b
bruteForceBi domain f = Bi f (inv domain f)
我认为您可以这样做invert (mapBi add1Bi) [1,5,6]
并获得[0,4,5]
. 如果您以明智的方式选择组合器,我认为您必须Bi
手动编写常量的次数可能非常有限。
毕竟,如果你知道一个函数是一个双射,你会希望在你的脑海里有一个事实的证明草图,Curry-Howard 同构应该能够变成一个程序:-)
我最近一直在处理这样的问题,不,我会说(a)在很多情况下并不难,但是(b)它根本没有效率。
基本上,假设您有f :: a -> b
,这f
确实是一个问题。f' :: b -> a
您可以以非常愚蠢的方式计算逆:
import Data.List
-- | Class for types whose values are recursively enumerable.
class Enumerable a where
-- | Produce the list of all values of type @a@.
enumerate :: [a]
-- | Note, this is only guaranteed to terminate if @f@ is a bijection!
invert :: (Enumerable a, Eq b) => (a -> b) -> b -> Maybe a
invert f b = find (\a -> f a == b) enumerate
如果f
是一个双射并enumerate
真正产生 的所有值a
,那么您最终会遇到a
这样的f a == b
。
可以轻松制作具有 aBounded
和实例的类型。也可以制作成对的类型:Enum
RecursivelyEnumerable
Enumerable
Enumerable
instance (Enumerable a, Enumerable b) => Enumerable (a, b) where
enumerate = crossWith (,) enumerate enumerate
crossWith :: (a -> b -> c) -> [a] -> [b] -> [c]
crossWith f _ [] = []
crossWith f [] _ = []
crossWith f (x0:xs) (y0:ys) =
f x0 y0 : interleave (map (f x0) ys)
(interleave (map (flip f y0) xs)
(crossWith f xs ys))
interleave :: [a] -> [a] -> [a]
interleave xs [] = xs
interleave [] ys = []
interleave (x:xs) ys = x : interleave ys xs
类型的析取也是如此Enumerable
:
instance (Enumerable a, Enumerable b) => Enumerable (Either a b) where
enumerate = enumerateEither enumerate enumerate
enumerateEither :: [a] -> [b] -> [Either a b]
enumerateEither [] ys = map Right ys
enumerateEither xs [] = map Left xs
enumerateEither (x:xs) (y:ys) = Left x : Right y : enumerateEither xs ys
我们可以为任何代数数据类型执行此操作,(,)
并且Either
可能意味着我们可以为任何代数数据类型执行此操作。
不是每个函数都有逆函数。如果您将讨论限制在一对一的函数上,那么反转任意函数的能力就可以破解任何密码系统。我们不得不希望这是不可行的,即使在理论上!
在某些情况下,可以通过将双射函数转换为符号表示来找到它的逆函数。基于这个例子,我编写了这个 Haskell 程序来查找一些简单多项式函数的逆:
bijective_function x = x*2+1
main = do
print $ bijective_function 3
print $ inverse_function bijective_function (bijective_function 3)
data Expr = X | Const Double |
Plus Expr Expr | Subtract Expr Expr | Mult Expr Expr | Div Expr Expr |
Negate Expr | Inverse Expr |
Exp Expr | Log Expr | Sin Expr | Atanh Expr | Sinh Expr | Acosh Expr | Cosh Expr | Tan Expr | Cos Expr |Asinh Expr|Atan Expr|Acos Expr|Asin Expr|Abs Expr|Signum Expr|Integer
deriving (Show, Eq)
instance Num Expr where
(+) = Plus
(-) = Subtract
(*) = Mult
abs = Abs
signum = Signum
negate = Negate
fromInteger a = Const $ fromIntegral a
instance Fractional Expr where
recip = Inverse
fromRational a = Const $ realToFrac a
(/) = Div
instance Floating Expr where
pi = Const pi
exp = Exp
log = Log
sin = Sin
atanh = Atanh
sinh = Sinh
cosh = Cosh
acosh = Acosh
cos = Cos
tan = Tan
asin = Asin
acos = Acos
atan = Atan
asinh = Asinh
fromFunction f = f X
toFunction :: Expr -> (Double -> Double)
toFunction X = \x -> x
toFunction (Negate a) = \a -> (negate a)
toFunction (Const a) = const a
toFunction (Plus a b) = \x -> (toFunction a x) + (toFunction b x)
toFunction (Subtract a b) = \x -> (toFunction a x) - (toFunction b x)
toFunction (Mult a b) = \x -> (toFunction a x) * (toFunction b x)
toFunction (Div a b) = \x -> (toFunction a x) / (toFunction b x)
with_function func x = toFunction $ func $ fromFunction x
simplify X = X
simplify (Div (Const a) (Const b)) = Const (a/b)
simplify (Mult (Const a) (Const b)) | a == 0 || b == 0 = 0 | otherwise = Const (a*b)
simplify (Negate (Negate a)) = simplify a
simplify (Subtract a b) = simplify ( Plus (simplify a) (Negate (simplify b)) )
simplify (Div a b) | a == b = Const 1.0 | otherwise = simplify (Div (simplify a) (simplify b))
simplify (Mult a b) = simplify (Mult (simplify a) (simplify b))
simplify (Const a) = Const a
simplify (Plus (Const a) (Const b)) = Const (a+b)
simplify (Plus a (Const b)) = simplify (Plus (Const b) (simplify a))
simplify (Plus (Mult (Const a) X) (Mult (Const b) X)) = (simplify (Mult (Const (a+b)) X))
simplify (Plus (Const a) b) = simplify (Plus (simplify b) (Const a))
simplify (Plus X a) = simplify (Plus (Mult 1 X) (simplify a))
simplify (Plus a X) = simplify (Plus (Mult 1 X) (simplify a))
simplify (Plus a b) = (simplify (Plus (simplify a) (simplify b)))
simplify a = a
inverse X = X
inverse (Const a) = simplify (Const a)
inverse (Mult (Const a) (Const b)) = Const (a * b)
inverse (Mult (Const a) X) = (Div X (Const a))
inverse (Plus X (Const a)) = (Subtract X (Const a))
inverse (Negate x) = Negate (inverse x)
inverse a = inverse (simplify a)
inverse_function x = with_function inverse x
这个例子只适用于算术表达式,但它可能也可以推广到使用列表。Haskell中还有几种计算机代数系统的实现,可用于找到双射函数的逆。
不,并非所有函数都具有逆函数。例如,这个函数的逆函数是什么?
f x = 1