Finite trees as initial algebra

In the last Theory Lunch session I talked about a category theoretic approach to finite trees. I presented an interesting procedure in the analysis of syntax and semantics of programming languages and formal languages in general, that is to focus the attention on the abstract representation of the syntax as the initial object in the category of algebras for an endofunctor. In this way any object in the category can be seen as a possible interpretation of the syntax and the unique morphisms from the initial algebra, usually called catamorphisms, can be seen as meaning functions.

A signature is a ranked alphabet \Sigma, i.e. \Sigma is a set together with a function \rho : \Sigma \rightarrow \mathbb{N} called arity. The elements of \Sigma are called function symbols.
A tree on the signature \Sigma is a partial function t : \mathbb{N}^* \rightharpoonup \Sigma such that

  • \varepsilon \in Dom(t);
  • if \alpha, \beta \in \mathbb{N}^*, \alpha\beta \in Dom(t) then \alpha \in Dom(t);
  • if t(\alpha) = f then, for every i \in \mathbb{N}, \alpha i \in Dom(t) iff i \le \rho(f).

As an example consider what follows. Let \Sigma = \{ a,b,c,d,e \} with \rho(a) = 2, \rho(b) = \rho(c) =1, \rho(d) = \rho(e) = 0. A possible tree on \Sigma is t(\varepsilon) = a, t(0) = b, t(00) = d, t(1) = c, t(10) = c, t(100) = e. We represent this tree as the string   a(bd,cce). In general we represent a tree with root f and direct subtrees t_1,\dots,t_{\rho(f)} as f(t_1,\dots,t_{\rho(f)}). Note that every tree on \Sigma can be represented in this way. We call M(\Sigma) the set of finite trees on the signature \Sigma.

Let \mathcal{C} be a category and F: \mathcal{C} \rightarrow \mathcal{C} an endofunctor. An algebra for F is a pair (A,a) where A is an object of \mathcal{C} and a: FA \rightarrow A is an arrow in \mathcal{C}. A morphism of algebras \pi : (A,a) \rightarrow (B,b)  is an arrow \pi : A \rightarrow B in \mathcal{C} such that \pi \circ a = b \circ F(\pi). Given an endofunctor F, algebras for F and related morphisms form a category.

Now we show that M(\Sigma) is an algebra for the functor F: Set \rightarrow Set,

F (A) = \sum_{f \in \Sigma} A^{\rho(f)}.

Note that every map a: FA \rightarrow A is actually a collection of maps [ a_f]_{f \in \Sigma} such that a_f : A^{\rho(f)} \rightarrow A, and if c \in \Sigma is a costant, i.e. has arity 0, then a_c is just an element of A. The map that makes M(\Sigma) an algebra for F is a_f (t_1,\dots,t_{\rho(f)}) = t' where

  • t'(\varepsilon) = f;
  • t'(\alpha i)=t_i (\alpha), for every i \le \rho(f);
  • t'(\alpha) undefined otherwise.

Basically a_f(t_1,\dots,t_{\rho(f)}) = f(t_1,\dots,t_{\rho(f)}), so a represents the standard operation for constructing a new tree from a function symbol f and a set of trees with cardinality \rho(f). Moreover M(\Sigma) is the initial object in the category of algebras for F, so is the initial algebra for F. We just need to find the catamorphisms. Let (B,b) be an algebra for F, then we define \pi : (M(\Sigma),a) \rightarrow (B.b) recursively as follows:

\pi(f(t_1,\dots,t_{\rho(f)}) = b_f (\pi(t_1),\dots,\pi(t_{\rho(f)})).

Note that \pi is well defined because we are dealing with finite trees. So for every finite tree t, \pi(t) depends on the values of \pi on constants c \in \Sigma, \pi(c) = b_c, and these values are univocally determined by b. Also it’s easy to see that \pi is a morphism of algebras and that is unique.


One thought on “Finite trees as initial algebra

  1. I was wondering if, instead of characterizing trees as partial functions from N* to Sigma (satisfying the given three conditions) one could characterize them simply as elements of Sigma* satisfying:

    1) the empty word in Sigma is a tree (ie the tree consisting of a single vertex)
    2) if t_1, t_2, … , t_n are trees and if f is a letter (ie an element of Sigma) with arity n, then the word f t_1 t_2 … t_n is a tree
    3) that’s all

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s