Although this thread started in the open-axiom list, I would like to try to continue it here since it seems unfinished. Gaby stated that he no longer wishes to discuss it on open-axiom.
On Mon, 24 Nov 2008 11:05:29 +0100 Ralf Hemmecke wrote: > >> CoercibleTo does not require that the 'retract' actually be defined. > > Exactly. > >> coerce >> A ---------> B >> | | >> id | pullback | retract >> | | >> \|/ \|/ >> A -------> Union(A,"failed") >> inj >> >> In other words the category CoercibleTo requires that coerce is an >> injection that is pulled-back along a retraction. This means that all >> values of A must be retractable from B. > > Bill, I like your categorial view on this. But I don't quite understand > that above you say 'retract' need not exist and then you speak about > a pull-back along a retraction. > I did not mean to imply that retract need not exist - only that in the current usage 'coerce' and 'retract' are not defined in pairs. I do wish to claim that whenever there is a valid 'coerce', then in principle it must be possible to define the correspondinging 'retractIfCan'. > If it were as you say, then why have the original developers made two > categories CoercibleTo and RetractableTo? Oh, well, this I could > understand, because they have to be applied to two different domains > (one to A and the other to B). But CoercibleFrom and RetractableTo > should be just one category. (Oh, CoercibleFrom does not exist in > original Axiom, and I guess there was a reason for this.) > I am not convinced that there was any specific reason. I expect that "CoercibleTo" was considered only a matter of "convenience". But Martin's recent comments here about the desired "transitivity" of CoercibleTo, reminded me of the need to define 'coerce' more formally. > When you speak about "inj" as an injection. That does not mean > that any (algebraic) structure of A must be preserved in > Union(A,"failed"). What I labeled 'inj' in the diagram is just the injection of A into the Union(A,"failed"). Union is just a categorical co-product. The requirement that this square forms a pullback does mean that 'coerce' must be monic (1-1 mapping). > Which means that nothing is said about whether or not 'a' and > 'retract(coerce(a))' gives the same thing (of non-failed). It does require retract(coerce(a)) = a Since the arrows in the pullback diagram must commute. The pullback is a limit like co-product. > That sounds reasonable to me. Of course, one basically wishes > for equality in such a case. But I don't think that is properly stated > in the documentation of 'RetractableTo'. > I think all of this should be defined in a more rigorous manner. > Another point that I would like to make in connection with coerce and > the interpreter is related to Doye's thesis. From that I got the impression > that the direction of the coerce arrows should not be symmetric. Rather > one should have commutativity of all diagrams of the form > > A ---> B > | | > v v > C ---> D > > where all the arrows denote 'coerce' functions. This property is for me > more important thant your stated coerce+retract relation. > I think that this follows from my definition. Regards, Bill Page. --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en -~----------~----~----~----~------~----~------~--~---
