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

100

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?

MaiaVictor
la source
5
Mathématiquement, il n'est pas faux de dire que, dans le cas de f x = 1, l'inverse de 1 est un ensemble d'entiers et l'inverse de toute autre chose est un ensemble vide. Indépendamment de ce que disent certaines réponses, la fonction n'étant pas bijective n'est pas le plus gros problème.
Karolis Juodelė
2
La bonne réponse est OUI, mais ce n'est pas efficace. Soit f: A -> B et A finis, alors, étant donné b € B, il faut "seulement" inspecter tout f (A) pour trouver tout a € A que f (a) = b. Dans un ordinateur quantique, aurait peut-être une complexité O (taille (a)). Bien sûr, vous recherchez un algorithme pratique. Ce n'est pas (a O (2 ^ taille (a))), mais existe ...
josejuan
QuickCheck le fait exactement (ils recherchent un False dans f: A -> Bool).
josejuan
4
@ KarolisJuodelė: Je ne suis pas d'accord; ce n'est généralement pas ce que l'on entend par inverse. Presque chaque fois que je rencontre le terme, l'inverse de fest une fonction gtelle que f . g = idet g . f = id. Votre candidat ne vérifie même pas la typographie dans ce cas.
Ben Millwood
3
@BenMillwood, vous avez raison. Ce que j'ai dit s'appelle une image inverse, pas une fonction inverse. Mon point était que les réponses indiquant qu'il f x = 1n'y a pas d'inverse adoptent une approche très étroite et ignorent toute la complexité du problème.
Karolis Juodelė

Réponses:

101

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.

Daniel Wagner
la source
3
Voici un article plus récent qui examine l'état de l'art en matière de bidirectionnalisation. Il comprend trois familles de techniques, y compris des approches "syntaxiques" et combinées: iai.uni-bonn.de/~jv/ssgip-bidirectional-final.pdf
sclv
Et juste pour mentionner, en 2008, il y avait ce message à -cafe, avec un hack diabolique pour inverser les putfonctions dans toutes les structures d'enregistrement dérivant Data: haskell.org/pipermail/haskell-cafe/2008-April/042193.html en utilisant une approche similaire à que plus tard présenté (plus rigoureusement, plus généralement, plus raisonné, etc.) dans «gratuitement».
sclv
Nous sommes en
Mina Gabriel
37

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.

                                                                                                                                   ⬜

à gauche
la source
19

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.

mck
la source
1
Serait-il faux de dire que fcela a un inverse, c'est juste que l'inverse est une fonction non déterministe?
Matt Fenwick
10
@MattFenwick Dans un langage comme Haskell par exemple, les fonctions ne sont tout simplement pas non déterministes (sans changer les types et la façon dont vous les utilisez). Il n'existe aucune fonction Haskell g :: Int -> aqui soit l'inverse de f, même si vous pouvez décrire l'inverse de fmathématiquement.
Ben
2
@Matt: Rechercher "en bas" dans la programmation fonctionnelle et la logique. Un «fond» est une valeur «impossible», soit parce qu'elle est contradictoire, non terminale, soit parce qu'elle est la solution à un problème indécidable (c'est plus que simplement contradictoire - nous pouvons méthodiquement «rechercher» une solution pendant que nous explorons une conception espace en utilisant "undefined" et "error" pendant le développement). Un x "bas" a le type a. Il "habite" (ou est une "valeur") de chaque type. C'est une contradiction logique, puisque les types sont des propositions et qu'il n'y a pas de valeur qui satisfait chaque proposition. Regardez sur Haskell-Cafe pour de bonnes discussions
Nomen
2
@Matt: Plutôt que de caractériser la non-existence des inverses en termes de non-déterminisme, il faut la caractériser en termes de fonds. L'inverse de f _ = 1 est en bas, car il doit habiter tous les types (alternativement, il est en bas puisque f n'a pas de fonction inverse pour tout type avec plus d'un élément - l'aspect sur lequel vous vous êtes concentré, je pense). Être au fond peut être considéré à la fois positivement et négativement comme des affirmations sur les valeurs. On peut raisonnablement parler de l'inverse d'une fonction arbitraire comme étant la «valeur» inférieure. (Même si ce n'est pas "vraiment" une valeur)
nomen
1
Ayant erré ici beaucoup plus tard, je pense voir ce que Matt veut dire: nous modélisons souvent le non-déterminisme via des listes, et nous pourrions faire de même pour les inverses. Soit l'inverse de f x = 2 * xbe f' x = [x / 2], puis l'inverse de f _ = 1is f' 1 = [minBound ..]; f' _ = []. Autrement dit, il existe de nombreux inverses pour 1 et aucun pour toute autre valeur.
amalloy
16

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.

amalloy
la source
1
Ou Mercury , qui partage par ailleurs beaucoup l'esprit de Haskell. - Bon point, +1.
gauche vers
11

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.)

Petr Pudlák
la source
11

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 :-)

yatima2975
la source
6

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.

Luis Casillas
la source
5

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!

Jeffrey Scofield
la source
13
Tout système cryptographique (à l'exception de quelques-uns étranges, comme des tampons ponctuels, qui sont irréalisables pour d'autres raisons) peut être craqué par la force brute. Cela ne les rend pas moins utiles et ne serait pas non plus une fonction d'inversion peu coûteuse.
Vraiment? si vous pensez à une fonction de cryptage commeString encrypt(String key, String text) sans la clé, vous ne pourrez toujours rien faire. EDIT: Plus ce que Delnan a dit.
mck
@MaciekAlbin Dépend de votre modèle d'attaque. Les attaques en clair choisies, par exemple, peuvent permettre d'extraire la clé, ce qui permettrait ensuite d'attaquer d'autres textes chiffrés chiffrés avec cette clé.
Par «faisable», je voulais dire quelque chose qui peut être fait dans un laps de temps raisonnable. Je ne voulais pas dire «calculable» (j'en suis presque sûr).
Jeffrey Scofield
@JeffreyScofield Je comprends votre point de vue. Mais je dois dire que je suis confus par «faisable en théorie» - (notre définition de) la faisabilité ne se réfère-t-elle pas seulement à la difficulté à faire en pratique?
5

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.

Vert Anderson
la source
4

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

f x = 1
Dirk Holsopple
la source
Votre fonction est une constante, ici il s'agit de fonctions bijectives.
Soleil - Mathieu Prévot