|
|
Пишет Journal de Chaource (![[info]](http://lj.rossia.org/img/syndicated.gif){kind=small} lj_chaource)@ 2016-06-10 20:25:00 |
 |
|
 |
|
|
|
|
|
|
 |
|
 |
Polynomial functors V: recursive functors
Recursive polynomial functors need some care when defining them. For example, a functor F(t)=t*t*t*... (infinite product of identity functors) can be "defined" using the fixpoint equation
F(t) = t*F(t).
This is a polynomial equation of the form F = P(t,F), where P(t,f) is a polynomial functor in two variables (i.e. a bifunctor C*C->C defined as a polynomial in the variables t and f).
Does this equation actually define anything? One point of view is that it does not define a nontrivial functor; i.e. the chosen solution is F(t)=0. Another point of view is that it does define a functor, which can be realized in a programming language by a "lazy" or "deferred" calculation of the rest of the infinite product.
Another example of a recursive polynomial functor is the "List" functor,
List(t) = 1 + t*List(t).
An alternative way of writing this functor could be
List(t) = 1 + t + t^2 + t^3 + ...,
where we use the shorthand notation t^n = t*t*...*t (with n factors of t).
Here again there are (at least) two points of view. First, that the sum does not contain the infinite product (i.e. the list must be finite, although of unknown length); second, that it does (so that the list could actually be infinite).
At this point, I'm not sure what is more useful. In practical programming, infinite data structures can be convenient as abstractions, but all actually used data structures are of course finite. In actual code, the defining bifunctor yields a recursive call to F, which may or may not be executed depending on what we are doing with the recursive functor.
It seems that, at the level of category theory and type theory, we can get quite far without worrying about this question. For now, let us prove some properties of recursive polynomial functors without making the definition more specific than this:
Definition. A recursive polynomial functor F is a solution of the fixpoint equation
F(t) = P(t, F(t)),
where P(t,f) is a polynomial bifunctor called the defining bifunctor of F.
Statement. A rec. poly. functor F is pointed iff its defining bifunctor P(t,f) is of the form
P(t,f) = t^m*f^n + Q(t,f), where the first monomial has zero or more factors of t or f (that is, m+n >= 0), and Q is some polynomial bifunctor.
A rec. poly. function F is co-pointed iff its defining bifunctor P(t,f) is of the form
P(t,f) = t*Q(t,f)+ f*R(t,f),
where Q and R are some polynomial bifunctors.
Theorem. Any recursive polynomial functor F is both distributive and co-distributive.
Lemma 1. Let P(t,f) be a polynomial bifunctor, and let F be a functor such that there exists a natural transformation t*F(s) ~> F(t) of functors C*C->C. (Any polynomial functor F satisfies this condition.) Then there exists a natural transformation
t*P(s,F(s)) ~> P(t,F(t)).
Proof: If the lemma holds for bifunctors P and Q, it will obviously hold for the bifunctor P+Q. We can write P(t,f) in the distributive normal form as a sum of monomials of the form c*t^m*f^n. It remains to prove the lemma for P being a single monomial of this form.
For P = c, P = t, and P = f the lemma holds by inspection. In all other cases, we need to construct a natural transformation
t*c*s^m*F(s)^n ~> c*t^m*F(t)^n,
where m>=1, n>=1 are integers. Since we have a natural transformation t*F(s) ~> F(t), and we have a factor "t" already, we can construct a natural transformation
t*c*s*F(s) ~> c*t*F(t)
by omitting the factor "s". Now we can duplicate the factors "t" and "F(t)" as many times as needed. Alternatively, we could "preserve more information" by converting each factor of "F(s)" into the corresponding factor of "F(t)" via the natural transformation t*F(s) ~> F(t), using the same given value of "t".
Q.E.D.
The following lemma was proved previously for non-recursive polynomial functors. It also holds for recursive ones.
Lemma 2. If F(t) is a rec.poly.functor, there exists a natural transformation t*F(s) ~> F(t).
Proof A. We can expand the functor F(t) in a (possibly infinite) normal form,
F(t) = c0 + c0*t + c0*t^2 + ...,
and then the lemma holds for each term separately, since these terms are ordinary (non-recursive) polynomial functors. Perhaps this proof is not enough, since the infinite sum is (possibly) ill-defined. So let's give another proof.
Proof B. We will prove the "property of the recursive step": If F(t) is any functor for which the lemma holds, and if P(t,f) is a polynomial bifunctor, then the lemma holds also for the functor P(t,F(t)). This is precisely the statement of Lemma 1 above.
Q.E.D.
Statement: If F(t) is distributive, Lemma 2 holds for F(t), and P(t,f) is a polynomial bifunctor, then the functor P(t,F(t)) is also distributive.
Proof. The proof will proceed by induction on the structure of P(t,f) written as a Horner formula
P(t,f) = c0(t) + f*(c1(t) + f*(... + cn(t))...).
Here, we consider P(t,f) as a polynomial in "f" with coefficients cj(t) that are themselves polynomials in "t".
The base of induction is P = cn(t). This is a non-recursive polynomial functor, for which case the distributivity was proved before.
The step of induction consists of showing that if distributivity holds for P(t,F(t)) then it also holds for the bifunctor c(t) + F(t)*P(t,F(t)), where c(t) is a polynomial functor.
To show this, we need to construct a natural transformation
(c(s)+F(s)*P(s,F(s)))*(c(t)+F(t)*P(t,F(t)
for which we can use the existence of the natural transformations
c(s)*c(t) ~> c(s*t),
F(s)*F(t) ~> F(s*t), (*) and
P(s,F(s))*P(t,F(t)) ~> P(s*t,F(s*t)). (**)
Expanding the brackets,
(c(s)+F(s)*P(s...))*(c(t)+F(t)*P(t...)) = c(s)*c(t) + c(s)*F(t)*P(t...) + ...,
we find that the only nontrivial natural transformations are sought as
F(s)*P(s,F(s))*c(t) ~> c(s*t)+F(s*t)*P(s*t,F(s*t)), as well as with t and s interchanged.
We will now rewrite for convenience
c(t) = a + s*b(t),
where "a" is a constant and b(t) is some polynomial functor.
Then the sought natural transformation is between
F(s)*P(s,F(s))*(a+t*b(t)) = a*F(s)*P(s,F(s)) + t*b(t)*F(s)*P(s,F(s))
and
a + s*t*b(s*t) + F(s*t)*P(s*t,F(s*t)).
The term a*F(s)*P(s,F(s)) can be mapped to the term "a" by ignoring other factors.
The term t*b(t)*F(s)*P(s,F(s)) can be mapped first to F(t) using Lemma 2. We can also map t*P(s,F(s)) to P(t,F(t)) using Lemma 1. This gives us a natural transformation
t*b(t)*F(s)*P(s,F(s)) ~> F(t)*F(s)*P(s,F(s))*P(t,F(t)).
From this, we obtain F(s*t)*P(s*t,F(s*t)) via natural transformations (*) and (**) that we were justified in assuming above.
Q.E.D.
Statement. If F(t) is co-distributive, if Lemma 2 holds for F, and if P(t,f) is a polynomial bifunctor, then the functor P(t,F(t)) is co-distributive.
Proof. Co-distributivity means the existence of a natural transformation
P(s+t,F(s+t)) ~> P(s,F(s)) + P(t,F(t)).
If this statement holds for bifunctors P and Q, it will also hold for P+Q. So it remains to prove the statement for monomial P of the form P(t,f) = c*t^m*f^n.
We will prove this by induction on the structure of the monomial P. For P = c, P = t, and P = f the statement holds by inspection. Note that P(t,f)=t is co-pointed in the argument "t", and P(t,f)=f is co-pointed in the argument f. This provides the base of the induction.
We will now prove that if the statement holds for a non-constant P, and if P(t,f) is co-pointed in t or co-pointed in f, then the statement holds for P*t and also for P*f. This will prove the statement for any monomial.
The step of the induction requires us to construct natural transformations
(s+t)*P(s+t,F(s+t)) ~> s*P(s,F(s)) + t*P(t,F(t)) (*)
and
F(s+t)*P(s+t,F(s+t)) ~> F(s)*P(s,F(s)) + F(t)*P(t,F(t)), (**)
where we can assume the existence of natural transformations
F(s+t) ~> F(s)+F(t),
P(s+t,F(s+t)) ~> P(s,F(s)) + P(t,F(t)), (***) and
either P(t,f)~>t or P(t,f)~>f.
Both (*) and (**) and proved similarly. Consider (*). We begin by using (***) to obtain
(s+t)*P(s+t,F(s+t)) ~> (s+t)*(P(s,F(s)) + P(t,F(t))).
This can be mapped to s*P(s,F(s)) + t*P(t,F(t)) if we can find a natural transformation
t*P(s,F(s)) ~> s*P(s,F(s)) + t*P(t,F(t)) and similarly for "s" and "t" interchanged.
By assumption, P is co-pointed in one of its arguments. If P(t,f) is co-pointed in t, we can convert P(s,F(s)) ~> s. Hence we obtain the required natural transformation
t*P(s,F(s)) ~> s*P(s,F(s)).
If P(t,f) is co-pointed in f, we can convert P(s,F(s))~>F(s). We will then obtain t*F(s)*P(s,F(s)). We can use Lemma 2 to convert t*F(s) ~> F(t) and Lemma 1 to convert F(t)*P(s,F(s)) ~> P(t,F(t)). Hence, we get the required natural transformation
t*P(s,F(s)) ~> t*P(t,F(t)).
Q.E.D.
Now I think we can prove the Theorem. For any recursive polynomial functor F with the defining bifunctor P, we can either prove that it is itself (co)-distributive, or that F=P(t,G(t)) is (co)-distributive if G has the same property. In this way, we postpone the verification of co-distributivity to the recursive call to G. When the recursion is "well-defined", the recursive calls will at some point terminate at some base case, and the property will be proved.
Conclusion
So far, we have found that polynomial type constructors are always functors, and that polynomial functors are always (co)distributive and weakly (co)monadic. However, they are not always (co)pointed. Recursive polynomial functors are always (co)distributive. We have also characterized the subset of polynomial functors that are (co)pointed.
The usual definition of applicative functors and monadic functors includes the pointed property and some additional properties ("laws"). As far as I checked, the laws will hold for the applicative and co-applicative polynomial functors as constructed in a previous post. I have not yet checked the monadic laws, and I also have not yet checked the recursive case.
In all cases, the existence of natural transformations is proved constructively, i.e. algorithms can be derived for constructing the natural transformations from functors. A sufficiently sophisticated compiler could derive these properties automatically.
Monadic and co-monadic properties are more complicated for recursively defined functors than for non-recursive functors. It does not seem to be easy to prove these properties just from types. For instance, the monadic property of the List functor depends (at least, in the common implementation) on converting a list of lists to a flat list. This conversion is a somewhat involved inductive construction, which does not seem to be easily derivable in full generality just based on the defining bifunctor P(t,f)=1+t*f.
Recursive polynomial functors need some care when defining them. For example, a functor F(t)=t*t*t*... (infinite product of identity functors) can be "defined" using the fixpoint equation
F(t) = t*F(t).
This is a polynomial equation of the form F = P(t,F), where P(t,f) is a polynomial functor in two variables (i.e. a bifunctor C*C->C defined as a polynomial in the variables t and f).
Does this equation actually define anything? One point of view is that it does not define a nontrivial functor; i.e. the chosen solution is F(t)=0. Another point of view is that it does define a functor, which can be realized in a programming language by a "lazy" or "deferred" calculation of the rest of the infinite product.
Another example of a recursive polynomial functor is the "List" functor,
List(t) = 1 + t*List(t).
An alternative way of writing this functor could be
List(t) = 1 + t + t^2 + t^3 + ...,
where we use the shorthand notation t^n = t*t*...*t (with n factors of t).
Here again there are (at least) two points of view. First, that the sum does not contain the infinite product (i.e. the list must be finite, although of unknown length); second, that it does (so that the list could actually be infinite).
At this point, I'm not sure what is more useful. In practical programming, infinite data structures can be convenient as abstractions, but all actually used data structures are of course finite. In actual code, the defining bifunctor yields a recursive call to F, which may or may not be executed depending on what we are doing with the recursive functor.
It seems that, at the level of category theory and type theory, we can get quite far without worrying about this question. For now, let us prove some properties of recursive polynomial functors without making the definition more specific than this:
Definition. A recursive polynomial functor F is a solution of the fixpoint equation
F(t) = P(t, F(t)),
where P(t,f) is a polynomial bifunctor called the defining bifunctor of F.
Statement. A rec. poly. functor F is pointed iff its defining bifunctor P(t,f) is of the form
P(t,f) = t^m*f^n + Q(t,f), where the first monomial has zero or more factors of t or f (that is, m+n >= 0), and Q is some polynomial bifunctor.
A rec. poly. function F is co-pointed iff its defining bifunctor P(t,f) is of the form
P(t,f) = t*Q(t,f)+ f*R(t,f),
where Q and R are some polynomial bifunctors.
Theorem. Any recursive polynomial functor F is both distributive and co-distributive.
Lemma 1. Let P(t,f) be a polynomial bifunctor, and let F be a functor such that there exists a natural transformation t*F(s) ~> F(t) of functors C*C->C. (Any polynomial functor F satisfies this condition.) Then there exists a natural transformation
t*P(s,F(s)) ~> P(t,F(t)).
Proof: If the lemma holds for bifunctors P and Q, it will obviously hold for the bifunctor P+Q. We can write P(t,f) in the distributive normal form as a sum of monomials of the form c*t^m*f^n. It remains to prove the lemma for P being a single monomial of this form.
For P = c, P = t, and P = f the lemma holds by inspection. In all other cases, we need to construct a natural transformation
t*c*s^m*F(s)^n ~> c*t^m*F(t)^n,
where m>=1, n>=1 are integers. Since we have a natural transformation t*F(s) ~> F(t), and we have a factor "t" already, we can construct a natural transformation
t*c*s*F(s) ~> c*t*F(t)
by omitting the factor "s". Now we can duplicate the factors "t" and "F(t)" as many times as needed. Alternatively, we could "preserve more information" by converting each factor of "F(s)" into the corresponding factor of "F(t)" via the natural transformation t*F(s) ~> F(t), using the same given value of "t".
Q.E.D.
The following lemma was proved previously for non-recursive polynomial functors. It also holds for recursive ones.
Lemma 2. If F(t) is a rec.poly.functor, there exists a natural transformation t*F(s) ~> F(t).
Proof A. We can expand the functor F(t) in a (possibly infinite) normal form,
F(t) = c0 + c0*t + c0*t^2 + ...,
and then the lemma holds for each term separately, since these terms are ordinary (non-recursive) polynomial functors. Perhaps this proof is not enough, since the infinite sum is (possibly) ill-defined. So let's give another proof.
Proof B. We will prove the "property of the recursive step": If F(t) is any functor for which the lemma holds, and if P(t,f) is a polynomial bifunctor, then the lemma holds also for the functor P(t,F(t)). This is precisely the statement of Lemma 1 above.
Q.E.D.
Statement: If F(t) is distributive, Lemma 2 holds for F(t), and P(t,f) is a polynomial bifunctor, then the functor P(t,F(t)) is also distributive.
Proof. The proof will proceed by induction on the structure of P(t,f) written as a Horner formula
P(t,f) = c0(t) + f*(c1(t) + f*(... + cn(t))...).
Here, we consider P(t,f) as a polynomial in "f" with coefficients cj(t) that are themselves polynomials in "t".
The base of induction is P = cn(t). This is a non-recursive polynomial functor, for which case the distributivity was proved before.
The step of induction consists of showing that if distributivity holds for P(t,F(t)) then it also holds for the bifunctor c(t) + F(t)*P(t,F(t)), where c(t) is a polynomial functor.
To show this, we need to construct a natural transformation
(c(s)+F(s)*P(s,F(s)))*(c(t)+F(t)*P(t,F(t)
for which we can use the existence of the natural transformations
c(s)*c(t) ~> c(s*t),
F(s)*F(t) ~> F(s*t), (*) and
P(s,F(s))*P(t,F(t)) ~> P(s*t,F(s*t)). (**)
Expanding the brackets,
(c(s)+F(s)*P(s...))*(c(t)+F(t)*P(t...)) = c(s)*c(t) + c(s)*F(t)*P(t...) + ...,
we find that the only nontrivial natural transformations are sought as
F(s)*P(s,F(s))*c(t) ~> c(s*t)+F(s*t)*P(s*t,F(s*t)), as well as with t and s interchanged.
We will now rewrite for convenience
c(t) = a + s*b(t),
where "a" is a constant and b(t) is some polynomial functor.
Then the sought natural transformation is between
F(s)*P(s,F(s))*(a+t*b(t)) = a*F(s)*P(s,F(s)) + t*b(t)*F(s)*P(s,F(s))
and
a + s*t*b(s*t) + F(s*t)*P(s*t,F(s*t)).
The term a*F(s)*P(s,F(s)) can be mapped to the term "a" by ignoring other factors.
The term t*b(t)*F(s)*P(s,F(s)) can be mapped first to F(t) using Lemma 2. We can also map t*P(s,F(s)) to P(t,F(t)) using Lemma 1. This gives us a natural transformation
t*b(t)*F(s)*P(s,F(s)) ~> F(t)*F(s)*P(s,F(s))*P(t,F(t)).
From this, we obtain F(s*t)*P(s*t,F(s*t)) via natural transformations (*) and (**) that we were justified in assuming above.
Q.E.D.
Statement. If F(t) is co-distributive, if Lemma 2 holds for F, and if P(t,f) is a polynomial bifunctor, then the functor P(t,F(t)) is co-distributive.
Proof. Co-distributivity means the existence of a natural transformation
P(s+t,F(s+t)) ~> P(s,F(s)) + P(t,F(t)).
If this statement holds for bifunctors P and Q, it will also hold for P+Q. So it remains to prove the statement for monomial P of the form P(t,f) = c*t^m*f^n.
We will prove this by induction on the structure of the monomial P. For P = c, P = t, and P = f the statement holds by inspection. Note that P(t,f)=t is co-pointed in the argument "t", and P(t,f)=f is co-pointed in the argument f. This provides the base of the induction.
We will now prove that if the statement holds for a non-constant P, and if P(t,f) is co-pointed in t or co-pointed in f, then the statement holds for P*t and also for P*f. This will prove the statement for any monomial.
The step of the induction requires us to construct natural transformations
(s+t)*P(s+t,F(s+t)) ~> s*P(s,F(s)) + t*P(t,F(t)) (*)
and
F(s+t)*P(s+t,F(s+t)) ~> F(s)*P(s,F(s)) + F(t)*P(t,F(t)), (**)
where we can assume the existence of natural transformations
F(s+t) ~> F(s)+F(t),
P(s+t,F(s+t)) ~> P(s,F(s)) + P(t,F(t)), (***) and
either P(t,f)~>t or P(t,f)~>f.
Both (*) and (**) and proved similarly. Consider (*). We begin by using (***) to obtain
(s+t)*P(s+t,F(s+t)) ~> (s+t)*(P(s,F(s)) + P(t,F(t))).
This can be mapped to s*P(s,F(s)) + t*P(t,F(t)) if we can find a natural transformation
t*P(s,F(s)) ~> s*P(s,F(s)) + t*P(t,F(t)) and similarly for "s" and "t" interchanged.
By assumption, P is co-pointed in one of its arguments. If P(t,f) is co-pointed in t, we can convert P(s,F(s)) ~> s. Hence we obtain the required natural transformation
t*P(s,F(s)) ~> s*P(s,F(s)).
If P(t,f) is co-pointed in f, we can convert P(s,F(s))~>F(s). We will then obtain t*F(s)*P(s,F(s)). We can use Lemma 2 to convert t*F(s) ~> F(t) and Lemma 1 to convert F(t)*P(s,F(s)) ~> P(t,F(t)). Hence, we get the required natural transformation
t*P(s,F(s)) ~> t*P(t,F(t)).
Q.E.D.
Now I think we can prove the Theorem. For any recursive polynomial functor F with the defining bifunctor P, we can either prove that it is itself (co)-distributive, or that F=P(t,G(t)) is (co)-distributive if G has the same property. In this way, we postpone the verification of co-distributivity to the recursive call to G. When the recursion is "well-defined", the recursive calls will at some point terminate at some base case, and the property will be proved.
Conclusion
So far, we have found that polynomial type constructors are always functors, and that polynomial functors are always (co)distributive and weakly (co)monadic. However, they are not always (co)pointed. Recursive polynomial functors are always (co)distributive. We have also characterized the subset of polynomial functors that are (co)pointed.
The usual definition of applicative functors and monadic functors includes the pointed property and some additional properties ("laws"). As far as I checked, the laws will hold for the applicative and co-applicative polynomial functors as constructed in a previous post. I have not yet checked the monadic laws, and I also have not yet checked the recursive case.
In all cases, the existence of natural transformations is proved constructively, i.e. algorithms can be derived for constructing the natural transformations from functors. A sufficiently sophisticated compiler could derive these properties automatically.
Monadic and co-monadic properties are more complicated for recursively defined functors than for non-recursive functors. It does not seem to be easy to prove these properties just from types. For instance, the monadic property of the List functor depends (at least, in the common implementation) on converting a list of lists to a flat list. This conversion is a somewhat involved inductive construction, which does not seem to be easily derivable in full generality just based on the defining bifunctor P(t,f)=1+t*f.
