Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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".
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.
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/
Node ITree ITree | Var a (i.e. without the initial Leaf in the second code box above?)
$\endgroup$
– Luciano
Jan 17 at 7:51
