Lo que hace esto combinador hacer: s (SK)

Ahora entiendo la firma tipo de s (s k):Lo que hace esto combinador hacer: s (SK)

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1

Y puede crear ejemplos que funcionan sin error en la herramienta de Haskell WinGHCi:

Ejemplo:

s (s k) (\g -> 2) (\x -> 3)

vuelve 2.

Ejemplo:

s (s k) (\g -> g 3) successor

rendimientos 4.

donde successor se define como así:

successor = (\x -> x + 1)

No obstante, todavía no tengo una sensación intuitiva s (s k) para lo hace.

El combinador s (s k) toma dos funciones f y g. ¿Qué hace s (s k) con f y g? ¿Me daría la imagen completa en lo que s (s k) hace por favor?

Fuente

2012-03-12 Roger Costello

Falta la definición para 'S (S K)'. ¿Es este el mismo 's' y' k' en http://stackoverflow.com/questions/9592191/the-type-signature-of-a-combinator-does-not-match-the-type-signature-of- ¿es-equi? –

Por cierto, ¿qué es intuitivo? ¿Has encontrado http://en.wikipedia.org/wiki/Ouroboros intuitivo? ¿Te imaginas que una serpiente se come a sí misma y se desvanece? ¿O un robot que se construye a sí mismo? Necesitas tener mejor sentido sobre algo que actúa sobre sí mismo. –

Bien, veamos qué significa S (S K). Voy a utilizar estas definiciones:

S = \x y z -> x z (y z) 
K = \x y -> x 

S (S K) = (\x y z -> x z (y z)) ((\x y z -> x z (y z)) (\a b -> a)) -- rename bound variables in K 
     = (\x y z -> x z (y z)) (\y z -> (\a b -> a) z (y z)) -- apply S to K 
     = (\x y z -> x z (y z)) (\y z -> (\b -> z) (y z)) -- apply K to z 
     = (\x y z -> x z (y z)) (\y z -> z) -- apply (\_ -> z) to (y z) 
     = (\x y z -> x z (y z)) (\a b -> b) -- rename bound variables 
     = (\y z -> (\a b -> b) z (y z)) -- apply S to (\a b -> b) 
     = (\y z -> (\b -> b) (y z)) -- apply (\a b -> b) to z 
     = (\y z -> y z) -- apply id to (y z)

Como se puede ver, es sólo ($) con el tipo más específico.

Fuente

2012-03-12 10:08:01 Vitus

Otra forma de ver esto: el tipo es '((t1 -> t2) -> t1) -> (t1 -> t2) -> t1'. Al agregar paréntesis, obtenemos '((t1 -> t2) -> t1) -> ((t1 -> t2) -> t1)'. Dejando que el tipo 'α' represente' (t1 -> t2) -> t1', esto es simplemente 'α -> α', y así, por parametricidad,' s (sk) 'es la función de identidad con un tipo. (Y por supuesto, '($) :: (a -> b) -> a -> b' es * también * solo la función de identidad con un tipo más específico.) –

De hecho, si η-reducemos' \ y -> \ z -> yz', obtenemos '\ y -> y'. – Vitus

En los combinadores, S K y z = K z (y z) = z. Entonces S (S K) y z = S K z (y z) = K (y z) (z (y z)) = y z. – rickythesk8r

Lo que hace esto combinador hacer: s (SK)

Respuesta

Cuestiones relacionadas