\(\newcommand{\BA}{{\sf BA}}\)
Polyonomial Functors#
(under construction)
We use \(\mathcal P\) for the powerset functor and \(\mathcal H X=2^{2^X}\). In this section we indicate how to construct a modal logic for any functor \(T\) built according to the following context-free grammar.
We describe functors \(L:\BA\to\BA\) or \(L:\BA\times\BA\to\BA\) by generators and relations as follows.
\(L_{K_C}(A)\) is the free \(\BA\) given by generators \(c\in C\) and satisfying \(c_1\wedge c_2=\bot\) for all \(c_1\not=c_2\) and \(\bigvee_{c\in C} c = \top\).
\(L_+(A_1,A_2)\) is generated by \([\kappa_1]a_1\), \([\kappa_2]a_2\), \(a_i\in A_i\) where the \([\kappa_i]\) preserve finite joins and binary meets and satisfy \([\kappa_1] a_1\wedge [\kappa_2]a_2=\bot\), \([\kappa_1]\top\vee [\kappa_2]\top=\top\), \(\neg[\kappa_1]a_1=[\kappa_2]\top\vee[\kappa_1]\neg a_1\), \(\neg[\kappa_2]a_2=[\kappa_1]\top\vee[\kappa_2]\neg a_2\).
\(L_\times(A_1,A_2)\) is generated by \([\pi_1]a_1\), \([\pi_2]a_2\), \(a_i\in A_i\) where \([\pi_i]\) preserve Boolean operations.
\(L_\mathcal P(A)\) is generated by \(\Box a\), \(a \in A\), and \(\Box\) preserves finite meets.
\(L_\mathcal H(A)\) is generated by \(\Box a\), \(a \in A\) (no equations).
For the semantics, we define Boolean algebra morphisms \(\delta_T\)
\(L_{K_C}\Pi X \to \Pi C\) by \(c\mapsto \{c\}\),
\(L_+(\Pi X_1,\Pi X_2) \to \Pi(X_1+X_2)\) by \([\kappa_i]a_i\mapsto a_i\),
\(L_\times(\Pi X,\Pi Y) \to \Pi(X_1\times X_2)\) by \([\pi_1]a_1\mapsto a_1\times X_2\), \([\pi_2]a_2\mapsto X_1\times a_2\),
\(L_\mathcal P \Pi X\to \Pi\mathcal P X\) by \(\Box a \mapsto \{b\subseteq X\mid b\subseteq a\}\),
\(L_\mathcal H \Pi X\to \Pi\mathcal H X\) by \(\Box a \mapsto \{s\in \mathcal H X \mid a \in s \}\).
and extend them inductively to \(\delta_T:L_T\Pi\to\Pi T \) for all \(T\). Items (1)-(3) are slight variations of cases appearing in [Abramsky, 1991], (4) is in [Abramsky, 2005], and \(\delta_X\) in (5) is given by the identity on \(2^{2^{2^X}}\).