Listas de iglesias en Haskell

lambda-calculus church-encoding

Question

Tuve que implementar la función de mapa de haskell para trabajar con listas de iglesias que se definen de la siguiente manera:

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

En el cálculo lambda, las listas se codifican 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 sé cómo crear esa 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 entender y resolver tales problemas para mi examen la próxima semana. ¿Podría alguien, por favor, darme una buena fuente donde pueda aprender a resolver tales problemas o darme una pequeña guía sobre cómo funciona?

Answer 1

Así que comencemos por codificar los dos constructores de listas, usando su ejemplo como referencia:

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

[] es el final del constructor de listas, y podemos sacar eso directamente del ejemplo. [] ya tiene significado en haskell, así que llamemos 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, considere el propósito de la función de mapa: es aplicar la función dada a cada elemento de la lista. Así que veamos cómo funciona eso para cada uno de los constructores.

nil no tiene elementos, por lo que mapChurch f nil debería ser 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 lista, por lo que, para que mapChurch f funcione correctamente, debe aplicar f al elemento y mapChurch f al resto de la lista. Es decir, mapChurch f (cons x xs) debe ser igual que cons (fx) (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)

Por lo tanto, dado que todas las listas se hacen a partir de esos dos constructores, y mapChurch funciona en ambos como se espera, mapChurch debe funcionar como se espera en todas las listas.

Answer 2

Bueno, podemos comentar el tipo Churchlist de esta manera para 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 esto está íntimamente relacionado 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 funciones de lista. Un ejemplo trivial que te ayudará es implementar una copia de lista con foldr :

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

Usando el tipo comentado anteriormente, foldr (:) [] significa esto: "si ve una lista vacía, devuelva la lista vacía, y si ve una head:tailResult retorno de par head:tailResult ".

Usando Churchlist , puedes escribir fácilmente la contraparte 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 el map , solo necesita reemplazar los cons con una función adecuada, como esta:

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 textualmente, se aplica f a cada uno de ellos.

Estudia todo esto con cuidado, y deberías poder escribir mapChurchlist :: (t -> t'') -> Churchlist tu -> Churchlist t'' u por tu cuenta.

Ejercicio adicional (fácil): escriba estas funciones de lista en términos de foldr , y escriba las contrapartes para 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 tienes ganas de enfrentarte a algo más difícil, intenta escribir tail para Churchlist . (Comience escribiendo la tail para [a] usando foldr .)

Answer 3

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 "pliegue". Las listas de enlaces individuales inmutables usualmente se definen List a = Cons a (List a) | Nil List a = Cons a (List a) | Nil , lo que significa que las únicas formas en que puede construir una lista es Nil o Cons anElement anotherList . Si lo escribe en estilo lisp, donde c es Cons y n es Nil , entonces la lista [1,2,3] ve así:

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

Cuando realiza un pliegue sobre una lista, simplemente proporcione sus propios " Cons " y " Nil " para reemplazar los de la lista. En Haskell, la función de biblioteca para esto es foldr

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

¿Parecer familiar? Saque la [a] y tendrá el mismo tipo que Churchlist ab . Como dije, la codificación de la iglesia representa las listas como su función de plegado.

Así que el ejemplo define el map . Observe cómo se usa l como una función: es la función que se pliega sobre alguna lista, después de todo. /cn -> l (cf) n básicamente dice "reemplazar 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))

Debería ser evidente ahora que esta es de hecho una función de mapeo, porque se parece al original, excepto que 1 convirtió en (f 1) , 2 a (f 2) y 3 a (f 3) .