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

No, no es posible en general.

Prueba: considere las funciones biyectivas de tipo

type F = [Bit] -> [Bit]

Con

data Bit = B0 | B1

Supongamos que tenemos un inversor inv :: F -> F tal 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 primer B0 en la salida debe haber llegado después de algún tiempo finito, tenemos un límite superior n tanto en la profundidad a la que inv realmente había evaluado nuestra entrada de prueba para obtener este resultado, así como la número de veces que puede haber llamado f. Definir 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 j es una biyección, de hecho auto-inversa. Así que debemos ser capaces de confirmar

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

Pero para cumplir esto, inv (g j) habría necesitado ya sea{[26]]}

• evaluar g j (B1 : repeat B0) a una profundidad de n+j > n
• evaluar head $ g j l para al menos n diferentes listas coincidentes replicate (n+j) B0 ++ B1 : ls

Hasta ese punto, al menos uno de los g j es indistinguible de f, y dado que inv f no había hecho ninguna de estas evaluaciones, inv no podría haberlo separado, sin hacer algunas mediciones de tiempo de ejecución por sí sola, lo que solo es posible en el IO Monad.

Puedes buscarlo en Wikipedia, se llama Computación Reversible.

En general no puedes hacerlo y ninguno de los lenguajes funcionales tiene esa opción. Por ejemplo:

f :: a -> Int
f _ = 1

Esta función no tiene una inversa.

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

Tareas como esta son casi siempre 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 Barendregt, H. P. El Cálculo Lambda: Su Sintaxis y Semántica. Holanda del Norte, Amsterdam (1984):

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

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

(Esto se aplica al cálculo lambda sin tipo. TBH No se si el argumento puede ser adaptado directamente a un cálculo lambda mecanografiado cuando sabemos el tipo de una función que queremos invertir. Pero Estoy bastante seguro de que será similar.)

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

Lo que desea hacer es correr a través de los elementos del dominio y ver si son iguales al elemento del rango que está tratando de invertir, y tomar el primero que obras:

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

Puesto que usted ha declarado que f es una biyección, está obligado a haber uno y solo uno de esos elementos. El truco, por supuesto, es asegurarse de que su enumeración del dominio realmente alcance todos los elementos en un tiempo finito. Si estás intentando invertir una biyección de Integer a Integer, usar [0,1 ..] ++ [-1,-2 ..] no funcionará ya que nunca llegarás a los números negativos. Concretamente, inv ([0,1 ..] ++ [-1,-2 ..]) (+1) (-3) nunca dará un valor.

Sin embargo, 0 : concatMap (\x -> [x,-x]) [1..] funcionará, ya que esto se ejecuta a través de la 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) rápidamente vuelve -4!

El Control .Mónada.El paquete Omega puede ayudarte a ejecutar listas de tuplas, etc. de una buena manera; estoy seguro de que hay más paquetes como ese, pero no los conozco.

Por supuesto, este enfoque es bastante de frente baja y fuerza bruta, ¡por no mencionar feo e ineficiente! Así que terminaré con algunos comentarios sobre la última parte de tu pregunta, sobre cómo 'escribir' bijecciones. El sistema de tipos de Haskell no está a la altura de 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 el código no probado)

Así que puedes definir un tipo de datos de Bijection s entre los tipos a y b:

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

Junto con tantas constantes (donde puedes decir 'Yo sé son bijecciones!') como quieras, tales como:

notBi :: Bi Bool Bool
notBi = Bi not not

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

Y un par de combinadores inteligentes, tales 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)

I piensa que entonces podrías hacer invert (mapBi add1Bi) [1,5,6] y obtener [0,4,5]. Si eliges tus combinadores de una manera inteligente, creo que el número de veces que tendrás que escribir una constante Bi a mano podría ser bastante limitado.

Después de todo, si sabes que una función es una biyección, con suerte tendrás un boceto de prueba de ese hecho en tu cabeza, que el isomorfismo de Curry-Howard debería ser capaz de convertir en un programa: -)

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

Básicamente, supongamos que tienes f :: a -> b, y que f es de hecho una bjiección. Puedes calcular la inversa f' :: b -> a de 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 f es una biyección y enumerate realmente produce todos los valores de a, entonces eventualmente alcanzarás un a tal que f a == b.

Tipos que tienen un Bounded y un Enum la instancia se puede hacer trivialmente RecursivelyEnumerable. Los pares de tipos Enumerable también se pueden hacer 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 Enumerable tipos:

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 tanto para (,) y Either probablemente 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!

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

f x = 1