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 , i.e. is a set together with a function called arity. The elements of are called function symbols.
A tree on the signature is a partial function such that
- if then ;
- if then, for every , iff .
As an example consider what follows. Let with . A possible tree on is . We represent this tree as the string . In general we represent a tree with root and direct subtrees as . Note that every tree on can be represented in this way. We call the set of finite trees on the signature .
Let be a category and an endofunctor. An algebra for is a pair where is an object of and is an arrow in . A morphism of algebras is an arrow in such that . Given an endofunctor , algebras for and related morphisms form a category.
Now we show that is an algebra for the functor ,
Note that every map is actually a collection of maps such that , and if is a costant, i.e. has arity 0, then is just an element of . The map that makes an algebra for is where
- , for every ;
- undefined otherwise.
Basically , so represents the standard operation for constructing a new tree from a function symbol and a set of trees with cardinality . Moreover is the initial object in the category of algebras for , so is the initial algebra for . We just need to find the catamorphisms. Let be an algebra for , then we define recursively as follows:
Note that is well defined because we are dealing with finite trees. So for every finite tree , depends on the values of on constants , , and these values are univocally determined by . Also it’s easy to see that is a morphism of algebras and that is unique.