Comment utiliser fix et comment fonctionne-t-il ?

Question

J'ai été quelque peu déconcerté par la documentation relative à fix (bien que je pense comprendre ce qu'il est censé faire maintenant), j'ai donc regardé le code source. Cela m'a laissé encore plus perplexe :

fix :: (a -> a) -> a
fix f = let x = f x in x

Comment cela permet-il de retrouver un point fixe ?

J'ai décidé de l'essayer en ligne de commande :

Prelude Data.Function> fix id
...

Et c'est là qu'il s'accroche. Maintenant, pour être juste, c'est sur mon vieux macbook qui est assez lent. Cependant, cette fonction ne peut pas être aussi coûteux en termes de calcul, puisque tout ce qui est transmis à id lui est rendu (sans parler du fait qu'il ne consomme pas de temps d'unité centrale). Qu'est-ce que je fais de travers ?

Answer 1

Vous ne faites rien de mal. fix id est une boucle infinie.

Lorsque nous disons que fix renvoie le plus petit point fixe d'une fonction, nous voulons dire que dans le théorie des domaines sens. Ainsi, les fix (\x -> 2*x-1) es no va revenir 1 car bien que 1 est un point fixe de cette fonction, il n'est pas le le moins dans l'ordre des domaines.

Il m'est impossible de décrire l'ordonnancement des domaines en un ou deux paragraphes, je vous renvoie donc au lien de la théorie des domaines ci-dessus. Il s'agit d'un excellent tutoriel, facile à lire et très instructif. Je le recommande vivement.

Pour la vue à 10 000 pieds d'altitude, fix est une fonction d'ordre supérieur qui encode l'idée de récursivité . Si vous avez l'expression :

let x = 1:x in x

Ce qui donne la liste infinie [1,1..] On pourrait dire la même chose en utilisant fix :

fix (\x -> 1:x)

(Ou simplement fix (1:) ), ce qui signifie qu'il faut me trouver un point fixe de l'équation (1:) une valeur x tel que x = 1:x ... comme nous l'avons défini ci-dessus. Comme vous pouvez le voir dans la définition, fix n'est rien d'autre que cette idée : la récursivité encapsulée dans une fonction.

Il s'agit également d'un concept très général de récursivité : vous pouvez écrire n'importe quelle fonction récursive de cette manière, y compris les fonctions qui utilisent la récursivité polymorphe . Ainsi, par exemple, la fonction typique de Fibonacci :

fib n = if n < 2 then n else fib (n-1) + fib (n-2)

Peut être écrit en utilisant fix de cette manière :

fib = fix (\f -> \n -> if n < 2 then n else f (n-1) + f (n-2))

Exercice : développez la définition de fix pour montrer que ces deux définitions de fib sont équivalents.

Mais pour bien comprendre, lisez la théorie des domaines. C'est vraiment très intéressant.

Answer 2

Je ne prétends pas comprendre cela du tout, mais si cela peut aider quelqu'un... alors youpi.

Considérons la définition de fix . fix f = let x = f x in x . Ce qui est le plus étonnant, c'est que x est défini comme suit f x . Mais réfléchissez-y un instant.

x = f x

Puisque x = f x, nous pouvons substituer la valeur de x sur le côté droit, n'est-ce pas ? Donc...

x = f . f $ x -- or x = f (f x)
x = f . f . f $ x -- or x = f (f (f x))
x = f . f . f . f . f . f . f . f . f . f . f $ x -- etc.

L'astuce consiste donc à mettre un terme à la procédure, f doit générer une sorte de structure, de sorte qu'un f peut faire une correspondance avec cette structure et mettre fin à la récursion, sans se soucier de la "valeur" complète de son paramètre ( ?).

Sauf, bien sûr, si vous souhaitez créer une liste infinie, comme l'a illustré luqui.

L'explication factorielle de TomMD est bonne. La signature de type de Fix est (a -> a) -> a . La signature de type pour (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) es (b -> b) -> b -> b en d'autres termes, (b -> b) -> (b -> b) . On peut donc dire que a = (b -> b) . De cette façon, fix prend notre fonction, qui est a -> a ou vraiment, (b -> b) -> (b -> b) et renvoie un résultat du type a en d'autres termes, b -> b En d'autres termes, une autre fonction !

Attendez, je pensais qu'il était censé retourner un point fixe... et non une fonction. Et bien c'est le cas, en quelque sorte (puisque les fonctions sont des données). Vous pouvez imaginer qu'il nous a donné la fonction définitive pour trouver une factorielle. Nous lui avons donné une fonction qui ne savait pas comment réintégrer (c'est pourquoi l'un de ses paramètres est une fonction utilisée pour réintégrer), et fix lui a appris la récursivité.

Vous vous souvenez que j'ai dit que f doit générer une sorte de structure afin qu'un futur f peut-elle correspondre à un modèle et se terminer ? Ce n'est pas tout à fait exact, je suppose. TomMD a illustré la façon dont nous pouvons étendre x pour appliquer la fonction et se rapprocher du cas de base. Pour sa fonction, il a utilisé un if/then, et c'est ce qui provoque la terminaison. Après des remplacements répétés, le in partie de l'ensemble de la définition de fix finit par ne plus être défini en termes de x et c'est à ce moment-là qu'il est calculable et complet.

Answer 3

Vous avez besoin d'un moyen pour que le point fixe se termine. En développant votre exemple, il est évident qu'il ne se terminera pas :

fix id
--> let x = id x in x
--> id x
--> id (id x)
--> id (id (id x))
--> ...

Voici un exemple réel de mon utilisation de fix (notez que je n'utilise pas souvent fix et que j'étais probablement fatigué / je ne me préoccupais pas d'un code lisible lorsque j'ai écrit ceci) :

(fix (\f h -> if (pred h) then f (mutate h) else h)) q

WTF, dites-vous ! Eh bien, oui, mais il y a quelques points vraiment utiles ici. Tout d'abord, votre première fix doit généralement être une fonction, ce qui correspond au cas "recurse", et le second argument est la donnée sur laquelle agir. Voici le même code en tant que fonction nommée :

getQ h
      | pred h = getQ (mutate h)
      | otherwise = h

Si vous n'êtes toujours pas convaincu, l'exemple de la factorielle sera peut-être plus facile à comprendre :

fix (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) 5 -->* 120

Remarquez l'évaluation :

fix (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) 3 -->
let x = (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) x in x 3 -->
let x = ... in (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) x 3 -->
let x = ... in (\d -> if d > 0 then d * (x (d-1)) else 1) 3

Oh, vous venez de voir ça ? C'est x est devenue une fonction à l'intérieur de notre then branche.

let x = ... in if 3 > 0 then 3 * (x (3 - 1)) else 1) -->
let x = ... in 3 * x 2 -->
let x = ... in 3 * (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) x 2 -->

Dans ce qui précède, vous devez vous rappeler x = f x , d'où les deux arguments de x 2 à la fin au lieu de 2 .

let x = ... in 3 * (\d -> if d > 0 then d * (x (d-1)) else 1) 2 -->

Et je m'arrête là !

Answer 4

Une définition claire est la suivante Vous auriez pu aussi réinventer la fixation !

Answer 5

Si j'ai bien compris, il s'agit de trouver une valeur pour la fonction, de telle sorte qu'elle produise la même chose que ce que vous lui donnez. Le problème est qu'il choisira toujours undefined (ou une boucle infinie, en haskell, undefined et les boucles infinies sont identiques) ou ce qui contient le plus d'undefined. Par exemple, avec id,

λ <*Main Data.Function>: id undefined
*** Exception: Prelude.undefined

Comme vous pouvez le voir, undefined est un point fixe, donc fix le choisira. Si vous faites plutôt ( \x ->1:x).

λ <*Main Data.Function>: undefined
*** Exception: Prelude.undefined
λ <*Main Data.Function>: (\x->1:x) undefined
[1*** Exception: Prelude.undefined

Así que fix ne peut pas choisir indéfini. Pour que ce soit un peu plus lié aux boucles infinies.

λ <*Main Data.Function>: let y=y in y
^CInterrupted.
λ <*Main Data.Function>: (\x->1:x) (let y=y in y)
[1^CInterrupted.

Là encore, il s'agit d'une légère différence. Quel est donc le point fixe ? Essayons repeat 1 .

λ <*Main Data.Function>: repeat 1
[1,1,1,1,1,1, and so on
λ <*Main Data.Function>: (\x->1:x) $ repeat 1
[1,1,1,1,1,1, and so on

C'est la même chose ! Puisque c'est le seul point fixe, fix doit s'en contenter. Désolé fix pas de boucles infinies ni d'indéfinis pour vous.