uso recorrido partir grado estructura ejemplos datos construir clasificacion binarios binario arboles arbol haskell zipper comonad

haskell - recorrido - ¿Cómo hacer una cremallera de árbol binario una instancia de Comonad?



grado de un arbol (1)

En el cálculo diferencial, la notación de Leibniz causa menos confusión que la de Newton porque es explícita acerca de la variable con respecto a la cual nos diferenciamos. Los contextos en las cosas se dan por diferenciación, por lo que debemos cuidar lo que se contextualiza. Aquí, hay dos nociones de "subestructura" en el trabajo: subárboles y elementos . Cada uno tiene nociones diferentes (pero relacionadas) de "contexto" y, por lo tanto, de "cremallera", donde una cremallera es el par de una cosa y su contexto.

Su tipo BTZ se presenta como la noción de cremallera para subárboles . Sin embargo, la construcción comonadic de cremallera funciona en cremalleras para elementos : extract significa "dar elemento aquí"; duplicate significa "decorar cada elemento con su contexto". Así que necesitas contextos de elementos. Confusamente, para estos árboles binarios, las cremalleras de elementos y las cremalleras de subárbol son isomorfas, pero esto se debe a una razón muy particular (es decir, que forman una comuna de cofree).

En general, las cremalleras de elementos y subárboles difieren, por ejemplo, para listas. Si comenzamos por construir el comonad de cremallera de elementos para las listas, es menos probable que nos perdamos cuando regresemos a los árboles. Déjame intentar también completar un poco más de la imagen general, tanto para los demás como para ti.

Contextos Sublistas

Los subconjuntos de la sublista para [a] solo están dados por [a] , siendo la lista de elementos que pasamos al salir de la sublista a la lista completa. El contexto sublista para [3,4] en [1,2,3,4] es [2,1] . Los contextos de subnodo para datos recursivos son siempre listas que representan lo que se ve en la ruta desde el nodo hasta la raíz. El tipo de cada paso viene dado por la derivada parcial de la fórmula para un nodo de datos con respecto a la variable recursiva. Asi que aqui

[a] = t where -- t is the recursive variable standing for [a] t = 1 + a*t -- lists of a are either [] or an (a : t) pair ∂/∂t (1 + a*t) = a -- that''s one step on a path from node to root sublist contexts are [a] -- a list of such steps

Así que una sublista-cremallera es un par.

data LinLZ a = LinLZ { subListCtxt :: [a] , subList :: [a] }

Podemos escribir la función que conecta una sublista de nuevo en su contexto, retrocediendo la ruta

plugLinLZ :: LinLZ a -> [a] plugLinLZ (LinLZ { subListCtxt = [], subList = ys}) = ys plugLinLZ (LinLZ { subListCtxt = x : xs, subList = ys}) = plugLinLZ (LinLZ { subListCtxt = xs, subList = x : ys})

Pero no podemos hacer de LinLZ un Comonad , porque (por ejemplo) de

LinLZ { subListCtxt = [], subList = [] }

no podemos extract un elemento (una a de LinLZ a ), solo una lista secundaria.

Enumerar los contextos de los elementos

Un contexto de elemento de lista es un par de listas: los elementos antes del elemento en foco y los elementos después de él. Un contexto de elemento en una estructura recursiva es siempre un par: primero proporcione el subnodo-contexto para el subnodo donde se almacena el elemento, luego proporcione el contexto para el elemento en su nodo. Obtenemos el contexto del elemento en su nodo al diferenciar la fórmula de un nodo con respecto a la variable que representa los elementos.

[a] = t where -- t is the recursive variable standing for [a] t = 1 + a*t -- lists of a are either [] or an (a : t) pair ∂/∂a (1 + a*t) = t = [a] -- the context for the head element is the tail list

Así que un elemento de contexto está dado por un par

type DL a = ( [a] -- the sublist context for the node where the element is , [a] -- the tail of the node where the element is )

y un elemento de cremallera se da al vincular dicho contexto con el elemento "en el orificio".

data ZL a = ZL { this :: a , between :: DL a } deriving (Show, Eq, Functor)

Puede convertir una cremallera de este tipo en una lista (salir "de un elemento") reconstituyendo primero la sublista donde se encuentra el elemento, dándonos una cremallera sublista, y luego conectando la sublista en su contexto sublista.

outZL :: ZL a -> [a] outZL (ZL { this = x, between = (zs, xs) }) = plugLinLZ (LinLZ { subListCtxt = zs, subList = x : xs })

Poniendo cada elemento en contexto

Dada una lista, podemos emparejar cada elemento con su contexto. Obtenemos la lista de formas en que podemos "entrar" en uno de los elementos. Empezamos así,

into :: [a] -> [ZL a] into xs = moreInto (LinLZ { subListCtxt = [], subList = xs })

pero el trabajo real lo realiza la función auxiliar que funciona en una lista en contexto.

moreInto :: LinLZ a -> [ZL a] moreInto (LinLZ { subListCtxt = _, subList = [] }) = [] moreInto (LinLZ { subListCtxt = zs, subList = x : xs }) = ZL { this = x, between = (zs, xs) } : moreInto (LinLZ { subListCtxt = x : zs, subList = xs })

Observe que la salida hace eco de la forma de la subList actual. Además, la cremallera en el lugar de x tiene this = x . Además, la cremallera generadora para decorar xs tiene subList = xs y el contexto correcto, registrando que hemos pasado más allá de x . Pruebas,

into [1,2,3,4] = [ ZL {this = 1, between = ([],[2,3,4])} , ZL {this = 2, between = ([1],[3,4])} , ZL {this = 3, between = ([2,1],[4])} , ZL {this = 4, between = ([3,2,1],[])} ]

Estructura comónica para cremalleras de elementos de lista.

Hemos visto cómo salir de un elemento, o hacia uno de los elementos disponibles. La estructura comonádica nos dice cómo movernos entre elementos, ya sea quedándonos donde estamos o moviéndonos hacia uno de los otros.

instance Comonad ZL where

El extract nos da el elemento que estamos visitando.

extract = this

Para duplicate una cremallera, reemplazamos el elemento actual x con toda la cremallera actual zl (cuyo this = x ) ...

duplicate zl@(ZL { this = x, between = (zs, ys) }) = ZL { this = zl

... y nos abrimos paso a través del contexto, mostrando cómo reenfocar en cada elemento. Nuestro moreInto existente nos permite movernos hacia adentro, pero también debemos movernos outward ...

, between = ( outward (LinLZ { subListCtxt = zs, subList = x : ys }) , moreInto (LinLZ { subListCtxt = x : zs, subList = ys }) ) }

... lo que implica viajar de regreso a lo largo del contexto, mover elementos a la sublista, como sigue

where outward (LinLZ { subListCtxt = [], subList = _ }) = [] outward (LinLZ { subListCtxt = z : zs, subList = ys }) = ZL { this = z, between = (zs, ys) } : outward (LinLZ { subListCtxt = zs, subList = z : ys })

Así obtenemos

duplicate ZL {this = 2, between = ([1],[3,4])} = ZL { this = ZL {this = 2, between = ([1],[3,4])} , between = ( [ ZL {this = 1, between = ([],[2,3,4])} ] , [ ZL {this = 3, between = ([2,1],[4])} , ZL {this = 4, between = ([3,2,1],[])} ] ) }

donde this es "permanecer en 2 " y estamos between "movernos a 1 " y "movernos a 3 o movernos a 4 ".

Entonces, la estructura comonádica nos muestra cómo podemos movernos entre diferentes elementos ubicados dentro de una lista. La estructura sublista juega un papel clave en la búsqueda de los nodos donde se encuentran los elementos, pero la estructura de la cremallera duplicate d es una cremallera del elemento .

Entonces, ¿qué pasa con los árboles?

Digresión: los árboles etiquetados son comonads ya

Permítanme refactorizar su tipo de árboles binarios para resaltar alguna estructura. Literalmente, vamos a sacar el elemento que etiqueta una hoja o un tenedor como un factor común. También aislemos el functor ( TF ) que explica esta estructura de subárbol hoja-o-tenedor.

data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor) data BT a = a :& TF (BT a) deriving (Show, Eq, Functor)

Es decir, cada nodo de árbol tiene una etiqueta, ya sea una hoja o un tenedor.

Dondequiera que tengamos la estructura de que cada nodo tiene una etiqueta y un blob de subestructuras, tenemos un comonad: el comonad cofree . Déjame refactorizar un poco más, abstrayendo TF ...

data CoFree f a = a :& f (CoFree f a) deriving (Functor)

... así que tenemos una f general donde teníamos TF antes. Podemos recuperar nuestros árboles específicos.

data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor) type BT = CoFree TF deriving instance Show a => Show (BT a) deriving instance Eq a => Eq (BT a)

Y ahora, de una vez por todas, podemos dar la construcción de comonad cofree. Como cada subárbol tiene un elemento raíz, cada elemento puede decorarse con el árbol cuya raíz es.

instance Functor f => Comonad (CoFree f) where extract (a :& _) = a -- extract root element duplicate t@(a :& ft) = t :& fmap duplicate ft -- replace root element by whole tree

Vamos a tener un ejemplo

aTree = 0 :& Fork ( 1 :& Fork ( 2 :& Leaf , 3 :& Leaf ) , 4 :& Leaf ) duplicate aTree = (0 :& Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf)) :& Fork ( (1 :& Fork (2 :& Leaf,3 :& Leaf)) :& Fork ( (2 :& Leaf) :& Leaf , (3 :& Leaf) :& Leaf ) , (4 :& Leaf) :& Leaf )

¿Ver? ¡Cada elemento ha sido emparejado con su subárbol!

Las listas no dan lugar a una combinación de cónyuges, porque no todos los nodos tienen un elemento: específicamente, [] no tiene ningún elemento. En una asociación de café, siempre hay un elemento en el que estás y puedes ver más abajo en la estructura del árbol, pero no más arriba .

En una comonad de cremallera de elemento, siempre hay un elemento donde se encuentra, y puede ver tanto hacia arriba como hacia abajo.

Subárbol y contextos de elementos en árboles binarios.

Algebraicamente

d/dt (TF t) = d/dt (1 + t*t) = 0 + (1*t + t*1)

para que podamos definir

type DTF t = Either ((), t) (t, ())

diciendo que un subárbol dentro de la "burbuja de subestructuras" está a la izquierda oa la derecha. Podemos comprobar que "enchufar" funciona.

plugF :: t -> DTF t -> TF t plugF t (Left ((), r)) = Fork (t, r) plugF t (Right (l, ())) = Fork (l, t)

Si creamos una instancia de t y emparejamos con la etiqueta del nodo, obtenemos un paso del contexto del subárbol

type BTStep a = (a, DTF (BT a))

Lo cual es isomorfo a Partial en la pregunta.

plugBTinBT :: BT a -> BTStep a -> BT a plugBTinBT t (a, d) = a :& plugF t d

Por lo tanto, [BTStep a] subárbol para un BT a dentro de otro.

Pero ¿qué pasa con un elemento de contexto? Bueno, cada elemento etiqueta un subárbol, por lo que debemos registrar tanto el contexto de ese subárbol como el resto del árbol etiquetado por el elemento.

data DBT a = DBT { below :: TF (BT a) -- the rest of the element''s node , above :: [BTStep a] -- the subtree context of the element''s node } deriving (Show, Eq)

Molesto, tengo que rodar mi propia instancia de Functor .

instance Functor DBT where fmap f (DBT { above = a, below = b }) = DBT { below = fmap (fmap f) b , above = fmap (f *** (either (Left . (id *** fmap f)) (Right . (fmap f *** id)))) a }

Ahora puedo decir qué es un elemento cremallera.

data BTZ a = BTZ { here :: a , ctxt :: DBT a } deriving (Show, Eq, Functor)

Si estás pensando "¿qué hay de nuevo?", Tienes razón. Tenemos un contexto de subárbol, above , junto con un subárbol dado por here y below . Y eso es porque los únicos elementos son aquellos que etiquetan los nodos. Dividir un nodo en un elemento y su contexto es lo mismo que dividirlo en su etiqueta y su blob de subestructuras. Es decir, obtenemos esta coincidencia para los comandos de café, pero no en general.

Sin embargo, esta coincidencia es solo una distracción! Como vimos con las listas, no necesitamos que las cremalleras de elementos sean lo mismo que las cremalleras de subnodo para hacer que las cremalleras de elementos sean un elemento común.

Siguiendo el mismo patrón que las listas anteriores, podemos decorar cada elemento con su contexto. El trabajo se realiza mediante una función auxiliar que acumula el contexto del subárbol que estamos visitando actualmente.

down :: BT a -> BT (BTZ a) down t = downIn t [] downIn :: BT a -> [BTStep a] -> BT (BTZ a) downIn (a :& ft) ads = BTZ { here = a, ctxt = DBT { below = ft, above = ads } } :& furtherIn a ft ads

Tenga en cuenta que a se reemplaza por una cremallera enfocada en a . Los subárboles son manejados por otro ayudante.

furtherIn :: a -> TF (BT a) -> [BTStep a] -> TF (BT (BTZ a)) furtherIn a Leaf ads = Leaf furtherIn a (Fork (l, r)) ads = Fork ( downIn l ((a, Left ((), r)) : ads) , downIn r ((a, Right (l, ())) : ads) )

Vea que furtherIn conserva la estructura de árbol, pero crece el contexto del subárbol adecuadamente cuando visita un subárbol.

Vamos a verificarlo

down aTree = BTZ { here = 0, ctxt = DBT { below = Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf), above = []}} :& Fork ( BTZ { here = 1, ctxt = DBT { below = Fork (2 :& Leaf,3 :& Leaf), above = [(0,Left ((),4 :& Leaf))]}} :& Fork ( BTZ { here = 2, ctxt = DBT { below = Leaf, above = [(1,Left ((),3 :& Leaf)),(0,Left ((),4 :& Leaf))]}} :& Leaf , BTZ { here = 3, ctxt = DBT { below = Leaf, above = [(1,Right (2 :& Leaf,())),(0,Left ((),4 :& Leaf))]}} :& Leaf ) , BTZ { here = 4, ctxt = DBT { below = Leaf, above = [(0,Right (1 :& Fork (2 :& Leaf,3 :& Leaf),()))]}} :& Leaf)

¿Ver? Cada elemento está decorado con todo su contexto, no solo el árbol debajo de él.

Cremalleras de árboles binarios forman un Comonad.

Ahora que podemos decorar elementos con sus contextos, construyamos la instancia de Comonad . Como antes...

instance Comonad BTZ where extract = here

... el extract nos dice el elemento en foco, y podemos hacer uso de nuestra maquinaria existente para ir más lejos en el árbol, pero necesitamos construir un nuevo kit para explorar las formas en que podemos avanzar.

duplicate z@(BTZ { here = a, ctxt = DBT { below = ft, above = ads }}) = BTZ { here = z , ctxt = DBT { below = furtherIn a ft ads -- move somewhere below a , above = go_a (a :& ft) ads -- go above a } } where

Para salir, al igual que con las listas, debemos retroceder por el camino hacia la raíz. Al igual que con las listas, cada paso en el camino es un lugar que podemos visitar.

go_a t [] = [] go_a t (ad : ads) = go_ad t ad ads : go_a (plugBTinBT t ad) ads go_ad t (a, d) ads = ( BTZ { here = a, ctxt = DBT { below = plugF t d, above = ads } } -- visit here , go_d t a d ads -- try other subtree )

A diferencia de las listas, hay ramas alternativas a lo largo de ese camino para explorar. Donde sea que el camino almacene un subárbol no visitado, debemos decorar sus elementos con sus contextos.

go_d t a (Left ((), r)) ads = Left ((), downIn r ((a, Right (t, ())) : ads)) go_d t a (Right (l, ())) ads = Right (downIn l ((a, Left ((), t)) : ads), ())

Así que ahora hemos explicado cómo reenfocar desde cualquier posición de elemento a cualquier otra.

Veamos. Aquí estábamos visitando 1 :

duplicate (BTZ {here = 1, ctxt = DBT { below = Fork (2 :& Leaf,3 :& Leaf), above = [(0,Left ((),4 :& Leaf))]}}) = BTZ {here = BTZ {here = 1, ctxt = DBT { below = Fork (2 :& Leaf,3 :& Leaf), above = [(0,Left ((),4 :& Leaf))]}}, ctxt = DBT { below = Fork (BTZ {here = 2, ctxt = DBT { below = Leaf, above = [(1,Left ((),3 :& Leaf)),(0,Left ((),4 :& Leaf))]}} :& Leaf ,BTZ {here = 3, ctxt = DBT { below = Leaf, above = [(1,Right (2 :& Leaf,())),(0,Left ((),4 :& Leaf))]}} :& Leaf ), above = [(BTZ {here = 0, ctxt = DBT { below = Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf), above = []}} ,Left ((),BTZ {here = 4, ctxt = DBT { below = Leaf, above = [(0,Right (1 :& Fork (2 :& Leaf,3 :& Leaf),()))]}} :& Leaf) ) ]}}

Para probar las leyes de Comonad en una pequeña muestra de datos, verifiquemos:

fmap (/ z -> extract (duplicate z) == z) (down aTree) = True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf) fmap (/ z -> fmap extract (duplicate z) == z) (down aTree) = True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf) fmap (/ z -> fmap duplicate (duplicate z) == duplicate (duplicate z)) (down aTree) = True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf)

Quiero hacer una cremallera de árbol binario en una instancia de Comonad, pero no puedo encontrar la forma de implementar el duplicate correctamente.

Aquí está mi intento:

{-# LANGUAGE DeriveFunctor #-} import Data.Function import Control.Arrow import Control.Comonad data BinTree a = Leaf a | Branch a (BinTree a) (BinTree a) deriving (Functor, Show, Eq) data Dir = L | R deriving (Show, Eq) -- an incomplete binary tree, aka data context data Partial a = Missing Dir (BinTree a) a deriving (Show, Eq, Functor) -- BTZ for BinTree Zipper newtype BTZ a = BTZ { getBTZ :: ([Partial a], BinTree a) } deriving (Show, Eq) instance Functor BTZ where fmap f (BTZ (cs,t)) = BTZ (map (fmap f) cs, fmap f t) -- | replace every node label with the zipper focusing on that node dup :: BinTree a -> BinTree (BTZ a) dup (Leaf v) = Leaf (BTZ ([], Leaf v)) dup t@(Branch v tl tr) = Branch (BTZ ([],t)) tlZ trZ where tlZ = fmap (BTZ . first (++ [Missing L tr v]) . getBTZ) (dup tl) trZ = fmap (BTZ . first (++ [Missing R tl v]) . getBTZ) (dup tr) -- | extract root label rootVal :: BinTree a -> a rootVal (Leaf v) = v rootVal (Branch v _ _) = v -- | move zipper focus around goUp, goLeft, goRight :: BTZ a -> BTZ a goUp (BTZ ([], _)) = error "already at root" goUp (BTZ (Missing wt t2 v:xs, t1)) = case wt of L -> BTZ (xs, Branch v t1 t2) R -> BTZ (xs, Branch v t2 t1) goLeft z = let (cs,t) = getBTZ z in case t of Leaf _ -> error "already at leaf" Branch v t1 t2 -> BTZ (Missing L t2 v:cs, t1) goRight z = let (cs,t) = getBTZ z in case t of Leaf _ -> error "already at leaf" Branch v t1 t2 -> BTZ (Missing R t1 v:cs, t2) instance Comonad BTZ where extract (BTZ (_,t)) = case t of Leaf v -> v Branch v _ _ -> v duplicate z@(BTZ (cs, bt)) = case bt of Leaf _ -> BTZ (csZ, Leaf z) -- extract . duplicate = id Branch v tl tr -> -- for each subtree, use "dup" to build zippers, -- and attach the current focusing root(bt) and rest of the data context to it let tlZ = fmap (BTZ . first (++Missing L tr v :cs) . getBTZ) (dup tl) trZ = fmap (BTZ . first (++Missing R tl v :cs) . getBTZ) (dup tr) in BTZ (csZ, Branch z tlZ trZ) where -- go up and duplicate, we''ll have a "BTZ (BTZ a)" -- from which we can grab "[Partial (BTZ a)]" out -- TODO: not sure if it works upZippers = take (length cs-1) . tail $ iterate goUp z csZ = fmap (head . fst . getBTZ . duplicate) upZippers main :: IO () main = do let tr :: BTZ Int tr = rootVal $ dup (Branch 1 (Leaf 2) (Branch 3 (Leaf 4) (Leaf 5))) equalOnTr :: Eq a => (BTZ Int -> a) -> (BTZ Int -> a) -> Bool equalOnTr = (==) `on` ($ tr) print $ (extract . duplicate) `equalOnTr` id print $ (fmap extract . duplicate) `equalOnTr` id print $ (duplicate . duplicate) `equalOnTr` (fmap duplicate . duplicate)

Alguna explicación:

  • BinTree a es el tipo de datos del árbol binario y cada nodo del árbol contiene una etiqueta.
  • Partial a es un árbol binario con subárbol izquierdo o derecho. Una pila de Partial a en mi código desempeña el papel de contexto de datos.
  • BTZ significa la cremallera de BinTree , que quiero hacer una instancia de Comonad , que consiste en un contexto de datos y el subárbol de enfoque.

Para convertirlo en una instancia de Comonad , mi plan es implementar extract y duplicate , y verificar si las propiedades de Comonad se mantienen al tomar algunos árboles binarios aleatorios.

El extract es sencillo, simplemente sacando el subárbol de enfoque.

La función dup sirve como una función auxiliar que reemplaza cada etiqueta de nodo con la cremallera del árbol enfocada en ese nodo.

Para duplicate z , la etiqueta del nodo debe ser z sí para que se extract . duplicate == id extract . duplicate == id retiene. Para los nodos sin hojas, uso dup para tratar sus subárboles como si no tuvieran padres, y el enfoque actual de z el resto del contexto de datos se adjunta a estas cremalleras después.

Hasta ahora, las dos primeras propiedades de Comonad están satisfechas ( extract . duplicate = id y fmap extract . duplicate ), pero no tengo idea de qué hacer con el contexto de datos. Lo que actualmente hago es tomar la cremallera z y seguir subiendo. En el camino tomamos la parte superior de cada pila de contexto de datos para construir la nueva pila de contexto de datos, lo que parece correcto y también es del tipo correcto ( [Partial (BTZ a)] . Pero mi enfoque no puede satisfacer la tercera ley.

Dada la definición de tipo de datos de la cremallera del árbol binario anterior, ¿es posible convertirla en una instancia de Comonad? Si la respuesta es sí, ¿hay algún problema con mi enfoque?