在像Haskell这样的纯函数语言中，当函数是双射函数时，是否有一种算法可以获得函数的逆(编辑)？有没有一种特定的方法来编程你的函数？
在某些情况下，是的！有一篇美丽的论文叫《双向免费》！它讨论了一些情况——当你的函数足够多态时——在那里可以完全自动地导出反函数。(它还讨论了当函数不是多态的时，是什么使问题变得困难。)
在函数是可逆的情况下，你得到的是反函数(带有虚假输入)；在其他情况下，您会得到一个试图"合并"旧输入值和新输出值的函数。
不，一般情况下是不可能的。
证明：考虑类型的双射函数
type F = [Bit] -> [Bit]
带有
data Bit = B0 | B1
假设我们具有反相器CCD_ 1，使得CCD_。假设我们已经对其功能f = id进行了测试，确认
inv f (repeat B0) -> (B0 : ls)
由于输出中的第一个B0一定是在某个有限的时间之后出现的，因此我们对inv实际评估测试输入以获得该结果的深度以及它调用f的次数都有一个上限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 :: F -> F0需要
- 评估
g j (B1 : repeat B0)到n+j > n的深度 - 针对与
replicate (n+j) B0 ++ B1 : ls匹配的至少n个不同列表评估head $ g j l
到目前为止，至少有一个g j与f无法区分，并且由于inv f没有进行这两项评估，inv不可能将其区分开来——除了自己进行一些运行时测量之外，这只有在inv f . f ≡ id0中才有可能。
⬜
您可以在维基百科上查找它，它被称为可逆计算。
一般来说，你不能这样做，而且没有一种函数式语言有这个选项。例如：
f :: a -> Int
f _ = 1
此函数没有反函数。
不是在大多数函数式语言中，而是在逻辑编程或关系编程中，您定义的大多数函数实际上不是函数，而是"关系"，这些函数可以双向使用。例如，请参阅prolog或kanren。
像这样的任务几乎总是不可决定的。您可以为某些特定的功能提供解决方案，但不是一般的解决方案。
在这里，您甚至无法识别哪些函数具有反函数。引用Barendrigt，H.P.Lambda微积分：它的语法和语义。北荷兰，阿姆斯特丹(1984)：
如果lambda项集既不是空集也不是全集，则它是非平凡的。如果A和B是在(贝塔)等式下闭合的两个非平凡的、不相交的lambda项集，那么A和B递归地不可分。
让我们把A作为表示可逆函数的lambda项的集合，把B作为其余项。两者都是非空的，并且在贝塔等式下是封闭的。所以不可能决定一个函数是否可逆。
(这适用于非类型化的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是一个双射，那么必然会有一个并且只有一个这样的元素。当然，诀窍是确保域的枚举在有限的时间内真正到达的所有元素。如果你试图将双射从Integer反转为Integer，那么使用[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这样的东西——但它愿意信任你。
(警告：未经测试的代码如下)
那么，你能在类型a和b:之间定义一个Bijections的数据类型吗
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常数的次数可能会非常有限。
毕竟，如果你知道一个函数是一个双射，你会希望在你的脑海中有一个这个事实的证明草图，库里-霍华德同构应该能够把它变成一个程序：-)
我最近一直在处理这样的问题，不，我想说(a)在很多情况下这并不困难，但(b)它根本没有效率。
基本上，假设您有f :: a -> b，并且f确实是一个bjiction。你可以用一种非常愚蠢的方式来计算逆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。
具有Bounded和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