Dans les langages fonctionnels pures, y a-t-il un algorithme pour obtenir la fonction inverse ?

Question

Dans les langages fonctionnels pures comme Haskell, existe-t-il un algorithme pour obtenir l’inverse d’une fonction, (edit) lorsqu’elle est bijective ? Et est-il possible de programmer votre fonction n’est spécifique ?

Answer 1

Dans certains cas, oui! Il y a un beau papier appelé Bidirectionalization Gratuitement! qui parle de quelques cas, lorsque votre fonction est assez polymorphe, où il est possible, de manière entièrement automatique pour dériver une fonction inverse. (Il explique également ce qui rend le problème plus difficile lorsque les fonctions ne sont pas polymorphes.)

Ce que vous obtenir dans le cas où votre fonction est inversible est l'inverse (avec une fausse entrée); dans d'autres cas, vous avez une fonction qui tente de "fusion" un vieux de la valeur d'entrée et une nouvelle valeur de sortie.

Answer 2

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

Preuve: considérons bijective fonctions de type

type F = [Bit] -> [Bit]

avec

data Bit = B0 | B1

Supposons que nous avons un onduleur inv :: F -> F tels que inv f . f ≡ id. Dire que nous avons testé pour la fonction f = id, en confirmant que

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

Depuis cette première B0 de la production doit venir après un certain temps fini, nous avons une limite supérieure n sur à la fois la profondeur à laquelle le inv avaient effectivement évalué notre test d'entrée pour obtenir ce résultat, ainsi que le nombre de fois où il peut avoir appelé f. Définissons 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 j est une bijection, en fait auto-inverse. Donc, nous devrions être en mesure de confirmer

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

mais pour accomplir cette, inv (g j) aurait fallu que ce soit

• évaluer g j (B1 : repeat B0) jusqu'à une profondeur de n+j > n
• évaluer head $ g j l pendant au moins n différentes listes de correspondance replicate (n+j) B0 ++ B1 : ls

Jusqu'à ce point, au moins l'une de la g j est impossible de distinguer f, et depuis inv f n'avait pas fait une de ces évaluations, inv ne pouvait pas avoir dit à part – court de faire de certains à l'exécution des mesures sur son propre, ce qui n'est possible que dans l' IO Monad.

⬜

Answer 3

Vous pouvez chercher sur wikipedia, ça s’appelle Calcul réversible.

En général vous ne pouvez pas le faire bien et aucun d'entre les langages fonctionnels ont cette option. Par exemple :

Cette fonction n’a pas l’inverse.

Answer 4

Pas en langues plus fonctionnels, mais en programmation logique ou programmation relationnelle, vous définissez la plupart des fonctions sont en fait pas des fonctions mais des « relations », et ils peuvent servir dans les deux sens. Voir par exemple prolog ou kanren.

Answer 5

Les tâches de ce genre sont presque toujours indécidable. 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 les fonctions qui ont un inverse. Citant Barendregt, H. P. Le Lambda Calcul: Sa Syntaxe et de la Sémantique. North Holland, Amsterdam (1984):

Un ensemble de lambda-termes est non triviale si ce n'est ni le vide, ni le jeu complet. Si A et B sont deux non-triviale, ensembles disjoints de lambda-termes clos (bêta) de l'égalité, alors A et B sont récursivement inséparables.

Prenons Un être à l'ensemble de lambda-termes qui représentent inversible fonctions et B le reste. Les deux sont non-vide et fermé en vertu de la bêta de l'égalité. Il n'est donc pas possible de décider si une fonction est inversible ou non.

(Ceci s'applique à la non typée lambda calcul. TBH je ne sais pas si l'argument peut être directement adapté à un lambda calcul typé quand on sait que le type d'une fonction que nous voulons inverser. Mais je suis sûr que ce sera le même.)