haskell - teorema - problemas de aplicacion de funcion inversa

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

Question

En lenguajes funcionales puros como Haskell, ¿hay un algoritmo para obtener el inverso de una función, (editar) cuando es biyectivo? ¿Y hay una forma específica de programar tu función así es?

Answer 1

En algunos casos, ¡sí! ¡Hay un hermoso artículo llamado Bidirectionalization gratis! que discute unos pocos casos, cuando tu función es suficientemente polimórfica, donde es posible, de forma completamente automática derivar una función inversa. (También discute qué hace que el problema sea difícil cuando las funciones no son polimórficas).

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

Answer 2

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 funciones sino "relaciones", y pueden utilizarse en ambas direcciones. Ver por ejemplo prolog o kanren.

Answer 3

No todas las funciones tienen una inversa. Si limita la discusión a funciones de 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!

Answer 4

No, no es posible en general.

Prueba: considerar 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 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 un tiempo finito, tenemos un límite superior n en la profundidad a la que inv evaluó realmente nuestra entrada de prueba para obtener este resultado, así como también la cantidad 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 todo 0<j≤n , gj es una biyección, de hecho auto inverso. Entonces deberíamos poder confirmar

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

pero para cumplir esto, inv (gj) habría necesitado

• evalúa gj (B1 : repeat B0) a una profundidad de n+j > n
• evalúa head $ gjl para al menos n listas diferentes que coinciden con replicate (n+j) B0 ++ B1 : ls

Hasta ese momento, al menos uno de los gj es indistinguible de f , y como inv f no había hecho ninguna de estas evaluaciones, inv no podría haberlo distinguido, salvo algunas mediciones en tiempo de ejecución, que solo es posible en la IO Monad .

⬜

Answer 5

No, no todas las funciones tienen inversos. Por ejemplo, ¿cuál sería el inverso de esta función?

f x = 1

Answer 6

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

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

f :: a -> Int
f _ = 1

Esta función no tiene un inverso.

Answer 7

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 para nada eficiente.

Básicamente, supongamos que tiene f :: a -> b , y que f es de hecho una bjiection. Puede calcular el inverso 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 llegarás a tal que fa == b .

Los tipos que tienen una instancia Bounded y una instancia de Enum pueden 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 tipos de 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

El hecho de que podamos hacer esto tanto para (,) como para Either probablemente signifique que podemos hacerlo para cualquier tipo de datos algebraicos.

Answer 8

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

Lo que quieres hacer es recorrer los elementos del dominio y ver si son iguales al elemento del rango que intentas 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 has declarado que f es una biyección, es probable que exista uno y solo uno de esos elementos. El truco, por supuesto, es asegurarse de que su enumeración del dominio llegue realmente a todos los elementos en un tiempo finito . Si intentas 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 arrojará un valor.

Sin embargo, 0 : concatMap (/x -> [x,-x]) [1..] funcionará, ya que se ejecuta a través de los 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) devuelve prontamente -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 bajo-frente y fuerza bruta, por no mencionar feo e ineficiente! Así que terminaré con algunas observaciones sobre la última parte de su pregunta, sobre cómo ''escribir'' biyecciones. El sistema de tipos de Haskell no está a la altura de la prueba de que una función es una biyección; realmente quieres algo así como Agda para eso, pero está dispuesto a confiar en ti.

(Advertencia: sigue el código no probado)

Entonces, ¿puedes definir un tipo de datos de Bijection s entre los tipos 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 por ejemplo:

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 podrías invert (mapBi add1Bi) [1,5,6] y obtener [0,4,5] . Si seleccionas los combinadores de una manera inteligente, creo que la cantidad de veces que tendrás que escribir una constante Bi manualmente podría ser bastante limitada.

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

Answer 9

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

Aquí, ni siquiera puedes reconocer qué funciones tienen una inversa. Citando a Barendregt, HP The Lambda Calculus: Its Syntax and Semantics. Holanda Septentrional, 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 y disjuntos de términos lambda cerrados bajo igualdad (beta), entonces A y B son recursivamente inseparables.

Tomemos A para ser el conjunto de términos lambda que representan funciones invertibles y B el resto. Ambos no están vacíos y se cierran bajo la igualdad beta. Por lo 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 tipado cuando conocemos el tipo de función que queremos invertir. Pero estoy bastante seguro de que será similar.)