Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Journal de Chaource ([info]lj_chaource)
@ 2016-06-22 21:13:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Polynomial functors VII. Pointed and co-pointed recursive polynomial functors
Polynomial functors I. Basic motivations. All polynomial type constructors are functors.
Polynomial functors II. Basic definitions: (co)pointed, (co)distributive, (co)monadic. Monadic functors are distributive.
Co-pointed functors are co-distributive
Polynomial functors III: all polynomial functors are (co)distributive
Polynomial functors IV: all polynomial functors are pre-(co)-monadic
Polynomial functors V: recursive functors are (co)distributive
Polynomial functors VI: how to characterize pairs of functors with natural transformations between them
Polynomial functors VII. Pointed and co-pointed recursive polynomial functors (this post)

Characterization of co-pointed functors

We denote by 0 the initial object in the category. (This is the "void" type, i.e. a type with no values.) As before, we denote by 1 the final object in the category. We assume that they both exist. For example, in Scala the initial object is "Nothing" and the final object is "()".

A functor F is co-pointed if there exists a natural transformation to the identity functor, F(t) ~> t.

Statement: A polynomial functor F is co-pointed iff there is a morphism F(0) -> 0.
Proof: Write the polynomial functor in the distributive normal form: F(t) = c0 + c1*t +c2*t*t + ... Then F(0) = c0. The condition F(0) -> 0 means that c0 = 0, in other words, this term is absent from the distributive normal form. In that case, F(t) = t*G(t) for some functor G(t). This is the same as the condition for the functor F to be co-pointed.

Statement: A recursive polynomial functor F is co-pointed iff there is a morphism P(0,0) -> 0 for the defining bifunctor P(t,f). Equivalently, P(t,f) = t*A(t,f) + f*B(t,f) for some bifunctors A and B.

Proof: The functor F satisfies F(t) = P(t,F(t)). If we have F(0) -> 0 then we have P(0,F(0)) -> 0. Since 0 is the initial object, we have 0 -> F(0). Since P(t,f) is a functor in the argument f, we can lift 0 -> F(0) to P(0,0) -> P(0,F(0)). Therefore, we can construct P(0,0) -> P(0,F(0))->0 as required.

Conversely, if we have P(0,0)->0, we can write P in the distributive normal form and conclude that P(t,f) = t*A(t,f) + f*B(t,f) for some bifunctors A and B. If the bifunctor A is nonzero then we can have a natural transformation P(t,f)~>t. This makes F co-pointed since F = P(t,F). If A is zero but B is nonzero then we have a natural transformation P(t,f)~>f. This gives is the construction of F(t) ~> t recursively: if the functor G is co-pointed then the functor P(t,G) is also co-pointed.

Statement: A recursive polynomial functor F is pointed if the defining bifunctor P(t,f) has the form

P(t,f) = t^m * f^n + Q(t,f), where m>=0 and n>=0, and Q is some bifunctor.

Proof: We will show the recursion step: if G is pointed (i.e. t ~> G(t)) then there is a natural transformation t ~> P(t,G(t)). This is easy since P(t, G(t)) = t^m * G(t)^n + Q, and we have t ~> G(t). So we can construct a natural transformation t ~> P(t, G(t)) by generating the term of type t^m * G(t)^n.


(Читать комментарии) (Добавить комментарий)