En los lenguajes funcionales puros, ¿existe un algoritmo para obtener la función inversa?

En lenguajes funcionales puros como Haskell, ¿existe un algoritmo para obtener la inversa de una función, (editar) cuando es biyectiva? ¿Y hay una forma específica de programar su función para que sea así?

En algunos casos, ¡sí! ¡Hay un hermoso artículo llamado Bidireccionalización gratis! que analiza algunos casos, cuando su función es suficientemente polimórfica, donde es posible, de forma completamente automática, derivar una función inversa. (También analiza qué dificulta el problema cuando las funciones no son polimórficas).

Lo que se obtiene en el caso de que su función sea invertible es la inversa (con una entrada falsa); en otros casos, obtiene una función que intenta "fusionar" un valor de entrada antiguo y un valor de salida nuevo.

No, no es posible en general.

Prueba: considere funciones biyectivas de tipo

type F = [Bit] -> [Bit]

con

data Bit = B0 | B1

Supongamos que tenemos un inversor inv :: F -> Ftal que inv f . f ≡ id. Digamos que lo hemos probado para la función f = id, confirmando que

inv f (repeat B0) -> (B0 : ls)

Dado que este primero B0en la salida debe haber llegado después de un tiempo finito, tenemos un límite superior ntanto en la profundidad a la que invrealmente se evaluó nuestra entrada de prueba para obtener este resultado, como en el número de veces que puede haber llamado f. Defina ahora una familia de funciones

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

Claramente, para todos 0<j≤n, g jes una biyección, de hecho, autoinversa. Entonces deberíamos poder confirmar

inv (g j) (replicate (n+j) B0 ++ B1 : repeat B0) -> (B1 : ls)

pero para cumplir con esto, inv (g j)habría necesitado

• evaluar g j (B1 : repeat B0)a una profundidad den+j > n
• evaluar head $ g j lal menos ndiferentes listas que coincidanreplicate (n+j) B0 ++ B1 : ls

Hasta ese momento, al menos uno de los g jes indistinguible de f, y dado que inv fno había realizado ninguna de estas evaluaciones, invno podría haberlo diferenciado, salvo realizar algunas mediciones en tiempo de ejecución por sí solo, lo que solo es posible en el IO Monad.

                                                                                                                                   ⬜

Puede buscarlo en wikipedia, se llama Computación reversible .

Sin embargo, en general no puede hacerlo y ninguno de los lenguajes funcionales tiene esa opción. Por ejemplo:

f :: a -> Int
f _ = 1

Esta función no tiene inversa.

No en la mayoría de los lenguajes funcionales, pero en la programación lógica o la programación relacional, la mayoría de las funciones que define no son funciones, sino "relaciones", y se pueden utilizar en ambas direcciones. Consulte, por ejemplo, prolog o kanren.

Tareas como esta casi siempre son indecidibles. Puede tener una solución para algunas funciones específicas, pero no en general.

Aquí, ni siquiera puede reconocer qué funciones tienen una inversa. Citando a Barendregt, HP El cálculo Lambda: su sintaxis y semántica. Holanda Septentrional, Amsterdam (1984) :

Un conjunto de términos lambda no es trivial si no es ni el conjunto vacío ni el completo. Si A y B son dos conjuntos no triviales, disjuntos de términos lambda cerrados bajo igualdad (beta), entonces A y B son recursivamente inseparables.

Tomemos A como el conjunto de términos lambda que representan funciones invertibles y B el resto. Ambos no están vacíos y cerrados bajo igualdad beta. Por tanto, no es posible decidir si una función es invertible o no.

(Esto se aplica al cálculo lambda sin tipo. TBH no sé si el argumento se puede adaptar directamente a un cálculo lambda con tipo cuando conocemos el tipo de función que queremos invertir. Pero estoy bastante seguro de que será similar.)

Si puede enumerar el dominio de la función y comparar elementos del rango para determinar la igualdad, puede hacerlo de una manera bastante sencilla. Por enumerar me refiero a tener una lista de todos los elementos disponibles. Me quedaré con Haskell, ya que no sé Ocaml (ni siquiera cómo capitalizarlo correctamente ;-)

Lo que desea hacer es ejecutar los elementos del dominio y ver si son iguales al elemento del rango que está tratando de invertir, y tomar el primero que funcione:

inv :: Eq b => [a] -> (a -> b) -> (b -> a)
inv domain f b = head [ a | a <- domain, f a == b ]

Como ha dicho que fes una biyección, es probable que haya uno y solo uno de esos elementos. El truco, por supuesto, es asegurarse de que su enumeración del dominio alcance realmente todos los elementos en un tiempo finito . Si está tratando de invertir una biyección de Integera Integer, el uso [0,1 ..] ++ [-1,-2 ..]no funcionará ya que nunca obtendrá los números negativos. Concretamente,inv ([0,1 ..] ++ [-1,-2 ..]) (+1) (-3) nunca rendirá un valor.

Sin embargo, 0 : concatMap (\x -> [x,-x]) [1..]funcionará, ya que se ejecuta a través de los números enteros en el siguiente orden [0,1,-1,2,-2,3,-3, and so on]. De hecho inv (0 : concatMap (\x -> [x,-x]) [1..]) (+1) (-3)regresa rápidamente-4 !

El paquete Control.Monad.Omega puede ayudarlo a ejecutar listas de tuplas, etcétera, de una buena manera; Estoy seguro de que hay más paquetes como ese, pero no los conozco.

Por supuesto, este enfoque es bastante sencillo y de fuerza bruta, ¡sin mencionar que es feo e ineficiente! Así que terminaré con algunos comentarios sobre la última parte de su pregunta, sobre cómo 'escribir' bijecciones. El sistema de tipos de Haskell no está preparado para demostrar que una función es una biyección (realmente quieres algo como Agda para eso) pero está dispuesto a confiar en ti.

(Advertencia: sigue un código no probado)

Entonces, ¿puede definir un tipo de datos de Bijections entre tipos ay b:

data Bi a b = Bi {
    apply :: a -> b,
    invert :: b -> a 
}

junto con tantas constantes (donde puede decir '¡ Sé que son biyecciones!') como desee, como:

notBi :: Bi Bool Bool
notBi = Bi not not

add1Bi :: Bi Integer Integer
add1Bi = Bi (+1) (subtract 1)

y un par de combinadores inteligentes, como:

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)

Creo que entonces podrías hacer invert (mapBi add1Bi) [1,5,6]y conseguir [0,4,5]. Si elige sus combinadores de una manera inteligente, creo que la cantidad de veces que tendrá que escribir unBi constante a mano podría ser bastante limitada.

Después de todo, si sabe que una función es una biyección, es de esperar que tenga un bosquejo de prueba de ese hecho en su cabeza, que el isomorfismo de Curry-Howard debería poder convertir en un programa :-)

Recientemente he estado lidiando con problemas como este, y no, diría que (a) no es difícil en muchos casos, pero (b) no es eficiente en absoluto.

Básicamente, suponga que lo ha hecho f :: a -> b, y eso fes de hecho un error. Puedes calcular la inversa f' :: b -> ade una manera realmente tonta:

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

Si fes una biyección y enumeraterealmente produce todos los valores de a, eventualmente llegará a atal que f a == b.

Los tipos que tienen una instancia Boundedy una se Enumpueden hacer trivialmente RecursivelyEnumerable. EnumerableTambién se pueden hacer pares de tipos 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

Lo mismo ocurre con las disyunciones de Enumerabletipos:

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

El hecho de que podamos hacer esto para (,)y Eitherprobablemente significa que podemos hacerlo para cualquier tipo de datos algebraicos.

No todas las funciones tienen una inversa. Si limita la discusión a funciones uno a uno, la capacidad de invertir una función arbitraria otorga la capacidad de descifrar cualquier criptosistema. Tenemos que esperar que esto no sea factible, ¡incluso en teoría!

En algunos casos, es posible encontrar la inversa de una función biyectiva convirtiéndola en una representación simbólica. Basado en este ejemplo , escribí este programa de Haskell para encontrar inversas de algunas funciones polinomiales simples:

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

Este ejemplo solo funciona con expresiones aritméticas, pero probablemente podría generalizarse para trabajar también con listas.

No, ni siquiera todas las funciones tienen inversas. Por ejemplo, ¿cuál sería la inversa de esta función?

f x = 1