Dans les langages fonctionnels purs, existe-t-il un algorithme pour obtenir la fonction inverse?

Dans les langages fonctionnels purs comme Haskell, existe-t-il un algorithme pour obtenir l'inverse d'une fonction, (modifier) ​​quand elle est bijective? Et y a-t-il une manière spécifique de programmer votre fonction ainsi?

Dans certains cas, oui! Il existe un beau papier appelé Bidirectionalization for Free! qui traite de quelques cas - lorsque votre fonction est suffisamment polymorphe - où il est possible, de manière complètement automatique, de dériver une fonction inverse. (Il discute également de ce qui rend le problème difficile lorsque les fonctions ne sont pas polymorphes.)

Ce que vous obtenez dans le cas où votre fonction est inversible est l'inverse (avec une entrée fausse); dans d'autres cas, vous obtenez une fonction qui essaie de "fusionner" une ancienne valeur d'entrée et une nouvelle valeur de sortie.

Non, ce n'est pas possible en général.

Preuve: considérez les fonctions bijectives de type

type F = [Bit] -> [Bit]

avec

data Bit = B0 | B1

Supposons que nous ayons un onduleur inv :: F -> Ftel que inv f . f ≡ id. Disons que nous l'avons testé pour la fonction f = id, en confirmant que

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

Puisque ce premier B0dans la sortie doit être venu après un temps fini, nous avons une limite supérieure nà la fois sur la profondeur à laquelle invavait réellement évalué notre entrée de test pour obtenir ce résultat, ainsi que sur le nombre de fois qu'il a pu appeler f. Définissez maintenant une famille de fonctions

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

Clairement, pour tous 0<j≤n, g jest une bijection, en fait auto-inverse. On devrait donc pouvoir confirmer

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

mais pour y parvenir, inv (g j)il aurait fallu soit

• évaluer g j (B1 : repeat B0)à une profondeur den+j > n
• évaluer head $ g j lpour au moins ndifférentes listes correspondantesreplicate (n+j) B0 ++ B1 : ls

Jusque-là, au moins une des évaluations g jest indiscernable de f, et depuis inv fn'a fait aucune de ces évaluations, invn'aurait pas pu la distinguer - à moins de faire certaines mesures d'exécution par elle-même, ce qui n'est possible que dans le IO Monad.

                                                                                                                                   ⬜

Vous pouvez le rechercher sur wikipedia, il s'appelle Reversible Computing .

En général, vous ne pouvez pas le faire et aucun des langages fonctionnels n'a cette option. Par exemple:

f :: a -> Int
f _ = 1

Cette fonction n'a pas d'inverse.

Pas dans la plupart des langages fonctionnels, mais dans la programmation logique ou la programmation relationnelle, la plupart des fonctions que vous définissez ne sont en fait pas des fonctions mais des «relations», et celles-ci peuvent être utilisées dans les deux sens. Voir par exemple prolog ou kanren.

Des tâches comme celle-ci sont presque toujours indécidables. Vous pouvez avoir une solution pour certaines fonctions spécifiques, mais pas en général.

Ici, vous ne pouvez même pas reconnaître quelles fonctions ont un inverse. Citant Barendregt, HP Le calcul Lambda: sa syntaxe et sa sémantique. Hollande du Nord, Amsterdam (1984) :

Un ensemble de termes lambda n'est pas trivial s'il ne s'agit ni de l'ensemble vide ni de l'ensemble complet. Si A et B sont deux ensembles non triviaux et disjoints de termes lambda fermés sous l'égalité (bêta), alors A et B sont inséparables récursivement.

Prenons A pour l'ensemble des termes lambda qui représentent des fonctions inversibles et B le reste. Les deux sont non vides et fermés sous l'égalité bêta. Il n'est donc pas possible de décider si une fonction est inversible ou non.

(Cela s'applique au calcul lambda non typé. TBH Je ne sais pas si l'argument peut être directement adapté à un calcul lambda typé lorsque nous connaissons le type de fonction que nous voulons inverser. Mais je suis presque sûr que ce sera similaire.)

Si vous pouvez énumérer le domaine de la fonction et comparer les éléments de la plage pour l'égalité, vous pouvez - d'une manière assez simple. Par énumérer, j'entends avoir une liste de tous les éléments disponibles. Je m'en tiens à Haskell, car je ne connais pas Ocaml (ni même comment le capitaliser correctement ;-)

Ce que vous voulez faire, c'est parcourir les éléments du domaine et voir s'ils sont égaux à l'élément de la plage que vous essayez d'inverser, puis prenez le premier qui fonctionne:

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

Puisque vous avez déclaré que fc'est une bijection, il y a forcément un et un seul élément de ce type. L'astuce, bien sûr, est de vous assurer que votre énumération du domaine atteint réellement tous les éléments dans un temps fini . Si vous essayez d'inverser une bijection de Integeren Integer, l'utilisation [0,1 ..] ++ [-1,-2 ..]ne fonctionnera pas car vous n'obtiendrez jamais les nombres négatifs. Concrètement,inv ([0,1 ..] ++ [-1,-2 ..]) (+1) (-3) ne donnera jamais de valeur.

Cependant, 0 : concatMap (\x -> [x,-x]) [1..]cela fonctionnera, car cela parcourt les entiers dans l'ordre suivant [0,1,-1,2,-2,3,-3, and so on]. En effet inv (0 : concatMap (\x -> [x,-x]) [1..]) (+1) (-3)revient rapidement -4!

Le package Control.Monad.Omega peut vous aider à parcourir des listes de tuples, etc. d'une bonne manière; Je suis sûr qu'il y a plus de paquets comme ça - mais je ne les connais pas.

Bien sûr, cette approche est plutôt discrète et brutale, pour ne pas mentionner laide et inefficace! Je terminerai donc par quelques remarques sur la dernière partie de votre question, sur la manière d '«écrire» des bijections. Le système de types de Haskell n'est pas à la hauteur de prouver qu'une fonction est une bijection - vous voulez vraiment quelque chose comme Agda pour cela - mais il est prêt à vous faire confiance.

(Attention: le code non testé suit)

Alors pouvez-vous définir un type de données de Bijections entre les types aet b:

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

avec autant de constantes (où vous pouvez dire `` Je sais que ce sont des bijections! '') que vous le souhaitez, telles que:

notBi :: Bi Bool Bool
notBi = Bi not not

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

et quelques combinateurs intelligents, tels que:

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)

Je pense que vous pourriez alors faire invert (mapBi add1Bi) [1,5,6]et obtenir [0,4,5]. Si vous choisissez vos combinateurs de manière intelligente, je pense que le nombre de fois que vous devrez écrire une Biconstante à la main pourrait être assez limité.

Après tout, si vous savez qu'une fonction est une bijection, vous aurez, espérons-le, un croquis de preuve de ce fait dans votre tête, que l'isomorphisme de Curry-Howard devrait pouvoir transformer en programme :-)

J'ai récemment été confronté à des problèmes comme celui-ci, et non, je dirais que (a) ce n'est pas difficile dans de nombreux cas, mais (b) ce n'est pas du tout efficace.

Fondamentalement, supposons que vous ayez f :: a -> b, et c'est en feffet une bjiection. Vous pouvez calculer l'inverse f' :: b -> ad'une manière vraiment stupide:

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 fest une bijection et enumerateproduit vraiment toutes les valeurs de a, alors vous finirez par frapper une atelle chose f a == b.

Les types qui ont un Boundedet une Enuminstance peuvent être créés de manière simple RecursivelyEnumerable. Des paires de Enumerabletypes peuvent également être réalisées 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

Il en va de même pour les disjonctions de Enumerabletypes:

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

Le fait que nous puissions le faire à la fois pour (,)et Eithersignifie probablement que nous pouvons le faire pour n'importe quel type de données algébriques.

Toutes les fonctions n'ont pas d'inverse. Si vous limitez la discussion à des fonctions individuelles, la possibilité d'inverser une fonction arbitraire donne la possibilité de casser n'importe quel cryptosystème. Nous devons en quelque sorte espérer que ce n'est pas faisable, même en théorie!

Dans certains cas, il est possible de trouver l'inverse d'une fonction bijective en la convertissant en une représentation symbolique. Sur la base de cet exemple , j'ai écrit ce programme Haskell pour trouver les inverses de certaines fonctions polynomiales 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

Cet exemple ne fonctionne qu'avec des expressions arithmétiques, mais il pourrait probablement être généralisé pour fonctionner également avec des listes.

Non, toutes les fonctions n'ont même pas d'inverses. Par exemple, quel serait l'inverse de cette fonction?

f x = 1