Caso 07 y 12, Eta reduccion con variables ligadas por case.

Caso 07 y 12, Eta reduccion con variables ligadas por case.

de Jonathan Nahuel Rodriguez Dores -
Número de respuestas: 2

Hola, el caso 07 tiene la funcion:

qux = \xs -> (\ys -> case ys of [] -> 0; (x : xs) -> 1 + xs) xs

y la sugerencia en caso07-sug es : 

Función: qux
**Sugerencia para:
\xs -> (\ys -> case ys of 
    [] -> 0; 
    (x : xs) -> 1 + xs) xs
Usar eta-reducción. Reemplazar por:
\ys -> case ys of 
    [] -> 0; 
    (x : xs) -> 1 + xs

Sin embargo la eta-reduccion se aplica para la forma /x -> e x
en este caso x = xs;  e =  \ys -> case ys of [] -> 0; (x : xs) -> 1 + xs
Pero xs aparece en e, solo podira estar ligada por \ys, ¿case ys of (x : xs), liga a x y xs junto a ys?

Lo mismo sucede con el caso 12.

**Sugerencia para:
\xs -> (\ls -> case ls of 
    [] -> []; 
    (x : xs) -> x + 1 : incr xs) xs
Usar eta-reducción. Reemplazar por:
\ls -> case ls of 
    [] -> []; 
    (x : xs) -> x + 1 : incr xs

En respuesta a Jonathan Nahuel Rodriguez Dores

Re: Caso 07 y 12, Eta reduccion con variables ligadas por case.

de Marcos Viera - InCo -
Hola,

El xs que aparece dentro del case no ocurre libre, está ligado por el patrón (x:xs). En otras palabras, el xs de e no es el mismo xs que vamos a sacar con la eta-reducción.
Noten que es lo mismo escribir:
\xs -> (\ys -> case ys of
[] -> 0;
(x : xs) -> 1 + xs) xs
que:
\xs -> (\ys -> case ys of
[] -> 0;
(x : zs) -> 1 + zs) xs

saludos