Do "factoradic" lists form a finitary monad?

Question

I'm trying to understand better what it means for a monad to be finitary. I know that Lawvere theories correspond to finitary monads, but I don't really understand the definition in terms of filtered colimits.

Normal lists satisfy

$$L(X) = 1 + X\cdot L(X).$$

Now suppose that at position n in the list, we can use either an element of X or one of n extra values:

$$F(X) = 1 + X\cdot F(X + 1)$$

An element of F(0) is a numeral in "factoradic" or "base factorial".

$F$ is a monad with the usual list operations. Is it finitary? If so, what does the corresponding Lawvere theory look like? If not, how does it fail to preserve filtered colimits?

Answer 1

Yes, it is finitary. If you think about $X$ as a set of variable and about $T(X)$ as a set of structures of some sort, then $T : Set \to Set$ is finitary if every structure $t \in T(X)$ can use only finite number of variables (roughly speaking). Every list uses only a finite number of variables (up to its length), so does every $F$-structure.

Another example of a functor like yours is the functor of untyped lambda terms which satisfies the following equation: $$C(X) = X + C(X) \times C(X) + C(X + 1)$$ Elements of $C(X)$ are untyped lambda terms whose free variables belong to $X$. Since any lambda term can use only a finite number of variables from $X$, this functor is also finitary.

An example of a non-finitary monad is the monad of trees with infinite number of children: $$I(X) = X + (\mathbb{N} \to I(X))$$ Since an infinite tree can use an infinite number of variables, it is not finitary. A formal proof of this fact goes like this. Let $X$ be an infinte set. Then it is a directed colimit of its finite subsets, but every tree in the colimit $colim_{Y \subset_{fin} X}(I(Y))$ uses only a finite number of variables (namely, the variables from $Y$), so it is not (canonically) isomorphic to the set of all trees $I(X)$. Thus $I$ does not preserve directed colimits.

Algebraic theories is a more explicit way of talking about theories than Lawvere theories. You can always describe an algebraic theory that corresponds to a (finitary) monad $T$ as a theory with $T(\{x_1, \ldots x_n\})$ $n$-ary operations. Sometimes there is a more simple description. For example, the theory that corresponds to $L$ is equivalent to the theory of monoids. Another way to present this theory as the theory with one $n$-ary operation for every $n$ (and a bunch of axioms). You can think of such operation as the concatenation of $n$ elements of a monoid.

Now, you can present the theory for $F$ in a similar way. It will have the same operation as the theory for $L$, but it will also have operations that correspond to the concatenation of a list in which some elements are not elements of your structure, but the new elements that you add in the definition of $F$. Overall, it will have infinitely many $n$-ary operations for every $n > 0$. You can explicitly describe them in terms of lists in which you may have $n$ different holes in $n$-th place. In general, it is a non-trivial task to find a simple presentation for a monad in terms of operations. There is probably a more simple description of the theory for $F$ than the one that I have in mind.