3
$\begingroup$

I'm reading the paper "Dual of substitution is Redecoration". And I'm struggling with understanding the usage of the word "not-well-founded cotrees".

  1. what is a cotree compared to a tree ? I suspect it is a tree for which all relations are inverted, but it is just my assumption.
  2. what it is to be "well-founded" for a tree, for a cotree.

Probably, to have an insight, it would be helpful to give me examples of a well-founded and of a not-well-founded tree/cotree.

Improve this question
$\endgroup$
3
$\begingroup$

I'm not sure what you mean by "all relations are inverted" (what's the relation of a tree?), but perhaps I can provide some insight.

In Haskell, one might write the type of binary trees as such:

data Tree = Leaf | Node Tree Tree

in the terminology of the paper, the type of "incomplete trees" would then be

data ITree a = Leaf | Node ITree ITree | Var a

allowing for an "incomplete" tree with holes marked by an instance of Var a. The paper observes that the type ITree a forms a monad, where a Var a can be "substituted" with f a given a suitable function f :: a -> ITree b.

Now our intuition is that the type Tree is the type of finite, or well-founded binary trees, of which an example is

 myTree :: Tree
 myTree = Node (Node Leaf Leaf) (Node Leaf Leaf)

However, it is untrue in a language like Haskell that all trees are of this form. Indeed, following definition is perfectly acceptable:

infTree :: Tree
infTree = Node infTree infTree

intuitively, this tree represents the infinite "full" binary tree. So really the type Tree may contain either finite binary trees, or trees which may contain infinite paths. Such trees are called non-well founded trees.

So, in Haskell, the type Tree is in reality the type of co-trees, which allows such elements as infTree. This may be a bit confusing, since we rarely think about such elements when considering that type.

Hopefully this provides useful intuition.

The main observation of the paper, is that the type of co-trees has a construction dual to that if ITree, which one might call DTree, defined as

 DTree a = DLeaf a | DNode a (DTree a) (DTree a)

such that we can define a comonad structure:

extract :: DTree a -> a
extract (DLeaf a) = a
extract (DNode a _ _) = a

duplicate :: DTree a -> DTree (DTree a)
duplicate (DLeaf a) = DLeaf (DLeaf a)
duplicate (DNode a l r) = DNode (DNode a l r) (duplicate l) (duplicate r)

The paper goes on to explain some intuition about this structure and why it should be considered as interesting.

Oh by the way, the paper you are reading seems pretty heavy in abstract nonsense, and if you're coming from the CS side of things, you might want to take a look at these blog posts first:

https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/

http://5outh.blogspot.com/2013/01/comonads.html

Improve this answer
$\endgroup$
  • $\begingroup$ "What's the relation in a tree ?" It may be naive, but I was thinking of this relationship: Parent to Children nodes. The assumed inverted/dual structure would have been a graph, with lots of parents/roots and each could have only one child, but this child can have several/numerous parent nodes. The graph is terminated on a unique leaf which would be the final unique child ( dual to the unique root of a normal tree). That was an assumption :-) $\endgroup$ – Stephane Rolland Jun 1 '18 at 13:31
  • 1
    $\begingroup$ @StephaneRolland I see. In this case however, cotrees have the same "shape" as trees, just potentially infinite paths in them. $\endgroup$ – cody Jun 1 '18 at 18:33
  • $\begingroup$ Shouldn't "incomplete trees" be defined by Node ITree ITree | Var a (i.e. without the initial Leaf in the second code box above?) $\endgroup$ – Luciano Jan 17 '20 at 7:51
  • $\begingroup$ @Luciano No, in this case, "incomplete trees" really means "potentially incomplete trees". In particular, a tree without variables is also an incomplete tree. $\endgroup$ – cody Jan 17 '20 at 14:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.