¿Cómo utilizo fix y cómo funciona?

87

Estaba un poco confundido por la documentación de fix(aunque creo que entiendo lo que se supone que debe hacer ahora), así que miré el código fuente. Eso me dejó más confundido:

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

¿Cómo devuelve esto exactamente un punto fijo?

Decidí probarlo en la línea de comando:

Prelude Data.Function> fix id
...

Y cuelga ahí. Ahora, para ser justos, esto está en mi viejo macbook, que es un poco lento. Sin embargo, esta función no puede ser demasiado costosa desde el punto de vista computacional, ya que cualquier cosa que se pase a id devuelve lo mismo (sin mencionar que no consume tiempo de CPU). ¿Qué estoy haciendo mal?

Jason Baker
fuente
68
La respuesta de la broma es "fix no tiene ningún uso real, está ahí para que pueda escribir fix errorghci y sentirse bien consigo mismo".
Thomas M. DuBuisson
3
@TomMD - Gracioso. Lo recordaré si alguien alguna vez me pregunta qué hace la solución y me siento malhumorado. :-)
Jason Baker
2
Normalmente escribo fixcomo fix f = f (fix f). Breve, simple, funciona e idéntica a la definición matemática.
newacct
20
@newacct, sí, así es como lo pienso yo también. Pero el de aquí puede conducir a estructuras más eficientes. Se puede ver la diferencia si se evalúa, por ejemplo, fix (1:) !! (10^8). El original lo hace en memoria constante, el tuyo toma memoria lineal (lo que también lo hace un poco más lento). Es decir, usar let "ata un nudo más fuerte" y permite que se genere una estructura de datos circular, mientras que la suya no.
luqui
22
¡Tú también podrías haberlo reinventado fix! me ayudó a entender fixmucho.
fredoverflow

Respuestas:

90

No estás haciendo nada malo. fix ides un bucle infinito.

Cuando decimos que fixdevuelve el punto mínimo fijo de una función, lo queremos decir en el sentido de la teoría del dominio . Así fix (\x -> 2*x-1)es que no va a volver 1, ya que si bien 1es un punto de esa función fija, no es la menos uno en el dominio de pedidos.

No puedo describir el orden de los dominios en uno o dos párrafos, así que los referiré al enlace de la teoría de dominios anterior. Es un tutorial excelente, fácil de leer y bastante esclarecedor. Lo recomiendo altamente.

Para la vista desde 10,000 pies, fixes una función de orden superior que codifica la idea de recursividad . Si tienes la expresión:

let x = 1:x in x

Lo que da como resultado la lista infinita [1,1..], podría decir lo mismo usando fix:

fix (\x -> 1:x)

(O simplemente fix (1:)), que dice que me encuentre un punto fijo de la (1:)función, IOW un valor xtal que x = 1:x... tal como definimos anteriormente. Como puede ver en la definición, fixno es más que esta idea: recursividad encapsulada en una función.

También es un concepto verdaderamente general de recursividad: puede escribir cualquier función recursiva de esta manera, incluidas las funciones que utilizan la recursividad polimórfica . Entonces, por ejemplo, la función típica de fibonacci:

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

Se puede escribir de fixesta manera:

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

Ejercicio: expanda la definición de fixpara mostrar que estas dos definiciones de fibson equivalentes.

Pero para una comprensión completa, lea sobre la teoría de dominios. Es algo realmente genial.

luqui
fuente
32
Aquí hay una forma de pensar relacionada fix id: fixtoma una función de tipo a -> ay devuelve un valor de tipo a. Como ides polimórfico para cualquiera a, fix idtendrá el tipo a, es decir, cualquier valor posible. En Haskell, el único valor que puede ser de cualquier tipo es bottom, ⊥, y es indistinguible de un cálculo no final. Entonces fix idproduce exactamente lo que debería, el valor mínimo. Un peligro fixes que si ⊥ es un punto fijo de su función, entonces, por definición, es el punto menos fijo, por fixlo tanto , no terminará.
John L
4
@JohnL en Haskell undefinedtambién es un valor de cualquier tipo. Se puede definir fixcomo: fix f = foldr (\_ -> f) undefined (repeat undefined).
Didest
1
@Diego tu código es equivalente a _Y f = f (_Y f).
Will Ness
25

No pretendo entender esto en absoluto, pero si esto ayuda a alguien ... entonces yippee.

Considere la definición de fix. fix f = let x = f x in x. La parte alucinante es que xse define como f x. Pero piénselo por un minuto.

x = f x

Dado que x = fx, entonces podemos sustituir el valor de xen el lado derecho de eso, ¿verdad? Asi que, por lo tanto...

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.

Entonces, el truco es, para terminar, ftiene que generar algún tipo de estructura, de modo que un fpatrón posterior pueda coincidir con esa estructura y terminar la recursividad, sin preocuparse realmente por el "valor" completo de su parámetro (?)

A menos que, por supuesto, quieras hacer algo como crear una lista infinita, como lo ilustró luqui.

La explicación factorial de TomMD es buena. La firma de tipo de Fix es (a -> a) -> a. La firma de tipo de (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1)es (b -> b) -> b -> b, en otras palabras, (b -> b) -> (b -> b). Entonces podemos decir eso a = (b -> b). De esa forma, la corrección toma nuestra función, que es a -> a, o realmente,(b -> b) -> (b -> b) y devolverá un resultado de tipo a, en otras palabras b -> b, en otras palabras, ¡otra función!

Espera, pensé que se suponía que devolvería un punto fijo ... no una función. Bueno, lo hace, algo así (ya que las funciones son datos). Puedes imaginar que nos dio la función definitiva para encontrar un factorial. Le dimos una función que no sabía cómo recurrir (por lo tanto, uno de los parámetros es una función que se usa para recurrir) y le fixenseñamos cómo recurrir.

¿Recuerdas cómo dije que ftiene que generar algún tipo de estructura para que un fpatrón posterior pueda coincidir y terminar? Bueno, eso no es exactamente correcto, supongo. TomMD ilustró cómo podemos expandirnos xpara aplicar la función y avanzar hacia el caso base. Para su función, usó un if / then, y eso es lo que provoca la terminación. Después de repetidos reemplazos, la inparte de la definición total de fixeventualmente deja de definirse en términos de xy es entonces cuando es computable y completa.

Dan Burton
fuente
Gracias. Esta es una explicación muy útil y práctica.
kizzx2
17

Necesita una forma de que termine el punto fijo. Ampliando su ejemplo, es obvio que no terminará:

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

Aquí hay un ejemplo real de mí usando fix (tenga en cuenta que no uso fix a menudo y probablemente estaba cansado / no preocupado por el código legible cuando escribí esto):

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

¡WTF, dices! Bueno, sí, pero hay algunos puntos realmente útiles aquí. En primer lugar, su primer fixargumento debería ser normalmente una función que es el caso 'recurse' y el segundo argumento son los datos sobre los que actuar. Aquí está el mismo código que una función nombrada:

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

Si todavía está confundido, quizás el factorial sea un ejemplo más fácil:

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

Note la evaluación:

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, ¿acabas de ver eso? Eso se xconvirtió en una función dentro de nuestra thensucursal.

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

En lo anterior, debe recordar x = f x, por lo tanto, los dos argumentos de x 2al final en lugar de solo 2.

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

¡Y me detendré aquí!

Thomas M. DuBuisson
fuente
Tu respuesta es lo que realmente fixtiene sentido para mí. Mi respuesta depende en gran medida de lo que ya ha dicho.
Dan Burton
@ Thomas, ambas secuencias de reducción son incorrectas. :) id xsolo se reduce a x(que luego se reduce de nuevo a id x). - Luego, en la segunda muestra ( fact), cuando el xprocesador se fuerza por primera vez, el valor resultante se recuerda y se reutiliza. El nuevo cálculo de (\recurse ...) xocurriría con la definición de no compartiry g = g (y g) , no con esta definición de compartirfix . - Realicé la edición de prueba aquí . Puede usarla o podría hacer la edición si lo aprueba.
Will Ness
en realidad, cuando fix idse reduce, let x = id x in xtambién fuerza el valor de la aplicación id xdentro del letmarco (thunk), por lo que se reduce a let x = x in x, y este bucle. Lo parece.
Will Ness
Correcto. Mi respuesta es usar el razonamiento ecuacional. Mostrar la reducción a la Haskell, que se ocupa del orden de evaluación, solo sirve para confundir el ejemplo sin ninguna ganancia real.
Thomas M. DuBuisson
1
La pregunta está etiquetada tanto con haskell como con letrec (es decir, let recursiva, con compartir). La distinción entre fixe Y es muy clara e importante en Haskell. No veo de qué sirve mostrar el orden de reducción incorrecto cuando el correcto es aún más corto, mucho más claro y más fácil de seguir, y refleja correctamente lo que realmente está sucediendo.
Will Ness
3

Según tengo entendido, encuentra un valor para la función, de modo que genera lo mismo que le das. El problema es que siempre elegirá indefinido (o un bucle infinito, en haskell, los bucles indefinidos e infinitos son lo mismo) o lo que tenga más indefinidos. Por ejemplo, con id,

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

Como puede ver, undefined es un punto fijo, así que fixlo elegiremos. Si en cambio lo hace (\ x-> 1: x).

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

Así fixque no puedo elegir indefinido. Para hacerlo un poco más conectado a bucles infinitos.

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

Nuevamente, una pequeña diferencia. Entonces, ¿qué es el punto fijo? Probemos 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

¡Es lo mismo! Dado que este es el único punto fijo, fixdebe asentarse en él. Lo siento fix, no hay bucles infinitos o indefinidos para ti.

PyRulez
fuente