listas Iglesia en Haskell

Question

que tenían que implementar la función de mapa de Haskell para trabajar con las listas de la iglesia que se definen de la siguiente manera:

type Churchlist t u = (t->u->u)->u->u 

En el cálculo lambda, listas están codificados de la siguiente manera:

[] := λc. λn. n 
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n)) 

La solución de muestra de este ejercicio es:

mapChurch :: (t->s) -> (Churchlist t u) -> (Churchlist s u) 
mapChurch f l = \c n -> l (c.f) n 

No tengo idea de cómo funciona esta solución y no lo hago. Saber cómo crear tal función. Ya tengo experiencia con el cálculo lambda y los números de la iglesia, pero este ejercicio ha sido un gran dolor de cabeza para mí y tengo que ser capaz de comprender y resolver esos problemas para mi examen de la próxima semana. ¿Podría alguien por favor darme una buena fuente donde podría aprender a resolver esos problemas o darme un poco de orientación sobre cómo funciona?

Answer 1

Todas las estructuras de datos de cálculo lambda son, bueno, funciones, porque eso es todo lo que hay en el cálculo lambda. Eso significa que la representación de un booleano, tupla, lista, número o cualquier cosa, tiene que ser alguna función que represente el comportamiento activo de esa cosa.

Para las listas, es un "doblez". Las listas de enlaces individuales inmutables generalmente se definen como List a = Cons a (List a) | Nil, lo que significa que la única manera en que puede crear una lista es Nil o Cons anElement anotherList.Si usted lo escribe en estilo Lisp, donde c es Cons y n es Nil, a continuación, la lista [1,2,3] se ve así:

(c 1 (c 2 (c 3 n))) 

Cuando se realiza un pliegue más de una lista, sólo tiene que proporcionar su propia "Cons "y" Nil "para reemplazar los de la lista. En Haskell, la función de biblioteca para esto es familiar foldr

foldr :: (a -> b -> b) -> b -> [a] -> b 

Look? Saque el [a] y usted tiene exactamente el mismo tipo que Churchlist a b. Como dije, la codificación de iglesias representa listas como su función de plegado.

---

Así que el ejemplo define map. Observe cómo se usa l como función: es la función que se pliega sobre una lista, después de todo. \c n -> l (c.f) n dice básicamente "reemplace cada c con c . f y cada n con n".

(c 1 (c 2 (c 3 n))) 
-- replace `c` with `(c . f)`, and `n` with `n` 
((c . f) 1 ((c . f) 2) ((c . f) 3 n))) 
-- simplify `(foo . bar) baz` to `foo (bar baz)` 
(c (f 1) (c (f 2) (c (f 3) n)) 

Debe ser evidente ahora que esto es de hecho una función de mapeo, porque se ve igual que el original, excepto 1 convirtió en (f 1), 2-(f 2) y 3-.

Answer 2

Así que vamos a empezar mediante la codificación de los dos constructores de la lista, usando tu ejemplo como referencia:

[] := λc. λn. n 
[1,2,3] := λc. λn. c 1 (c 2 (c 3 n)) 

[] es el final de la lista constructor, y podemos levantar esa recta desde el ejemplo. [] ya ha sentido en Haskell, así que vamos a llamar a nuestro nil:

nil = \c n -> n 

El otro constructor que necesitamos toma un elemento y una lista existente y crea una nueva lista. Canónicamente, esto se llama cons, con la definición:

cons x xs = \c n -> c x (xs c n) 

Podemos comprobar que esto es consistente con el ejemplo anterior, ya que

cons 1 (cons 2 (cons 3 nil))) = 
cons 1 (cons 2 (cons 3 (\c n -> n)) = 
cons 1 (cons 2 (\c n -> c 3 ((\c' n' -> n') c n))) = 
cons 1 (cons 2 (\c n -> c 3 n)) = 
cons 1 (\c n -> c 2 ((\c' n' -> c' 3 n') c n)) = 
cons 1 (\c n -> c 2 (c 3 n)) = 
\c n -> c 1 ((\c' n' -> c' 2 (c' 3 n')) c n) = 
\c n -> c 1 (c 2 (c 3 n)) = 

Ahora, tenga en cuenta el propósito de la función de mapa - es para aplicar la función dada a cada elemento de la lista. Entonces veamos cómo funciona eso para cada uno de los constructores.

nil no tiene elementos, por lo mapChurch f nil debe ser sólo nil:

mapChurch f nil 
= \c n -> nil (c.f) n 
= \c n -> (\c' n' -> n') (c.f) n 
= \c n -> n 
= nil 

cons tiene un elemento y un resto de la lista, por lo que, con el fin de mapChurch f para trabajar hotel fenomenal, se debe aplicar f al elemento y mapChurch f para el resto de la lista. Es decir, mapChurch f (cons x xs) debe ser el mismo que cons (f x) (mapChurch f xs).

mapChurch f (cons x xs) 
= \c n -> (cons x xs) (c.f) n 
= \c n -> (\c' n' -> c' x (xs c' n')) (c.f) n 
= \c n -> (c.f) x (xs (c.f) n) 
-- (c.f) x = c (f x) by definition of (.) 
= \c n -> c (f x) (xs (c.f) n) 
= \c n -> c (f x) ((\c' n' -> xs (c'.f) n') c n) 
= \c n -> c (f x) ((mapChurch f xs) c n) 
= cons (f x) (mapChurch f xs) 

Así que desde todas las listas se hacen de esos dos constructores, y mapChurch funciona tanto en ellos como se espera, mapChurch deben funcionar como se espera en todas las listas.

Answer 3

Bueno, podemos comentar el tipo Churchlist esta forma de aclararlo:

-- Tell me... 
type Churchlist t u = (t -> u -> u) -- ...how to handle a pair 
        -> u   -- ...and how to handle an empty list 
        -> u   -- ...and then I'll transform a list into 
            -- the type you want 

Tenga en cuenta que este está íntimamente relacionada con la función foldr:

foldr :: (t -> u -> u) -> u -> [t] -> u 
foldr k z [] = z 
foldr k z (x:xs) = k x (foldr k z xs) 

foldr es una función muy general que puede implementar todo tipo de otras funciones de lista. Un ejemplo trivial que le ayudará a está implementando una copia lista con foldr:

copyList :: [t] -> [t] 
copyList xs = foldr (:) [] xs 

El uso del tipo comentado anteriormente, foldr (:) [] que esto significa: "si ves una lista vacía devuelve la lista vacía, y si ves un par devuelva head:tailResult. "

Usando Churchlist, puede escribir fácilmente la contrapartida de esta manera:

-- Note that the definitions of nil and cons mirror the two foldr equations! 
nil :: Churchlist t u 
nil = \k z -> z 

cons :: t -> Churchlist t u -> Churchlist t u 
cons x xs = \k z -> k x (xs k z) 

copyChurchlist :: ChurchList t u -> Churchlist t u 
copyChurchlist xs = xs cons nil 

Ahora, para implementar map, sólo tiene que sustituir cons con una función adecuada, así:

map :: (a -> b) -> [a] -> [b] 
map f xs = foldr (\x xs' -> f x:xs') [] xs 

El mapeo es como copiar una lista, excepto que en lugar de simplemente copiar los elementos al pie de la letra, aplica f a cada uno de ellos.

Estudie todo esto cuidadosamente, y debería poder escribir mapChurchlist :: (t -> t') -> Churchlist t u -> Churchlist t' u usted mismo.

ejercicio extra (fácil): escribir estas funciones de lista en términos de foldr, y escribir homólogos de Churchlist:

filter :: (a -> Bool) -> [a] -> [a] 
append :: [a] -> [a] -> [a] 

-- Return first element of list that satisfies predicate, or Nothing 
find :: (a -> Bool) -> [a] -> Maybe a 

Si te sientes como hacer frente a algo más difícil, trate de escribir tail para Churchlist. (Empieza por escribir tail de [a] usando foldr.)