Comportamiento eta-reducción

Comportamiento eta-reducción

de Ian Ignacy Arazny Casanovas -
Número de respuestas: 1

Buenas tardes, quería consultar respecto al comportamiento esperado para el siguiente ejemplo de eta-reducción dado que no me queda del todo claro el comportamiento

Para el siguiente ejemplo:

  f5 = \x -> \y -> f x y

El resultado esperado debería ser:

  No hay sugerencias ( pues y está libre en f x),

ó por lo contrario se podría empezar por el lambda más interno \y -> f x y sustituyendo por f x y luego sustituyendo \x -> f x por f.

De otra forma, cómo se debería aplicar la reducción?

Muchas gracias, 

Saludos, 

Ian.

En respuesta a Ian Ignacy Arazny Casanovas

Re: Comportamiento eta-reducción

de Marcos Viera - InCo -
Hola,

Para ese caso las sugerencias deberían de ser:

Función: f5
**Sugerencia para:
\y -> f x y
Usar eta-reducción. Reemplazar por:
f x
**Sugerencia para:
\x -> f x
Usar eta-reducción. Reemplazar por:
f
--------------------------------------------------------------------------------

La función f5 es equivalente a:

f5 = \x -> (\y -> (f x) y)

Entonces la primera eta-reducción que se va a sugerir es la más interna:
\y -> (f x) y ==> f x
notar que y no ocurre libre en la expresión (f x).

Luego, si reescribimos f5 según la sugerencia como
f5 = \x -> f x

tenemos la posibilidad de hacer otra eta-reducción:
f5 = f


saludos