3
$\begingroup$

Given a polynomial functor $F$, its initial algebra is denoted by $\mu X.F(X)$. Now, if $F$ is a 2-variable polynomial functor, $Y \mapsto \mu X.F(X,Y)$ turns out to be functorial and we can, again, (check some hypotheses and) compute the initial algebra $\mu Y. \mu X.F(X,Y)$.

Is it true (with or without additional hypotheses) that $\mu Y. \mu X.F(X,Y) \simeq \mu Z.F(Z, Z)$?

For example, if $F(X,Y) := 1+X+Y$, it amounts to the equality $(x+y)^{\ast} = (x^{\ast} (\varepsilon + y))^{\ast}$ on words.

I tried to find a proof using only the initiality of the algebras, but I couldn't — and I suppose it's good news, because if it was true in general, mutual induction wouldn't be of any interest, am I right?

So I guess I have to look at the characterisation of initial algebras by Adamek's theorem, but again I'm not sure what to look for.

Improve this question
$\endgroup$
8
  • $\begingroup$ Try $F(X, Y) := 1 + X \times Y$. $\endgroup$
    – Andrej Bauer
    Commented Jun 14, 2023 at 21:09
  • $\begingroup$ Thanks for the hint ! but I'm not sure to understand the counterexample. If I make no mistake, $\mu X.1+X\times Y$ is the set of all $(\dots((\bullet, y),y)\dots)$, ie. sequences of leftmost edges of a binary tree, with right edges pointing to elements of $Y$. Then $\mu Y.\mathrm{this}$ is a description of all binary trees, which are also the elements of $\mu X.1+X\times X$. What I understand is that the difference is the same as the one between BFS and DFS. Where am I wrong? $\endgroup$
    – sparusaurata
    Commented Jun 15, 2023 at 8:52
  • $\begingroup$ First, $L(Y) = \mu X . 1 + X \times Y$ are lists of elements of type $Y$, and then $\mu Y . L(Y)$ are unlabeled rose trees. On the other hand $\mu Z . 1 + Z \times Z$ is the type of unlabeled binary trees. $\endgroup$
    – Andrej Bauer
    Commented Jun 15, 2023 at 21:12
  • $\begingroup$ Yes, but these are isomorphic. $L(Y)$, aka lists of type $Y$, are isomorphic to left combs with leaves of type $Y$; then $\mu Y.L(Y)$, aka rose trees, is the type of left combs with leaves of type [left combs with...], which is a description of binary trees. (Similarly, λ-terms can be defined by the alternative "head" signature $M,N ::= x\ |\ \lambda x_1\dots x_m.(M_0)M_1\dots M_n$.) Since we were not 100% confident not to forget something, my colleagues proved the isomorphism in Coq for this $F(X,Y)$: it works! $\endgroup$
    – sparusaurata
    Commented Jun 22, 2023 at 12:08
  • 1
    $\begingroup$ I guess it's in the category of $F\circ\Delta$-algebras (where $\Delta$ is the diagonal, ie. $F\circ\Delta : X \mapsto F(X,X)$). In practice, I want the isomorphism to be compatible with the signature carried by $F$. $\endgroup$
    – sparusaurata
    Commented Jun 26, 2023 at 13:17

1 Answer 1

Reset to default
2
$\begingroup$

I finally came up with a proof under the hypotheses of (and thoroughly using) Adamek's fix-point theorem, I'll post it here as soon as I write it down properly.

Anyway, I found a bit late that this is also Corollary 1 of Theorem 4.2 in (Lehmann and Smyth 1981), where “Theorem 4.2” is the categorical Bekić lemma. It is also what the “double dagger law” means in (Bloom and Ésik 1993). Back to the setting of lattices, the corresponding result is standard and is presented as the “Golden lemma” by (Arnold and Niwiński 2001). This answers the call for references!

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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